chore: replace anonymous morphism constructors with named fields (#7015)

eric-wieser · eric-wieser · commit 2bffb702994d · 2023-09-12T12:40:23.000Z
This makes it easier to refactor the order or inheritance structure of morphisms without having to change all of the anonymous constructors.

This is far from exhaustive.
diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean
@@ -491,9 +491,7 @@ end CategoryTheory.Aut
 instance GroupCat.forget_reflects_isos : ReflectsIsomorphisms (forget GroupCat.{u}) where
   reflects {X Y} f _ := by
     let i := asIso ((forget GroupCat).map f)
-    let e : X ≃* Y := MulEquiv.mk i.toEquiv
-      -- Porting note: this would ideally be `by aesop`, as in `MonCat.forget_reflects_isos`
-      (MonoidHom.map_mul (show MonoidHom X Y from f))
+    let e : X ≃* Y := { i.toEquiv with map_mul' := by aesop }
     exact IsIso.of_iso e.toGroupCatIso
 set_option linter.uppercaseLean3 false in
 #align Group.forget_reflects_isos GroupCat.forget_reflects_isos
@@ -504,9 +502,7 @@ set_option linter.uppercaseLean3 false in
 instance CommGroupCat.forget_reflects_isos : ReflectsIsomorphisms (forget CommGroupCat.{u}) where
   reflects {X Y} f _ := by
     let i := asIso ((forget CommGroupCat).map f)
-    let e : X ≃* Y := MulEquiv.mk i.toEquiv
-      -- Porting note: this would ideally be `by aesop`, as in `MonCat.forget_reflects_isos`
-      (MonoidHom.map_mul (show MonoidHom X Y from f))
+    let e : X ≃* Y := { i.toEquiv with map_mul' := by aesop }
     exact IsIso.of_iso e.toCommGroupCatIso
 set_option linter.uppercaseLean3 false in
 #align CommGroup.forget_reflects_isos CommGroupCat.forget_reflects_isos
diff --git a/Mathlib/Algebra/Category/MonCat/Limits.lean b/Mathlib/Algebra/Category/MonCat/Limits.lean
@@ -103,7 +103,7 @@ noncomputable def limitCone (F : J ⥤ MonCatMax.{u,v}) : Cone F :=
 @[to_additive "(Internal use only; use the limits API.)"]
 noncomputable def limitConeIsLimit (F : J ⥤ MonCatMax.{u,v}) : IsLimit (limitCone F) := by
   refine IsLimit.ofFaithful (forget MonCatMax) (Types.limitConeIsLimit.{v,u} _)
-    (fun s => ⟨⟨_, ?_⟩, ?_⟩) (fun s => rfl) <;>
+    (fun s => { toFun := _, map_one' := ?_, map_mul' := ?_ }) (fun s => rfl) <;>
   aesop_cat
 #align Mon.has_limits.limit_cone_is_limit MonCat.HasLimits.limitConeIsLimit
 #align AddMon.has_limits.limit_cone_is_limit AddMonCat.HasLimits.limitConeIsLimit
diff --git a/Mathlib/Algebra/Category/Ring/Limits.lean b/Mathlib/Algebra/Category/Ring/Limits.lean
@@ -99,10 +99,12 @@ set_option linter.uppercaseLean3 false in
 -/
 def limitConeIsLimit (F : J ⥤ SemiRingCatMax.{v, u}) : IsLimit (limitCone F) := by
   refine IsLimit.ofFaithful (forget SemiRingCatMax.{v, u}) (Types.limitConeIsLimit.{v, u} _)
-    (fun s : Cone F => ofHom ⟨⟨⟨_, Subtype.ext <| funext fun j => by exact (s.π.app j).map_one⟩,
-      fun x y => Subtype.ext <| funext fun j => by exact (s.π.app j).map_mul x y⟩,
-      Subtype.ext <| funext fun j => by exact (s.π.app j).map_zero,
-      fun x y => Subtype.ext <| funext fun j => by exact (s.π.app j).map_add x y⟩)
+    (fun s : Cone F => ofHom
+      { toFun := _
+        map_one' := Subtype.ext <| funext fun j => by exact (s.π.app j).map_one
+        map_mul' := fun x y => Subtype.ext <| funext fun j => by exact (s.π.app j).map_mul x y
+        map_zero' := Subtype.ext <| funext fun j => by exact (s.π.app j).map_zero
+        map_add' := fun x y => Subtype.ext <| funext fun j => by exact (s.π.app j).map_add x y })
     fun s => rfl
 set_option linter.uppercaseLean3 false in
 #align SemiRing.has_limits.limit_cone_is_limit SemiRingCat.HasLimits.limitConeIsLimit
@@ -245,10 +247,12 @@ instance (F : J ⥤ CommSemiRingCatMax.{v, u}) :
         refine IsLimit.ofFaithful (forget₂ CommSemiRingCatMax.{v, u} SemiRingCatMax.{v, u})
           (SemiRingCat.HasLimits.limitConeIsLimit.{v, u} _)
           (fun s : Cone F => CommSemiRingCat.ofHom
-            ⟨⟨⟨_, Subtype.ext <| funext fun j => by exact (s.π.app j).map_one⟩,
-            fun x y => Subtype.ext <| funext fun j => by exact (s.π.app j).map_mul x y⟩,
-            Subtype.ext <| funext fun j => by exact (s.π.app j).map_zero,
-            fun x y => Subtype.ext <| funext fun j => by exact (s.π.app j).map_add x y⟩)
+            { toFun := _
+              map_one' := Subtype.ext <| funext fun j => by exact (s.π.app j).map_one
+              map_mul' := fun x y => Subtype.ext <| funext fun j => by exact (s.π.app j).map_mul x y
+              map_zero' := Subtype.ext <| funext fun j => by exact (s.π.app j).map_zero
+              map_add' := fun x y => Subtype.ext <| funext fun j => by exact (s.π.app j).map_add x y
+              })
           fun s => rfl }
 
 /-- A choice of limit cone for a functor into `CommSemiRingCat`.
diff --git a/Mathlib/Algebra/Free.lean b/Mathlib/Algebra/Free.lean
@@ -373,7 +373,7 @@ instance : Semigroup (AssocQuotient α) where
 
 /-- Embedding from magma to its free semigroup. -/
 @[to_additive "Embedding from additive magma to its free additive semigroup."]
-def of : α →ₙ* AssocQuotient α := ⟨Quot.mk _, fun _x _y ↦ rfl⟩
+def of : α →ₙ* AssocQuotient α where toFun := Quot.mk _; map_mul' _x _y := rfl
 #align magma.assoc_quotient.of Magma.AssocQuotient.of
 
 @[to_additive]
diff --git a/Mathlib/Algebra/Hom/Units.lean b/Mathlib/Algebra/Hom/Units.lean
@@ -102,8 +102,8 @@ theorem map_id : map (MonoidHom.id M) = MonoidHom.id Mˣ := by ext; rfl
 
 /-- Coercion `Mˣ → M` as a monoid homomorphism. -/
 @[to_additive "Coercion `AddUnits M → M` as an AddMonoid homomorphism."]
-def coeHom : Mˣ →* M :=
-  ⟨⟨Units.val, val_one⟩, val_mul⟩
+def coeHom : Mˣ →* M where
+  toFun := Units.val; map_one' := val_one; map_mul' := val_mul
 #align units.coe_hom Units.coeHom
 #align add_units.coe_hom AddUnits.coeHom
 
diff --git a/Mathlib/Algebra/Lie/Basic.lean b/Mathlib/Algebra/Lie/Basic.lean
@@ -187,22 +187,30 @@ theorem lie_sub : ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆ := by simp [sub_eq_ad
 
 @[simp]
 theorem nsmul_lie (n : ℕ) : ⁅n • x, m⁆ = n • ⁅x, m⁆ :=
-  AddMonoidHom.map_nsmul ⟨⟨fun x : L => ⁅x, m⁆, zero_lie m⟩, fun _ _ => add_lie _ _ _⟩ _ _
+  AddMonoidHom.map_nsmul
+    { toFun := fun x : L => ⁅x, m⁆, map_zero' := zero_lie m, map_add' := fun _ _ => add_lie _ _ _ }
+    _ _
 #align nsmul_lie nsmul_lie
 
 @[simp]
 theorem lie_nsmul (n : ℕ) : ⁅x, n • m⁆ = n • ⁅x, m⁆ :=
-  AddMonoidHom.map_nsmul ⟨⟨fun m : M => ⁅x, m⁆, lie_zero x⟩, fun _ _ => lie_add _ _ _⟩ _ _
+  AddMonoidHom.map_nsmul
+    { toFun := fun m : M => ⁅x, m⁆, map_zero' := lie_zero x, map_add' := fun _ _ => lie_add _ _ _}
+    _ _
 #align lie_nsmul lie_nsmul
 
 @[simp]
 theorem zsmul_lie (a : ℤ) : ⁅a • x, m⁆ = a • ⁅x, m⁆ :=
-  AddMonoidHom.map_zsmul ⟨⟨fun x : L => ⁅x, m⁆, zero_lie m⟩, fun _ _ => add_lie _ _ _⟩ _ _
+  AddMonoidHom.map_zsmul
+    { toFun := fun x : L => ⁅x, m⁆, map_zero' := zero_lie m, map_add' := fun _ _ => add_lie _ _ _ }
+    _ _
 #align zsmul_lie zsmul_lie
 
 @[simp]
 theorem lie_zsmul (a : ℤ) : ⁅x, a • m⁆ = a • ⁅x, m⁆ :=
-  AddMonoidHom.map_zsmul ⟨⟨fun m : M => ⁅x, m⁆, lie_zero x⟩, fun _ _ => lie_add _ _ _⟩ _ _
+  AddMonoidHom.map_zsmul
+    { toFun := fun m : M => ⁅x, m⁆, map_zero' := lie_zero x, map_add' := fun _ _ => lie_add _ _ _ }
+    _ _
 #align lie_zsmul lie_zsmul
 
 @[simp]
@@ -935,7 +943,9 @@ theorem smul_apply (t : R) (f : M →ₗ⁅R,L⁆ N) (m : M) : (t • f) m = t 
 #align lie_module_hom.smul_apply LieModuleHom.smul_apply
 
 instance : Module R (M →ₗ⁅R,L⁆ N) :=
-  Function.Injective.module R ⟨⟨fun f => f.toLinearMap.toFun, rfl⟩, coe_add⟩ coe_injective coe_smul
+  Function.Injective.module R
+    { toFun := fun f => f.toLinearMap.toFun, map_zero' := rfl, map_add' := coe_add }
+    coe_injective coe_smul
 
 end LieModuleHom
 
diff --git a/Mathlib/Algebra/Order/AbsoluteValue.lean b/Mathlib/Algebra/Order/AbsoluteValue.lean
@@ -460,8 +460,8 @@ theorem abv_one' : abv 1 = 1 :=
 #align is_absolute_value.abv_one' IsAbsoluteValue.abv_one'
 
 /-- An absolute value as a monoid with zero homomorphism, assuming the target is a semifield. -/
-def abvHom' : R →*₀ S :=
-  ⟨⟨abv, abv_zero abv⟩, abv_one' abv, abv_mul abv⟩
+def abvHom' : R →*₀ S where
+  toFun := abv; map_zero' := abv_zero abv; map_one' := abv_one' abv; map_mul' := abv_mul abv
 #align is_absolute_value.abv_hom' IsAbsoluteValue.abvHom'
 
 end Semiring
diff --git a/Mathlib/Algebra/Order/Interval.lean b/Mathlib/Algebra/Order/Interval.lean
@@ -305,7 +305,8 @@ namespace NonemptyInterval
 @[to_additive]
 theorem coe_pow_interval [OrderedCommMonoid α] (s : NonemptyInterval α) (n : ℕ) :
     (s ^ n : Interval α) = (s : Interval α) ^ n :=
-  map_pow (⟨⟨(↑), coe_one_interval⟩, coe_mul_interval⟩ : NonemptyInterval α →* Interval α) _ _
+  map_pow ({ toFun := (↑), map_one' := coe_one_interval, map_mul' := coe_mul_interval }
+    : NonemptyInterval α →* Interval α) _ _
 #align nonempty_interval.coe_pow_interval NonemptyInterval.coe_pow_interval
 #align nonempty_interval.coe_nsmul_interval NonemptyInterval.coe_nsmul_interval
 
@@ -666,7 +667,8 @@ theorem length_sub : (s - t).length = s.length + t.length := by simp [sub_eq_add
 @[simp]
 theorem length_sum (f : ι → NonemptyInterval α) (s : Finset ι) :
     (∑ i in s, f i).length = ∑ i in s, (f i).length :=
-  map_sum (⟨⟨length, length_zero⟩, length_add⟩ : NonemptyInterval α →+ α) _ _
+  map_sum ({ toFun := length, map_zero' := length_zero, map_add' := length_add}
+    : NonemptyInterval α →+ α) _ _
 #align nonempty_interval.length_sum NonemptyInterval.length_sum
 
 end NonemptyInterval
diff --git a/Mathlib/Algebra/Ring/Basic.lean b/Mathlib/Algebra/Ring/Basic.lean
@@ -30,15 +30,17 @@ namespace AddHom
 
 /-- Left multiplication by an element of a type with distributive multiplication is an `AddHom`. -/
 @[simps (config := { fullyApplied := false })]
-def mulLeft [Distrib R] (r : R) : AddHom R R :=
-  ⟨(· * ·) r, mul_add r⟩
+def mulLeft [Distrib R] (r : R) : AddHom R R where
+  toFun := (· * ·) r
+  map_add' := mul_add r
 #align add_hom.mul_left AddHom.mulLeft
 #align add_hom.mul_left_apply AddHom.mulLeft_apply
 
 /-- Left multiplication by an element of a type with distributive multiplication is an `AddHom`. -/
 @[simps (config := { fullyApplied := false })]
-def mulRight [Distrib R] (r : R) : AddHom R R :=
-  ⟨fun a => a * r, fun _ _ => add_mul _ _ r⟩
+def mulRight [Distrib R] (r : R) : AddHom R R where
+  toFun a := a * r
+  map_add' _ _ := add_mul _ _ r
 #align add_hom.mul_right AddHom.mulRight
 #align add_hom.mul_right_apply AddHom.mulRight_apply
 
diff --git a/Mathlib/Data/Finset/Pointwise.lean b/Mathlib/Data/Finset/Pointwise.lean
@@ -146,8 +146,8 @@ theorem card_one : (1 : Finset α).card = 1 :=
 
 /-- The singleton operation as a `OneHom`. -/
 @[to_additive "The singleton operation as a `ZeroHom`."]
-def singletonOneHom : OneHom α (Finset α) :=
-  ⟨singleton, singleton_one⟩
+def singletonOneHom : OneHom α (Finset α) where
+  toFun := singleton; map_one' := singleton_one
 #align finset.singleton_one_hom Finset.singletonOneHom
 #align finset.singleton_zero_hom Finset.singletonZeroHom
 
@@ -487,8 +487,8 @@ theorem image_mul : (s * t).image (f : α → β) = s.image f * t.image f :=
 
 /-- The singleton operation as a `MulHom`. -/
 @[to_additive "The singleton operation as an `AddHom`."]
-def singletonMulHom : α →ₙ* Finset α :=
-  ⟨singleton, fun _ _ => (singleton_mul_singleton _ _).symm⟩
+def singletonMulHom : α →ₙ* Finset α where
+  toFun := singleton; map_mul' _ _ := (singleton_mul_singleton _ _).symm
 #align finset.singleton_mul_hom Finset.singletonMulHom
 #align finset.singleton_add_hom Finset.singletonAddHom
 
@@ -1776,13 +1776,13 @@ scoped[Pointwise]
 multiplicative action on `Finset β`. -/
 protected def distribMulActionFinset [Monoid α] [AddMonoid β] [DistribMulAction α β] :
     DistribMulAction α (Finset β) :=
-  Function.Injective.distribMulAction ⟨⟨(↑), coe_zero⟩, coe_add⟩ coe_injective coe_smul_finset
+  Function.Injective.distribMulAction coeAddMonoidHom coe_injective coe_smul_finset
 #align finset.distrib_mul_action_finset Finset.distribMulActionFinset
 
 /-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `Set β`. -/
 protected def mulDistribMulActionFinset [Monoid α] [Monoid β] [MulDistribMulAction α β] :
     MulDistribMulAction α (Finset β) :=
-  Function.Injective.mulDistribMulAction ⟨⟨(↑), coe_one⟩, coe_mul⟩ coe_injective coe_smul_finset
+  Function.Injective.mulDistribMulAction coeMonoidHom coe_injective coe_smul_finset
 #align finset.mul_distrib_mul_action_finset Finset.mulDistribMulActionFinset
 
 scoped[Pointwise]
diff --git a/Mathlib/Data/Set/Pointwise/Basic.lean b/Mathlib/Data/Set/Pointwise/Basic.lean
@@ -140,8 +140,8 @@ theorem Nonempty.subset_one_iff (h : s.Nonempty) : s ⊆ 1 ↔ s = 1 :=
 
 /-- The singleton operation as a `OneHom`. -/
 @[to_additive "The singleton operation as a `ZeroHom`."]
-noncomputable def singletonOneHom : OneHom α (Set α) :=
-  ⟨singleton, singleton_one⟩
+noncomputable def singletonOneHom : OneHom α (Set α) where
+  toFun := singleton; map_one' := singleton_one
 #align set.singleton_one_hom Set.singletonOneHom
 #align set.singleton_zero_hom Set.singletonZeroHom
 
@@ -546,8 +546,9 @@ theorem mul_iInter₂_subset (s : Set α) (t : ∀ i, κ i → Set α) :
 
 /-- The singleton operation as a `MulHom`. -/
 @[to_additive "The singleton operation as an `AddHom`."]
-noncomputable def singletonMulHom : α →ₙ* Set α :=
-  ⟨singleton, fun _ _ => singleton_mul_singleton.symm⟩
+noncomputable def singletonMulHom : α →ₙ* Set α where
+  toFun := singleton
+  map_mul' _ _ := singleton_mul_singleton.symm
 #align set.singleton_mul_hom Set.singletonMulHom
 #align set.singleton_add_hom Set.singletonAddHom
 
diff --git a/Mathlib/GroupTheory/GroupAction/Quotient.lean b/Mathlib/GroupTheory/GroupAction/Quotient.lean
@@ -130,8 +130,8 @@ end QuotientAction
 open QuotientGroup
 
 /-- The canonical map to the left cosets. -/
-def _root_.MulActionHom.toQuotient (H : Subgroup α) : α →[α] α ⧸ H :=
-  ⟨(↑), Quotient.smul_coe H⟩
+def _root_.MulActionHom.toQuotient (H : Subgroup α) : α →[α] α ⧸ H where
+  toFun := (↑); map_smul' := Quotient.smul_coe H
 #align mul_action_hom.to_quotient MulActionHom.toQuotient
 
 @[simp]
diff --git a/Mathlib/GroupTheory/GroupAction/SubMulAction.lean b/Mathlib/GroupTheory/GroupAction/SubMulAction.lean
@@ -242,8 +242,8 @@ instance (priority := 75) toMulAction : MulAction R S' :=
 #align sub_mul_action.smul_mem_class.to_mul_action SubMulAction.SMulMemClass.toMulAction
 
 /-- The natural `MulActionHom` over `R` from a `SubMulAction` of `M` to `M`. -/
-protected def subtype : S' →[R] M :=
-  ⟨Subtype.val, fun _ _ => rfl⟩
+protected def subtype : S' →[R] M where
+  toFun := Subtype.val; map_smul' _ _ := rfl
 #align sub_mul_action.smul_mem_class.subtype SubMulAction.SMulMemClass.subtype
 
 @[simp]
diff --git a/Mathlib/GroupTheory/Perm/Basic.lean b/Mathlib/GroupTheory/Perm/Basic.lean
@@ -630,7 +630,8 @@ variable [AddGroup α] (a b : α)
 #align equiv.pow_add_right Equiv.pow_addRight
 
 @[simp] lemma zpow_addLeft (n : ℤ) : Equiv.addLeft a ^ n = Equiv.addLeft (n • a) :=
-  (map_zsmul (⟨⟨Equiv.addLeft, addLeft_zero⟩, addLeft_add⟩ : α →+ Additive (Perm α)) _ _).symm
+  (map_zsmul ({ toFun := Equiv.addLeft, map_zero' := addLeft_zero, map_add' := addLeft_add }
+    : α →+ Additive (Perm α)) _ _).symm
 #align equiv.zpow_add_left Equiv.zpow_addLeft
 
 @[simp] lemma zpow_addRight : ∀ (n : ℤ), Equiv.addRight a ^ n = Equiv.addRight (n • a)
@@ -681,7 +682,8 @@ lemma pow_mulRight (n : ℕ) : Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n) :=
 
 @[to_additive existing (attr := simp) zpow_addLeft]
 lemma zpow_mulLeft (n : ℤ) : Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n) :=
-  (map_zpow (⟨⟨Equiv.mulLeft, mulLeft_one⟩, mulLeft_mul⟩ : α →* Perm α) _ _).symm
+  (map_zpow ({ toFun := Equiv.mulLeft, map_one' := mulLeft_one, map_mul' := mulLeft_mul }
+    : α →* Perm α) _ _).symm
 #align equiv.zpow_mul_left Equiv.zpow_mulLeft
 
 @[to_additive existing (attr := simp) zpow_addRight]
diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean
@@ -279,8 +279,8 @@ instance (priority := 75) toLinearOrderedCommGroup {G : Type*} [LinearOrderedCom
 /-- The natural group hom from a subgroup of group `G` to `G`. -/
 @[to_additive (attr := coe)
   "The natural group hom from an additive subgroup of `AddGroup` `G` to `G`."]
-protected def subtype : H →* G :=
-  ⟨⟨((↑) : H → G), rfl⟩, fun _ _ => rfl⟩
+protected def subtype : H →* G where
+  toFun := ((↑) : H → G); map_one' := rfl; map_mul' := fun _ _ => rfl
 #align subgroup_class.subtype SubgroupClass.subtype
 #align add_subgroup_class.subtype AddSubgroupClass.subtype
 
@@ -783,8 +783,8 @@ instance toLinearOrderedCommGroup {G : Type*} [LinearOrderedCommGroup G] (H : Su
 
 /-- The natural group hom from a subgroup of group `G` to `G`. -/
 @[to_additive "The natural group hom from an `AddSubgroup` of `AddGroup` `G` to `G`."]
-protected def subtype : H →* G :=
-  ⟨⟨((↑) : H → G), rfl⟩, fun _ _ => rfl⟩
+protected def subtype : H →* G where
+  toFun := ((↑) : H → G); map_one' := rfl; map_mul' _ _ := rfl
 #align subgroup.subtype Subgroup.subtype
 #align add_subgroup.subtype AddSubgroup.subtype
 
diff --git a/Mathlib/GroupTheory/Submonoid/Operations.lean b/Mathlib/GroupTheory/Submonoid/Operations.lean
@@ -645,8 +645,8 @@ instance (priority := 75) toLinearOrderedCancelCommMonoid {M} [LinearOrderedCanc
 
 /-- The natural monoid hom from a submonoid of monoid `M` to `M`. -/
 @[to_additive "The natural monoid hom from an `AddSubmonoid` of `AddMonoid` `M` to `M`."]
-def subtype : S' →* M :=
-  ⟨(⟨Subtype.val, rfl⟩ : OneHom S' M), by simp⟩
+def subtype : S' →* M where
+  toFun := Subtype.val; map_one' := rfl; map_mul' _ _ := by simp
 #align submonoid_class.subtype SubmonoidClass.subtype
 #align add_submonoid_class.subtype AddSubmonoidClass.subtype
 
@@ -778,8 +778,8 @@ instance toLinearOrderedCancelCommMonoid {M} [LinearOrderedCancelCommMonoid M] (
 
 /-- The natural monoid hom from a submonoid of monoid `M` to `M`. -/
 @[to_additive "The natural monoid hom from an `AddSubmonoid` of `AddMonoid` `M` to `M`."]
-def subtype : S →* M :=
-  ⟨(⟨Subtype.val, rfl⟩ : OneHom S M), by simp⟩
+def subtype : S →* M where
+  toFun := Subtype.val; map_one' := rfl; map_mul' _ _ := by simp
 #align submonoid.subtype Submonoid.subtype
 #align add_submonoid.subtype AddSubmonoid.subtype
 
diff --git a/Mathlib/GroupTheory/Subsemigroup/Operations.lean b/Mathlib/GroupTheory/Subsemigroup/Operations.lean
@@ -568,8 +568,8 @@ instance toCommSemigroup {M} [CommSemigroup M] {A : Type*} [SetLike A M] [MulMem
 /-- The natural semigroup hom from a subsemigroup of semigroup `M` to `M`. -/
 @[to_additive "The natural semigroup hom from an `AddSubsemigroup` of
 `AddSubsemigroup` `M` to `M`."]
-def subtype : S' →ₙ* M :=
-  ⟨Subtype.val, fun _ _ => rfl⟩
+def subtype : S' →ₙ* M where
+  toFun := Subtype.val; map_mul' := fun _ _ => rfl
 #align mul_mem_class.subtype MulMemClass.subtype
 #align add_mem_class.subtype AddMemClass.subtype
 
diff --git a/Mathlib/Order/Filter/Germ.lean b/Mathlib/Order/Filter/Germ.lean
@@ -419,8 +419,8 @@ instance monoid [Monoid M] : Monoid (Germ l M) :=
 
 /-- Coercion from functions to germs as a monoid homomorphism. -/
 @[to_additive "Coercion from functions to germs as an additive monoid homomorphism."]
-def coeMulHom [Monoid M] (l : Filter α) : (α → M) →* Germ l M :=
-  ⟨⟨ofFun, rfl⟩, fun _ _ => rfl⟩
+def coeMulHom [Monoid M] (l : Filter α) : (α → M) →* Germ l M where
+  toFun := ofFun; map_one' := rfl; map_mul' _ _ := rfl
 #align filter.germ.coe_mul_hom Filter.Germ.coeMulHom
 #align filter.germ.coe_add_hom Filter.Germ.coeAddHom
 
diff --git a/Mathlib/Order/Filter/Pointwise.lean b/Mathlib/Order/Filter/Pointwise.lean
@@ -148,8 +148,8 @@ theorem one_prod_one [One β] : (1 : Filter α) ×ˢ (1 : Filter β) = 1 :=
 
 /-- `pure` as a `OneHom`. -/
 @[to_additive "`pure` as a `ZeroHom`."]
-def pureOneHom : OneHom α (Filter α) :=
-  ⟨pure, pure_one⟩
+def pureOneHom : OneHom α (Filter α) where
+  toFun := pure; map_one' := pure_one
 #align filter.pure_one_hom Filter.pureOneHom
 #align filter.pure_zero_hom Filter.pureZeroHom
 
@@ -390,8 +390,8 @@ protected theorem map_mul [MulHomClass F α β] (m : F) : (f₁ * f₂).map m =
 
 /-- `pure` operation as a `MulHom`. -/
 @[to_additive "The singleton operation as an `AddHom`."]
-def pureMulHom : α →ₙ* Filter α :=
-  ⟨pure, fun _ _ => pure_mul_pure.symm⟩
+def pureMulHom : α →ₙ* Filter α where
+  toFun := pure; map_mul' _ _ := pure_mul_pure.symm
 #align filter.pure_mul_hom Filter.pureMulHom
 #align filter.pure_add_hom Filter.pureAddHom
 
diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -1673,12 +1673,13 @@ theorem nat_add_aleph0 (n : ℕ) : ↑n + ℵ₀ = ℵ₀ := by rw [add_comm, al
 
 /-- This function sends finite cardinals to the corresponding natural, and infinite cardinals
   to 0. -/
-def toNat : ZeroHom Cardinal ℕ :=
-  ⟨fun c => if h : c < aleph0.{v} then Classical.choose (lt_aleph0.1 h) else 0, by
+def toNat : ZeroHom Cardinal ℕ where
+  toFun c := if h : c < aleph0.{v} then Classical.choose (lt_aleph0.1 h) else 0
+  map_zero' := by
     have h : 0 < ℵ₀ := nat_lt_aleph0 0
     dsimp only
     rw [dif_pos h, ← Cardinal.natCast_inj, ← Classical.choose_spec (lt_aleph0.1 h),
-      Nat.cast_zero]⟩
+      Nat.cast_zero]
 #align cardinal.to_nat Cardinal.toNat
 
 theorem toNat_apply_of_lt_aleph0 {c : Cardinal} (h : c < ℵ₀) :
diff --git a/Mathlib/Topology/Algebra/Monoid.lean b/Mathlib/Topology/Algebra/Monoid.lean
