chore(Logic/Relation): use ≤ to spell subrelation (#30526)

Replace every `∀ x y, r x y → r' x y` with `r ≤ r'`

Author: SnirBroshi

Mathlib/CategoryTheory/IsConnected.lean

@@ -381,7 +381,7 @@ def Zigzag.setoid (J : Type u₂) [Category.{v₁} J] : Setoid J where
 -/
 theorem zigzag_prefunctor_obj_of_zigzag (F : J ⥤q K) {j₁ j₂ : J} (h : Zigzag j₁ j₂) :
     Zigzag (F.obj j₁) (F.obj j₂) :=
-  h.lift _ fun _ _ => Or.imp (Nonempty.map fun f => F.map f) (Nonempty.map fun f => F.map f)
+  h.lift F.obj fun _ _ => Or.imp (Nonempty.map fun f => F.map f) (Nonempty.map fun f => F.map f)
 
 /-- If there is a zigzag from `j₁` to `j₂`, then there is a zigzag from `F j₁` to
 `F j₂` as long as `F` is a functor.

Mathlib/CategoryTheory/Limits/Types/Coequalizers.lean

@@ -65,7 +65,7 @@ theorem coequalizer_preimage_image_eq_of_preimage_eq (π : Y ⟶ Z) (e : f ≫ 
       (mono_iff_injective
             (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv).mp
         inferInstance
-    refine (eqv.eqvGen_iff.mp (Relation.EqvGen.mono lem (Quot.eqvGen_exact ?_))).mp hy
+    refine (eqv.eqvGen_iff.mp (Relation.EqvGen.mono lem y _ (Quot.eqvGen_exact ?_))).mp hy
     apply e''
     convert! e'
   · exact fun hx => ⟨_, hx, rfl⟩

Mathlib/CategoryTheory/Limits/Types/Filtered.lean

@@ -117,7 +117,7 @@ protected theorem rel_eq_eqvGen_colimitTypeRel :
   constructor
   · apply eqvGen_colimitTypeRel_of_rel
   · rw [← (FilteredColimit.rel_equiv F).eqvGen_iff]
-    exact Relation.EqvGen.mono (rel_of_colimitTypeRel F)
+    exact Relation.EqvGen.mono (rel_of_colimitTypeRel F) _ _
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -203,7 +203,7 @@ theorem church_rosser : Red L₁ L₂ → Red L₁ L₃ → Join Red L₂ L₃ :
 
 @[to_additive]
 theorem cons_cons {p} : Red L₁ L₂ → Red (p :: L₁) (p :: L₂) :=
-  ReflTransGen.lift (List.cons p) fun _ _ => Step.cons
+  ReflTransGen.lift (List.cons p) (fun _ _ => Step.cons) L₁ L₂
 
 @[to_additive]
 theorem cons_cons_iff (p) : Red (p :: L₁) (p :: L₂) ↔ Red L₁ L₂ :=
@@ -322,11 +322,8 @@ theorem Step.sublist (H : Red.Step L₁ L₂) : L₂ <+ L₁ := by
 @[to_additive
 /-- If `w₁ w₂` are words such that `w₁` reduces to `w₂`, then `w₂` is a sublist of `w₁`. -/]
 protected theorem sublist : Red L₁ L₂ → L₂ <+ L₁ :=
-  @reflTransGen_of_isTrans_reflexive
-    _ (fun a b => b <+ a) _ _ _
-    ⟨List.Sublist.refl⟩
-    ⟨fun _a _b _c hab hbc => List.Sublist.trans hbc hab⟩
-    (fun _ _ => Red.Step.sublist)
+  @reflTransGen_le_of_le _ (fun a b => b <+ a) _ ⟨List.Sublist.refl⟩
+    ⟨fun _a _b _c hab hbc => List.Sublist.trans hbc hab⟩ (fun _ _ => Red.Step.sublist) L₁ L₂
 
 @[to_additive]
 theorem length_le (h : Red L₁ L₂) : L₂.length ≤ L₁.length :=
@@ -369,16 +366,16 @@ theorem equivalence_join_red : Equivalence (Join (@Red α)) :=
 @[to_additive]
 theorem join_red_of_step (h : Red.Step L₁ L₂) : Join Red L₁ L₂ := by
   unfold Red
-  exact join_of_single h.to_red
+  exact le_join_of_refl L₁ L₂ h.to_red
 
 @[to_additive]
 theorem eqvGen_step_iff_join_red : EqvGen Red.Step L₁ L₂ ↔ Join Red L₁ L₂ :=
   Iff.intro
     (fun h =>
       have : EqvGen (Join Red) L₁ L₂ := h.mono fun _ _ => join_red_of_step
       equivalence_join_red.eqvGen_iff.1 this)
-    (join_of_equivalence (Relation.EqvGen.is_equivalence _) fun _ _ =>
-      reflTransGen_of_equivalence (Relation.EqvGen.is_equivalence _) EqvGen.rel)
+    (join_le_of_equivalence_of_le (Relation.EqvGen.is_equivalence _)
+      (reflTransGen_le_of_equivalence_of_le (Relation.EqvGen.is_equivalence _) EqvGen.rel) L₁ L₂)
 
 /-! ### Reduced words -/
 
@@ -589,7 +586,7 @@ theorem Red.Step.invRev {L₁ L₂ : List (α × Bool)} (h : Red.Step L₁ L₂)
 
 @[to_additive]
 theorem Red.invRev {L₁ L₂ : List (α × Bool)} (h : Red L₁ L₂) : Red (invRev L₁) (invRev L₂) :=
-  Relation.ReflTransGen.lift _ (fun _a _b => Red.Step.invRev) h
+  Relation.ReflTransGen.lift FreeGroup.invRev (fun _a _b => Red.Step.invRev) L₁ L₂ h
 
 @[to_additive (attr := simp)]
 theorem Red.step_invRev_iff :

Mathlib/Logic/Relation.lean

@@ -9,6 +9,7 @@ public import Mathlib.Logic.Relator
 public import Mathlib.Tactic.Use
 public import Mathlib.Tactic.MkIffOfInductiveProp
 public import Mathlib.Tactic.SimpRw
+public import Mathlib.Order.Defs.Prop
 public import Mathlib.Order.Defs.Unbundled
 public import Batteries.Logic
 public import Batteries.Tactic.Trans
@@ -53,7 +54,7 @@ the bundled version, see `Rel`.
 
 open Function
 
-variable {α β γ δ ε ζ : Sort*}
+variable {α β γ δ ε ζ : Type*}
 
 section NeImp
 
@@ -76,19 +77,21 @@ theorem Std.Refl.ne_imp_iff [Std.Refl r] {x y : α} : x ≠ y → r x y ↔ r x
   ⟨Std.Refl.rel_of_ne_imp, fun hr _ ↦ hr⟩
 
 @[deprecated (since := "2026-03-27")] alias Reflexive.ne_imp_iff := Std.Refl.ne_imp_iff
-
 @[deprecated (since := "2026-03-27")] alias reflexive_ne_imp_iff := Std.Refl.ne_imp_iff
 
-theorem refl_iff_subrelation_eq : Std.Refl r ↔ Subrelation Eq r := by
-  grind [Std.Refl, Subrelation]
+theorem refl_iff_eq_le : Std.Refl r ↔ Eq ≤ r := by
+  unfold Pi.hasLe Prop.le
+  grind [Std.Refl]
 
-@[deprecated (since := "2026-03-27")] alias reflexive_iff_subrelation_eq := refl_iff_subrelation_eq
+@[deprecated (since := "2026-06-30")] alias refl_iff_subrelation_eq := refl_iff_eq_le
+@[deprecated (since := "2026-03-27")] alias reflexive_iff_subrelation_eq := refl_iff_eq_le
 
-theorem irrefl_iff_subrelation_ne : Std.Irrefl r ↔ Subrelation r Ne := by
-  grind [Std.Irrefl, Subrelation]
+theorem irrefl_iff_le_ne : Std.Irrefl r ↔ r ≤ Ne := by
+  unfold Pi.hasLe Prop.le
+  grind [Std.Irrefl]
 
-@[deprecated (since := "2026-02-12")]
-alias irreflexive_iff_subrelation_ne := irrefl_iff_subrelation_ne
+@[deprecated (since := "2026-06-30")] alias irrefl_iff_subrelation_ne := irrefl_iff_le_ne
+@[deprecated (since := "2026-02-12")] alias irreflexive_iff_subrelation_ne := irrefl_iff_le_ne
 
 protected theorem Std.Symm.iff [Std.Symm r] (x y : α) : r x y ↔ r y x :=
   ⟨symm_of r, symm_of r⟩
@@ -280,22 +283,21 @@ lemma map_equivalence {r : α → α → Prop} (hr : Equivalence r) (f : α →
   symm := @(hr.stdSymm.map f |>.symm)
   trans := @(hr.isTrans.map hf_ker |>.trans)
 
--- TODO: state this using `≤`, after adjusting imports.
-lemma map_mono {r s : α → β → Prop} {f : α → γ} {g : β → δ} (h : ∀ x y, r x y → s x y) :
-    ∀ x y, Relation.Map r f g x y → Relation.Map s f g x y :=
+lemma map_mono {r s : α → β → Prop} {f : α → γ} {g : β → δ} (h : r ≤ s) :
+    Relation.Map r f g ≤ Relation.Map s f g :=
   fun _ _ ⟨x, y, hxy, hx, hy⟩ => ⟨x, y, h _ _ hxy, hx, hy⟩
 
-lemma le_onFun_map {r : α → α → Prop} (f : α → β) : Subrelation r (Relation.Map r f f on f) := by
-  intro
+lemma le_onFun_map {r : α → α → Prop} (f : α → β) : r ≤ (Relation.Map r f f on f) := by
+  unfold Pi.hasLe Prop.le
   grind [Relation.Map]
 
 lemma onFun_map_eq_of_injective {r : α → α → Prop} {f : α → β} (hinj : f.Injective) :
     (Relation.Map r f f on f) = r := by
   ext x y
   exact ⟨fun ⟨x', y', hr, hx, hy⟩ ↦ hinj hx ▸ hinj hy ▸ hr, fun h ↦ ⟨x, y, h, rfl, rfl⟩⟩
 
-lemma map_onFun_le {r : β → β → Prop} (f : α → β) : Subrelation (Relation.Map (r on f) f f) r := by
-  intro
+lemma map_onFun_le {r : β → β → Prop} (f : α → β) : Relation.Map (r on f) f f ≤ r := by
+  unfold Pi.hasLe Prop.le
   grind [Relation.Map]
 
 lemma map_onFun_eq_of_surjective {r : β → β → Prop} {f : α → β} (hsurj : f.Surjective) :
@@ -355,13 +357,16 @@ inductive EqvGen : α → α → Prop
 attribute [mk_iff] TransGen
 attribute [grind] TransGen
 
+theorem reflGen_le_reflTransGen : ReflGen r ≤ ReflTransGen r
+  | a, _, .refl => by rfl
+  | _, _, .single h => ReflTransGen.tail ReflTransGen.refl h
+
 namespace ReflGen
 
-theorem to_reflTransGen : ∀ {a b}, ReflGen r a b → ReflTransGen r a b
-  | a, _, refl => by rfl
-  | _, _, single h => ReflTransGen.tail ReflTransGen.refl h
+theorem to_reflTransGen {a b} : ReflGen r a b → ReflTransGen r a b :=
+  reflGen_le_reflTransGen a b
 
-theorem mono {p : α → α → Prop} (hp : ∀ a b, r a b → p a b) : ∀ {a b}, ReflGen r a b → ReflGen p a b
+theorem mono {p : α → α → Prop} (hp : r ≤ p) : ReflGen r ≤ ReflGen p
   | a, _, ReflGen.refl => by rfl
   | a, b, single h => single (hp a b h)
 
@@ -436,6 +441,9 @@ theorem trans (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransG
 theorem single (hab : r a b) : ReflTransGen r a b :=
   refl.tail hab
 
+theorem le_reflTransGen : r ≤ ReflTransGen r :=
+  fun _ _ ↦ single
+
 theorem head (hab : r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c := by
   induction hbc with
   | refl => exact refl.tail hab
@@ -497,13 +505,17 @@ theorem total_of_right_unique (U : Relator.RightUnique r) (ab : ReflTransGen r a
 
 end ReflTransGen
 
-namespace TransGen
-
-theorem to_reflTransGen {a b} (h : TransGen r a b) : ReflTransGen r a b := by
+theorem transGen_le_reflTransGen : TransGen r ≤ ReflTransGen r := by
+  intro a _ h
   induction h with
   | single h => exact ReflTransGen.single h
   | tail _ bc ab => exact ReflTransGen.tail ab bc
 
+namespace TransGen
+
+theorem to_reflTransGen {a b} : TransGen r a b → ReflTransGen r a b :=
+  transGen_le_reflTransGen a b
+
 theorem trans_left (hab : TransGen r a b) (hbc : ReflTransGen r b c) : TransGen r a c := by
   induction hbc with
   | refl => assumption
@@ -586,9 +598,8 @@ lemma reflGen_eq_self [Std.Refl r] : ReflGen r = r := by
 @[deprecated inferInstance (since := "2026-03-27")]
 lemma reflexive_reflGen : Std.Refl (ReflGen r) := inferInstance
 
-lemma reflGen_minimal {r' : α → α → Prop} [Std.Refl r'] (h : ∀ x y, r x y → r' x y) {x y : α}
-    (hxy : ReflGen r x y) : r' x y := by
-  simpa [reflGen_eq_self] using ReflGen.mono h hxy
+lemma reflGen_minimal {r' : α → α → Prop} [Std.Refl r'] (h : r ≤ r') : ReflGen r ≤ r' := by
+  simpa [reflGen_eq_self] using ReflGen.mono h
 
 end reflGen
 
@@ -641,40 +652,39 @@ theorem transitive_transGen : IsTrans α (TransGen r) := inferInstance
 theorem transGen_idem : TransGen (TransGen r) = TransGen r :=
   transGen_eq_self
 
-theorem TransGen.lift {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → p (f a) (f b))
-    (hab : TransGen r a b) : TransGen p (f a) (f b) := by
+theorem TransGen.lift {p : β → β → Prop} (f : α → β) (h : r ≤ (p on f)) :
+    TransGen r ≤ (TransGen p on f) := by
+  intro a _ hab
   induction hab with
   | single hac => exact TransGen.single (h a _ hac)
   | tail _ hcd hac => exact TransGen.tail hac (h _ _ hcd)
 
-theorem TransGen.lift' {p : β → β → Prop} {a b : α} (f : α → β)
-    (h : ∀ a b, r a b → TransGen p (f a) (f b)) (hab : TransGen r a b) :
-    TransGen p (f a) (f b) := by
+theorem TransGen.lift' {p : β → β → Prop} (f : α → β) (h : r ≤ (TransGen p on f)) :
+    TransGen r ≤ (TransGen p on f) := by
+  intro _ _ hab
   simpa [transGen_eq_self] using hab.lift f h
 
-theorem TransGen.closed {p : α → α → Prop} :
-    (∀ a b, r a b → TransGen p a b) → TransGen r a b → TransGen p a b :=
+theorem TransGen.closed {p : α → α → Prop} : r ≤ TransGen p → TransGen r ≤ TransGen p :=
   TransGen.lift' id
 
 lemma TransGen.closed' {P : α → Prop} (dc : ∀ {a b}, r a b → P b → P a)
     {a b : α} (h : TransGen r a b) : P b → P a :=
   h.head_induction_on dc fun hr _ hi ↦ dc hr ∘ hi
 
-theorem TransGen.mono {p : α → α → Prop} :
-    (∀ a b, r a b → p a b) → TransGen r a b → TransGen p a b :=
+theorem TransGen.mono {p : α → α → Prop} : r ≤ p → TransGen r ≤ TransGen p :=
   TransGen.lift id
 
-lemma transGen_minimal {r' : α → α → Prop} [IsTrans α r'] (h : ∀ x y, r x y → r' x y) {x y : α}
-    (hxy : TransGen r x y) : r' x y := by
-  simpa [transGen_eq_self] using TransGen.mono h hxy
+lemma transGen_minimal {r' : α → α → Prop} [IsTrans α r'] (h : r ≤ r') : TransGen r ≤ r' := by
+  simpa [transGen_eq_self] using TransGen.mono h
 
-theorem TransGen.swap (h : TransGen r b a) : TransGen (swap r) a b := by
+theorem TransGen.swap : swap (TransGen r) ≤ TransGen (swap r) := by
+  intro _ _ h
   induction h with
   | single h => exact TransGen.single h
   | tail _ hbc ih => exact ih.head hbc
 
 theorem transGen_swap : TransGen (swap r) a b ↔ TransGen r b a :=
-  ⟨TransGen.swap, TransGen.swap⟩
+  ⟨TransGen.swap b a, TransGen.swap a b⟩
 
 end TransGen
 
@@ -696,12 +706,11 @@ theorem reflTransGen_iff_eq_or_transGen : ReflTransGen r a b ↔ b = a ∨ Trans
     · rfl
     · exact h.to_reflTransGen
 
-theorem ReflTransGen.lift {p : β → β → Prop} {a b : α} (f : α → β)
-    (h : ∀ a b, r a b → p (f a) (f b)) (hab : ReflTransGen r a b) : ReflTransGen p (f a) (f b) :=
-  ReflTransGen.trans_induction_on hab (fun _ ↦ refl) (ReflTransGen.single ∘ h _ _) fun _ _ ↦ trans
+theorem ReflTransGen.lift {p : β → β → Prop} (f : α → β) (h : r ≤ (p on f)) :
+    ReflTransGen r ≤ (ReflTransGen p on f) :=
+  fun _ _ hab ↦ trans_induction_on hab (fun _ ↦ refl) (single ∘ h _ _) fun _ _ ↦ trans
 
-theorem ReflTransGen.mono {p : α → α → Prop} : (∀ a b, r a b → p a b) →
-    ReflTransGen r a b → ReflTransGen p a b :=
+theorem ReflTransGen.mono {p : α → α → Prop} : r ≤ p → ReflTransGen r ≤ ReflTransGen p :=
   ReflTransGen.lift id
 
 @[grind =]
@@ -734,22 +743,23 @@ theorem transitive_reflTransGen : IsTrans α (ReflTransGen r) := inferInstance
 theorem reflTransGen_idem : ReflTransGen (ReflTransGen r) = ReflTransGen r :=
   reflTransGen_eq_self
 
-theorem ReflTransGen.lift' {p : β → β → Prop} {a b : α} (f : α → β)
-    (h : ∀ a b, r a b → ReflTransGen p (f a) (f b))
-    (hab : ReflTransGen r a b) : ReflTransGen p (f a) (f b) := by
+theorem ReflTransGen.lift' {p : β → β → Prop} (f : α → β) (h : r ≤ (ReflTransGen p on f)) :
+    ReflTransGen r ≤ (ReflTransGen p on f) := by
+  intro _ _ hab
   simpa [reflTransGen_eq_self] using hab.lift f h
 
 theorem reflTransGen_closed {p : α → α → Prop} :
-    (∀ a b, r a b → ReflTransGen p a b) → ReflTransGen r a b → ReflTransGen p a b :=
+    r ≤ ReflTransGen p → ReflTransGen r ≤ ReflTransGen p :=
   ReflTransGen.lift' id
 
-theorem ReflTransGen.swap (h : ReflTransGen r b a) : ReflTransGen (swap r) a b := by
+theorem ReflTransGen.swap : swap (ReflTransGen r) ≤ ReflTransGen (swap r) := by
+  intro _ _ h
   induction h with
   | refl => rfl
   | tail _ hbc ih => exact ih.head hbc
 
 theorem reflTransGen_swap : ReflTransGen (swap r) a b ↔ ReflTransGen r b a :=
-  ⟨ReflTransGen.swap, ReflTransGen.swap⟩
+  ⟨ReflTransGen.swap b a, ReflTransGen.swap a b⟩
 
 @[simp, grind =] lemma reflGen_transGen : ReflGen (TransGen r) = ReflTransGen r := by
   ext x y
@@ -758,10 +768,10 @@ theorem reflTransGen_swap : ReflTransGen (swap r) a b ↔ ReflTransGen r b a :=
 @[simp, grind =] lemma transGen_reflGen : TransGen (ReflGen r) = ReflTransGen r := by
   ext x y
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-  · simpa [reflTransGen_eq_self] using (h.mono fun _ _ ↦ ReflGen.to_reflTransGen).to_reflTransGen
+  · simpa [reflTransGen_eq_self] using h.mono reflGen_le_reflTransGen x y |>.to_reflTransGen
   · obtain (rfl | h) := reflTransGen_iff_eq_or_transGen.mp h
     · exact .single .refl
-    · exact TransGen.mono (fun _ _ ↦ .single) h
+    · exact h.mono (fun _ _ ↦ .single) x y
 
 @[simp, grind =] lemma reflTransGen_reflGen : ReflTransGen (ReflGen r) = ReflTransGen r := by
   simp only [← transGen_reflGen, reflGen_eq_self]
@@ -794,8 +804,8 @@ see for example `Quot.eqvGen_exact` and `Quot.eqvGen_sound`. -/
 def setoid : Setoid α :=
   Setoid.mk _ (EqvGen.is_equivalence r)
 
-theorem mono {r p : α → α → Prop} (hrp : ∀ a b, r a b → p a b) (h : EqvGen r a b) :
-    EqvGen p a b := by
+theorem mono {r p : α → α → Prop} (hrp : r ≤ p) : EqvGen r ≤ EqvGen p := by
+  intro _ _ h
   induction h with
   | rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)
   | refl => exact EqvGen.refl _
@@ -840,9 +850,10 @@ theorem church_rosser (h : ∀ a b c, r a b → r a c → ∃ d, ReflGen r b d 
     | refl => exact ⟨b, hea, hcb⟩
     | single hba => exact ⟨a, hea, hcb.tail hba⟩
 
+theorem le_join_of_refl [Std.Refl r] : r ≤ Join r :=
+  fun _ b hab ↦ ⟨b, hab, refl b⟩
 
-theorem join_of_single [Std.Refl r] (hab : r a b) : Join r a b :=
-  ⟨b, hab, refl b⟩
+@[deprecated (since := "2026-06-30")] alias join_of_single := le_join_of_refl
 
 protected instance Join.symm : Std.Symm (Join r) where
   symm _ _ := fun ⟨c, hac, hcb⟩ ↦ ⟨c, hcb, hac⟩
@@ -871,23 +882,30 @@ theorem equivalence_join_reflTransGen
     Equivalence (Join (ReflTransGen r)) :=
   equivalence_join fun _ _ _ ↦ church_rosser h
 
-theorem join_of_equivalence {r' : α → α → Prop} (hr : Equivalence r) (h : ∀ a b, r' a b → r a b) :
-    Join r' a b → r a b
-  | ⟨_, hac, hbc⟩ => hr.trans (h _ _ hac) (hr.symm <| h _ _ hbc)
+theorem join_le_of_equivalence_of_le {r' : α → α → Prop} (hr : Equivalence r) (h : r' ≤ r) :
+    Join r' ≤ r :=
+  fun a b ⟨c, hac, hbc⟩ ↦ hr.trans (h a c hac) (hr.symm <| h b c hbc)
 
-theorem reflTransGen_of_isTrans_reflexive {r' : α → α → Prop} [Std.Refl r] [IsTrans α r]
-    (h : ∀ a b, r' a b → r a b) (h' : ReflTransGen r' a b) : r a b := by
-  simpa [reflTransGen_eq_self] using ReflTransGen.mono h h'
+@[deprecated (since := "2026-06-30")] alias join_of_equivalence := join_le_of_equivalence_of_le
+
+theorem reflTransGen_le_of_le {r' : α → α → Prop} [Std.Refl r] [IsTrans α r]
+    (h : r' ≤ r) : ReflTransGen r' ≤ r := by
+  simpa [reflTransGen_eq_self] using ReflTransGen.mono h
+
+@[deprecated (since := "2026-06-30")]
+alias reflTransGen_of_isTrans_reflexive := reflTransGen_le_of_le
 
 @[deprecated (since := "2026-02-21")]
-alias reflTransGen_of_transitive_reflexive := reflTransGen_of_isTrans_reflexive
+alias reflTransGen_of_transitive_reflexive := reflTransGen_le_of_le
+
+@[deprecated (since := "2025-12-17")] alias reflTransGen_minimal := reflTransGen_le_of_le
 
-@[deprecated (since := "2025-12-17")] alias reflTransGen_minimal :=
-  reflTransGen_of_transitive_reflexive
+theorem reflTransGen_le_of_equivalence_of_le {r' : α → α → Prop} (hr : Equivalence r) :
+    r' ≤ r → ReflTransGen r' ≤ r :=
+  @reflTransGen_le_of_le _ _ _ hr.stdRefl hr.isTrans
 
-theorem reflTransGen_of_equivalence {r' : α → α → Prop} (hr : Equivalence r) :
-    (∀ a b, r' a b → r a b) → ReflTransGen r' a b → r a b :=
-  @reflTransGen_of_isTrans_reflexive _ _ _ _ _ hr.stdRefl hr.isTrans
+@[deprecated (since := "2026-06-30")]
+alias reflTransGen_of_equivalence := reflTransGen_le_of_equivalence_of_le
 
 end Join