perf: improve some instances in GroupTheory/Congruence (#6874)

ChrisHughes24 · ChrisHughes24 · commit 701760004fa3 · 2023-09-29T10:41:02.000Z
diff --git a/Mathlib/GroupTheory/Congruence.lean b/Mathlib/GroupTheory/Congruence.lean
@@ -732,10 +732,8 @@ variable [MulOneClass M] [MulOneClass N] [MulOneClass P] (c : Con M)
 /-- The quotient of a monoid by a congruence relation is a monoid. -/
 @[to_additive "The quotient of an `AddMonoid` by an additive congruence relation is
 an `AddMonoid`."]
-instance mulOneClass : MulOneClass c.Quotient
-    where
+instance mulOneClass : MulOneClass c.Quotient where
   one := ((1 : M) : c.Quotient)
-  mul := (· * ·)
   mul_one x := Quotient.inductionOn' x fun _ => congr_arg ((↑) : M → c.Quotient) <| mul_one _
   one_mul x := Quotient.inductionOn' x fun _ => congr_arg ((↑) : M → c.Quotient) <| one_mul _
 #align con.mul_one_class Con.mulOneClass
@@ -1148,7 +1146,7 @@ protected theorem pow {M : Type*} [Monoid M] (c : Con M) :
 #align add_con.nsmul AddCon.nsmul
 
 @[to_additive]
-instance [MulOneClass M] (c : Con M) : One c.Quotient where
+instance one [MulOneClass M] (c : Con M) : One c.Quotient where
   -- Using Quotient.mk'' here instead of c.toQuotient
   -- since c.toQuotient is not reducible.
   -- This would lead to non-defeq diamonds since this instance ends up in
@@ -1176,32 +1174,52 @@ instance {M : Type*} [Monoid M] (c : Con M) : Pow c.Quotient ℕ where
 @[to_additive "The quotient of an `AddSemigroup` by an additive congruence relation is
 an `AddSemigroup`."]
 instance semigroup {M : Type*} [Semigroup M] (c : Con M) : Semigroup c.Quotient :=
-  Function.Surjective.semigroup _ Quotient.surjective_Quotient_mk'' fun _ _ => rfl
+  { (Function.Surjective.semigroup _ Quotient.surjective_Quotient_mk'' fun _ _ => rfl :
+      Semigroup c.Quotient) with
+    /- The `toMul` field is given explicitly for performance reasons.
+    This avoids any need to unfold `Function.Surjective.semigroup` when the type checker is checking
+    that instance diagrams commute -/
+    toMul := Con.hasMul _ }
 #align con.semigroup Con.semigroup
 #align add_con.add_semigroup AddCon.addSemigroup
 
 /-- The quotient of a commutative semigroup by a congruence relation is a semigroup. -/
 @[to_additive "The quotient of an `AddCommSemigroup` by an additive congruence relation is
 an `AddCommSemigroup`."]
 instance commSemigroup {M : Type*} [CommSemigroup M] (c : Con M) : CommSemigroup c.Quotient :=
-  Function.Surjective.commSemigroup _ Quotient.surjective_Quotient_mk'' fun _ _ => rfl
+  { (Function.Surjective.commSemigroup _ Quotient.surjective_Quotient_mk'' fun _ _ => rfl :
+      CommSemigroup c.Quotient) with
+    /- The `toSemigroup` field is given explicitly for performance reasons.
+    This avoids any need to unfold `Function.Surjective.commSemigroup` when the type checker is
+    checking that instance diagrams commute -/
+    toSemigroup := Con.semigroup _ }
 #align con.comm_semigroup Con.commSemigroup
 #align add_con.add_comm_semigroup AddCon.addCommSemigroup
 
 /-- The quotient of a monoid by a congruence relation is a monoid. -/
 @[to_additive "The quotient of an `AddMonoid` by an additive congruence relation is
 an `AddMonoid`."]
 instance monoid {M : Type*} [Monoid M] (c : Con M) : Monoid c.Quotient :=
-  Function.Surjective.monoid _ Quotient.surjective_Quotient_mk'' rfl (fun _ _ => rfl) fun _ _ => rfl
+  { (Function.Surjective.monoid _ Quotient.surjective_Quotient_mk'' rfl
+      (fun _ _ => rfl) fun _ _ => rfl : Monoid c.Quotient) with
+    /- The `toSemigroup` and `toOne` fields are given explicitly for performance reasons.
+    This avoids any need to unfold `Function.Surjective.monoid` when the type checker is
+    checking that instance diagrams commute -/
+    toSemigroup := Con.semigroup _
+    toOne := Con.one _ }
 #align con.monoid Con.monoid
 #align add_con.add_monoid AddCon.addMonoid
 
 /-- The quotient of a `CommMonoid` by a congruence relation is a `CommMonoid`. -/
 @[to_additive "The quotient of an `AddCommMonoid` by an additive congruence
 relation is an `AddCommMonoid`."]
 instance commMonoid {M : Type*} [CommMonoid M] (c : Con M) : CommMonoid c.Quotient :=
-  Function.Surjective.commMonoid _ Quotient.surjective_Quotient_mk'' rfl (fun _ _ => rfl) fun _ _ =>
-    rfl
+  { (Function.Surjective.commMonoid _ Quotient.surjective_Quotient_mk'' rfl
+      (fun _ _ => rfl) fun _ _ => rfl : CommMonoid c.Quotient) with
+    /- The `toMonoid` field is given explicitly for performance reasons.
+    This avoids any need to unfold `Function.Surjective.commMonoid` when the type checker is
+    checking that instance diagrams commute -/
+    toMonoid := Con.monoid _ }
 #align con.comm_monoid Con.commMonoid
 #align add_con.add_comm_monoid AddCon.addCommMonoid
 
@@ -1291,9 +1309,12 @@ instance zpowinst : Pow c.Quotient ℤ :=
 @[to_additive "The quotient of an `AddGroup` by an additive congruence relation is
 an `AddGroup`."]
 instance group : Group c.Quotient :=
-  Function.Surjective.group Quotient.mk''
-    Quotient.surjective_Quotient_mk'' rfl (fun _ _ => rfl) (fun _ => rfl)
-    (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl
+  { (Function.Surjective.group Quotient.mk''
+      Quotient.surjective_Quotient_mk'' rfl (fun _ _ => rfl) (fun _ => rfl)
+        (fun _ _ => rfl) (fun _ _ => rfl) fun _ _ => rfl : Group c.Quotient) with
+    toMonoid := Con.monoid _
+    toInv := Con.hasInv _
+    toDiv := Con.hasDiv _ }
 #align con.group Con.group
 #align add_con.add_group AddCon.addGroup
 
@@ -1371,18 +1392,15 @@ theorem coe_smul {α M : Type*} [MulOneClass M] [SMul α M] [IsScalarTower α M
 
 @[to_additive]
 instance mulAction {α M : Type*} [Monoid α] [MulOneClass M] [MulAction α M] [IsScalarTower α M M]
-    (c : Con M) : MulAction α c.Quotient
-    where
-  smul := (· • ·)
+    (c : Con M) : MulAction α c.Quotient where
   one_smul := Quotient.ind' fun _ => congr_arg Quotient.mk'' <| one_smul _ _
   mul_smul _ _ := Quotient.ind' fun _ => congr_arg Quotient.mk'' <| mul_smul _ _ _
 #align con.mul_action Con.mulAction
 #align add_con.add_action AddCon.addAction
 
 instance mulDistribMulAction {α M : Type*} [Monoid α] [Monoid M] [MulDistribMulAction α M]
     [IsScalarTower α M M] (c : Con M) : MulDistribMulAction α c.Quotient :=
-  { c.mulAction with
-    smul_one := fun _ => congr_arg Quotient.mk'' <| smul_one _
+  { smul_one := fun _ => congr_arg Quotient.mk'' <| smul_one _
     smul_mul := fun _ => Quotient.ind₂' fun _ _ => congr_arg Quotient.mk'' <| smul_mul' _ _ _ }
 #align con.mul_distrib_mul_action Con.mulDistribMulAction
 
