diff --git a/Mathlib/GroupTheory/Congruence/Basic.lean b/Mathlib/GroupTheory/Congruence/Basic.lean
index 3bae7589d7021..0c9e3103728fb 100644
--- a/Mathlib/GroupTheory/Congruence/Basic.lean
+++ b/Mathlib/GroupTheory/Congruence/Basic.lean
@@ -298,9 +298,8 @@ lemma comapQuotientEquivOfSurj_symm_mk (c : Con M) {f : N →* M} (hf : Function
 /-- This version infers the surjectivity of the function from a MulEquiv function -/
 @[simp]
 lemma comapQuotientEquivOfSurj_symm_mk' (c : Con M) (f : N ≃* M) (x : N) :
-    ((@MulEquiv.symm (Con.Quotient (comap ⇑f _ c)) _ (hasMul (comap ⇑f _ c))
-    _ (comapQuotientEquivOfSurj c ↑f f.surjective))
-    ⟦f x⟧) = ↑x :=
+    ((@MulEquiv.symm (Con.Quotient (comap ⇑f _ c)) _ _ _
+    (comapQuotientEquivOfSurj c f f.surjective)) ⟦f x⟧) = ↑x :=
   (MulEquiv.symm_apply_eq (@comapQuotientEquivOfSurj M N _ _ c f _)).mpr rfl
 
 /-- The **second isomorphism theorem for monoids**. -/