feat(order/basic): Simple shortcut lemmas (#13421)

Add convenience lemmas to make the API a bit more symmetric and easier to translate between `transitive` and `is_trans`. Also rename `_ge'` to `_le` in lemmas and fix the `is_max_` aliases.

src/algebra/order/floor.lean

@@ -93,7 +93,7 @@ lemma le_floor (h : (n : α) ≤ a) : n ≤ ⌊a⌋₊ := (le_floor_iff $ n.cast
 
 lemma floor_lt (ha : 0 ≤ a) : ⌊a⌋₊ < n ↔ a < n := lt_iff_lt_of_le_iff_le $ le_floor_iff ha
 
-lemma lt_of_floor_lt (h : ⌊a⌋₊ < n) : a < n := lt_of_not_ge' $ λ h', (le_floor h').not_lt h
+lemma lt_of_floor_lt (h : ⌊a⌋₊ < n) : a < n := lt_of_not_le $ λ h', (le_floor h').not_lt h
 
 lemma floor_le (ha : 0 ≤ a) : (⌊a⌋₊ : α) ≤ a := (le_floor_iff ha).1 le_rfl
 

src/algebra/parity.lean

@@ -296,10 +296,10 @@ lemma odd.pow_nonpos_iff (hn : odd n) : a ^ n ≤ 0 ↔ a ≤ 0 :=
 ⟨λ h, le_of_not_lt (λ ha, h.not_lt $ pow_pos ha _), hn.pow_nonpos⟩
 
 lemma odd.pow_pos_iff (hn : odd n) : 0 < a ^ n ↔ 0 < a :=
-⟨λ h, lt_of_not_ge' (λ ha, h.not_le $ hn.pow_nonpos ha), λ ha, pow_pos ha n⟩
+⟨λ h, lt_of_not_le (λ ha, h.not_le $ hn.pow_nonpos ha), λ ha, pow_pos ha n⟩
 
 lemma odd.pow_neg_iff (hn : odd n) : a ^ n < 0 ↔ a < 0 :=
-⟨λ h, lt_of_not_ge' (λ ha, h.not_le $ pow_nonneg ha _), hn.pow_neg⟩
+⟨λ h, lt_of_not_le (λ ha, h.not_le $ pow_nonneg ha _), hn.pow_neg⟩
 
 lemma even.pow_pos_iff (hn : even n) (h₀ : 0 < n) : 0 < a ^ n ↔ a ≠ 0 :=
 ⟨λ h ha, by { rw [ha, zero_pow h₀] at h, exact lt_irrefl 0 h }, hn.pow_pos⟩

src/analysis/special_functions/pow.lean

@@ -603,7 +603,7 @@ begin
 end
 
 @[simp] lemma rpow_lt_rpow_left_iff (hx : 1 < x) : x ^ y < x ^ z ↔ y < z :=
-by rw [lt_iff_not_ge', rpow_le_rpow_left_iff hx, lt_iff_not_ge']
+by rw [lt_iff_not_le, rpow_le_rpow_left_iff hx, lt_iff_not_le]
 
 lemma rpow_lt_rpow_of_exponent_gt (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) :
   x^y < x^z :=
@@ -628,7 +628,7 @@ end
 
 @[simp] lemma rpow_lt_rpow_left_iff_of_base_lt_one (hx0 : 0 < x) (hx1 : x < 1) :
   x ^ y < x ^ z ↔ z < y :=
-by rw [lt_iff_not_ge', rpow_le_rpow_left_iff_of_base_lt_one hx0 hx1, lt_iff_not_ge']
+by rw [lt_iff_not_le, rpow_le_rpow_left_iff_of_base_lt_one hx0 hx1, lt_iff_not_le]
 
 lemma rpow_lt_one {x z : ℝ} (hx1 : 0 ≤ x) (hx2 : x < 1) (hz : 0 < z) : x^z < 1 :=
 by { rw ← one_rpow z, exact rpow_lt_rpow hx1 hx2 hz }

src/data/real/hyperreal.lean

@@ -170,10 +170,10 @@ have HR₁ : S.nonempty :=
 have HR₂ : bdd_above S :=
   ⟨ r₂, λ y hy, le_of_lt (coe_lt_coe.1 (lt_of_lt_of_le hy (not_lt.mp hr₂))) ⟩,
 λ δ hδ,
-  ⟨ lt_of_not_ge' $ λ c,
+  ⟨ lt_of_not_le $ λ c,
       have hc : ∀ y ∈ S, y ≤ R - δ := λ y hy, coe_le_coe.1 $ le_of_lt $ lt_of_lt_of_le hy c,
       not_lt_of_le (cSup_le HR₁ hc) $ sub_lt_self R hδ,
-    lt_of_not_ge' $ λ c,
+    lt_of_not_le $ λ c,
       have hc : ↑(R + δ / 2) < x :=
         lt_of_lt_of_le (add_lt_add_left (coe_lt_coe.2 (half_lt_self hδ)) R) c,
       not_lt_of_le (le_cSup HR₂ hc) $ (lt_add_iff_pos_right _).mpr $ half_pos hδ⟩

src/group_theory/subgroup/basic.lean

@@ -714,7 +714,7 @@ end
   λ h, by simp [h]⟩
 
 @[to_additive] lemma one_lt_card_iff_ne_bot [fintype H] : 1 < fintype.card H ↔ H ≠ ⊥ :=
-lt_iff_not_ge'.trans (not_iff_not.mpr H.card_le_one_iff_eq_bot)
+lt_iff_not_le.trans H.card_le_one_iff_eq_bot.not
 
 /-- The inf of two subgroups is their intersection. -/
 @[to_additive "The inf of two `add_subgroups`s is their intersection."]

src/order/basic.lean

@@ -57,48 +57,90 @@ open function
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w} {r : α → α → Prop}
 
-lemma ge_antisymm [partial_order α] {a b : α} (hab : a ≤ b) (hba : b ≤ a) : b = a :=
-le_antisymm hba hab
+section preorder
+variables [preorder α] {a b c : α}
+
+lemma le_trans' : b ≤ c → a ≤ b → a ≤ c := flip le_trans
+lemma lt_trans' : b < c → a < b → a < c := flip lt_trans
+lemma lt_of_le_of_lt' : b ≤ c → a < b → a < c := flip lt_of_lt_of_le
+lemma lt_of_lt_of_le' : b < c → a ≤ b → a < c := flip lt_of_le_of_lt
+
+end preorder
+
+section partial_order
+variables [partial_order α] {a b : α}
+
+lemma ge_antisymm : a ≤ b → b ≤ a → b = a := flip le_antisymm
+lemma lt_of_le_of_ne' : a ≤ b → b ≠ a → a < b := λ h₁ h₂, lt_of_le_of_ne h₁ h₂.symm
+lemma ne.lt_of_le : a ≠ b → a ≤ b → a < b := flip lt_of_le_of_ne
+lemma ne.lt_of_le' : b ≠ a → a ≤ b → a < b := flip lt_of_le_of_ne'
+
+end partial_order
 
 attribute [simp] le_refl
 attribute [ext] has_le
 
 alias le_trans        ← has_le.le.trans
+alias le_trans'       ← has_le.le.trans'
 alias lt_of_le_of_lt  ← has_le.le.trans_lt
+alias lt_of_le_of_lt' ← has_le.le.trans_lt'
 alias le_antisymm     ← has_le.le.antisymm
 alias ge_antisymm     ← has_le.le.antisymm'
 alias lt_of_le_of_ne  ← has_le.le.lt_of_ne
+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 decidable.lt_or_eq_of_le ← has_le.le.lt_or_eq_dec
 
 alias le_of_lt        ← has_lt.lt.le
 alias lt_trans        ← has_lt.lt.trans
+alias lt_trans'       ← has_lt.lt.trans'
 alias lt_of_lt_of_le  ← has_lt.lt.trans_le
+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
 
 attribute [nolint decidable_classical] has_le.le.lt_or_eq_dec
 
+section
+variables [preorder α] {a b c : α}
+
 /-- A version of `le_refl` where the argument is implicit -/
-lemma le_rfl [preorder α] {x : α} : x ≤ x := le_refl x
+lemma le_rfl : a ≤ a := le_refl a
+
+@[simp] lemma lt_self_iff_false (x : α) : x < x ↔ false := ⟨lt_irrefl x, false.elim⟩
+
+lemma le_of_le_of_eq (hab : a ≤ b) (hbc : b = c) : a ≤ c := hab.trans hbc.le
+lemma le_of_eq_of_le (hab : a = b) (hbc : b ≤ c) : a ≤ c := hab.le.trans hbc
+lemma lt_of_lt_of_eq (hab : a < b) (hbc : b = c) : a < c := hab.trans_le hbc.le
+lemma lt_of_eq_of_lt (hab : a = b) (hbc : b < c) : a < c := hab.le.trans_lt hbc
+lemma le_of_le_of_eq' : b ≤ c → a = b → a ≤ c := flip le_of_eq_of_le
+lemma le_of_eq_of_le' : b = c → a ≤ b → a ≤ c := flip le_of_le_of_eq
+lemma lt_of_lt_of_eq' : b < c → a = b → a < c := flip lt_of_eq_of_lt
+lemma lt_of_eq_of_lt' : b = c → a < b → a < c := flip lt_of_lt_of_eq
+
+alias le_of_le_of_eq  ← has_le.le.trans_eq
+alias le_of_le_of_eq' ← has_le.le.trans_eq'
+alias lt_of_lt_of_eq  ← has_lt.lt.trans_eq
+alias lt_of_lt_of_eq' ← has_lt.lt.trans_eq'
+alias le_of_eq_of_le  ← eq.trans_le
+alias le_of_eq_of_le' ← eq.trans_ge
+alias lt_of_eq_of_lt  ← eq.trans_lt
+alias lt_of_eq_of_lt' ← eq.trans_gt
 
-@[simp] lemma lt_self_iff_false [preorder α] (x : α) : x < x ↔ false :=
-⟨lt_irrefl x, false.elim⟩
+end
 
 namespace eq
+variables [preorder α] {x y z : α}
 
 /-- If `x = y` then `y ≤ x`. Note: this lemma uses `y ≤ x` instead of `x ≥ y`, because `le` is used
 almost exclusively in mathlib. -/
-protected lemma ge [preorder α] {x y : α} (h : x = y) : y ≤ x := h.symm.le
-
-lemma trans_le [preorder α] {x y z : α} (h1 : x = y) (h2 : y ≤ z) : x ≤ z := h1.le.trans h2
+protected lemma ge (h : x = y) : y ≤ x := h.symm.le
 
-lemma not_lt [preorder α] {x y : α} (h : x = y) : ¬(x < y) := λ h', h'.ne h
-
-lemma not_gt [preorder α] {x y : α} (h : x = y) : ¬(y < x) := h.symm.not_lt
+lemma not_lt (h : x = y) : ¬ x < y := λ h', h'.ne h
+lemma not_gt (h : x = y) : ¬ y < x := h.symm.not_lt
 
 end eq
 
@@ -107,8 +149,6 @@ namespace has_le.le
 @[nolint ge_or_gt] -- see Note [nolint_ge]
 protected lemma ge [has_le α] {x y : α} (h : x ≤ y) : y ≥ x := h
 
-lemma trans_eq [preorder α] {x y z : α} (h1 : x ≤ y) (h2 : y = z) : x ≤ z := h1.trans h2.le
-
 lemma lt_iff_ne [partial_order α] {x y : α} (h : x ≤ y) : x < y ↔ x ≠ y := ⟨λ h, h.ne, h.lt_of_ne⟩
 
 lemma le_iff_eq [partial_order α] {x y : α} (h : x ≤ y) : y ≤ x ↔ y = x :=
@@ -148,9 +188,9 @@ protected lemma gt.lt [has_lt α] {x y : α} (h : x > y) : y < x := h
 theorem ge_of_eq [preorder α] {a b : α} (h : a = b) : a ≥ b := h.ge
 
 @[simp, nolint ge_or_gt] -- see Note [nolint_ge]
-lemma ge_iff_le [preorder α] {a b : α} : a ≥ b ↔ b ≤ a := iff.rfl
+lemma ge_iff_le [has_le α] {a b : α} : a ≥ b ↔ b ≤ a := iff.rfl
 @[simp, nolint ge_or_gt] -- see Note [nolint_ge]
-lemma gt_iff_lt [preorder α] {a b : α} : a > b ↔ b < a := iff.rfl
+lemma gt_iff_lt [has_lt α] {a b : α} : a > b ↔ b < a := iff.rfl
 
 lemma not_le_of_lt [preorder α] {a b : α} (h : a < b) : ¬ b ≤ a := (le_not_le_of_lt h).right
 
@@ -205,17 +245,17 @@ lemma ne.le_iff_lt [partial_order α] {a b : α} (h : a ≠ b) : a ≤ b ↔ a <
 ⟨λ h', lt_of_le_of_ne h' h, λ h, h.le⟩
 
 -- See Note [decidable namespace]
-protected lemma decidable.ne_iff_lt_iff_le [partial_order α] [decidable_eq α]
-  {a b : α} : (a ≠ b ↔ a < b) ↔ a ≤ b :=
+protected lemma decidable.ne_iff_lt_iff_le [partial_order α] [decidable_eq α] {a b : α} :
+  (a ≠ b ↔ a < b) ↔ a ≤ b :=
 ⟨λ h, decidable.by_cases le_of_eq (le_of_lt ∘ h.mp), λ h, ⟨lt_of_le_of_ne h, ne_of_lt⟩⟩
 
 @[simp] lemma ne_iff_lt_iff_le [partial_order α] {a b : α} : (a ≠ b ↔ a < b) ↔ a ≤ b :=
 by haveI := classical.dec; exact decidable.ne_iff_lt_iff_le
 
-lemma lt_of_not_ge' [linear_order α] {a b : α} (h : ¬ b ≤ a) : a < b :=
+lemma lt_of_not_le [linear_order α] {a b : α} (h : ¬ b ≤ a) : a < b :=
 ((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'⟩
+lemma lt_iff_not_le [linear_order α] {x y : α} : x < y ↔ ¬ y ≤ x := ⟨not_le_of_lt, lt_of_not_le⟩
 
 lemma ne.lt_or_lt [linear_order α] {x y : α} (h : x ≠ y) : x < y ∨ y < x := lt_or_gt_of_ne h
 
@@ -234,7 +274,7 @@ 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', (H h').not_lt h
+lt_of_not_le $ λ h', (H h').not_lt 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) :=

