feat(algebra/ordered_*): cleanup and projection notation (#3850)

Also add a few new projection notations.

src/algebra/order.lean

@@ -22,16 +22,21 @@ This file contains some lemmas about `≤`/`≥`/`<`/`>`, and `cmp`.
 universe u
 variables {α : Type u}
 
-alias le_trans ← has_le.le.trans
-alias lt_of_le_of_lt ← has_le.le.trans_lt
-alias le_antisymm ← has_le.le.antisymm
-alias lt_of_le_of_ne ← has_le.le.lt_of_ne
-alias le_of_lt ← has_lt.lt.le
-alias lt_trans ← has_lt.lt.trans
-alias lt_of_lt_of_le ← has_lt.lt.trans_le
-alias ne_of_lt ← has_lt.lt.ne
-alias lt_asymm ← has_lt.lt.asymm has_lt.lt.not_lt
-alias le_of_eq ← eq.le
+alias le_trans        ← has_le.le.trans
+alias lt_of_le_of_lt  ← has_le.le.trans_lt
+alias le_antisymm     ← has_le.le.antisymm
+alias lt_of_le_of_ne  ← has_le.le.lt_of_ne
+alias lt_of_le_not_le ← has_le.le.lt_of_not_le
+alias lt_or_eq_of_le  ← has_le.le.lt_or_eq
+
+alias le_of_lt        ← has_lt.lt.le
+alias lt_trans        ← has_lt.lt.trans
+alias lt_of_lt_of_le  ← has_lt.lt.trans_le
+alias ne_of_lt        ← has_lt.lt.ne
+alias lt_asymm        ← has_lt.lt.asymm has_lt.lt.not_lt
+
+alias le_of_eq        ← eq.le
+
 
 /-- A version of `le_refl` where the argument is implicit -/
 lemma le_rfl [preorder α] {x : α} : x ≤ x := le_refl x
@@ -87,28 +92,27 @@ lemma not_le_of_lt [preorder α] {a b : α} (h : a < b) : ¬ b ≤ a :=
 alias not_le_of_lt ← has_lt.lt.not_le
 
 lemma not_lt_of_le [preorder α] {a b : α} (h : a ≤ b) : ¬ b < a
-| hab := not_le_of_gt hab h
+| hab := hab.not_le h
 
 alias not_lt_of_le ← has_le.le.not_lt
 
 lemma le_iff_eq_or_lt [partial_order α] {a b : α} : a ≤ b ↔ a = b ∨ a < b :=
 le_iff_lt_or_eq.trans or.comm
 
 lemma lt_iff_le_and_ne [partial_order α] {a b : α} : a < b ↔ a ≤ b ∧ a ≠ b :=
-⟨λ h, ⟨le_of_lt h, ne_of_lt h⟩, λ ⟨h1, h2⟩, lt_of_le_of_ne h1 h2⟩
+⟨λ h, ⟨le_of_lt h, ne_of_lt h⟩, λ ⟨h1, h2⟩, h1.lt_of_ne h2⟩
 
 lemma eq_iff_le_not_lt [partial_order α] {a b : α} : a = b ↔ a ≤ b ∧ ¬ a < b :=
-⟨λ h, ⟨le_of_eq h, h ▸ lt_irrefl _⟩, λ ⟨h₁, h₂⟩, le_antisymm h₁ $
-  classical.by_contradiction $ λ h₃, h₂ (lt_of_le_not_le h₁ h₃)⟩
+⟨λ h, ⟨h.le, h ▸ lt_irrefl _⟩, λ ⟨h₁, h₂⟩, h₁.antisymm $
+  classical.by_contradiction $ λ h₃, h₂ (h₁.lt_of_not_le h₃)⟩
 
 lemma eq_or_lt_of_le [partial_order α] {a b : α} (h : a ≤ b) : a = b ∨ a < b :=
-(lt_or_eq_of_le h).symm
+h.lt_or_eq.symm
 
 alias eq_or_lt_of_le ← has_le.le.eq_or_lt
-alias lt_or_eq_of_le ← has_le.le.lt_or_eq
 
 lemma lt_of_not_ge' [linear_order α] {a b : α} (h : ¬ b ≤ a) : a < b :=
-lt_of_le_not_le ((le_total _ _).resolve_right h) h
+((le_total _ _).resolve_right h).lt_of_not_le h
 
 lemma lt_iff_not_ge' [linear_order α] {x y : α} : x < y ↔ ¬ y ≤ x :=
 ⟨not_le_of_gt, lt_of_not_ge'⟩
@@ -123,27 +127,27 @@ lemma lt_or_le [linear_order α] : ∀ a b : α, a < b ∨ b ≤ a := lt_or_ge
 lemma le_or_lt [linear_order α] : ∀ a b : α, a ≤ b ∨ b < a := le_or_gt
 
 lemma has_le.le.lt_or_le [linear_order α] {a b : α} (h : a ≤ b) (c : α) : a < c ∨ c ≤ b :=
-(lt_or_le a c).imp id (λ hc, hc.trans h)
+(lt_or_le a c).imp id $ λ hc, hc.trans h
 
 lemma has_le.le.le_or_lt [linear_order α] {a b : α} (h : a ≤ b) (c : α) : a ≤ c ∨ c < b :=
-(le_or_lt a c).imp id (λ hc, hc.trans_le h)
+(le_or_lt a c).imp id $ λ hc, hc.trans_le h
 
 lemma not_lt_iff_eq_or_lt [linear_order α] {a b : α} : ¬ a < b ↔ a = b ∨ b < a :=
 not_lt.trans $ le_iff_eq_or_lt.trans $ or_congr eq_comm iff.rfl
 
 lemma exists_ge_of_linear [linear_order α] (a b : α) : ∃ c, a ≤ c ∧ b ≤ c :=
 match le_total a b with
-| or.inl h := ⟨_, h, le_refl _⟩
-| or.inr h := ⟨_, le_refl _, h⟩
+| or.inl h := ⟨_, h, le_rfl⟩
+| or.inr h := ⟨_, le_rfl, h⟩
 end
 
 lemma lt_imp_lt_of_le_imp_le {β} [linear_order α] [preorder β] {a b : α} {c d : β}
   (H : a ≤ b → c ≤ d) (h : d < c) : b < a :=
-lt_of_not_ge' $ λ h', not_lt_of_ge (H h') h
+lt_of_not_ge' $ λ h', (H h').not_lt h
 
 lemma le_imp_le_of_lt_imp_lt {β} [preorder α] [linear_order β] {a b : α} {c d : β}
   (H : d < c → b < a) (h : a ≤ b) : c ≤ d :=
-le_of_not_gt $ λ h', not_le_of_gt (H h') h
+le_of_not_gt $ λ h', (H h').not_le h
 
 lemma le_imp_le_iff_lt_imp_lt {β} [linear_order α] [linear_order β] {a b : α} {c d : β} :
   (a ≤ b → c ≤ d) ↔ (d < c → b < a) :=
@@ -155,11 +159,11 @@ lt_iff_le_not_le.trans $ (and_congr H' (not_congr H)).trans lt_iff_le_not_le.sym
 
 lemma lt_iff_lt_of_le_iff_le {β} [linear_order α] [linear_order β] {a b : α} {c d : β}
   (H : a ≤ b ↔ c ≤ d) : b < a ↔ d < c :=
-not_le.symm.trans $ iff.trans (not_congr H) $ not_le
+not_le.symm.trans $ (not_congr H).trans $ not_le
 
 lemma le_iff_le_iff_lt_iff_lt {β} [linear_order α] [linear_order β] {a b : α} {c d : β} :
   (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c) :=
-⟨lt_iff_lt_of_le_iff_le, λ H, not_lt.symm.trans $ iff.trans (not_congr H) $ not_lt⟩
+⟨lt_iff_lt_of_le_iff_le, λ H, not_lt.symm.trans $ (not_congr H).trans $ not_lt⟩
 
 lemma eq_of_forall_le_iff [partial_order α] {a b : α}
   (H : ∀ c, c ≤ a ↔ c ≤ b) : a = b :=
@@ -258,7 +262,7 @@ lemma ne_iff_lt_or_gt [decidable_linear_order α] {a b : α} : a ≠ b ↔ a < b
 -- See Note [decidable namespace]
 lemma le_imp_le_of_lt_imp_lt {β} [preorder α] [decidable_linear_order β]
   {a b : α} {c d : β} (H : d < c → b < a) (h : a ≤ b) : c ≤ d :=
-le_of_not_lt $ λ h', not_le_of_gt (H h') h
+le_of_not_lt $ λ h', (H h').not_le h
 
 -- See Note [decidable namespace]
 lemma le_imp_le_iff_lt_imp_lt {β} [linear_order α] [decidable_linear_order β]
