chore: deprecate Setoid.Rel

Mathlib/CategoryTheory/Limits/Shapes/SingleObj.lean

@@ -75,7 +75,7 @@ variable {G : Type v} [Group G] (J : SingleObj G ⥤ Type u)
 equivalent to the `MulAction.orbitRel` equivalence relation on `J.obj (SingleObj.star G)`. -/
 lemma Types.Quot.Rel.iff_orbitRel (x y : J.obj (SingleObj.star G)) :
     Types.Quot.Rel J ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩
-    ↔ Setoid.Rel (MulAction.orbitRel G (J.obj (SingleObj.star G))) x y := by
+    ↔ MulAction.orbitRel G (J.obj (SingleObj.star G)) x y := by
   have h (g : G) : y = g • x ↔ g • x = y := ⟨symm, symm⟩
   conv => rhs; rw [Setoid.comm']
   show (∃ g : G, y = g • x) ↔ (∃ g : G, g • x = y)

Mathlib/Data/Setoid/Partition.lean

@@ -53,9 +53,9 @@ def mkClasses (c : Set (Set α)) (H : ∀ a, ∃! b ∈ c, a ∈ b) : Setoid α
 
 /-- Makes the equivalence classes of an equivalence relation. -/
 def classes (r : Setoid α) : Set (Set α) :=
-  { s | ∃ y, s = { x | r.Rel x y } }
+  { s | ∃ y, s = { x | r x y } }
 
-theorem mem_classes (r : Setoid α) (y) : { x | r.Rel x y } ∈ r.classes :=
+theorem mem_classes (r : Setoid α) (y) : { x | r x y } ∈ r.classes :=
   ⟨y, rfl⟩
 
 theorem classes_ker_subset_fiber_set {β : Type*} (f : α → β) :
@@ -74,10 +74,10 @@ theorem card_classes_ker_le {α β : Type*} [Fintype β] (f : α → β)
 
 /-- Two equivalence relations are equal iff all their equivalence classes are equal. -/
 theorem eq_iff_classes_eq {r₁ r₂ : Setoid α} :
-    r₁ = r₂ ↔ ∀ x, { y | r₁.Rel x y } = { y | r₂.Rel x y } :=
+    r₁ = r₂ ↔ ∀ x, { y | r₁ x y } = { y | r₂ x y } :=
   ⟨fun h _x => h ▸ rfl, fun h => ext' fun x => Set.ext_iff.1 <| h x⟩
 
-theorem rel_iff_exists_classes (r : Setoid α) {x y} : r.Rel x y ↔ ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c :=
+theorem rel_iff_exists_classes (r : Setoid α) {x y} : r x y ↔ ∃ c ∈ r.classes, x ∈ c ∧ y ∈ c :=
   ⟨fun h => ⟨_, r.mem_classes y, h, r.refl' y⟩, fun ⟨c, ⟨z, hz⟩, hx, hy⟩ => by
     subst c
     exact r.trans' hx (r.symm' hy)⟩
@@ -92,7 +92,7 @@ theorem empty_not_mem_classes {r : Setoid α} : ∅ ∉ r.classes := fun ⟨y, h
 
 /-- Equivalence classes partition the type. -/
 theorem classes_eqv_classes {r : Setoid α} (a) : ∃! b ∈ r.classes, a ∈ b :=
-  ExistsUnique.intro { x | r.Rel x a } ⟨r.mem_classes a, r.refl' _⟩ <| by
+  ExistsUnique.intro { x | r x a } ⟨r.mem_classes a, r.refl' _⟩ <| by
     rintro y ⟨⟨_, rfl⟩, ha⟩
     ext x
     exact ⟨fun hx => r.trans' hx (r.symm' ha), fun hx => r.trans' hx ha⟩
