chore: remove uses of Subrelation (leanprover-community#41450)

Following up on the description of leanprover-community#40792, this removes additional uses of `Subrelation` now that leanprover-community#30526 has been merged.

Author: chenson2018

Mathlib/Logic/Relation.lean

@@ -56,9 +56,9 @@ open Function
 
 variable {α β γ δ ε ζ : Type*}
 
-theorem Subrelation.antisymm {r r' : α → α → Prop} (h1 : Subrelation r r') (h2 : Subrelation r' r) :
+theorem Subrelation.antisymm {r r' : α → α → Prop} (h1 : r ≤ r') (h2 : r' ≤ r) :
     r = r' :=
-  funext₂ fun _ _ => propext ⟨h1, h2⟩
+  funext₂ fun a b => propext ⟨h1 a b, h2 a b⟩
 
 section NeImp
 
@@ -816,34 +816,33 @@ theorem mono {r p : α → α → Prop} (hrp : r ≤ p) : EqvGen r ≤ EqvGen p
   | symm a b _ ih => exact EqvGen.symm _ _ ih
   | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc
 
-lemma eqvGen_le {r r' : α → α → Prop} [IsEquiv α r'] (h : Subrelation r r') :
-    Subrelation (EqvGen r) r'
+lemma eqvGen_le {r r' : α → α → Prop} [IsEquiv α r'] (h : r ≤ r') : EqvGen r ≤ r'
   | _, _, .refl _ => _root_.refl _
-  | _, _, .symm _ _ hxy => _root_.symm (eqvGen_le h hxy :)
-  | _, _, .trans _ _ _ hxy hyz => _root_.trans (eqvGen_le h hxy :) (eqvGen_le h hyz :)
-  | _, _, .rel _ _ hab => h hab
+  | _, _, .symm _ _ hxy => _root_.symm (eqvGen_le h _ _ hxy)
+  | _, _, .trans _ _ _ hxy hyz => _root_.trans (eqvGen_le h _ _ hxy) (eqvGen_le h _ _ hyz)
+  | _, _, .rel _ _ hab => h _ _ hab
 
-lemma eqvGen_mono {r r' : α → α → Prop} (h : Subrelation r r') : Subrelation (EqvGen r) (EqvGen r')
+lemma eqvGen_mono {r r' : α → α → Prop} (h : r ≤ r') : EqvGen r ≤ EqvGen r'
   | _, _, .refl _ => .refl _
-  | _, _, .symm _ _ hxy => .symm _ _ (eqvGen_mono h hxy)
-  | _, _, .trans _ _ _ hxy hyz => .trans _ _ _ (eqvGen_mono h hxy) (eqvGen_mono h hyz)
-  | _, _, .rel _ _ hab => .rel _ _ (h hab)
+  | _, _, .symm _ _ hxy => .symm _ _ (eqvGen_mono h _ _ hxy)
+  | _, _, .trans _ _ _ hxy hyz => .trans _ _ _ (eqvGen_mono h _ _ hxy) (eqvGen_mono h _ _ hyz)
+  | _, _, .rel _ _ hab => .rel _ _ (h _ _ hab)
 
-lemma reflGen_le_eqvGen : Subrelation (ReflGen r) (EqvGen r)
+lemma reflGen_le_eqvGen : ReflGen r ≤ EqvGen r
   |  _, _, .refl => .refl _
   |  _, _, .single h => .rel _ _ h
 
-lemma symmGen_le_eqvGen : Subrelation (SymmGen r) (EqvGen r)
+lemma symmGen_le_eqvGen : SymmGen r ≤ EqvGen r
   | _, _, .inl h => .rel _ _ h
   | _, _, .inr h => _root_.symm <| .rel _ _ h
 
-lemma transGen_le_eqvGen : Subrelation (TransGen r) (EqvGen r) := by
+lemma transGen_le_eqvGen : TransGen r ≤ EqvGen r := by
   intro _ _ h
   induction h using TransGen.trans_induction_on with
   | trans _ _ h1 h2 => exact _root_.trans h1 h2
   | single h => exact .rel _ _ h
 
-lemma reflTransGen_le_eqvGen : Subrelation (ReflTransGen r) (EqvGen r) := by
+lemma reflTransGen_le_eqvGen : ReflTransGen r ≤ EqvGen r := by
   intro _ _ h
   induction h using ReflTransGen.trans_induction_on with
   | refl => exact .refl _
@@ -853,27 +852,27 @@ lemma reflTransGen_le_eqvGen : Subrelation (ReflTransGen r) (EqvGen r) := by
 @[simp, grind =]
 lemma eqvGen_reflGen : EqvGen (ReflGen r) = EqvGen r :=
   Subrelation.antisymm
-    (eqvGen_le (reflGen_le_eqvGen _)) (eqvGen_mono (.single))
+    (eqvGen_le (reflGen_le_eqvGen _)) (eqvGen_mono fun _ _ => .single)
 
 @[simp, grind =]
 lemma eqvGen_transGen : EqvGen (TransGen r) = EqvGen r :=
   Subrelation.antisymm
-    (eqvGen_le (transGen_le_eqvGen _)) (eqvGen_mono .single)
+    (eqvGen_le (transGen_le_eqvGen _)) (eqvGen_mono fun _ _ => .single)
 
 @[simp, grind =]
 lemma eqvGen_symmGen : EqvGen (SymmGen r) = EqvGen r :=
   Subrelation.antisymm
-    (eqvGen_le (symmGen_le_eqvGen _)) (eqvGen_mono .inl)
+    (eqvGen_le (symmGen_le_eqvGen _)) (eqvGen_mono fun _ _ => .inl)
 
 @[simp, grind =]
 lemma eqvGen_reflTransGen : EqvGen (ReflTransGen r) = EqvGen r :=
   Subrelation.antisymm
-    (eqvGen_le (reflTransGen_le_eqvGen _)) (eqvGen_mono .single)
+    (eqvGen_le (reflTransGen_le_eqvGen _)) (eqvGen_mono fun _ _ => .single)
 
 @[grind =]
 lemma eqvGen_eq_reflTransGen [Std.Symm r] : EqvGen r = ReflTransGen r :=
   have : IsEquiv α (ReflTransGen r) := ⟨⟩
-  Subrelation.antisymm (eqvGen_le .single) (reflTransGen_le_eqvGen _)
+  Subrelation.antisymm (eqvGen_le fun _ _ => .single) (reflTransGen_le_eqvGen _)
 
 lemma reflTransGen_symmGen : ReflTransGen (SymmGen r) = EqvGen r := by
   rw [← eqvGen_eq_reflTransGen, eqvGen_symmGen]

Mathlib/Order/JordanHolder.lean

@@ -116,7 +116,7 @@ theorem Iso.rel
     (h_rel : ∀ {x y}, IsMaximal x (x ⊔ y) → e (x, x ⊔ y) (x ⊓ y, y))
     {x y : X × X} (h_iso : Iso x y) : e x y := by
   have : IsEquiv (X × X) e := { refl _ := h_refl, symm _ _ := h_symm, trans _ _ _ := h_trans }
-  refine Relation.EqvGen.eqvGen_le ?_ h_iso
+  refine Relation.EqvGen.eqvGen_le ?_ _ _ h_iso
   rintro ⟨a, b⟩ ⟨c, d⟩ ⟨h, rfl : b = a ⊔ d, rfl : c = a ⊓ d⟩
   exact h_rel h