@@ -268,7 +272,7 @@ lemma le_imp_le_iff_lt_imp_lt {β} [linear_order α] [decidable_linear_order β]
 -- See Note [decidable namespace]
 lemma le_iff_le_iff_lt_iff_lt {β} [decidable_linear_order α] [decidable_linear_order β]
   {a b : α} {c d : β} : (a ≤ b ↔ c ≤ d) ↔ (b < a ↔ d < c) :=
-⟨lt_iff_lt_of_le_iff_le, λ H, not_lt.symm.trans $ iff.trans (not_congr H) $ not_lt⟩
+⟨lt_iff_lt_of_le_iff_le, λ H, not_lt.symm.trans $ (not_congr H).trans $ not_lt⟩
 
 end decidable
 

src/algebra/ordered_field.lean

@@ -36,7 +36,7 @@ variables [linear_ordered_field α] {a b c d e : α}
 @[simp] lemma inv_pos : 0 < a⁻¹ ↔ 0 < a :=
 suffices ∀ a : α, 0 < a → 0 < a⁻¹,
 from ⟨λ h, inv_inv' a ▸ this _ h, this a⟩,
-assume a ha, flip lt_of_mul_lt_mul_left (le_of_lt ha) $ by simp [ne_of_gt ha, zero_lt_one]
+assume a ha, flip lt_of_mul_lt_mul_left ha.le $ by simp [ne_of_gt ha, zero_lt_one]
 
 @[simp] lemma inv_nonneg : 0 ≤ a⁻¹ ↔ 0 ≤ a :=
 by simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]
