chore(Logic/Relation): use Subrelation to state theorems

Author: SnirBroshi

Mathlib/CategoryTheory/Limits/Types/Filtered.lean

@@ -112,7 +112,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)
 
 @[deprecated (since := "2025-06-22")] alias rel_eq_eqvGen_quot_rel :=
   FilteredColimit.rel_eq_eqvGen_colimitTypeRel

Mathlib/CategoryTheory/Limits/Types/Shapes.lean

@@ -518,7 +518,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 e'
-    exact (eqv.eqvGen_iff.mp (Relation.EqvGen.mono lem (Quot.eqvGen_exact e'))).mp hy
+    exact (eqv.eqvGen_iff.mp (Relation.EqvGen.mono @lem (Quot.eqvGen_exact e'))).mp hy
   · exact fun hx => ⟨_, hx, rfl⟩
 
 /-- The categorical coequalizer in `Type u` is the quotient by `f g ~ g x`. -/

Mathlib/Data/Setoid/Basic.lean

@@ -369,7 +369,7 @@ def map (r : Setoid α) (f : α → β) : Setoid β :=
 equivalence relation on f's codomain defined by x ≈ y ↔ the elements of f⁻¹(x) are related to
 the elements of f⁻¹(y) by r. -/
 def mapOfSurjective (r : Setoid α) (f : α → β) (h : ker f ≤ r) (hf : Surjective f) : Setoid β :=
-  ⟨Relation.Map r f f, Relation.map_equivalence r.iseqv f hf h⟩
+  ⟨Relation.Map r f f, Relation.map_equivalence r.iseqv f hf @h⟩
 
 /-- A special case of the equivalence closure of an equivalence relation r equaling r. -/
 theorem mapOfSurjective_eq_map (h : ker f ≤ r) (hf : Surjective f) :

Mathlib/GroupTheory/FreeGroup/Basic.lean

@@ -196,7 +196,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) Step.cons
 
 @[to_additive]
 theorem cons_cons_iff (p) : Red (p :: L₁) (p :: L₂) ↔ Red L₁ L₂ :=
@@ -226,7 +226,7 @@ theorem append_append_left_iff : ∀ L, Red (L ++ L₁) (L ++ L₂) ↔ Red L₁
 
 @[to_additive]
 theorem append_append (h₁ : Red L₁ L₃) (h₂ : Red L₂ L₄) : Red (L₁ ++ L₂) (L₃ ++ L₄) :=
-  (h₁.lift (fun L => L ++ L₂) fun _ _ => Step.append_right).trans ((append_append_left_iff _).2 h₂)
+  (h₁.lift (fun L => L ++ L₂) Step.append_right).trans ((append_append_left_iff _).2 h₂)
 
 @[to_additive]
 theorem to_append_iff : Red L (L₁ ++ L₂) ↔ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂ :=
@@ -316,10 +316,10 @@ theorem Step.sublist (H : Red.Step L₁ L₂) : L₂ <+ L₁ := by
 /-- 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_transitive_reflexive
-    _ (fun a b => b <+ a) _ _ _
+    _ (fun a b => b <+ a) _
     (fun l => List.Sublist.refl l)
     (fun _a _b _c hab hbc => List.Sublist.trans hbc hab)
-    (fun _ _ => Red.Step.sublist)
+    Red.Step.sublist _ _
 
 @[to_additive]
 theorem length_le (h : Red L₁ L₂) : L₂.length ≤ L₁.length :=
@@ -367,11 +367,9 @@ theorem join_red_of_step (h : Red.Step L₁ L₂) : Join Red L₁ L₂ :=
 @[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)
+    (fun h ↦ equivalence_join_red.eqvGen_iff.mp <| h.mono join_red_of_step)
+    (join_of_equivalence (Relation.EqvGen.is_equivalence _) <|
+      reflTransGen_of_equivalence (Relation.EqvGen.is_equivalence _) @(EqvGen.rel))
 
 /-! ### Reduced words -/
 
@@ -582,7 +580,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
+  ReflTransGen.lift FreeGroup.invRev Red.Step.invRev h
 
 @[to_additive (attr := simp)]
 theorem Red.step_invRev_iff :

Mathlib/Logic/Relation.lean

@@ -223,13 +223,13 @@ lemma map_symmetric {r : α → α → Prop} (hr : Symmetric r) (f : α → β)
   rintro _ _ ⟨x, y, hxy, rfl, rfl⟩; exact ⟨_, _, hr hxy, rfl, rfl⟩
 
 lemma map_transitive {r : α → α → Prop} (hr : Transitive r) {f : α → β}
-    (hf : ∀ x y, f x = f y → r x y) :
+    (hf : Subrelation ((· = ·) on f) r) :
     Transitive (Relation.Map r f f) := by
   rintro _ _ _ ⟨x, y, hxy, rfl, rfl⟩ ⟨y', z, hyz, hy, rfl⟩
-  exact ⟨x, z, hr hxy <| hr (hf _ _ hy.symm) hyz, rfl, rfl⟩
+  exact ⟨x, z, hr hxy <| hr (hf hy.symm) hyz, rfl, rfl⟩
 
 lemma map_equivalence {r : α → α → Prop} (hr : Equivalence r) (f : α → β)
-    (hf : f.Surjective) (hf_ker : ∀ x y, f x = f y → r x y) :
+    (hf : f.Surjective) (hf_ker : Subrelation ((· = ·) on f) r) :
     Equivalence (Relation.Map r f f) where
   refl := map_reflexive hr.reflexive hf
   symm := @(map_symmetric hr.symmetric _)
@@ -272,13 +272,13 @@ attribute [refl] ReflGen.refl
 
 namespace ReflGen
 
-theorem to_reflTransGen : ∀ {a b}, ReflGen r a b → ReflTransGen r a b
+theorem to_reflTransGen : Subrelation (ReflGen r) (ReflTransGen r)
   | a, _, refl => by rfl
   | _, _, single h => ReflTransGen.tail ReflTransGen.refl h
 
-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 : Subrelation r p) : Subrelation (ReflGen r) (ReflGen p)
   | a, _, ReflGen.refl => by rfl
-  | a, b, single h => single (hp a b h)
+  | a, b, single h => single <| hp h
 
 instance : IsRefl α (ReflGen r) :=
   ⟨@refl α r⟩
@@ -293,8 +293,8 @@ theorem trans (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransG
   | refl => assumption
   | tail _ hcd hac => exact hac.tail hcd
 
-theorem single (hab : r a b) : ReflTransGen r a b :=
-  refl.tail hab
+theorem single : Subrelation r (ReflTransGen r) :=
+  refl.tail
 
 theorem head (hab : r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c := by
   induction hbc with
@@ -357,7 +357,7 @@ end ReflTransGen
 
 namespace TransGen
 
-theorem to_reflTransGen {a b} (h : TransGen r a b) : ReflTransGen r a b := by
+theorem to_reflTransGen : Subrelation (TransGen r) (ReflTransGen r) := fun h ↦ by
   induction h with
   | single h => exact ReflTransGen.single h
   | tail _ bc ab => exact ReflTransGen.tail ab bc
@@ -432,8 +432,8 @@ lemma reflGen_eq_self (hr : Reflexive r) : ReflGen r = r := by
 
 lemma reflexive_reflGen : Reflexive (ReflGen r) := fun _ ↦ .refl
 
-lemma reflGen_minimal {r' : α → α → Prop} (hr' : Reflexive r') (h : ∀ x y, r x y → r' x y) {x y : α}
-    (hxy : ReflGen r x y) : r' x y := by
+lemma reflGen_minimal {r' : α → α → Prop} (hr' : Reflexive r') (h : Subrelation r r') :
+    Subrelation (ReflGen r) r' := fun hxy ↦ by
   simpa [reflGen_eq_self hr'] using ReflGen.mono h hxy
 
 end reflGen
@@ -467,41 +467,44 @@ theorem transitive_transGen : Transitive (TransGen r) := fun _ _ _ ↦ TransGen.
 theorem transGen_idem : TransGen (TransGen r) = TransGen r :=
   transGen_eq_self transitive_transGen
 
-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 : Subrelation r (p on f)) :
+    Subrelation (TransGen r) (TransGen p on f) := fun hab ↦ by
   induction hab with
-  | single hac => exact TransGen.single (h a _ hac)
-  | tail _ hcd hac => exact TransGen.tail hac (h _ _ hcd)
+  | single hac => exact TransGen.single <| h 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 : Subrelation r (TransGen p on f)) :
+    Subrelation (TransGen r) (TransGen p on f) := fun hab ↦ by
   simpa [transGen_idem] 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 :=
+    (Subrelation r (TransGen p)) → Subrelation (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
+lemma TransGen.closed' {P : α → Prop} (dc : Subrelation r (swap (· → ·) on P)) :
+    Subrelation (TransGen r) (swap (· → ·) on P) :=
+  fun h ↦ 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 :=
+    (Subrelation r p) → Subrelation (TransGen r) (TransGen p) :=
   TransGen.lift id
 
-lemma transGen_minimal {r' : α → α → Prop} (hr' : Transitive r') (h : ∀ x y, r x y → r' x y)
-    {x y : α} (hxy : TransGen r x y) : r' x y := by
+lemma transGen_minimal {r' : α → α → Prop} (hr' : Transitive r') (h : Subrelation r r') :
+    Subrelation (TransGen r) r' := fun hxy ↦ by
   simpa [transGen_eq_self hr'] using TransGen.mono h hxy
 
-theorem TransGen.swap (h : TransGen r b a) : TransGen (swap r) a b := by
+theorem TransGen.swap : Subrelation (swap (TransGen r)) (TransGen (swap r)) := fun h ↦ by
   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 :=
+theorem transGen_swap : TransGen (swap r) a b ↔ swap (TransGen r) a b :=
   ⟨TransGen.swap, TransGen.swap⟩
 
+theorem transGen_swap_eq_swap_transGen : TransGen (swap r) = swap (TransGen r) := by
+  ext a b
+  exact transGen_swap
+
 end TransGen
 
 section ReflTransGen
@@ -520,12 +523,12 @@ 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 : Subrelation r (p on f)) :
+    Subrelation (ReflTransGen r) (ReflTransGen p on f) := fun hab ↦
+  ReflTransGen.trans_induction_on hab (fun _ ↦ refl) (ReflTransGen.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} : (Subrelation r p) →
+    Subrelation (ReflTransGen r) (ReflTransGen p) :=
   ReflTransGen.lift id
 
 theorem reflTransGen_eq_self (refl : Reflexive r) (trans : Transitive r) : ReflTransGen r = r :=
@@ -536,7 +539,7 @@ theorem reflTransGen_eq_self (refl : Reflexive r) (trans : Transitive r) : ReflT
       | tail _ h₂ IH => exact trans IH h₂, single⟩
 
 lemma reflTransGen_minimal {r' : α → α → Prop} (hr₁ : Reflexive r') (hr₂ : Transitive r')
-    (h : ∀ x y, r x y → r' x y) {x y : α} (hxy : ReflTransGen r x y) : r' x y := by
+    (h : Subrelation r r') : Subrelation (ReflTransGen r) r' := fun hxy ↦ by
   simpa [reflTransGen_eq_self hr₁ hr₂] using ReflTransGen.mono h hxy
 
 theorem reflexive_reflTransGen : Reflexive (ReflTransGen r) := fun _ ↦ refl
@@ -558,23 +561,28 @@ instance : IsTrans α (ReflTransGen r) :=
 theorem reflTransGen_idem : ReflTransGen (ReflTransGen r) = ReflTransGen r :=
   reflTransGen_eq_self reflexive_reflTransGen transitive_reflTransGen
 
-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 : Subrelation r (ReflTransGen p on f)) : Subrelation (ReflTransGen r) (ReflTransGen p on f)
+    := fun hab ↦ by
   simpa [reflTransGen_idem] 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 :=
+    (Subrelation r (ReflTransGen p)) → Subrelation (ReflTransGen r) (ReflTransGen p) :=
   ReflTransGen.lift' id
 
-theorem ReflTransGen.swap (h : ReflTransGen r b a) : ReflTransGen (swap r) a b := by
+theorem ReflTransGen.swap : Subrelation (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⟩
 
+theorem reflTransGen_swap_eq_swap_reflTransGen : ReflTransGen (swap r) = swap (ReflTransGen r) := by
+  ext a b
+  exact reflTransGen_swap
+
 @[simp] lemma reflGen_transGen : ReflGen (TransGen r) = ReflTransGen r := by
   ext x y
   simp_rw [reflTransGen_iff_eq_or_transGen, reflGen_iff]
@@ -583,10 +591,10 @@ theorem reflTransGen_swap : ReflTransGen (swap r) a b ↔ ReflTransGen r b a :=
   ext x y
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
   · simpa [reflTransGen_idem]
-      using TransGen.to_reflTransGen <| TransGen.mono (fun _ _ ↦ ReflGen.to_reflTransGen) h
+      using TransGen.to_reflTransGen <| TransGen.mono (ReflGen.to_reflTransGen) h
   · obtain (rfl | h) := reflTransGen_iff_eq_or_transGen.mp h
     · exact .single .refl
-    · exact TransGen.mono (fun _ _ ↦ .single) h
+    · exact TransGen.mono (.single) h
 
 @[simp] lemma reflTransGen_reflGen : ReflTransGen (ReflGen r) = ReflTransGen r := by
   simp only [← transGen_reflGen, reflGen_eq_self reflexive_reflGen]
@@ -618,10 +626,10 @@ 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 : Subrelation r p) : Subrelation (EqvGen r) (EqvGen p) := by
+  intro _ _ h
   induction h with
-  | rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)
+  | rel a b h => exact EqvGen.rel _ _ <| hrp h
   | refl => exact EqvGen.refl _
   | symm a b _ ih => exact EqvGen.symm _ _ ih
   | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc
@@ -665,8 +673,8 @@ theorem church_rosser (h : ∀ a b c, r a b → r a c → ∃ d, ReflGen r b d 
     | single hba => exact ⟨a, hea, hcb.tail hba⟩
 
 
-theorem join_of_single (h : Reflexive r) (hab : r a b) : Join r a b :=
-  ⟨b, hab, h b⟩
+theorem join_of_single (h : Reflexive r) : Subrelation r (Join r) :=
+  fun hab ↦ ⟨_, hab, h _⟩
 
 theorem symmetric_join : Symmetric (Join r) := fun _ _ ⟨c, hac, hcb⟩ ↦ ⟨c, hcb, hac⟩
 
@@ -687,18 +695,18 @@ theorem equivalence_join_reflTransGen
     Equivalence (Join (ReflTransGen r)) :=
   equivalence_join reflexive_reflTransGen transitive_reflTransGen 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_of_equivalence {r' : α → α → Prop} (hr : Equivalence r) (h : Subrelation r' r) :
+    Subrelation (Join r') r :=
+  fun ⟨_, hac, hbc⟩ ↦ hr.trans (h hac) (hr.symm <| h hbc)
 
 theorem reflTransGen_of_transitive_reflexive {r' : α → α → Prop} (hr : Reflexive r)
-    (ht : Transitive r) (h : ∀ a b, r' a b → r a b) (h' : ReflTransGen r' a b) : r a b := by
+    (ht : Transitive r) (h : Subrelation r' r) : Subrelation (ReflTransGen r') r := fun h' ↦ by
   induction h' with
   | refl => exact hr _
-  | tail _ hbc ih => exact ht ih (h _ _ hbc)
+  | tail _ hbc ih => exact ht ih <| h hbc
 
 theorem reflTransGen_of_equivalence {r' : α → α → Prop} (hr : Equivalence r) :
-    (∀ a b, r' a b → r a b) → ReflTransGen r' a b → r a b :=
+    (Subrelation r' r) → Subrelation (ReflTransGen r') r :=
   reflTransGen_of_transitive_reflexive hr.1 (fun _ _ _ ↦ hr.trans)
 
 end Join
@@ -711,12 +719,12 @@ open Relation
 
 variable {r : α → α → Prop} {a b : α}
 
-theorem Quot.eqvGen_exact (H : Quot.mk r a = Quot.mk r b) : EqvGen r a b :=
-  @Quotient.exact _ (EqvGen.setoid r) a b (congrArg
-    (Quot.lift (Quotient.mk (EqvGen.setoid r)) (fun x y h ↦ Quot.sound (EqvGen.rel x y h))) H)
+theorem Quot.eqvGen_exact : Subrelation ((· = ·) on Quot.mk r) (EqvGen r) :=
+  fun H ↦ Quotient.exact <| congrArg
+    (Quot.lift (Quotient.mk <| EqvGen.setoid r) (fun _ _ h ↦ Quot.sound <| EqvGen.rel _ _ h)) H
 
-theorem Quot.eqvGen_sound (H : EqvGen r a b) : Quot.mk r a = Quot.mk r b :=
-  EqvGen.rec
+theorem Quot.eqvGen_sound : Subrelation (EqvGen r) ((· = ·) on Quot.mk r) :=
+  fun H ↦ EqvGen.rec
     (fun _ _ h ↦ Quot.sound h)
     (fun _ ↦ rfl)
     (fun _ _ _ IH ↦ Eq.symm IH)

Mathlib/Order/Interval/Finset/Basic.lean

@@ -1170,22 +1170,22 @@ lemma monotone_iff_forall_wcovBy [Preorder α] [LocallyFiniteOrder α] [Preorder
     (f : α → β) : Monotone f ↔ ∀ a b : α, a ⩿ b → f a ≤ f b := by
   refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩
   simpa [transGen_eq_self (r := (· ≤ · : β → β → Prop)) transitive_le]
-    using TransGen.lift f h <| le_iff_transGen_wcovBy.mp hab
+    using TransGen.lift f @h <| le_iff_transGen_wcovBy.mp hab
 
 /-- A function from a locally finite partial order is monotone if and only if it is monotone when
 restricted to pairs satisfying `a ⋖ b`. -/
 lemma monotone_iff_forall_covBy [PartialOrder α] [LocallyFiniteOrder α] [Preorder β]
     (f : α → β) : Monotone f ↔ ∀ a b : α, a ⋖ b → f a ≤ f b := by
   refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩
   simpa [reflTransGen_eq_self (r := (· ≤ · : β → β → Prop)) IsRefl.reflexive transitive_le]
-    using ReflTransGen.lift f h <| le_iff_reflTransGen_covBy.mp hab
+    using ReflTransGen.lift f @h <| le_iff_reflTransGen_covBy.mp hab
 
 /-- A function from a locally finite preorder is strictly monotone if and only if it is strictly
 monotone when restricted to pairs satisfying `a ⋖ b`. -/
 lemma strictMono_iff_forall_covBy [Preorder α] [LocallyFiniteOrder α] [Preorder β]
     (f : α → β) : StrictMono f ↔ ∀ a b : α, a ⋖ b → f a < f b := by
   refine ⟨fun hf _ _ h ↦ hf h.lt, fun h a b hab ↦ ?_⟩
-  have := Relation.TransGen.lift f h (a := a) (b := b)
+  have := Relation.TransGen.lift f @h (x := a) (y := b)
   rw [← lt_iff_transGen_covBy, transGen_eq_self (@lt_trans β _)] at this
   exact this hab