[Merged by Bors] - chore(Order/RelIso/Basic): [s : Setoid α] => {s : Setoid α}

Mathlib/Order/Antisymmetrization.lean

@@ -119,11 +119,11 @@ theorem AntisymmRel.image {a b : α} (h : AntisymmRel (· ≤ ·) a b) {f : α 
   ⟨hf h.1, hf h.2⟩
 
 instance instPartialOrderAntisymmetrization : PartialOrder (Antisymmetrization α (· ≤ ·)) where
-  le a b :=
-    (Quotient.liftOn₂' a b (· ≤ ·)) fun (_ _ _ _ : α) h₁ h₂ =>
+  le :=
+    Quotient.lift₂ (· ≤ ·) fun (_ _ _ _ : α) h₁ h₂ =>
       propext ⟨fun h => h₁.2.trans <| h.trans h₂.1, fun h => h₁.1.trans <| h.trans h₂.2⟩
-  lt a b :=
-    (Quotient.liftOn₂' a b (· < ·)) fun (_ _ _ _ : α) h₁ h₂ =>
+  lt :=
+    Quotient.lift₂ (· < ·) fun (_ _ _ _ : α) h₁ h₂ =>
       propext ⟨fun h => h₁.2.trans_lt <| h.trans_le h₂.1, fun h =>
                 h₁.1.trans_lt <| h.trans_le h₂.2⟩
   le_refl a := Quotient.inductionOn' a <| le_refl
@@ -138,11 +138,11 @@ theorem antisymmetrization_fibration :
 
 theorem acc_antisymmetrization_iff : Acc (· < ·)
     (@toAntisymmetrization α (· ≤ ·) _ a) ↔ Acc (· < ·) a :=
-  acc_liftOn₂'_iff
+  acc_lift₂_iff
 
 theorem wellFounded_antisymmetrization_iff :
     WellFounded (@LT.lt (Antisymmetrization α (· ≤ ·)) _) ↔ WellFounded (@LT.lt α _) :=
-  wellFounded_liftOn₂'_iff
+  wellFounded_lift₂_iff
 
 instance [WellFoundedLT α] : WellFoundedLT (Antisymmetrization α (· ≤ ·)) :=
   ⟨wellFounded_antisymmetrization_iff.2 IsWellFounded.wf⟩
@@ -167,12 +167,12 @@ theorem toAntisymmetrization_lt_toAntisymmetrization_iff :
 @[simp]
 theorem ofAntisymmetrization_le_ofAntisymmetrization_iff {a b : Antisymmetrization α (· ≤ ·)} :
     ofAntisymmetrization (· ≤ ·) a ≤ ofAntisymmetrization (· ≤ ·) b ↔ a ≤ b :=
-  (Quotient.out'RelEmbedding _).map_rel_iff
+  (Quotient.outRelEmbedding _).map_rel_iff
 
 @[simp]
 theorem ofAntisymmetrization_lt_ofAntisymmetrization_iff {a b : Antisymmetrization α (· ≤ ·)} :
     ofAntisymmetrization (· ≤ ·) a < ofAntisymmetrization (· ≤ ·) b ↔ a < b :=
-  (Quotient.out'RelEmbedding _).map_rel_iff
+  (Quotient.outRelEmbedding _).map_rel_iff
 
 @[mono]
 theorem toAntisymmetrization_mono : Monotone (@toAntisymmetrization α (· ≤ ·) _) := fun _ _ => id
@@ -209,7 +209,7 @@ variable (α)
 /-- `ofAntisymmetrization` as an order embedding. -/
 @[simps]
 noncomputable def OrderEmbedding.ofAntisymmetrization : Antisymmetrization α (· ≤ ·) ↪o α :=
-  { Quotient.out'RelEmbedding _ with toFun := _root_.ofAntisymmetrization _ }
+  { Quotient.outRelEmbedding _ with toFun := _root_.ofAntisymmetrization _ }
 
 /-- `Antisymmetrization` and `orderDual` commute. -/
 def OrderIso.dualAntisymmetrization :

Mathlib/Order/RelIso/Basic.lean

@@ -349,15 +349,15 @@ instance Subtype.wellFoundedGT [LT α] [WellFoundedGT α] (p : α → Prop) :
     WellFoundedGT (Subtype p) :=
   (Subtype.relEmbedding (· > ·) p).isWellFounded
 
-/-- `Quotient.mk'` as a relation homomorphism between the relation and the lift of a relation. -/
+/-- `Quotient.mk` as a relation homomorphism between the relation and the lift of a relation. -/
 @[simps]
-def Quotient.mkRelHom [Setoid α] {r : α → α → Prop}
+def Quotient.mkRelHom {_ : Setoid α} {r : α → α → Prop}
     (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) : r →r Quotient.lift₂ r H :=
-  ⟨@Quotient.mk' α _, id⟩
+  ⟨Quotient.mk _, id⟩
 
 /-- `Quotient.out` as a relation embedding between the lift of a relation and the relation. -/
 @[simps!]
-noncomputable def Quotient.outRelEmbedding [Setoid α] {r : α → α → Prop}
+noncomputable def Quotient.outRelEmbedding {_ : Setoid α} {r : α → α → Prop}
     (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂) : Quotient.lift₂ r H ↪r r :=
   ⟨Embedding.quotientOut α, by
     refine @fun x y => Quotient.inductionOn₂ x y fun a b => ?_
@@ -371,7 +371,7 @@ noncomputable def Quotient.out'RelEmbedding {_ : Setoid α} {r : α → α → P
   { Quotient.outRelEmbedding H with toFun := Quotient.out' }
 
 @[simp]
-theorem acc_lift₂_iff [Setoid α] {r : α → α → Prop}
+theorem acc_lift₂_iff {_ : Setoid α} {r : α → α → Prop}
     {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂} {a} :
     Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a := by
   constructor
@@ -389,7 +389,7 @@ theorem acc_liftOn₂'_iff {s : Setoid α} {r : α → α → Prop} {H} {a} :
 
 /-- A relation is well founded iff its lift to a quotient is. -/
 @[simp]
-theorem wellFounded_lift₂_iff [Setoid α] {r : α → α → Prop}
+theorem wellFounded_lift₂_iff {_ : Setoid α} {r : α → α → Prop}
     {H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂} :
     WellFounded (Quotient.lift₂ r H) ↔ WellFounded r := by
   constructor