@@ -88,10 +88,10 @@ mul_nonpos_of_nonneg_of_nonpos ha (inv_nonpos.2 hb)
 -/
 
 lemma le_div_iff (hc : 0 < c) : a ≤ b / c ↔ a * c ≤ b :=
-⟨λ h, div_mul_cancel b (ne_of_lt hc).symm ▸ mul_le_mul_of_nonneg_right h (le_of_lt hc),
+⟨λ h, div_mul_cancel b (ne_of_lt hc).symm ▸ mul_le_mul_of_nonneg_right h hc.le,
   λ h, calc
     a   = a * c * (1 / c) : mul_mul_div a (ne_of_lt hc).symm
-    ... ≤ b * (1 / c)     : mul_le_mul_of_nonneg_right h (le_of_lt (one_div_pos.2 hc))
+    ... ≤ b * (1 / c)     : mul_le_mul_of_nonneg_right h (one_div_pos.2 hc).le
     ... = b / c           : (div_eq_mul_one_div b c).symm⟩
 
 lemma le_div_iff' (hc : 0 < c) : a ≤ b / c ↔ c * a ≤ b :=
@@ -100,10 +100,10 @@ by rw [mul_comm, le_div_iff hc]
 lemma div_le_iff (hb : 0 < b) : a / b ≤ c ↔ a ≤ c * b :=
 ⟨λ h, calc
   a = a / b * b : by rw (div_mul_cancel _ (ne_of_lt hb).symm)
-  ... ≤ c * b     : mul_le_mul_of_nonneg_right h (le_of_lt hb),
+  ... ≤ c * b     : mul_le_mul_of_nonneg_right h hb.le,
   λ h, calc
   a / b = a * (1 / b)     : div_eq_mul_one_div a b
-  ... ≤ (c * b) * (1 / b) : mul_le_mul_of_nonneg_right h $ le_of_lt $ one_div_pos.2 hb
+  ... ≤ (c * b) * (1 / b) : mul_le_mul_of_nonneg_right h (one_div_pos.2 hb).le
   ... = (c * b) / b       : (div_eq_mul_one_div (c * b) b).symm
   ... = c                 : by refine (div_eq_iff (ne_of_gt hb)).mpr rfl⟩
 
@@ -123,10 +123,10 @@ lemma div_lt_iff' (hc : 0 < c) : b / c < a ↔ b < c * a :=
 by rw [mul_comm, div_lt_iff hc]
 
 lemma div_le_iff_of_neg (hc : c < 0) : b / c ≤ a ↔ a * c ≤ b :=
