perf: remove overspecified fields (#6965)

This removes redundant field values of the form `add := add` for smaller terms and less unfolding during unification. 

A list of all files containing a structure instance of the form `{ a1, ... with x1 := val, ... }` where some `xi` is a field of some `aj` was generated by modifying the structure instance elaboration algorithm to print such overlaps to stdout in a custom toolchain. 

Using that toolchain, I went through each file on the list and attempted to remove algebraic fields that overlapped and were redundant, eg `add := add` and not `toFun` (though some other ones did creep in). If things broke (which was the case in a couple of cases), I did not push further and reverted. 

It is possible that pushing harder and trying to remove all redundant overlaps will yield further improvements.

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -448,7 +448,7 @@ def HomEquiv.toRestriction {X Y} (g : Y ⟶ (coextendScalars f).obj X) : (restri
     -- Porting note: should probably change CoeFun for obj above
     rw [← LinearMap.coe_toAddHom, ←AddHom.toFun_eq_coe]
     rw [CoextendScalars.smul_apply (s := f r) (g := g y) (s' := 1), one_mul]
-    rw [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]
+    simp
 #align category_theory.Module.restriction_coextension_adj.hom_equiv.to_restriction ModuleCat.RestrictionCoextensionAdj.HomEquiv.toRestriction
 
 -- Porting note: add to address timeout in unit'
@@ -459,7 +459,8 @@ def app' (Y : ModuleCat S) : Y →ₗ[S] (restrictScalars f ⋙ coextendScalars
         map_add' := fun s s' => add_smul _ _ _
         map_smul' := fun r (s : S) => by
           dsimp
-          erw [smul_eq_mul, mul_smul] }
+          erw [smul_eq_mul, mul_smul]
+          simp }
     map_add' := fun y1 y2 =>
       LinearMap.ext fun s : S => by
         -- Porting note: double dsimp seems odd

Mathlib/Algebra/DirectSum/Ring.lean

@@ -345,10 +345,6 @@ private theorem mul_comm (a b : ⨁ i, A i) : a * b = b * a := by
 /-- The `CommSemiring` structure derived from `GCommSemiring A`. -/
 instance commSemiring : CommSemiring (⨁ i, A i) :=
   { DirectSum.semiring A with
-    one := 1
-    mul := (· * ·)
-    zero := 0
-    add := (· + ·)
     mul_comm := mul_comm A }
 #align direct_sum.comm_semiring DirectSum.commSemiring
 
@@ -361,11 +357,7 @@ variable [∀ i, AddCommGroup (A i)] [Add ι] [GNonUnitalNonAssocSemiring A]
 /-- The `Ring` derived from `GSemiring A`. -/
 instance nonAssocRing : NonUnitalNonAssocRing (⨁ i, A i) :=
   { (inferInstance : NonUnitalNonAssocSemiring (⨁ i, A i)),
-    (inferInstance : AddCommGroup (⨁ i, A i)) with
-    mul := (· * ·)
-    zero := 0
-    add := (· + ·)
-    neg := Neg.neg }
+    (inferInstance : AddCommGroup (⨁ i, A i)) with }
 #align direct_sum.non_assoc_ring DirectSum.nonAssocRing
 
 end NonUnitalNonAssocRing
@@ -394,12 +386,7 @@ variable [∀ i, AddCommGroup (A i)] [AddCommMonoid ι] [GCommRing A]
 /-- The `CommRing` derived from `GCommSemiring A`. -/
 instance commRing : CommRing (⨁ i, A i) :=
   { DirectSum.ring A,
-    DirectSum.commSemiring A with
-    one := 1
-    mul := (· * ·)
-    zero := 0
-    add := (· + ·)
-    neg := Neg.neg }
+    DirectSum.commSemiring A with }
 #align direct_sum.comm_ring DirectSum.commRing
 
 end CommRing

Mathlib/Algebra/EuclideanDomain/Instances.lean