@@ -105,7 +105,7 @@ theorem eq_of_mem_classes {r : Setoid α} {x b} (hc : b ∈ r.classes) (hb : x 
 /-- The elements of a set of sets partitioning α are the equivalence classes of the
     equivalence relation defined by the set of sets. -/
 theorem eq_eqv_class_of_mem {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) {s y}
-    (hs : s ∈ c) (hy : y ∈ s) : s = { x | (mkClasses c H).Rel x y } := by
+    (hs : s ∈ c) (hy : y ∈ s) : s = { x | mkClasses c H x y } := by
   ext x
   constructor
   · intro hx _s' hs' hx'
@@ -117,11 +117,11 @@ theorem eq_eqv_class_of_mem {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b
 /-- The equivalence classes of the equivalence relation defined by a set of sets
     partitioning α are elements of the set of sets. -/
 theorem eqv_class_mem {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) {y} :
-    { x | (mkClasses c H).Rel x y } ∈ c :=
+    { x | mkClasses c H x y } ∈ c :=
   (H y).elim fun _ hc _ => eq_eqv_class_of_mem H hc.1 hc.2 ▸ hc.1
 
 theorem eqv_class_mem' {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) {x} :
-    { y : α | (mkClasses c H).Rel x y } ∈ c := by
+    { y : α | mkClasses c H x y } ∈ c := by
   convert @Setoid.eqv_class_mem _ _ H x using 3
   rw [Setoid.comm']
 
@@ -146,12 +146,12 @@ def setoidOfDisjointUnion {c : Set (Set α)} (hu : Set.sUnion c = @Set.univ α)
     relation r equals r. -/
 theorem mkClasses_classes (r : Setoid α) : mkClasses r.classes classes_eqv_classes = r :=
   ext' fun x _y =>
-    ⟨fun h => r.symm' (h { z | r.Rel z x } (r.mem_classes x) <| r.refl' x), fun h _b hb hx =>
+    ⟨fun h => r.symm' (h { z | r z x } (r.mem_classes x) <| r.refl' x), fun h _b hb hx =>
       eq_of_mem_classes (r.mem_classes x) (r.refl' x) hb hx ▸ r.symm' h⟩
 
 @[simp]
 theorem sUnion_classes (r : Setoid α) : ⋃₀ r.classes = Set.univ :=
-  Set.eq_univ_of_forall fun x => Set.mem_sUnion.2 ⟨{ y | r.Rel y x }, ⟨x, rfl⟩, Setoid.refl _⟩
+  Set.eq_univ_of_forall fun x => Set.mem_sUnion.2 ⟨{ y | r y x }, ⟨x, rfl⟩, Setoid.refl _⟩
 
 /-- The equivalence between the quotient by an equivalence relation and its
 type of equivalence classes. -/
@@ -177,8 +177,8 @@ noncomputable def quotientEquivClasses (r : Setoid α) : Quotient r ≃ Setoid.c
 
 @[simp]
 lemma quotientEquivClasses_mk_eq (r : Setoid α) (a : α) :
-    (quotientEquivClasses r (Quotient.mk r a) : Set α) = { x | r.Rel x a } :=
-  (@Subtype.ext_iff_val _ _ _ ⟨{ x | r.Rel x a }, Setoid.mem_classes r a⟩).mp rfl
+    (quotientEquivClasses r (Quotient.mk r a) : Set α) = { x | r x a } :=
+  (@Subtype.ext_iff_val _ _ _ ⟨{ x | r x a }, Setoid.mem_classes r a⟩).mp rfl
 
 section Partition
 
@@ -217,7 +217,7 @@ theorem IsPartition.sUnion_eq_univ {c : Set (Set α)} (hc : IsPartition c) : ⋃
 
 /-- All elements of a partition of α are the equivalence class of some y ∈ α. -/
 theorem exists_of_mem_partition {c : Set (Set α)} (hc : IsPartition c) {s} (hs : s ∈ c) :
-    ∃ y, s = { x | (mkClasses c hc.2).Rel x y } :=
+    ∃ y, s = { x | mkClasses c hc.2 x y } :=
   let ⟨y, hy⟩ := nonempty_of_mem_partition hc hs
   ⟨y, eq_eqv_class_of_mem hc.2 hs hy⟩
 
@@ -367,7 +367,7 @@ protected abbrev setoid (hs : IndexedPartition s) : Setoid α :=
 theorem index_some (i : ι) : hs.index (hs.some i) = i :=
   (mem_iff_index_eq _).1 <| hs.some_mem i
 
-theorem some_index (x : α) : hs.setoid.Rel (hs.some (hs.index x)) x :=
+theorem some_index (x : α) : hs.setoid (hs.some (hs.index x)) x :=
   hs.index_some (hs.index x)
 
 /-- The quotient associated to an indexed partition. -/
@@ -423,7 +423,7 @@ theorem index_out' (x : hs.Quotient) : hs.index x.out' = hs.index (hs.out x) :=
 theorem proj_out (x : hs.Quotient) : hs.proj (hs.out x) = x :=
   Quotient.inductionOn' x fun x => Quotient.sound' <| hs.some_index x
 
-theorem class_of {x : α} : setOf (hs.setoid.Rel x) = s (hs.index x) :=
+theorem class_of {x : α} : setOf (hs.setoid x) = s (hs.index x) :=
   Set.ext fun _y => eq_comm.trans hs.mem_iff_index_eq.symm
 
 theorem proj_fiber (x : hs.Quotient) : hs.proj ⁻¹' {x} = s (hs.equivQuotient.symm x) :=

Mathlib/GroupTheory/DoubleCoset.lean

@@ -72,15 +72,15 @@ def Quotient (H K : Set G) : Type _ :=
   _root_.Quotient (setoid H K)
 
 theorem rel_iff {H K : Subgroup G} {x y : G} :
-    (setoid ↑H ↑K).Rel x y ↔ ∃ a ∈ H, ∃ b ∈ K, y = a * x * b :=
+    setoid ↑H ↑K x y ↔ ∃ a ∈ H, ∃ b ∈ K, y = a * x * b :=
   Iff.trans
     ⟨fun (hxy : doset x H K = doset y H K) => hxy ▸ mem_doset_self H K y,
       fun hxy => (doset_eq_of_mem hxy).symm⟩ mem_doset
 
 theorem bot_rel_eq_leftRel (H : Subgroup G) :
-    (setoid ↑(⊥ : Subgroup G) ↑H).Rel = (QuotientGroup.leftRel H).Rel := by
+    ⇑(setoid ↑(⊥ : Subgroup G) ↑H) = ⇑(QuotientGroup.leftRel H) := by
   ext a b
-  rw [rel_iff, Setoid.Rel, QuotientGroup.leftRel_apply]
+  rw [rel_iff, QuotientGroup.leftRel_apply]
   constructor
   · rintro ⟨a, rfl : a = 1, b, hb, rfl⟩
     change a⁻¹ * (1 * a * b) ∈ H
@@ -89,9 +89,9 @@ theorem bot_rel_eq_leftRel (H : Subgroup G) :
     exact ⟨1, rfl, a⁻¹ * b, h, by rw [one_mul, mul_inv_cancel_left]⟩
 
 theorem rel_bot_eq_right_group_rel (H : Subgroup G) :
-    (setoid ↑H ↑(⊥ : Subgroup G)).Rel = (QuotientGroup.rightRel H).Rel := by
+    ⇑(setoid ↑H ↑(⊥ : Subgroup G)) = ⇑(QuotientGroup.rightRel H) := by
   ext a b
-  rw [rel_iff, Setoid.Rel, QuotientGroup.rightRel_apply]
+  rw [rel_iff, QuotientGroup.rightRel_apply]
   constructor
   · rintro ⟨b, hb, a, rfl : a = 1, rfl⟩
     change b * a * 1 * a⁻¹ ∈ H

Mathlib/GroupTheory/GroupAction/Basic.lean

@@ -369,11 +369,11 @@ def orbitRel : Setoid α where
 variable {G α}
 
 @[to_additive]
-theorem orbitRel_apply {a b : α} : (orbitRel G α).Rel a b ↔ a ∈ orbit G b :=
+theorem orbitRel_apply {a b : α} : orbitRel G α a b ↔ a ∈ orbit G b :=
   Iff.rfl
 
 @[to_additive]
-lemma orbitRel_r_apply {a b : α} : (orbitRel G _).r a b ↔ a ∈ orbit G b :=
+lemma orbitRel_r_apply {a b : α} : orbitRel G _ a b ↔ a ∈ orbit G b :=
   Iff.rfl
 
 @[to_additive]
@@ -702,7 +702,7 @@ theorem stabilizer_smul_eq_stabilizer_map_conj (g : G) (a : α) :
     inv_mul_cancel, one_smul, ← mem_stabilizer_iff, Subgroup.mem_map_equiv, MulAut.conj_symm_apply]
 
 /-- A bijection between the stabilizers of two elements in the same orbit. -/
-noncomputable def stabilizerEquivStabilizerOfOrbitRel {a b : α} (h : (orbitRel G α).Rel a b) :
+noncomputable def stabilizerEquivStabilizerOfOrbitRel {a b : α} (h : orbitRel G α a b) :
     stabilizer G a ≃* stabilizer G b :=
   let g : G := Classical.choose h
   have hg : g • b = a := Classical.choose_spec h
@@ -726,7 +726,7 @@ theorem stabilizer_vadd_eq_stabilizer_map_conj (g : G) (a : α) :
     AddAut.conj_symm_apply]
 
 /-- A bijection between the stabilizers of two elements in the same orbit. -/