-⟨λ h, div_mul_cancel b (ne_of_lt hc) ▸ mul_le_mul_of_nonpos_right h (le_of_lt hc),
+⟨λ h, div_mul_cancel b (ne_of_lt hc) ▸ mul_le_mul_of_nonpos_right h hc.le,
   λ h, calc
     a = a * c * (1 / c) : mul_mul_div a (ne_of_lt hc)
-  ... ≥ b * (1 / c)     : mul_le_mul_of_nonpos_right h (le_of_lt (one_div_neg.2 hc))
+  ... ≥ b * (1 / c)     : mul_le_mul_of_nonpos_right h (one_div_neg.2 hc).le
   ... = b / c           : (div_eq_mul_one_div b c).symm⟩
 
 lemma div_le_iff_of_neg' (hc : c < 0) : b / c ≤ a ↔ c * a ≤ b :=
@@ -160,7 +160,7 @@ by { rcases eq_or_lt_of_le hb with rfl|hb', simp [hc], rwa [div_le_iff hb'] }
 -/
 
 lemma inv_le_inv_of_le (ha : 0 < a) (h : a ≤ b) : b⁻¹ ≤ a⁻¹ :=
-by rwa [← one_div a, le_div_iff' ha, ← div_eq_mul_inv, div_le_iff (lt_of_lt_of_le ha h), one_mul]
+by rwa [← one_div a, le_div_iff' ha, ← div_eq_mul_inv, div_le_iff (ha.trans_le h), one_mul]
 
 /-- See `inv_le_inv_of_le` for the implication from right-to-left with one fewer assumption. -/
 lemma inv_le_inv (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b⁻¹ ↔ b ≤ a :=
@@ -200,13 +200,13 @@ lemma lt_inv_of_neg (ha : a < 0) (hb : b < 0) : a < b⁻¹ ↔ b < a⁻¹ :=
 lt_iff_lt_of_le_iff_le (inv_le_of_neg hb ha)
 
 lemma inv_lt_one (ha : 1 < a) : a⁻¹ < 1 :=
-by rwa [inv_lt (lt_trans (@zero_lt_one α _) ha) zero_lt_one, inv_one]
+by rwa [inv_lt ((@zero_lt_one α _).trans ha) zero_lt_one, inv_one]
 
 lemma one_lt_inv (h₁ : 0 < a) (h₂ : a < 1) : 1 < a⁻¹ :=
 by rwa [lt_inv (@zero_lt_one α _) h₁, inv_one]
 
 lemma inv_le_one (ha : 1 ≤ a) : a⁻¹ ≤ 1 :=
-by rwa [inv_le (lt_of_lt_of_le (@zero_lt_one α _) ha) zero_lt_one, inv_one]
+by rwa [inv_le ((@zero_lt_one α _).trans_le ha) zero_lt_one, inv_one]
 
 lemma one_le_inv (h₁ : 0 < a) (h₂ : a ≤ 1) : 1 ≤ a⁻¹ :=
 by rwa [le_inv (@zero_lt_one α _) h₁, inv_one]
@@ -224,7 +224,7 @@ end
 lemma div_le_div_of_le_left (ha : 0 ≤ a) (hc : 0 < c) (h : c ≤ b) : a / b ≤ a / c :=
 begin
   rw [div_eq_mul_inv, div_eq_mul_inv],
-  exact mul_le_mul_of_nonneg_left ((inv_le_inv (lt_of_lt_of_le hc h) hc).mpr h) ha
+  exact mul_le_mul_of_nonneg_left ((inv_le_inv (hc.trans_le h) hc).mpr h) ha
 end
 
 lemma div_le_div_of_le_of_nonneg (hab : a ≤ b) (hc : 0 ≤ c) : a / c ≤ b / c :=
@@ -249,10 +249,10 @@ begin
 end
 
 lemma div_le_div_right (hc : 0 < c) : a / c ≤ b / c ↔ a ≤ b :=
-⟨le_imp_le_of_lt_imp_lt $ div_lt_div_of_lt hc, div_le_div_of_le $ le_of_lt hc⟩
+⟨le_imp_le_of_lt_imp_lt $ div_lt_div_of_lt hc, div_le_div_of_le $ hc.le⟩
 
 lemma div_le_div_right_of_neg (hc : c < 0) : a / c ≤ b / c ↔ b ≤ a :=
-⟨le_imp_le_of_lt_imp_lt $ div_lt_div_of_neg_of_lt hc, div_le_div_of_nonpos_of_le $ le_of_lt hc⟩
+⟨le_imp_le_of_lt_imp_lt $ div_lt_div_of_neg_of_lt hc, div_le_div_of_nonpos_of_le $ hc.le⟩
 
 lemma div_lt_div_right (hc : 0 < c) : a / c < b / c ↔ a < b :=
 lt_iff_lt_of_le_iff_le $ div_le_div_right hc
@@ -274,18 +274,18 @@ lemma div_le_div_iff (b0 : 0 < b) (d0 : 0 < d) : a / b ≤ c / d ↔ a * d ≤ c
 by rw [le_div_iff d0, div_mul_eq_mul_div, div_le_iff b0]
 
 lemma div_le_div (hc : 0 ≤ c) (hac : a ≤ c) (hd : 0 < d) (hbd : d ≤ b) : a / b ≤ c / d :=
-by { rw div_le_div_iff (lt_of_lt_of_le hd hbd) hd, exact mul_le_mul hac hbd (le_of_lt hd) hc }
+by { rw div_le_div_iff (hd.trans_le hbd) hd, exact mul_le_mul hac hbd hd.le hc }
 
 lemma div_lt_div (hac : a < c) (hbd : d ≤ b) (c0 : 0 ≤ c) (d0 : 0 < d) :
   a / b < c / d :=
-(div_lt_div_iff (lt_of_lt_of_le d0 hbd) d0).2 (mul_lt_mul hac hbd d0 c0)
+(div_lt_div_iff (d0.trans_le hbd) d0).2 (mul_lt_mul hac hbd d0 c0)
 
 lemma div_lt_div' (hac : a ≤ c) (hbd : d < b) (c0 : 0 < c) (d0 : 0 < d) :
   a / b < c / d :=
-(div_lt_div_iff (lt_trans d0 hbd) d0).2 (mul_lt_mul' hac hbd (le_of_lt d0) c0)
+(div_lt_div_iff (d0.trans hbd) d0).2 (mul_lt_mul' hac hbd d0.le c0)
 
 lemma div_lt_div_of_lt_left (hb : 0 < b) (h : b < a) (hc : 0 < c) : c / a < c / b :=
-(div_lt_div_left hc (lt_trans hb h) hb).mpr h
+(div_lt_div_left hc (hb.trans h) hb).mpr h
 
 /-!
 ### Relating one division and involving `1`
@@ -346,13 +346,13 @@ lemma one_div_le_one_div_of_le (ha : 0 < a) (h : a ≤ b) : 1 / b ≤ 1 / a :=
 by simpa using inv_le_inv_of_le ha h
 
 lemma one_div_lt_one_div_of_lt (ha : 0 < a) (h : a < b) : 1 / b < 1 / a :=
-by rwa [lt_div_iff' ha, ← div_eq_mul_one_div, div_lt_one (lt_trans ha h)]
+by rwa [lt_div_iff' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)]
 
 lemma one_div_le_one_div_of_neg_of_le (hb : b < 0) (h : a ≤ b) : 1 / b ≤ 1 / a :=
-by rwa [div_le_iff_of_neg' hb, ← div_eq_mul_one_div, div_le_one_of_neg (lt_of_le_of_lt h hb)]
+by rwa [div_le_iff_of_neg' hb, ← div_eq_mul_one_div, div_le_one_of_neg (h.trans_lt hb)]
 
 lemma one_div_lt_one_div_of_neg_of_lt (hb : b < 0) (h : a < b) : 1 / b < 1 / a :=
-by rwa [div_lt_iff_of_neg' hb, ← div_eq_mul_one_div, div_lt_one_of_neg (lt_trans h hb)]
+by rwa [div_lt_iff_of_neg' hb, ← div_eq_mul_one_div, div_lt_one_of_neg (h.trans hb)]
 
 lemma le_of_one_div_le_one_div (ha : 0 < a) (h : 1 / a ≤ 1 / b) : b ≤ a :=
 le_imp_le_of_lt_imp_lt (one_div_lt_one_div_of_lt ha) h