@@ -22,8 +22,6 @@ import Mathlib.Data.Int.Order.Basic
 
 instance Int.euclideanDomain : EuclideanDomain ℤ :=
   { inferInstanceAs (CommRing Int), inferInstanceAs (Nontrivial Int) with
-    add := (· + ·), mul := (· * ·), one := 1, zero := 0,
-    neg := Neg.neg,
     quotient := (· / ·), quotient_zero := Int.ediv_zero, remainder := (· % ·),
     quotient_mul_add_remainder_eq := Int.ediv_add_emod,
     r := fun a b => a.natAbs < b.natAbs,

Mathlib/Algebra/Group/InjSurj.lean

@@ -66,7 +66,6 @@ semigroup, if it admits an injective map that preserves `+` to an additive left
 protected def leftCancelSemigroup [LeftCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f)
     (mul : ∀ x y, f (x * y) = f x * f y) : LeftCancelSemigroup M₁ :=
   { hf.semigroup f mul with
-    mul := (· * ·),
     mul_left_cancel := fun x y z H => hf <| (mul_right_inj (f x)).1 <| by erw [← mul, ← mul, H] }
 #align function.injective.left_cancel_semigroup Function.Injective.leftCancelSemigroup
 #align function.injective.add_left_cancel_semigroup Function.Injective.addLeftCancelSemigroup
@@ -79,7 +78,6 @@ semigroup."]
 protected def rightCancelSemigroup [RightCancelSemigroup M₂] (f : M₁ → M₂) (hf : Injective f)
     (mul : ∀ x y, f (x * y) = f x * f y) : RightCancelSemigroup M₁ :=
   { hf.semigroup f mul with
-    mul := (· * ·),
     mul_right_cancel := fun x y z H => hf <| (mul_left_inj (f y)).1 <| by erw [← mul, ← mul, H] }
 #align function.injective.right_cancel_semigroup Function.Injective.rightCancelSemigroup
 #align function.injective.add_right_cancel_semigroup Function.Injective.addRightCancelSemigroup

Mathlib/Algebra/Group/TypeTags.lean

@@ -257,39 +257,35 @@ instance Multiplicative.mulOneClass [AddZeroClass α] : MulOneClass (Multiplicat
 
 instance Additive.addMonoid [h : Monoid α] : AddMonoid (Additive α) :=
   { Additive.addZeroClass, Additive.addSemigroup with
-    zero := 0
-    add := (· + ·)
     nsmul := @Monoid.npow α h
     nsmul_zero := @Monoid.npow_zero α h
     nsmul_succ := @Monoid.npow_succ α h }
 
 instance Multiplicative.monoid [h : AddMonoid α] : Monoid (Multiplicative α) :=
   { Multiplicative.mulOneClass, Multiplicative.semigroup with
-    one := 1
-    mul := (· * ·)
     npow := @AddMonoid.nsmul α h
     npow_zero := @AddMonoid.nsmul_zero α h
     npow_succ := @AddMonoid.nsmul_succ α h }
 
 instance Additive.addLeftCancelMonoid [LeftCancelMonoid α] : AddLeftCancelMonoid (Additive α) :=
-  { Additive.addMonoid, Additive.addLeftCancelSemigroup with zero := 0, add := (· + ·) }
+  { Additive.addMonoid, Additive.addLeftCancelSemigroup with }
 
 instance Multiplicative.leftCancelMonoid [AddLeftCancelMonoid α] :
     LeftCancelMonoid (Multiplicative α) :=
-  { Multiplicative.monoid, Multiplicative.leftCancelSemigroup with one := 1, mul := (· * ·) }
+  { Multiplicative.monoid, Multiplicative.leftCancelSemigroup with }
 
 instance Additive.addRightCancelMonoid [RightCancelMonoid α] : AddRightCancelMonoid (Additive α) :=
-  { Additive.addMonoid, Additive.addRightCancelSemigroup with zero := 0, add := (· + ·) }
+  { Additive.addMonoid, Additive.addRightCancelSemigroup with }
 
 instance Multiplicative.rightCancelMonoid [AddRightCancelMonoid α] :
     RightCancelMonoid (Multiplicative α) :=
-  { Multiplicative.monoid, Multiplicative.rightCancelSemigroup with one := 1, mul := (· * ·) }
+  { Multiplicative.monoid, Multiplicative.rightCancelSemigroup with }
 
 instance Additive.addCommMonoid [CommMonoid α] : AddCommMonoid (Additive α) :=
-  { Additive.addMonoid, Additive.addCommSemigroup with zero := 0, add := (· + ·) }
+  { Additive.addMonoid, Additive.addCommSemigroup with }
 
 instance Multiplicative.commMonoid [AddCommMonoid α] : CommMonoid (Multiplicative α) :=
-  { Multiplicative.monoid, Multiplicative.commSemigroup with one := 1, mul := (· * ·) }
+  { Multiplicative.monoid, Multiplicative.commSemigroup with }
 
 instance Additive.neg [Inv α] : Neg (Additive α) :=
   ⟨fun x => ofAdd (toMul x)⁻¹⟩

Mathlib/Algebra/Group/Units.lean

@@ -198,7 +198,6 @@ instance : MulOneClass αˣ where
 @[to_additive "Additive units of an additive monoid form an additive group."]
 instance : Group αˣ :=
   { (inferInstance : MulOneClass αˣ) with
-    one := 1,
     mul_assoc := fun _ _ _ => ext <| mul_assoc _ _ _,
     inv := Inv.inv, mul_left_inv := fun u => ext u.inv_val }
 

Mathlib/Algebra/GroupRingAction/Basic.lean

@@ -82,7 +82,7 @@ variable {M N}
 See note [reducible non-instances]. -/
 @[reducible]
 def MulSemiringAction.compHom (f : N →* M) [MulSemiringAction M R] : MulSemiringAction N R :=
-  { DistribMulAction.compHom R f, MulDistribMulAction.compHom R f with smul := SMul.comp.smul f }
+  { DistribMulAction.compHom R f, MulDistribMulAction.compHom R f with }
 #align mul_semiring_action.comp_hom MulSemiringAction.compHom
 
 end

Mathlib/Algebra/GroupRingAction/Subobjects.lean

@@ -27,8 +27,7 @@ variable [Monoid M] [Group G] [Semiring R]
 /-- A stronger version of `Submonoid.distribMulAction`. -/
 instance Submonoid.mulSemiringAction [MulSemiringAction M R] (H : Submonoid M) :
     MulSemiringAction H R :=
-  { inferInstanceAs (DistribMulAction H R), inferInstanceAs (MulDistribMulAction H R)
-    with smul := (· • ·) }
+  { inferInstanceAs (DistribMulAction H R), inferInstanceAs (MulDistribMulAction H R) with }
 #align submonoid.mul_semiring_action Submonoid.mulSemiringAction
 
 /-- A stronger version of `Subgroup.distribMulAction`. -/

Mathlib/Algebra/Module/Basic.lean

@@ -156,7 +156,6 @@ See note [reducible non-instances]. -/
 @[reducible]
 def Module.compHom [Semiring S] (f : S →+* R) : Module S M :=
   { MulActionWithZero.compHom M f.toMonoidWithZeroHom, DistribMulAction.compHom M (f : S →* R) with
-    smul := SMul.comp.smul f
     -- Porting note: the `show f (r + s) • x = f r • x + f s • x ` wasn't needed in mathlib3.
     -- Somehow, now that `SMul` is heterogeneous, it can't unfold earlier fields of a definition for
     -- use in later fields.  See

Mathlib/Algebra/Module/LinearMap.lean

@@ -158,7 +158,6 @@ variable {σ : R →+* S}
 instance (priority := 100) addMonoidHomClass [SemilinearMapClass F σ M M₃] :
     AddMonoidHomClass F M M₃ :=
   { SemilinearMapClass.toAddHomClass with
-    coe := fun f ↦ (f : M → M₃)
     map_zero := fun f ↦
       show f 0 = 0 by
         rw [← zero_smul R (0 : M), map_smulₛₗ]
@@ -167,7 +166,6 @@ instance (priority := 100) addMonoidHomClass [SemilinearMapClass F σ M M₃] :
 instance (priority := 100) distribMulActionHomClass [LinearMapClass F R M M₂] :
     DistribMulActionHomClass F R M M₂ :=
   { SemilinearMapClass.addMonoidHomClass F with
-    coe := fun f ↦ (f : M → M₂)
     map_smul := fun f c x ↦ by rw [map_smulₛₗ, RingHom.id_apply] }
 
 variable {F} (f : F) [i : SemilinearMapClass F σ M M₃]
@@ -263,7 +261,7 @@ theorem coe_addHom_mk {σ : R →+* S} (f : AddHom M M₃) (h) :
 
 /-- Identity map as a `LinearMap` -/
 def id : M →ₗ[R] M :=
-  { DistribMulActionHom.id R with toFun := _root_.id }
+  { DistribMulActionHom.id R with }
 #align linear_map.id LinearMap.id
 
 theorem id_apply (x : M) : @id R M _ _ _ x = x :=
@@ -521,7 +519,6 @@ end
 @[simps]
 def _root_.RingHom.toSemilinearMap (f : R →+* S) : R →ₛₗ[f] S :=
   { f with
-    toFun := f
     map_smul' := f.map_mul }
 #align ring_hom.to_semilinear_map RingHom.toSemilinearMap
 #align ring_hom.to_semilinear_map_apply RingHom.toSemilinearMap_apply
@@ -1064,10 +1061,6 @@ instance _root_.Module.End.monoid : Monoid (Module.End R M) where
 
 instance _root_.Module.End.semiring : Semiring (Module.End R M) :=
   { AddMonoidWithOne.unary, Module.End.monoid, LinearMap.addCommMonoid with
-    mul := (· * ·)
-    one := (1 : M →ₗ[R] M)
-    zero := (0 : M →ₗ[R] M)
-    add := (· + ·)
     mul_zero := comp_zero
     zero_mul := zero_comp
     left_distrib := fun _ _ _ ↦ comp_add _ _ _
@@ -1085,10 +1078,6 @@ theorem _root_.Module.End.natCast_apply (n : ℕ) (m : M) : (↑n : Module.End R
 
 instance _root_.Module.End.ring : Ring (Module.End R N₁) :=
   { Module.End.semiring, LinearMap.addCommGroup with
-    mul := (· * ·)
-    one := (1 : N₁ →ₗ[R] N₁)
-    zero := (0 : N₁ →ₗ[R] N₁)
-    add := (· + ·)
     intCast := fun z ↦ z • (1 : N₁ →ₗ[R] N₁)
     intCast_ofNat := ofNat_zsmul _
     intCast_negSucc := negSucc_zsmul _ }

Mathlib/Algebra/Module/Submodule/Basic.lean

@@ -344,14 +344,11 @@ theorem coe_mem (x : p) : (x : M) ∈ p :=
 variable (p)
 
 instance addCommMonoid : AddCommMonoid p :=
-  { p.toAddSubmonoid.toAddCommMonoid with
-    add := (· + ·)
-    zero := 0 }
+  { p.toAddSubmonoid.toAddCommMonoid with }
 #align submodule.add_comm_monoid Submodule.addCommMonoid
 
 instance module' [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] : Module S p :=
   { (show MulAction S p from p.toSubMulAction.mulAction') with
-    smul := (· • ·)
     smul_zero := fun a => by ext; simp
     zero_smul := fun a => by ext; simp
     add_smul := fun a b x => by ext; simp [add_smul]
@@ -493,8 +490,6 @@ as turning it into a type and adding a module structure. -/
 @[simps (config := { simpRhs := true })]
 def restrictScalarsEquiv (p : Submodule R M) : p.restrictScalars S ≃ₗ[R] p :=
   { AddEquiv.refl p with
-    toFun := id
-    invFun := id
     map_smul' := fun _ _ => rfl }
 #align submodule.restrict_scalars_equiv Submodule.restrictScalarsEquiv
 #align submodule.restrict_scalars_equiv_symm_apply Submodule.restrictScalarsEquiv_symm_apply
@@ -592,10 +587,7 @@ theorem sub_mem_iff_right (hx : x ∈ p) : x - y ∈ p ↔ y ∈ p := by
 #align submodule.sub_mem_iff_right Submodule.sub_mem_iff_right
 
 instance addCommGroup : AddCommGroup p :=
-  { p.toAddSubgroup.toAddCommGroup with
-    add := (· + ·)
-    zero := 0
-    neg := Neg.neg }
+  { p.toAddSubgroup.toAddCommGroup with }
 #align submodule.add_comm_group Submodule.addCommGroup
 
 end AddCommGroup

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -52,7 +52,6 @@ This is available as an instance in the `Pointwise` locale. -/
 protected def pointwiseNeg : Neg (Submodule R M) where
   neg p :=
     { -p.toAddSubmonoid with
-      carrier := -(p : Set M)
       smul_mem' := fun r m hm => Set.mem_neg.2 <| smul_neg r m ▸ p.smul_mem r <| Set.mem_neg.1 hm }
 #align submodule.has_pointwise_neg Submodule.pointwiseNeg
 
@@ -176,9 +175,6 @@ theorem zero_eq_bot : (0 : Submodule R M) = ⊥ :=
 instance : CanonicallyOrderedAddMonoid (Submodule R M) :=
   { Submodule.pointwiseAddCommMonoid,
     Submodule.completeLattice with
-    zero := 0
-    bot := ⊥
-    add := (· + ·)
     add_le_add_left := fun _a _b => sup_le_sup_left
     exists_add_of_le := @fun _a b h => ⟨b, (sup_eq_right.2 h).symm⟩
     le_self_add := fun _a _b => le_sup_left }