diff --git a/Mathlib/Data/Quot.lean b/Mathlib/Data/Quot.lean
index 24e901a732024..a781d55aa2a06 100644
--- a/Mathlib/Data/Quot.lean
+++ b/Mathlib/Data/Quot.lean
@@ -240,13 +240,14 @@ variable {γ : Sort*} {sc : Setoid γ}
 /-- Map a function `f : α → β → γ` that sends equivalent elements to equivalent elements
 to a function `f : Quotient sa → Quotient sb → Quotient sc`.
 Useful to define binary operations on quotients. -/
-protected def map₂ (f : α → β → γ) (h : ∀ ⦃a₁ a₂⦄, a₁ ≈ a₂ → ∀ ⦃b₁ b₂⦄, b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂) :
+protected def map₂ (f : α → β → γ)
+ (h : ∀ ⦃a₁ a₂⦄, a₁ ≈ a₂ → ∀ ⦃b₁ b₂⦄, b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂) :
     Quotient sa → Quotient sb → Quotient sc :=
-  Quotient.lift₂ (fun x y ↦ ⟦f x y⟧) fun _ _ _ _ h₁ h₂ ↦ Quot.sound <| h _ _ _ _ h₁ h₂
+  Quotient.lift₂ (fun x y ↦ ⟦f x y⟧) fun _ _ _ _ h₁ h₂ ↦ Quot.sound <| h h₁ h₂
 
 @[simp]
 theorem map₂_mk (f : α → β → γ)
-(h : ∀ a₁ a₂ b₁ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂) (x : α) (y : β) :
+(h : ∀ a₁ a₂, a₁ ≈ a₂ → ∀ b₁ b₂, b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂) (x : α) (y : β) :
     Quotient.map₂ f h (⟦x⟧ : Quotient sa) (⟦y⟧ : Quotient sb) = (⟦f x y⟧ : Quotient sc) :=
   rfl
 
@@ -703,14 +704,12 @@ theorem map'_mk'' (f : α → β) (h) (x : α) :
   rfl
 
 /-- A version of `Quotient.map₂` using curly braces and unification. -/
-protected def map₂' (f : α → β → γ) (h : ∀ a₁ a₂ b₁ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ ≈ f a₂ b₂) :
-    Quotient s₁ → Quotient s₂ → Quotient s₃ :=
-  Quotient.map₂ f h
+@[deprecated (since := "2024-11-29")] protected alias map₂' := Quotient.map₂
 
 @[simp]
 theorem map₂'_mk'' (f : α → β → γ) (h) (x : α) :
     (Quotient.mk'' x : Quotient s₁).map₂' f h =
-      (Quotient.map' (f x) (fun _ _ => h _ _ _ _ (Setoid.refl x)) : Quotient s₂ → Quotient s₃) :=
+      (Quotient.map' (f x) (h (Setoid.refl x)) : Quotient s₂ → Quotient s₃) :=
   rfl
 
 theorem exact' {a b : α} :
diff --git a/Mathlib/GroupTheory/Coset/Basic.lean b/Mathlib/GroupTheory/Coset/Basic.lean
index 4f8c575b67fcf..92b002632be39 100644
--- a/Mathlib/GroupTheory/Coset/Basic.lean
+++ b/Mathlib/GroupTheory/Coset/Basic.lean
@@ -377,14 +377,14 @@ def quotientEquivProdOfLE' (h_le : s ≤ t) (f : α ⧸ t → α)
     ⟨a.map' id fun _ _ h => leftRel_apply.mpr (h_le (leftRel_apply.mp h)),
       a.map' (fun g : α => ⟨(f (Quotient.mk'' g))⁻¹ * g, leftRel_apply.mp (Quotient.exact' (hf g))⟩)
         fun b c h => by
-        rw [leftRel_apply]
+        simp only [HasEquiv.Equiv]; rw [leftRel_apply]
         change ((f b)⁻¹ * b)⁻¹ * ((f c)⁻¹ * c) ∈ s
         have key : f b = f c :=
           congr_arg f (Quotient.sound' (leftRel_apply.mpr (h_le (leftRel_apply.mp h))))
         rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]⟩
   invFun a := by
     refine a.2.map' (fun (b : { x // x ∈ t}) => f a.1 * b) fun b c h => by