src/order/bounded.lean

@@ -240,7 +240,7 @@ by simp_rw [← not_le, bounded_le_inter_not_le]
 
 theorem unbounded_le_inter_lt [linear_order α] (a : α) :
   unbounded (≤) (s ∩ {b | a < b}) ↔ unbounded (≤) s :=
-by { convert unbounded_le_inter_not_le a, ext, exact lt_iff_not_ge' }
+by { convert unbounded_le_inter_not_le a, ext, exact lt_iff_not_le }
 
 theorem bounded_le_inter_le [linear_order α] (a : α) :
   bounded (≤) (s ∩ {b | a ≤ b}) ↔ bounded (≤) s :=

src/order/bounded_order.lean

@@ -183,8 +183,8 @@ variables [partial_order α] [order_bot α] [preorder β] {f : α → β} {a b :
 lemma not_is_min_iff_ne_bot : ¬ is_min a ↔ a ≠ ⊥ := is_min_iff_eq_bot.not
 lemma not_is_bot_iff_ne_bot : ¬ is_bot a ↔ a ≠ ⊥ := is_bot_iff_eq_bot.not
 
-alias is_min_iff_eq_bot ↔ _ is_min.eq_bot
-alias is_bot_iff_eq_bot ↔ _ is_bot.eq_bot
+alias is_min_iff_eq_bot ↔ is_min.eq_bot _
+alias is_bot_iff_eq_bot ↔ is_bot.eq_bot _
 
 @[simp] lemma le_bot_iff : a ≤ ⊥ ↔ a = ⊥ := bot_le.le_iff_eq
 lemma bot_unique (h : a ≤ ⊥) : a = ⊥ := h.antisymm bot_le

src/order/rel_classes.lean

@@ -20,6 +20,8 @@ variables {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β 
 
 open function
 
+lemma of_eq [is_refl α r] : ∀ {a b}, a = b → r a b | _ _ ⟨h⟩ := refl _
+
 lemma comm [is_symm α r] {a b : α} : r a b ↔ r b a := ⟨symm, symm⟩
 lemma antisymm' [is_antisymm α r] {a b : α} : r a b → r b a → b = a := λ h h', antisymm h' h
 
@@ -95,6 +97,8 @@ begin
   exact trans h₁ h₃, rw ←h₃, exact h₁, exfalso, exact h₂ h₃
 end
 
+lemma transitive_of_trans (r : α → α → Prop) [is_trans α r] : transitive r := λ _ _ _, trans
+
 /-- Construct a partial order from a `is_strict_order` relation.
 
 See note [reducible non-instances]. -/
@@ -449,6 +453,11 @@ instance [linear_order α] : is_order_connected α (<) := by apply_instance
 instance [linear_order α] : is_incomp_trans α (<) := by apply_instance
 instance [linear_order α] : is_strict_weak_order α (<) := by apply_instance
 
+lemma transitive_le [preorder α] : transitive (@has_le.le α _) := transitive_of_trans _
+lemma transitive_lt [preorder α] : transitive (@has_lt.lt α _) := transitive_of_trans _
+lemma transitive_ge [preorder α] : transitive (@ge α _) := transitive_of_trans _
+lemma transitive_gt [preorder α] : transitive (@gt α _) := transitive_of_trans _
+
 instance order_dual.is_total_le [has_le α] [is_total α (≤)] : is_total (order_dual α) (≤) :=
 @is_total.swap α _ _
 

src/ring_theory/perfection.lean

@@ -353,7 +353,7 @@ lemma pre_val_mk {x : O} (hx : (ideal.quotient.mk _ x : mod_p K v O hv p) ≠ 0)
 begin
   obtain ⟨r, hr⟩ := ideal.mem_span_singleton'.1 (ideal.quotient.eq.1 $ quotient.sound' $
     @quotient.mk_out' O (ideal.span {p} : ideal O).quotient_rel x),
-  refine (if_neg hx).trans (v.map_eq_of_sub_lt $ lt_of_not_ge' _),
+  refine (if_neg hx).trans (v.map_eq_of_sub_lt $ lt_of_not_le _),
   erw [← ring_hom.map_sub, ← hr, hv.le_iff_dvd],
   exact λ hprx, hx (ideal.quotient.eq_zero_iff_mem.2 $ ideal.mem_span_singleton.2 $
     dvd_of_mul_left_dvd hprx),
@@ -388,7 +388,7 @@ end
 lemma v_p_lt_pre_val {x : mod_p K v O hv p} : v p < pre_val K v O hv p x ↔ x ≠ 0 :=
 begin
   refine ⟨λ h hx, by { rw [hx, pre_val_zero] at h, exact not_lt_zero' h },
-    λ h, lt_of_not_ge' $ λ hp, h _⟩,
+    λ h, lt_of_not_le $ λ hp, h _⟩,
   obtain ⟨r, rfl⟩ := ideal.quotient.mk_surjective x,
   rw [pre_val_mk h, ← map_nat_cast (algebra_map O K) p, hv.le_iff_dvd] at hp,
   rw [ideal.quotient.eq_zero_iff_mem, ideal.mem_span_singleton], exact hp
@@ -402,7 +402,7 @@ lemma pre_val_eq_zero {x : mod_p K v O hv p} : pre_val K v O hv p x = 0 ↔ x =
 variables (hv hvp)
 lemma v_p_lt_val {x : O} :
   v p < v (algebra_map O K x) ↔ (ideal.quotient.mk _ x : mod_p K v O hv p) ≠ 0 :=
-by rw [lt_iff_not_ge', not_iff_not, ← map_nat_cast (algebra_map O K) p, hv.le_iff_dvd,
+by rw [lt_iff_not_le, not_iff_not, ← map_nat_cast (algebra_map O K) p, hv.le_iff_dvd,
       ideal.quotient.eq_zero_iff_mem, ideal.mem_span_singleton]
 
 open nnreal

src/ring_theory/polynomial/basic.lean

@@ -77,7 +77,7 @@ theorem mem_degree_lt {n : ℕ} {f : R[X]} :
   f ∈ degree_lt R n ↔ degree f < n :=
 by { simp_rw [degree_lt, submodule.mem_infi, linear_map.mem_ker, degree,
     finset.sup_lt_iff (with_bot.bot_lt_coe n), mem_support_iff, with_bot.some_eq_coe,
-    with_bot.coe_lt_coe, lt_iff_not_ge', ne, not_imp_not], refl }
+    with_bot.coe_lt_coe, lt_iff_not_le, ne, not_imp_not], refl }
 
 @[mono] theorem degree_lt_mono {m n : ℕ} (H : m ≤ n) :
   degree_lt R m ≤ degree_lt R n :=

test/finish4.lean

@@ -56,4 +56,4 @@ constant  exp_add    : ∀ x y, exp (x + y) = exp x * exp y
 
 theorem log_mul' {x y : real} (hx : x > 0) (hy : y > 0) :
   log (x * y) = log x + log y :=
-by finish using [log_exp_eq, exp_log_eq, exp_add]
+by rw [←log_exp_eq (log x + log y), exp_add, exp_log_eq hx, exp_log_eq hy]