-noncomputable def stabilizerEquivStabilizerOfOrbitRel {a b : α} (h : (orbitRel G α).Rel a b) :
+noncomputable def stabilizerEquivStabilizerOfOrbitRel {a b : α} (h : orbitRel G α a b) :
     stabilizer G a ≃+ stabilizer G b :=
   let g : G := Classical.choose h
   have hg : g +ᵥ b = a := Classical.choose_spec h

Mathlib/GroupTheory/GroupAction/ConjAct.lean

@@ -276,7 +276,7 @@ theorem fixedPoints_eq_center : fixedPoints (ConjAct G) G = center G := by
 theorem mem_orbit_conjAct {g h : G} : g ∈ orbit (ConjAct G) h ↔ IsConj g h := by
   rw [isConj_comm, isConj_iff, mem_orbit_iff]; rfl
 
-theorem orbitRel_conjAct : (orbitRel (ConjAct G) G).Rel = IsConj :=
+theorem orbitRel_conjAct : ⇑(orbitRel (ConjAct G) G) = IsConj :=
   funext₂ fun g h => by rw [orbitRel_apply, mem_orbit_conjAct]
 
 theorem orbit_eq_carrier_conjClasses (g : G) :

Mathlib/GroupTheory/GroupAction/Quotient.lean

