removing HasMul

leanprover-community · Oct 23, 2024 · c336c4f · c336c4f
1 parent 5455d64
commit c336c4f
Showing 1 changed file with 2 additions and 3 deletions.
diff --git 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**. -/