chore: typeclass for non-dependent FunLike

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -65,8 +65,8 @@ instance {X Y : GroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
   coe (f : X →* Y) := f
 
 @[to_additive]
-instance FunLike_instance (X Y : GroupCat) : FunLike (X ⟶ Y) X (fun _ => Y) :=
-  show FunLike (X →* Y) X (fun _ => Y) from inferInstance
+instance FunLike_instance (X Y : GroupCat) : NDFunLike (X ⟶ Y) X Y :=
+  show NDFunLike (X →* Y) X Y from inferInstance
 
 -- porting note: added
 @[to_additive (attr := simp)]
@@ -217,8 +217,8 @@ instance {X Y : CommGroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
   coe (f : X →* Y) := f
 
 @[to_additive]
-instance FunLike_instance (X Y : CommGroupCat) : FunLike (X ⟶ Y) X (fun _ => Y) :=
-  show FunLike (X →* Y) X (fun _ => Y) from inferInstance
+instance FunLike_instance (X Y : CommGroupCat) : NDFunLike (X ⟶ Y) X Y :=
+  show NDFunLike (X →* Y) X Y from inferInstance
 
 -- porting note: added
 @[to_additive (attr := simp)]

Mathlib/Algebra/Category/GroupWithZeroCat.lean

@@ -53,7 +53,7 @@ instance : LargeCategory.{u} GroupWithZeroCat where
   assoc _ _ _ := MonoidWithZeroHom.comp_assoc _ _ _
 
 -- porting note: was not necessary in mathlib
-instance {M N : GroupWithZeroCat} : FunLike (M ⟶ N) M (fun _ => N) :=
+instance {M N : GroupWithZeroCat} : NDFunLike (M ⟶ N) M N :=
   ⟨fun f => f.toFun, fun f g h => by
     cases f
     cases g

Mathlib/Algebra/Category/MonCat/Basic.lean

@@ -86,8 +86,8 @@ instance {X Y : MonCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
   coe (f : X →* Y) := f
 
 @[to_additive]
-instance Hom_FunLike (X Y : MonCat) : FunLike (X ⟶ Y) X (fun _ => Y) :=
-  show FunLike (X →* Y) X (fun _ => Y) by infer_instance
+instance Hom_NDFunLike (X Y : MonCat) : NDFunLike (X ⟶ Y) X Y :=
+  show NDFunLike (X →* Y) X Y by infer_instance
 
 -- porting note: added
 @[to_additive (attr := simp)]
@@ -208,8 +208,8 @@ instance {X Y : CommMonCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
   coe (f : X →* Y) := f
 
 @[to_additive]
-instance Hom_FunLike (X Y : CommMonCat) : FunLike (X ⟶ Y) X (fun _ => Y) :=
-  show FunLike (X →* Y) X (fun _ => Y) by infer_instance
+instance Hom_NDFunLike (X Y : CommMonCat) : NDFunLike (X ⟶ Y) X Y :=
+  show NDFunLike (X →* Y) X Y by infer_instance
 
 -- porting note: added
 @[to_additive (attr := simp)]

Mathlib/Algebra/Hom/Freiman.lean

@@ -88,7 +88,7 @@ notation:25 (name := «FreimanHomLocal≺») A " →*[" n:25 "] " β:0 => Freima
 /-- `AddFreimanHomClass F A β n` states that `F` is a type of `n`-ary sums-preserving morphisms.
 You should extend this class when you extend `AddFreimanHom`. -/
 class AddFreimanHomClass (F : Type*) (A : outParam <| Set α) (β : outParam <| Type*)
-  [AddCommMonoid α] [AddCommMonoid β] (n : ℕ) [FunLike F α fun _ => β] : Prop where
+  [AddCommMonoid α] [AddCommMonoid β] (n : ℕ) [NDFunLike F α β] : Prop where
   /-- An additive `n`-Freiman homomorphism preserves sums of `n` elements. -/
   map_sum_eq_map_sum' (f : F) {s t : Multiset α} (hsA : ∀ ⦃x⦄, x ∈ s → x ∈ A)
     (htA : ∀ ⦃x⦄, x ∈ t → x ∈ A) (hs : Multiset.card s = n) (ht : Multiset.card t = n)
@@ -102,15 +102,15 @@ You should extend this class when you extend `FreimanHom`. -/
       "`AddFreimanHomClass F A β n` states that `F` is a type of `n`-ary
       sums-preserving morphisms. You should extend this class when you extend `AddFreimanHom`."]
 class FreimanHomClass (F : Type*) (A : outParam <| Set α) (β : outParam <| Type*) [CommMonoid α]
-  [CommMonoid β] (n : ℕ) [FunLike F α fun _ => β] : Prop where
+  [CommMonoid β] (n : ℕ) [NDFunLike F α β] : Prop where
   /-- An `n`-Freiman homomorphism preserves products of `n` elements. -/
   map_prod_eq_map_prod' (f : F) {s t : Multiset α} (hsA : ∀ ⦃x⦄, x ∈ s → x ∈ A)
     (htA : ∀ ⦃x⦄, x ∈ t → x ∈ A) (hs : Multiset.card s = n) (ht : Multiset.card t = n)
     (h : s.prod = t.prod) :
     (s.map f).prod = (t.map f).prod
 #align freiman_hom_class FreimanHomClass
 
-variable [FunLike F α fun _ => β]
+variable [NDFunLike F α β]
 
 section CommMonoid
 
@@ -154,7 +154,7 @@ theorem map_mul_map_eq_map_mul_map [FreimanHomClass F A β 2] (f : F) (ha : a 
 namespace FreimanHom
 
 @[to_additive]
-instance funLike : FunLike (A →*[n] β) α fun _ => β where
+instance funLike : NDFunLike (A →*[n] β) α β where
   coe := toFun
   coe_injective' f g h := by cases f; cases g; congr
 #align freiman_hom.fun_like FreimanHom.funLike

Mathlib/Algebra/Hom/Group/Defs.lean

@@ -91,7 +91,7 @@ structure ZeroHom (M : Type*) (N : Type*) [Zero M] [Zero N] where
 You should extend this typeclass when you extend `ZeroHom`.
 -/
 class ZeroHomClass (F : Type*) (M N : outParam (Type*)) [Zero M] [Zero N]
-  extends FunLike F M fun _ => N where
+  extends NDFunLike F M N where
   /-- The proposition that the function preserves 0 -/
   map_zero : ∀ f : F, f 0 = 0
 #align zero_hom_class ZeroHomClass
@@ -120,7 +120,7 @@ structure AddHom (M : Type*) (N : Type*) [Add M] [Add N] where
 You should declare an instance of this typeclass when you extend `AddHom`.
 -/
 class AddHomClass (F : Type*) (M N : outParam (Type*)) [Add M] [Add N]
-  extends FunLike F M fun _ => N where
+  extends NDFunLike F M N where
   /-- The proposition that the function preserves addition -/
   map_add : ∀ (f : F) (x y : M), f (x + y) = f x + f y
 #align add_hom_class AddHomClass
@@ -185,7 +185,7 @@ You should extend this typeclass when you extend `OneHom`.
 -/
 @[to_additive]
 class OneHomClass (F : Type*) (M N : outParam (Type*)) [One M] [One N]
-  extends FunLike F M fun _ => N where
+  extends NDFunLike F M N where
   /-- The proposition that the function preserves 1 -/
   map_one : ∀ f : F, f 1 = 1
 #align one_hom_class OneHomClass
@@ -281,7 +281,7 @@ You should declare an instance of this typeclass when you extend `MulHom`.
 -/
 @[to_additive]
 class MulHomClass (F : Type*) (M N : outParam (Type*)) [Mul M] [Mul N]
-  extends FunLike F M fun _ => N where
+  extends NDFunLike F M N where
   /-- The proposition that the function preserves multiplication -/
   map_mul : ∀ (f : F) (x y : M), f (x * y) = f x * f y
 #align mul_hom_class MulHomClass
@@ -443,7 +443,7 @@ theorem map_pow [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (a : G) :
 theorem map_zpow' [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H]
     (f : F) (hf : ∀ x : G, f x⁻¹ = (f x)⁻¹) (a : G) : ∀ n : ℤ, f (a ^ n) = f a ^ n
   | (n : ℕ) => by rw [zpow_ofNat, map_pow, zpow_ofNat]
-  | Int.negSucc n => by rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc, ← zpow_negSucc]
+  | Int.negSucc n => by rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc]
 #align map_zpow' map_zpow'
 #align map_zsmul' map_zsmul'
 

Mathlib/Algebra/Hom/GroupAction.lean

@@ -76,7 +76,7 @@ scalar multiplication by `M`.
 
 You should extend this class when you extend `MulActionHom`. -/
 class SMulHomClass (F : Type*) (M X Y : outParam <| Type*) [SMul M X] [SMul M Y] extends
-  FunLike F X fun _ => Y where
+  NDFunLike F X Y where
   /-- The proposition that the function preserves the action. -/
   map_smul : ∀ (f : F) (c : M) (x : X), f (c • x) = c • f x
 #align smul_hom_class SMulHomClass

Mathlib/Algebra/Hom/NonUnitalAlg.lean

@@ -119,12 +119,12 @@ variable [NonUnitalNonAssocSemiring B] [DistribMulAction R B]
 
 variable [NonUnitalNonAssocSemiring C] [DistribMulAction R C]
 
--- Porting note: Replaced with FunLike instance
+-- Porting note: Replaced with NDFunLike instance
 -- /-- see Note [function coercion] -/
 -- instance : CoeFun (A →ₙₐ[R] B) fun _ => A → B :=
 --   ⟨toFun⟩
 
-instance : FunLike (A →ₙₐ[R] B) A fun _ => B where
+instance : NDFunLike (A →ₙₐ[R] B) A B where
   coe f := f.toFun
   coe_injective' := by rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h; congr
 

Mathlib/Algebra/Lie/Basic.lean

@@ -308,7 +308,7 @@ attribute [coe] LieHom.toLinearMap
 instance : Coe (L₁ →ₗ⁅R⁆ L₂) (L₁ →ₗ[R] L₂) :=
   ⟨LieHom.toLinearMap⟩
 
-instance : FunLike (L₁ →ₗ⁅R⁆ L₂) L₁ (fun _ => L₂) :=
+instance : NDFunLike (L₁ →ₗ⁅R⁆ L₂) L₁ L₂ :=
   { coe := fun f => f.toFun,
     coe_injective' := fun x y h =>
       by cases x; cases y; simp at h; simp [h] }
@@ -734,7 +734,7 @@ attribute [coe] LieModuleHom.toLinearMap
 instance : CoeOut (M →ₗ⁅R,L⁆ N) (M →ₗ[R] N) :=
   ⟨LieModuleHom.toLinearMap⟩
 
-instance : FunLike (M →ₗ⁅R, L⁆ N) M (fun _ => N) :=
+instance : NDFunLike (M →ₗ⁅R, L⁆ N) M N :=
   { coe := fun f => f.toFun,
     coe_injective' := fun x y h =>
       by cases x; cases y; simp at h; simp [h] }

Mathlib/Algebra/Module/LinearMap.lean

@@ -208,7 +208,7 @@ instance semilinearMapClass : SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M
 #noalign LinearMap.has_coe_to_fun
 
 -- Porting note: adding this instance prevents a timeout in `ext_ring_op`
-instance instFunLike {σ : R →+* S} : FunLike (M →ₛₗ[σ] M₃) M (λ _ ↦ M₃) :=
+instance instFunLike {σ : R →+* S} : NDFunLike (M →ₛₗ[σ] M₃) M M₃ :=
   { AddHomClass.toFunLike with }
 
 /-- The `DistribMulActionHom` underlying a `LinearMap`. -/

Mathlib/Algebra/Order/Hom/Basic.lean

@@ -77,37 +77,37 @@ variable {ι F α β γ δ : Type*}
 
 /-- `NonnegHomClass F α β` states that `F` is a type of nonnegative morphisms. -/
 class NonnegHomClass (F : Type*) (α β : outParam (Type*)) [Zero β] [LE β] extends
-  FunLike F α fun _ => β where
+  NDFunLike F α β where
   /-- the image of any element is non negative. -/
   map_nonneg (f : F) : ∀ a, 0 ≤ f a
 #align nonneg_hom_class NonnegHomClass
 
 /-- `SubadditiveHomClass F α β` states that `F` is a type of subadditive morphisms. -/
 class SubadditiveHomClass (F : Type*) (α β : outParam (Type*)) [Add α] [Add β] [LE β] extends
-  FunLike F α fun _ => β where
+  NDFunLike F α β where
   /-- the image of a sum is less or equal than the sum of the images. -/
   map_add_le_add (f : F) : ∀ a b, f (a + b) ≤ f a + f b
 #align subadditive_hom_class SubadditiveHomClass
 
 /-- `SubmultiplicativeHomClass F α β` states that `F` is a type of submultiplicative morphisms. -/
 @[to_additive SubadditiveHomClass]
 class SubmultiplicativeHomClass (F : Type*) (α β : outParam (Type*)) [Mul α] [Mul β] [LE β]
-  extends FunLike F α fun _ => β where
+  extends NDFunLike F α β where
   /-- the image of a product is less or equal than the product of the images. -/
   map_mul_le_mul (f : F) : ∀ a b, f (a * b) ≤ f a * f b
 #align submultiplicative_hom_class SubmultiplicativeHomClass
 
 /-- `MulLEAddHomClass F α β` states that `F` is a type of subadditive morphisms. -/
 @[to_additive SubadditiveHomClass]
 class MulLEAddHomClass (F : Type*) (α β : outParam (Type*)) [Mul α] [Add β] [LE β]
-  extends FunLike F α fun _ => β where
+  extends NDFunLike F α β where
   /-- the image of a product is less or equal than the sum of the images. -/
   map_mul_le_add (f : F) : ∀ a b, f (a * b) ≤ f a + f b
 #align mul_le_add_hom_class MulLEAddHomClass
 
 /-- `NonarchimedeanHomClass F α β` states that `F` is a type of non-archimedean morphisms. -/
 class NonarchimedeanHomClass (F : Type*) (α β : outParam (Type*)) [Add α] [LinearOrder β]
-  extends FunLike F α fun _ => β where
+  extends NDFunLike F α β where
   /-- the image of a sum is less or equal than the maximum of the images. -/
   map_add_le_max (f : F) : ∀ a b, f (a + b) ≤ max (f a) (f b)
 #align nonarchimedean_hom_class NonarchimedeanHomClass

Mathlib/Algebra/Quandle.lean

@@ -358,7 +358,7 @@ namespace ShelfHom
 
 variable {S₁ : Type*} {S₂ : Type*} {S₃ : Type*} [Shelf S₁] [Shelf S₂] [Shelf S₃]
 
-instance : FunLike (S₁ →◃ S₂) S₁ fun _ => S₂ where
+instance : NDFunLike (S₁ →◃ S₂) S₁ S₂ where
   coe := toFun
   coe_injective' | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 

Mathlib/Algebra/Star/Basic.lean

@@ -505,7 +505,7 @@ section
 
 /-- `StarHomClass F R S` states that `F` is a type of `star`-preserving maps from `R` to `S`. -/
 class StarHomClass (F : Type*) (R S : outParam (Type*)) [Star R] [Star S] extends
-  FunLike F R fun _ => S where
+  NDFunLike F R S where
   /-- the maps preserve star -/
   map_star : ∀ (f : F) (r : R), f (star r) = star (f r)
 #align star_hom_class StarHomClass

Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

@@ -58,7 +58,7 @@ open Box Prepartition Finset
 variable {N : Type*} [AddCommMonoid M] [AddCommMonoid N] {I₀ : WithTop (Box ι)} {I J : Box ι}
   {i : ι}
 
-instance : FunLike (ι →ᵇᵃ[I₀] M) (Box ι) (fun _ ↦ M) where
+instance : NDFunLike (ι →ᵇᵃ[I₀] M) (Box ι) M where
   coe := toFun
   coe_injective' f g h := by cases f; cases g; congr
 

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -92,7 +92,7 @@ open SchwartzSpace
 -- porting note: removed
 -- instance : Coe 𝓢(E, F) (E → F) := ⟨toFun⟩
 
-instance instFunLike : FunLike 𝓢(E, F) E fun _ => F where
+instance instNDFunLike : NDFunLike 𝓢(E, F) E F where
   coe f := f.toFun
   coe_injective' f g h := by cases f; cases g; congr
 #align schwartz_map.fun_like SchwartzMap.instFunLike

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -360,7 +360,7 @@ theorem repr_injective :
 
 -- Porting note: `CoeFun` → `FunLike`
 /-- `b i` is the `i`th basis vector. -/
-instance instFunLike : FunLike (OrthonormalBasis ι 𝕜 E) ι fun _ => E where
+instance instNDFunLike : NDFunLike (OrthonormalBasis ι 𝕜 E) ι E where
   coe b i := by classical exact b.repr.symm (EuclideanSpace.single i (1 : 𝕜))
   coe_injective' b b' h := repr_injective <| LinearIsometryEquiv.toLinearEquiv_injective <|
     LinearEquiv.symm_bijective.injective <| LinearEquiv.toLinearMap_injective <| by

Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean

@@ -147,7 +147,7 @@ instance : LargeCategory.{u} SemiNormedGroupCat₁ where
   comp {X Y Z} f g := ⟨g.1.comp f.1, g.2.comp f.2⟩
 
 -- Porting Note: Added
-instance instFunLike (X Y : SemiNormedGroupCat₁) : FunLike (X ⟶ Y) X (fun _ => Y) where
+instance instNDFunLike (X Y : SemiNormedGroupCat₁) : NDFunLike (X ⟶ Y) X Y where
   coe f := f.1.toFun
   coe_injective' _ _ h := Subtype.val_inj.mp (NormedAddGroupHom.coe_injective h)
 

Mathlib/Analysis/NormedSpace/AffineIsometry.lean

@@ -71,7 +71,7 @@ theorem linear_eq_linearIsometry : f.linear = f.linearIsometry.toLinearMap := by
   rfl
 #align affine_isometry.linear_eq_linear_isometry AffineIsometry.linear_eq_linearIsometry
 
-instance : FunLike (P →ᵃⁱ[𝕜] P₂) P fun _ => P₂ :=
+instance : NDFunLike (P →ᵃⁱ[𝕜] P₂) P P₂ :=
   { coe := fun f => f.toFun,
     coe_injective' := fun f g => by cases f; cases g; simp }
 

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

@@ -98,29 +98,29 @@
 #noalign category_theory.forget_obj_eq_coe
 
 @[reducible]
-def ConcreteCategory.funLike {X Y : C} : FunLike (X ⟶ Y) X (fun _ => Y) where
+def ConcreteCategory.ndfunLike {X Y : C} : NDFunLike (X ⟶ Y) X Y where
   coe f := (forget C).map f
   coe_injective' _ _ h := (forget C).map_injective h
 attribute [local instance] ConcreteCategory.funLike
 
 /-- In any concrete category, we can test equality of morphisms by pointwise evaluations.-/
 @[ext low] -- Porting note: lowered priority
 theorem ConcreteCategory.hom_ext {X Y : C} (f g : X ⟶ Y) (w : ∀ x : X, f x = g x) : f = g := by
   apply @Faithful.map_injective C _ (Type w) _ (forget C) _ X Y
   dsimp [forget]
   funext x
   exact w x
 #align category_theory.concrete_category.hom_ext CategoryTheory.ConcreteCategory.hom_ext
 
 theorem forget_map_eq_coe {X Y : C} (f : X ⟶ Y) : (forget C).map f = f := rfl
 #align category_theory.forget_map_eq_coe CategoryTheory.forget_map_eq_coe
 
 /-- Analogue of `congr_fun h x`,
 when `h : f = g` is an equality between morphisms in a concrete category.
 -/
 theorem congr_hom {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : X) : f x = g x :=
   congrFun (congrArg (fun k : X ⟶ Y => (k : X → Y)) h) x
 #align category_theory.congr_hom CategoryTheory.congr_hom
 
 theorem coe_id {X : C} : (𝟙 X : X → X) = id :=
   (forget _).map_id X

Mathlib/Combinatorics/Additive/SalemSpencer.lean

@@ -118,7 +118,7 @@ section CommMonoid
 variable [CommMonoid α] [CommMonoid β] {s : Set α} {a : α}
 
 @[to_additive]
-theorem MulSalemSpencer.of_image [FunLike F α fun _ => β] [FreimanHomClass F s β 2] (f : F)
+theorem MulSalemSpencer.of_image [NDFunLike F α β] [FreimanHomClass F s β 2] (f : F)
     (hf : s.InjOn f) (h : MulSalemSpencer (f '' s)) : MulSalemSpencer s :=
   fun _ _ _ ha hb hc habc => hf ha hb <|
     h (mem_image_of_mem _ ha) (mem_image_of_mem _ hb) (mem_image_of_mem _ hc) <|

Mathlib/Combinatorics/Young/SemistandardTableau.lean

@@ -63,7 +63,7 @@ structure Ssyt (μ : YoungDiagram) where
 
 namespace Ssyt
 
-instance funLike {μ : YoungDiagram} : FunLike (Ssyt μ) ℕ fun _ ↦ ℕ → ℕ where
+instance ndfunLike {μ : YoungDiagram} : NDFunLike (Ssyt μ) ℕ (ℕ → ℕ) where
   coe := Ssyt.entry
   coe_injective' T T' h := by
     cases T

Mathlib/Data/Analysis/Filter.lean

@@ -53,7 +53,7 @@ instance : CoeFun (CFilter α σ) fun _ ↦ σ → α :=
   ⟨CFilter.f⟩
 
 /- Porting note: Due to the CoeFun instance, the lhs of this lemma has a variable (f) as its head
-symbol (simpnf linter problem). Replacing it with a FunLike instance would not be mathematically
+symbol (simpnf linter problem). Replacing it with a NDFunLike instance would not be mathematically
 meaningful here, since the coercion to f cannot be injective, hence need to remove @[simp]. -/
 -- @[simp]
 theorem coe_mk (f pt inf h₁ h₂ a) : (@CFilter.mk α σ _ f pt inf h₁ h₂) a = f a :=

Mathlib/Data/Finset/Image.lean

@@ -66,7 +66,7 @@ variable {f : α ↪ β} {s : Finset α}
 
 @[simp]
 theorem mem_map {b : β} : b ∈ s.map f ↔ ∃ a ∈ s, f a = b :=
-  mem_map.trans <| by simp only [exists_prop]; rfl
+  Multiset.mem_map
 #align finset.mem_map Finset.mem_map
 
 --Porting note: Higher priority to apply before `mem_map`.

Mathlib/Data/Finsupp/Defs.lean

@@ -116,7 +116,7 @@ section Basic
 
 variable [Zero M]
 
-instance funLike : FunLike (α →₀ M) α fun _ => M :=
+instance ndfunLike : NDFunLike (α →₀ M) α M :=
   ⟨toFun, by
     rintro ⟨s, f, hf⟩ ⟨t, g, hg⟩ (rfl : f = g)
     congr

Mathlib/Data/FunLike/Basic.lean

@@ -27,7 +27,7 @@ namespace MyHom
 variables (A B : Type*) [MyClass A] [MyClass B]
 
 -- This instance is optional if you follow the "morphism class" design below:
-instance : FunLike (MyHom A B) A (λ _, B) :=
+instance : NDFunLike (MyHom A B) A B :=
   { coe := MyHom.toFun, coe_injective' := λ f g h, by cases f; cases g; congr' }
 
 /-- Helper instance for when there's too many metavariables to apply
@@ -59,7 +59,7 @@ Continuing the example above:
 /-- `MyHomClass F A B` states that `F` is a type of `MyClass.op`-preserving morphisms.
 You should extend this class when you extend `MyHom`. -/
 class MyHomClass (F : Type*) (A B : outParam <| Type*) [MyClass A] [MyClass B]
-  extends FunLike F A (λ _, B) :=
+  extends NDFunLike F A B :=
 (map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))
 
 @[simp] lemma map_op {F A B : Type*} [MyClass A] [MyClass B] [MyHomClass F A B]
@@ -221,4 +221,16 @@ protected theorem congr_arg (f : F) {x y : α} (h₂ : x = y) : f x = f y :=
 
 end FunLike
 
+/-- The class `NDFunLike F α β` expresses that terms of type `F` have an
+injective coercion to functions from `α` to `β`.
+
+This typeclass is used in the definition of the homomorphism typeclasses,
+such as `ZeroHomClass`, `MulHomClass`, `MonoidHomClass`, ....
+-/
+class NDFunLike (F : Sort*) (α : outParam <| Sort*) (β : outParam <| Sort*) extends
+  FunLike F α fun _ ↦ β
+
+instance (priority := 110) hasCoeToFun {F α β} [NDFunLike F α β] : CoeFun F fun _ ↦ α → β where
+  coe := NDFunLike.toFunLike.coe
+
 end NonDependent

Mathlib/Data/FunLike/Embedding.lean

@@ -131,7 +131,7 @@ instead of linearly increasing the work per `MyEmbedding`-related declaration.
 /-- The class `EmbeddingLike F α β` expresses that terms of type `F` have an
 injective coercion to injective functions `α ↪ β`.
 -/
-class EmbeddingLike (F : Sort*) (α β : outParam (Sort*)) extends FunLike F α fun _ ↦ β where
+class EmbeddingLike (F : Sort*) (α β : outParam (Sort*)) extends NDFunLike F α β where
   /-- The coercion to functions must produce injective functions. -/
   injective' : ∀ f : F, Function.Injective (coe f)
 #align embedding_like EmbeddingLike