@@ -328,8 +328,7 @@ noncomputable def equivSubgroupOrbitsSetoidComap (H : Subgroup α) (ω : Ω) :
     have hx := x.property
     simp only [Set.mem_preimage, Set.mem_singleton_iff] at hx
     rwa [orbitRel.Quotient.mem_orbit, @Quotient.mk''_eq_mk]⟩⟧) fun a b h ↦ by
-      change Setoid.Rel _ _ _ at h
-      rw [Setoid.comap_rel, Setoid.Rel, ← Quotient.eq'', @Quotient.mk''_eq_mk] at h
+      rw [Setoid.comap_rel, ← Quotient.eq'', @Quotient.mk''_eq_mk] at h
       simp only [orbitRel.Quotient.subgroup_quotient_eq_iff]
       exact h
   left_inv := by

Mathlib/Order/Partition/Finpartition.lean

@@ -581,12 +581,12 @@ def ofSetoid (s : Setoid α) [DecidableRel s.r] : Finpartition (univ : Finset α
   sup_parts := by
     ext a
     simp only [sup_image, Function.id_comp, mem_univ, mem_sup, mem_filter, true_and, iff_true]
-    use a; exact s.refl a
+    use a
   not_bot_mem := by
     rw [bot_eq_empty, mem_image, not_exists]
     intro a
     simp only [filter_eq_empty_iff, not_forall, mem_univ, forall_true_left, true_and, not_not]
-    use a; exact s.refl a
+    use a
 
 theorem mem_part_ofSetoid_iff_rel {s : Setoid α} [DecidableRel s.r] {b : α} :
     b ∈ (ofSetoid s).part a ↔ s.r a b := by

Mathlib/RingTheory/AdicCompletion/Algebra.lean

@@ -197,7 +197,7 @@ theorem smul_mk {m n : ℕ} (hmn : m ≤ n) (r : AdicCauchySequence I R)
 good definitional behaviour for the module instance on adic completions -/
 instance : SMul (R ⧸ (I • ⊤ : Ideal R)) (M ⧸ (I • ⊤ : Submodule R M)) where
   smul r x :=
-    Quotient.liftOn r (· • x) fun b₁ b₂ (h : Setoid.Rel _ b₁ b₂) ↦ by
+    Quotient.liftOn r (· • x) fun b₁ b₂ h ↦ by
       refine Quotient.inductionOn' x (fun x ↦ ?_)
       have h : b₁ - b₂ ∈ (I : Submodule R R) := by
         rwa [show I = I • ⊤ by simp, ← Submodule.quotientRel_r_def]

Mathlib/RingTheory/Congruence/Basic.lean

@@ -74,7 +74,7 @@ instance : FunLike (RingCon R) R (R → Prop) where
     rcases x with ⟨⟨x, _⟩, _⟩
     rcases y with ⟨⟨y, _⟩, _⟩
     congr!
-    rw [Setoid.ext_iff, (show x.Rel = y.Rel from h)]
+    rw [Setoid.ext_iff, (show ⇑x = ⇑y from h)]
     simp
 
 theorem rel_eq_coe : c.r = c :=

Mathlib/RingTheory/Valuation/ValuationRing.lean

@@ -142,22 +142,22 @@ noncomputable instance linearOrder : LinearOrder (ValueGroup A K) where
 noncomputable instance linearOrderedCommGroupWithZero :
     LinearOrderedCommGroupWithZero (ValueGroup A K) :=
   { linearOrder .. with
-    mul_assoc := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; apply Quotient.sound'; rw [mul_assoc]; apply Setoid.refl'
-    one_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [one_mul]; apply Setoid.refl'
-    mul_one := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_one]; apply Setoid.refl'
-    mul_comm := by rintro ⟨a⟩ ⟨b⟩; apply Quotient.sound'; rw [mul_comm]; apply Setoid.refl'
+    mul_assoc := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; apply Quotient.sound'; rw [mul_assoc]
+    one_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [one_mul]
+    mul_one := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_one]
+    mul_comm := by rintro ⟨a⟩ ⟨b⟩; apply Quotient.sound'; rw [mul_comm]
     mul_le_mul_left := by
       rintro ⟨a⟩ ⟨b⟩ ⟨c, rfl⟩ ⟨d⟩
       use c; simp only [Algebra.smul_def]; ring