-      rw [leftRel_apply] at h ⊢
+      simp only [HasEquiv.Equiv] at *; rw [leftRel_apply] at *
       change (f a.1 * b)⁻¹ * (f a.1 * c) ∈ s
       rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
   left_inv := by
@@ -412,7 +412,7 @@ def quotientSubgroupOfEmbeddingOfLE (H : Subgroup α) (h : s ≤ t) :
     s ⧸ H.subgroupOf s ↪ t ⧸ H.subgroupOf t where
   toFun :=
     Quotient.map' (inclusion h) fun a b => by
-      simp_rw [leftRel_eq]
+      simp_rw [HasEquiv.Equiv, leftRel_eq]
       exact id
   inj' :=
     Quotient.ind₂' <| by
@@ -431,7 +431,7 @@ theorem quotientSubgroupOfEmbeddingOfLE_apply_mk (H : Subgroup α) (h : s ≤ t)
 def quotientSubgroupOfMapOfLE (H : Subgroup α) (h : s ≤ t) :
     H ⧸ s.subgroupOf H → H ⧸ t.subgroupOf H :=
   Quotient.map' id fun a b => by
-    simp_rw [leftRel_eq]
+    simp_rw [HasEquiv.Equiv, leftRel_eq]
     apply h
 
 -- Porting note: I had to add the type ascription to the right-hand side or else Lean times out.
@@ -445,7 +445,7 @@ theorem quotientSubgroupOfMapOfLE_apply_mk (H : Subgroup α) (h : s ≤ t) (g :
 @[to_additive "If `s ≤ t`, then there is a map `α ⧸ s → α ⧸ t`."]
 def quotientMapOfLE (h : s ≤ t) : α ⧸ s → α ⧸ t :=
   Quotient.map' id fun a b => by
-    simp_rw [leftRel_eq]
+    simp_rw [HasEquiv.Equiv, leftRel_eq]
     apply h
 
 @[to_additive (attr := simp)]
diff --git a/Mathlib/GroupTheory/Coset/Defs.lean b/Mathlib/GroupTheory/Coset/Defs.lean
index c57164adfbaee..a3def598e96b6 100644
--- a/Mathlib/GroupTheory/Coset/Defs.lean
+++ b/Mathlib/GroupTheory/Coset/Defs.lean
@@ -127,12 +127,12 @@ instance rightRelDecidable [DecidablePred (· ∈ s)] : DecidableRel (rightRel s
 def quotientRightRelEquivQuotientLeftRel : Quotient (QuotientGroup.rightRel s) ≃ α ⧸ s where
   toFun :=
     Quotient.map' (fun g => g⁻¹) fun a b => by
-      rw [leftRel_apply, rightRel_apply]
+      simp only [HasEquiv.Equiv]; rw [leftRel_apply, rightRel_apply]
       exact fun h => (congr_arg (· ∈ s) (by simp [mul_assoc])).mp (s.inv_mem h)
       -- Porting note: replace with `by group`
   invFun :=
     Quotient.map' (fun g => g⁻¹) fun a b => by
-      rw [leftRel_apply, rightRel_apply]
+      simp only [HasEquiv.Equiv]; rw [leftRel_apply, rightRel_apply]
       exact fun h => (congr_arg (· ∈ s) (by simp [mul_assoc])).mp (s.inv_mem h)
       -- Porting note: replace with `by group`
   left_inv g :=
diff --git a/Mathlib/NumberTheory/RamificationInertia/Basic.lean b/Mathlib/NumberTheory/RamificationInertia/Basic.lean
index 92cb53f8ad16f..8e69ed5882758 100644
--- a/Mathlib/NumberTheory/RamificationInertia/Basic.lean
+++ b/Mathlib/NumberTheory/RamificationInertia/Basic.lean
@@ -500,6 +500,7 @@ noncomputable def quotientToQuotientRangePowQuotSuccAux {i : ℕ} {a : S} (a_mem
       (P ^ i).map (Ideal.Quotient.mk (P ^ e)) ⧸ LinearMap.range (powQuotSuccInclusion f p P i) :=
   Quotient.map' (fun x : S => ⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_right x _ a_mem)⟩)
     fun x y h => by
+    simp only [HasEquiv.Equiv] at *
     rw [Submodule.quotientRel_def] at h ⊢
     simp only [_root_.map_mul, LinearMap.mem_range]
     refine ⟨⟨_, Ideal.mem_map_of_mem _ (Ideal.mul_mem_mul a_mem h)⟩, ?_⟩