chore(Order/Def): avoid relying on internal class projections in other files (leanprover-community#31808)

This PR removes references to lemmas that are class projections of `Preorder`, `PartialOrder` or `LinearOrder`. Instead, the global namespace lemmas should be used. To avoid accidentally referring to these lemmas, they are marked as `protected`.

I hope that it will be possible to hide these lemmas from the imports, using the module system. See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Should.20duplicated.20class.20projections.20be.20private.3F/with/558208782

Author: JovanGerb

Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

@@ -331,7 +331,7 @@ theorem trichotomy_of_mul_eq_mul
     (h : a * b = c * d) : (a = c ∧ b = d) ∨ a < c ∨ b < d := by
   obtain hac | rfl | hca := lt_trichotomy a c
   · grind
-  · left; simpa using mul_right_inj_of_comparable (LinearOrder.le_total d b) |>.1 h
+  · left; simpa using mul_right_inj_of_comparable (le_total d b) |>.1 h
   · obtain hbd | rfl | hdb := lt_trichotomy b d
     · grind
     · exact False.elim <| ne_of_lt (mul_lt_mul_left hca b) h.symm

Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean

@@ -107,7 +107,7 @@ theorem tendsto_integral_mul_one_add_inv_smul_sq_pow (g : E →ᵇ ℝ) (hε : 0
       (div_nonneg (mul_nonneg (le_of_lt hε) (mul_self_nonneg (g x))) (le_of_lt hnpos)))⟩
     apply le_trans (by linarith) (sub_nonneg_of_le ((div_le_one hnpos).mpr _))
     apply le_trans (le_trans _ (le_of_lt hgN)) (Nat.cast_le.mpr hn)
-    apply mul_le_mul (Preorder.le_refl ε) _ (mul_self_nonneg (g x)) (le_of_lt hε)
+    apply mul_le_mul (le_refl ε) _ (mul_self_nonneg (g x)) (le_of_lt hε)
     rw [← abs_le_iff_mul_self_le, abs_norm]
     exact norm_coe_le_norm g x
   · apply Eventually.of_forall

Mathlib/CategoryTheory/Category/Preorder.lean

@@ -48,7 +48,7 @@ See `CategoryTheory.homOfLE` and `CategoryTheory.leOfHom`. -/
 instance (priority := 100) smallCategory (α : Type u) [Preorder α] : SmallCategory α where
   Hom U V := ULift (PLift (U ≤ V))
   id X := ⟨⟨le_refl X⟩⟩
-  comp f g := ⟨⟨le_trans _ _ _ f.down.down g.down.down⟩⟩
+  comp f g := ⟨⟨le_trans f.down.down g.down.down⟩⟩
 
 instance subsingleton_hom {α : Type u} [Preorder α] (U V : α) : Subsingleton (U ⟶ V) :=
   ⟨fun _ _ => ULift.ext _ _ (Subsingleton.elim _ _ )⟩

Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean

@@ -138,14 +138,14 @@ lemma ofCoconeObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂
 when `c : Cocone F`. -/
 @[simps!]
 def restrictionLTOfCoconeIso :
-    SmallObject.restrictionLT (ofCocone c) (Preorder.le_refl j) ≅ F :=
+    SmallObject.restrictionLT (ofCocone c) (le_refl j) ≅ F :=
   NatIso.ofComponents (fun ⟨i, hi⟩ ↦ ofCoconeObjIso c i hi)
     (by intros; apply ofCoconeObjIso_hom_naturality)
 
 variable {c} in
-/-- If `c` is a colimit cocone, then so is `coconeOfLE (ofCocone c) (Preorder.le_refl j)`. -/
+/-- If `c` is a colimit cocone, then so is `coconeOfLE (ofCocone c) (le_refl j)`. -/
 def isColimitCoconeOfLEOfCocone (hc : IsColimit c) :
-    IsColimit (coconeOfLE (ofCocone c) (Preorder.le_refl j)) :=
+    IsColimit (coconeOfLE (ofCocone c) (le_refl j)) :=
   (IsColimit.precomposeInvEquiv (restrictionLTOfCoconeIso c) _).1
     (IsColimit.ofIsoColimit hc
       (Cocones.ext (ofCoconeObjIsoPt c).symm (fun ⟨i, hi⟩ ↦ by

Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -398,7 +398,7 @@ theorem eLpNorm_le_of_ae_enorm_bound {ε} [TopologicalSpace ε] [ESeminormedAddM
   · simp
   by_cases hp : p = 0
   · simp [hp]
-  have : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ := hfC.mono fun x hx ↦ hx.trans (Preorder.le_refl C)
+  have : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ ‖C‖ₑ := hfC.mono fun x hx ↦ hx.trans (le_refl C)
   refine (eLpNorm_mono_enorm_ae this).trans_eq ?_
   rw [eLpNorm_const _ hp (NeZero.ne μ), one_div, enorm_eq_self, smul_eq_mul]
 

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean

@@ -42,14 +42,14 @@ theorem abs_le_left_of_norm (m n : ℤ) : |n| ≤ ‖![n, m]‖ := by
     Matrix.cons_val_one, Matrix.cons_val_fin_one, Nat.cast_max, le_sup_iff]
   left
   rw [Int.abs_eq_natAbs]
-  exact Preorder.le_refl _
+  exact le_refl _
 
 theorem abs_le_right_of_norm (m n : ℤ) : |m| ≤ ‖![n, m]‖ := by
   simp only [EisensteinSeries.norm_eq_max_natAbs, Fin.isValue, Matrix.cons_val_zero,
     Matrix.cons_val_one, Matrix.cons_val_fin_one, Nat.cast_max, le_sup_iff]
   right
   rw [Int.abs_eq_natAbs]
-  exact Preorder.le_refl _
+  exact le_refl _
 
 lemma abs_norm_eq_max_natAbs (n : ℕ) : ‖![1, (n + 1 : ℤ)]‖ = n + 1 := by
   simp only [EisensteinSeries.norm_eq_max_natAbs, Matrix.cons_val_zero, Matrix.cons_val_one,

Mathlib/Order/Defs/LinearOrder.lean

@@ -57,7 +57,7 @@ macro "compareOfLessAndEq_rfl" : tactic =>
 We assume that every linear ordered type has decidable `(≤)`, `(<)`, and `(=)`. -/
 class LinearOrder (α : Type*) extends PartialOrder α, Min α, Max α, Ord α where
   /-- A linear order is total. -/
-  le_total (a b : α) : a ≤ b ∨ b ≤ a
+  protected le_total (a b : α) : a ≤ b ∨ b ≤ a
   /-- In a linearly ordered type, we assume the order relations are all decidable. -/
   toDecidableLE : DecidableLE α
   /-- In a linearly ordered type, we assume the order relations are all decidable. -/
@@ -67,9 +67,9 @@ class LinearOrder (α : Type*) extends PartialOrder α, Min α, Max α, Ord α w
   min := fun a b => if a ≤ b then a else b
   max := fun a b => if a ≤ b then b else a
   /-- The minimum function is equivalent to the one you get from `minOfLe`. -/
-  min_def : ∀ a b, min a b = if a ≤ b then a else b := by intros; rfl
+  protected min_def : ∀ a b, min a b = if a ≤ b then a else b := by intros; rfl
   /-- The minimum function is equivalent to the one you get from `maxOfLe`. -/
-  max_def : ∀ a b, max a b = if a ≤ b then b else a := by intros; rfl
+  protected max_def : ∀ a b, max a b = if a ≤ b then b else a := by intros; rfl
   compare a b := compareOfLessAndEq a b
   /-- Comparison via `compare` is equal to the canonical comparison given decidable `<` and `=`. -/
   compare_eq_compareOfLessAndEq : ∀ a b, compare a b = compareOfLessAndEq a b := by

Mathlib/Order/Defs/PartialOrder.lean

@@ -43,13 +43,10 @@ section Preorder
 
 /-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/
 class Preorder (α : Type*) extends LE α, LT α where
-  le_refl : ∀ a : α, a ≤ a
-  le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
+  protected le_refl : ∀ a : α, a ≤ a
+  protected le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c
   lt := fun a b => a ≤ b ∧ ¬b ≤ a
-  lt_iff_le_not_ge : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
-
-attribute [to_dual self (reorder := a c, 6 7)] Preorder.le_trans
-attribute [to_dual self] Preorder.lt_iff_le_not_ge
+  protected lt_iff_le_not_ge : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
 
 instance [Preorder α] : Std.LawfulOrderLT α where
   lt_iff := Preorder.lt_iff_le_not_ge
@@ -69,7 +66,10 @@ variable [Preorder α] {a b c : α}
 lemma le_rfl : a ≤ a := le_refl a
 
 /-- The relation `≤` on a preorder is transitive. -/
-@[to_dual ge_trans] lemma le_trans : a ≤ b → b ≤ c → a ≤ c := Preorder.le_trans _ _ _
+lemma le_trans : a ≤ b → b ≤ c → a ≤ c := Preorder.le_trans _ _ _
+
+@[to_dual existing le_trans]
+lemma ge_trans : b ≤ a → c ≤ b → c ≤ a := flip le_trans
 
 @[to_dual self]
 lemma lt_iff_le_not_ge : a < b ↔ a ≤ b ∧ ¬b ≤ a := Preorder.lt_iff_le_not_ge _ _
@@ -176,18 +176,18 @@ section PartialOrder
 
 /-- A partial order is a reflexive, transitive, antisymmetric relation `≤`. -/
 class PartialOrder (α : Type*) extends Preorder α where
-  le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
-
-attribute [to_dual self (reorder := 5 6)] PartialOrder.le_antisymm
+  protected le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
 
 instance [PartialOrder α] : Std.IsPartialOrder α where
   le_antisymm := PartialOrder.le_antisymm
 
 variable [PartialOrder α] {a b : α}
 
-@[to_dual ge_antisymm]
 lemma le_antisymm : a ≤ b → b ≤ a → a = b := PartialOrder.le_antisymm _ _
 
+@[to_dual existing le_antisymm]
+lemma ge_antisymm : b ≤ a → a ≤ b → a = b := flip le_antisymm
+
 @[to_dual eq_of_ge_of_le]
 alias eq_of_le_of_ge := le_antisymm
 

Mathlib/Order/Max.lean

@@ -198,7 +198,7 @@ theorem IsTop.isMax_iff {α} [PartialOrder α] {i j : α} (h : IsTop i) : IsMax
 
 theorem IsBot.isMin_iff {α} [PartialOrder α] {i j : α} (h : IsBot i) : IsMin j ↔ j = i := by
   simp_rw [le_antisymm_iff, h j, and_true]
-  exact ⟨fun a ↦ a (h j), fun a h' ↦ fun _ ↦ Preorder.le_trans j i h' a (h h')⟩
+  exact ⟨fun a ↦ a (h j), fun a h' ↦ fun _ ↦ le_trans a (h h')⟩
 
 @[simp]
 theorem isBot_toDual_iff : IsBot (toDual a) ↔ IsTop a :=

Mathlib/Order/RelClasses.lean

@@ -466,7 +466,7 @@ end Order.Preimage
 
 
 /-- An unbundled relation class stating that `r` is the nonstrict relation corresponding to the
-strict relation `s`. Compare `Preorder.lt_iff_le_not_ge`. This is mostly meant to provide dot
+strict relation `s`. Compare `lt_iff_le_not_ge`. This is mostly meant to provide dot
 notation on `(⊆)` and `(⊂)`. -/
 class IsNonstrictStrictOrder (α : Type*) (r : semiOutParam (α → α → Prop)) (s : α → α → Prop) :
     Prop where