-    zero_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [zero_mul]; apply Setoid.refl'
-    mul_zero := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_zero]; apply Setoid.refl'
+    zero_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [zero_mul]
+    mul_zero := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_zero]
     zero_le_one := ⟨0, by rw [zero_smul]⟩
     exists_pair_ne := by
       use 0, 1
       intro c; obtain ⟨d, hd⟩ := Quotient.exact' c
       apply_fun fun t => d⁻¹ • t at hd
       simp only [inv_smul_smul, smul_zero, one_ne_zero] at hd
-    inv_zero := by apply Quotient.sound'; rw [inv_zero]; apply Setoid.refl'
+    inv_zero := by apply Quotient.sound'; rw [inv_zero]
     mul_inv_cancel := by
       rintro ⟨a⟩ ha
       apply Quotient.sound'

Mathlib/Topology/DiscreteQuotient.lean

@@ -69,7 +69,7 @@ variable {α X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [Topologic
 @[ext] -- Porting note: in Lean 4, uses projection to `r` instead of `Setoid`.
 structure DiscreteQuotient (X : Type*) [TopologicalSpace X] extends Setoid X where
   /-- For every point `x`, the set `{ y | Rel x y }` is an open set. -/
-  protected isOpen_setOf_rel : ∀ x, IsOpen (setOf (toSetoid.Rel x))
+  protected isOpen_setOf_rel : ∀ x, IsOpen (setOf (toSetoid x))
 
 namespace DiscreteQuotient
 
@@ -81,13 +81,13 @@ lemma toSetoid_injective : Function.Injective (@toSetoid X _)
 /-- Construct a discrete quotient from a clopen set. -/
 def ofIsClopen {A : Set X} (h : IsClopen A) : DiscreteQuotient X where
   toSetoid := ⟨fun x y => x ∈ A ↔ y ∈ A, fun _ => Iff.rfl, Iff.symm, Iff.trans⟩
-  isOpen_setOf_rel x := by by_cases hx : x ∈ A <;> simp [Setoid.Rel, hx, h.1, h.2, ← compl_setOf]
+  isOpen_setOf_rel x := by by_cases hx : x ∈ A <;> simp [hx, h.1, h.2, ← compl_setOf]
 
-theorem refl : ∀ x, S.Rel x x := S.refl'
+theorem refl : ∀ x, S.toSetoid x x := S.refl'
 
-theorem symm (x y : X) : S.Rel x y → S.Rel y x := S.symm'
+theorem symm (x y : X) : S.toSetoid x y → S.toSetoid y x := S.symm'
 
-theorem trans (x y z : X) : S.Rel x y → S.Rel y z → S.Rel x z := S.trans'
+theorem trans (x y z : X) : S.toSetoid x y → S.toSetoid y z → S.toSetoid x z := S.trans'
 
 /-- The setoid whose quotient yields the discrete quotient. -/
 add_decl_doc toSetoid
@@ -101,7 +101,7 @@ instance : TopologicalSpace S :=
 /-- The projection from `X` to the given discrete quotient. -/
 def proj : X → S := Quotient.mk''
 
-theorem fiber_eq (x : X) : S.proj ⁻¹' {S.proj x} = setOf (S.Rel x) :=
+theorem fiber_eq (x : X) : S.proj ⁻¹' {S.proj x} = setOf (S.toSetoid x) :=
   Set.ext fun _ => eq_comm.trans Quotient.eq''
 
 theorem proj_surjective : Function.Surjective S.proj :=
@@ -130,7 +130,7 @@ theorem isOpen_preimage (A : Set S) : IsOpen (S.proj ⁻¹' A) :=
 theorem isClosed_preimage (A : Set S) : IsClosed (S.proj ⁻¹' A) :=
   (S.isClopen_preimage A).1
 
-theorem isClopen_setOf_rel (x : X) : IsClopen (setOf (S.Rel x)) := by
+theorem isClopen_setOf_rel (x : X) : IsClopen (setOf (S.toSetoid x)) := by
   rw [← fiber_eq]
   apply isClopen_preimage
 
@@ -359,7 +359,7 @@ lemma comp_finsetClopens [CompactSpace X] :
     (Set.image (fun (t : Clopens X) ↦ t.carrier) ∘ Finset.toSet) ∘
       finsetClopens X = fun ⟨f, _⟩ ↦ f.classes := by
   ext d
-  simp only [Setoid.classes, Setoid.Rel, Set.mem_setOf_eq, Function.comp_apply,
+  simp only [Setoid.classes, Set.mem_setOf_eq, Function.comp_apply,
     finsetClopens, Set.coe_toFinset, Set.mem_image, Set.mem_range,
     exists_exists_eq_and]
   constructor

Mathlib/Topology/MetricSpace/Contracting.lean

@@ -137,7 +137,7 @@ theorem efixedPoint_eq_of_edist_lt_top (hf : ContractingWith K f) {x : α} (hx :
     efixedPoint f hf x hx = efixedPoint f hf y hy := by
   refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')
     <;> try apply efixedPoint_isFixedPt
-  change edistLtTopSetoid.Rel _ _
+  change edistLtTopSetoid _ _
   trans x
   · apply Setoid.symm' -- Porting note: Originally `symm`
     exact hf.edist_efixedPoint_lt_top hx
@@ -221,7 +221,7 @@ theorem efixedPoint_eq_of_edist_lt_top' (hf : ContractingWith K f) {s : Set α}
     efixedPoint' f hsc hsf hfs x hxs hx = efixedPoint' f htc htf hft y hyt hy := by
   refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')
     <;> try apply efixedPoint_isFixedPt'
-  change edistLtTopSetoid.Rel _ _
+  change edistLtTopSetoid _ _
   trans x
   · apply Setoid.symm' -- Porting note: Originally `symm`
     apply edist_efixedPoint_lt_top'

Mathlib/Topology/Separation.lean

@@ -1629,7 +1629,7 @@ instance : TopologicalSpace (t2Quotient X) :=
 /-- The map from a topological space to its largest T2 quotient. -/
 def mk : X → t2Quotient X := Quotient.mk (t2Setoid X)
 
-lemma mk_eq {x y : X} : mk x = mk y ↔ ∀ s : Setoid X, T2Space (Quotient s) → s.Rel x y :=
+lemma mk_eq {x y : X} : mk x = mk y ↔ ∀ s : Setoid X, T2Space (Quotient s) → s x y :=
   Setoid.quotient_mk_sInf_eq
 
 variable (X)