refactor(*): abbreviation for non-dependent FunLike (#9833)

This follows up from #9785, which renamed `FunLike` to `DFunLike`, by introducing a new abbreviation `FunLike F α β := DFunLike F α (fun _ => β)`, to make the non-dependent use of `FunLike` easier.

I searched for the pattern `DFunLike.*fun` and `DFunLike.*λ` in all files to replace expressions of the form `DFunLike F α (fun _ => β)` with `FunLike F α β`. I did this everywhere except for `extends` clauses for two reasons: it would conflict with #8386, and more importantly `extends` must directly refer to a structure with no unfolding of `def`s or `abbrev`s.

Archive/Hairer.lean

@@ -46,7 +46,7 @@ namespace SmoothSupportedOn
 
 variable {n : ℕ∞} {s : Set E}
 
-instance : DFunLike (SmoothSupportedOn 𝕜 E F n s) E (fun _ ↦ F) where
+instance : FunLike (SmoothSupportedOn 𝕜 E F n s) E F where
   coe := Subtype.val
   coe_injective' := Subtype.coe_injective
 

Mathlib/Algebra/Algebra/NonUnitalHom.lean

@@ -124,7 +124,7 @@ variable [NonUnitalNonAssocSemiring C] [DistribMulAction R C]
 -- instance : CoeFun (A →ₙₐ[R] B) fun _ => A → B :=
 --   ⟨toFun⟩
 
-instance : DFunLike (A →ₙₐ[R] B) A fun _ => B where
+instance : FunLike (A →ₙₐ[R] B) A B where
   coe f := f.toFun
   coe_injective' := by rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h; congr
 

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -66,8 +66,8 @@ instance {X Y : GroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
   coe (f : X →* Y) := f
 
 @[to_additive]
-instance DFunLike_instance (X Y : GroupCat) : DFunLike (X ⟶ Y) X (fun _ => Y) :=
-  show DFunLike (X →* Y) X (fun _ => Y) from inferInstance
+instance FunLike_instance (X Y : GroupCat) : FunLike (X ⟶ Y) X Y :=
+  show FunLike (X →* Y) X Y from inferInstance
 
 -- porting note: added
 @[to_additive (attr := simp)]
@@ -215,8 +215,8 @@ instance {X Y : CommGroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
   coe (f : X →* Y) := f
 
 @[to_additive]
-instance DFunLike_instance (X Y : CommGroupCat) : DFunLike (X ⟶ Y) X (fun _ => Y) :=
-  show DFunLike (X →* Y) X (fun _ => Y) from inferInstance
+instance FunLike_instance (X Y : CommGroupCat) : FunLike (X ⟶ Y) X Y :=
+  show FunLike (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} : DFunLike (M ⟶ N) M (fun _ => N) :=
+instance {M N : GroupWithZeroCat} : FunLike (M ⟶ N) M N :=
   ⟨fun f => f.toFun, fun f g h => by
     cases f
     cases g

Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean

@@ -67,7 +67,7 @@ open MonoidalCategory
 -- porting note: `CoeFun` was replaced by `DFunLike`
 -- I can't seem to express the function coercion here without writing `@DFunLike.coe`.
 theorem monoidalClosed_curry {M N P : ModuleCat.{u} R} (f : M ⊗ N ⟶ P) (x : M) (y : N) :
-    @DFunLike.coe _ _ _ LinearMap.instDFunLike
+    @DFunLike.coe _ _ _ LinearMap.instFunLike
       ((MonoidalClosed.curry f : N →ₗ[R] M →ₗ[R] P) y) x = f (x ⊗ₜ[R] y) :=
   rfl
 set_option linter.uppercaseLean3 false in
@@ -77,7 +77,7 @@ set_option linter.uppercaseLean3 false in
 theorem monoidalClosed_uncurry
     {M N P : ModuleCat.{u} R} (f : N ⟶ M ⟶[ModuleCat.{u} R] P) (x : M) (y : N) :
     MonoidalClosed.uncurry f (x ⊗ₜ[R] y) =
-      @DFunLike.coe _ _ _ LinearMap.instDFunLike (f y) x :=
+      @DFunLike.coe _ _ _ LinearMap.instFunLike (f y) x :=
   rfl
 set_option linter.uppercaseLean3 false in
 #align Module.monoidal_closed_uncurry ModuleCat.monoidalClosed_uncurry

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_DFunLike (X Y : MonCat) : DFunLike (X ⟶ Y) X (fun _ => Y) :=
-  show DFunLike (X →* Y) X (fun _ => Y) by infer_instance
+instance Hom_FunLike (X Y : MonCat) : FunLike (X ⟶ Y) X Y :=
+  show FunLike (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_DFunLike (X Y : CommMonCat) : DFunLike (X ⟶ Y) X (fun _ => Y) :=
-  show DFunLike (X →* Y) X (fun _ => Y) by infer_instance
+instance Hom_FunLike (X Y : CommMonCat) : FunLike (X ⟶ Y) X Y :=
+  show FunLike (X →* Y) X Y by infer_instance
 
 -- porting note: added
 @[to_additive (attr := simp)]

Mathlib/Algebra/Category/MonCat/FilteredColimits.lean

@@ -330,7 +330,7 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
   uniq t m h := MonoidHom.ext fun y => congr_fun
       ((Types.colimitCoconeIsColimit (F ⋙ forget MonCat)).uniq ((forget MonCat).mapCocone t)
         ((forget MonCat).map m)
-        fun j => funext fun x => DFunLike.congr_fun (i := MonCat.Hom_DFunLike _ _) (h j) x) y
+        fun j => funext fun x => DFunLike.congr_fun (i := MonCat.Hom_FunLike _ _) (h j) x) y
 #align Mon.filtered_colimits.colimit_cocone_is_colimit MonCat.FilteredColimits.colimitCoconeIsColimit
 #align AddMon.filtered_colimits.colimit_cocone_is_colimit AddMonCat.FilteredColimits.colimitCoconeIsColimit
 
@@ -405,15 +405,15 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
     MonCat.FilteredColimits.colimitDesc.{v, u} (F ⋙ forget₂ CommMonCat MonCat.{max v u})
       ((forget₂ CommMonCat MonCat.{max v u}).mapCocone t)
   fac t j :=
-    DFunLike.coe_injective (i := CommMonCat.Hom_DFunLike _ _) <|
+    DFunLike.coe_injective (i := CommMonCat.Hom_FunLike _ _) <|
       (Types.colimitCoconeIsColimit.{v, u} (F ⋙ forget CommMonCat.{max v u})).fac
         ((forget CommMonCat).mapCocone t) j
   uniq t m h :=
-    DFunLike.coe_injective (i := CommMonCat.Hom_DFunLike _ _) <|
+    DFunLike.coe_injective (i := CommMonCat.Hom_FunLike _ _) <|
       (Types.colimitCoconeIsColimit.{v, u} (F ⋙ forget CommMonCat.{max v u})).uniq
         ((forget CommMonCat.{max v u}).mapCocone t)
         ((forget CommMonCat.{max v u}).map m) fun j => funext fun x =>
-          DFunLike.congr_fun (i := CommMonCat.Hom_DFunLike _ _) (h j) x
+          DFunLike.congr_fun (i := CommMonCat.Hom_FunLike _ _) (h j) x
 #align CommMon.filtered_colimits.colimit_cocone_is_colimit CommMonCat.FilteredColimits.colimitCoconeIsColimit
 #align AddCommMon.filtered_colimits.colimit_cocone_is_colimit AddCommMonCat.FilteredColimits.colimitCoconeIsColimit
 

Mathlib/Algebra/Category/Ring/Basic.lean

@@ -107,7 +107,7 @@ set_option linter.uppercaseLean3 false in
 @[simp]
 lemma RingEquiv_coe_eq {X Y : Type _} [Semiring X] [Semiring Y] (e : X ≃+* Y) :
     (@DFunLike.coe (SemiRingCat.of X ⟶ SemiRingCat.of Y) _ (fun _ => (forget SemiRingCat).obj _)
-      ConcreteCategory.instDFunLike (e : X →+* Y) : X → Y) = ↑e :=
+      ConcreteCategory.instFunLike (e : X →+* Y) : X → Y) = ↑e :=
   rfl
 
 instance : Inhabited SemiRingCat :=
@@ -246,7 +246,7 @@ set_option linter.uppercaseLean3 false in
 @[simp]
 lemma RingEquiv_coe_eq {X Y : Type _} [Ring X] [Ring Y] (e : X ≃+* Y) :
     (@DFunLike.coe (RingCat.of X ⟶ RingCat.of Y) _ (fun _ => (forget RingCat).obj _)
-      ConcreteCategory.instDFunLike (e : X →+* Y) : X → Y) = ↑e :=
+      ConcreteCategory.instFunLike (e : X →+* Y) : X → Y) = ↑e :=
   rfl
 
 instance hasForgetToSemiRingCat : HasForget₂ RingCat SemiRingCat :=
@@ -330,7 +330,7 @@ set_option linter.uppercaseLean3 false in
 lemma RingEquiv_coe_eq {X Y : Type _} [CommSemiring X] [CommSemiring Y] (e : X ≃+* Y) :
     (@DFunLike.coe (CommSemiRingCat.of X ⟶ CommSemiRingCat.of Y) _
       (fun _ => (forget CommSemiRingCat).obj _)
-      ConcreteCategory.instDFunLike (e : X →+* Y) : X → Y) = ↑e :=
+      ConcreteCategory.instFunLike (e : X →+* Y) : X → Y) = ↑e :=
   rfl
 
 -- Porting note: I think this is now redundant.
@@ -445,7 +445,7 @@ set_option linter.uppercaseLean3 false in
 @[simp]
 lemma RingEquiv_coe_eq {X Y : Type _} [CommRing X] [CommRing Y] (e : X ≃+* Y) :
     (@DFunLike.coe (CommRingCat.of X ⟶ CommRingCat.of Y) _ (fun _ => (forget CommRingCat).obj _)
-      ConcreteCategory.instDFunLike (e : X →+* Y) : X → Y) = ↑e :=
+      ConcreteCategory.instFunLike (e : X →+* Y) : X → Y) = ↑e :=
   rfl
 
 -- Porting note: I think this is now redundant.

Mathlib/Algebra/Category/SemigroupCat/Basic.lean

@@ -99,7 +99,7 @@ theorem coe_of (R : Type u) [Mul R] : (MagmaCat.of R : Type u) = R :=
 @[to_additive (attr := simp)]
 lemma mulEquiv_coe_eq {X Y : Type _} [Mul X] [Mul Y] (e : X ≃* Y) :
     (@DFunLike.coe (MagmaCat.of X ⟶ MagmaCat.of Y) _ (fun _ => (forget MagmaCat).obj _)
-      ConcreteCategory.instDFunLike (e : X →ₙ* Y) : X → Y) = ↑e :=
+      ConcreteCategory.instFunLike (e : X →ₙ* Y) : X → Y) = ↑e :=
   rfl
 
 /-- Typecheck a `MulHom` as a morphism in `MagmaCat`. -/
@@ -184,7 +184,7 @@ theorem coe_of (R : Type u) [Semigroup R] : (SemigroupCat.of R : Type u) = R :=
 @[to_additive (attr := simp)]
 lemma mulEquiv_coe_eq {X Y : Type _} [Semigroup X] [Semigroup Y] (e : X ≃* Y) :
     (@DFunLike.coe (SemigroupCat.of X ⟶ SemigroupCat.of Y) _ (fun _ => (forget SemigroupCat).obj _)
-      ConcreteCategory.instDFunLike (e : X →ₙ* Y) : X → Y) = ↑e :=
+      ConcreteCategory.instFunLike (e : X →ₙ* Y) : X → Y) = ↑e :=
   rfl
 
 /-- Typecheck a `MulHom` as a morphism in `SemigroupCat`. -/

Mathlib/Algebra/Group/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 : ℕ) [DFunLike F α fun _ => β] : Prop where
+  [AddCommMonoid α] [AddCommMonoid β] (n : ℕ) [FunLike 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 : ℕ) [DFunLike F α fun _ => β] : Prop where
+  [CommMonoid β] (n : ℕ) [FunLike 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 [DFunLike F α fun _ => β]
+variable [FunLike F α β]
 
 section CommMonoid
 
@@ -154,11 +154,11 @@ theorem map_mul_map_eq_map_mul_map [FreimanHomClass F A β 2] (f : F) (ha : a 
 namespace FreimanHom
 
 @[to_additive]
-instance instDFunLike : DFunLike (A →*[n] β) α fun _ => β where
+instance instFunLike : FunLike (A →*[n] β) α β where
   coe := toFun
   coe_injective' f g h := by cases f; cases g; congr
-#align freiman_hom.fun_like FreimanHom.instDFunLike
-#align add_freiman_hom.fun_like AddFreimanHom.instDFunLike
+#align freiman_hom.fun_like FreimanHom.instFunLike
+#align add_freiman_hom.fun_like AddFreimanHom.instFunLike
 
 @[to_additive addFreimanHomClass]
 instance freimanHomClass : FreimanHomClass (A →*[n] β) A β n where

Mathlib/Algebra/Homology/ImageToKernel.lean

@@ -64,7 +64,7 @@ theorem subobject_ofLE_as_imageToKernel (w : f ≫ g = 0) (h) :
   rfl
 #align subobject_of_le_as_image_to_kernel subobject_ofLE_as_imageToKernel
 
-attribute [local instance] ConcreteCategory.instDFunLike
+attribute [local instance] ConcreteCategory.instFunLike
 
 -- porting note: removed elementwise attribute which does not seem to be helpful here
 -- a more suitable lemma is added below
@@ -303,7 +303,7 @@ theorem homology'.π_map (p : α.right = β.left) :
 
 section
 
-attribute [local instance] ConcreteCategory.instDFunLike
+attribute [local instance] ConcreteCategory.instFunLike
 
 @[simp]
 lemma homology'.π_map_apply [ConcreteCategory.{w} V] (p : α.right = β.left)

Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean

@@ -121,7 +121,7 @@ section abelian
 variable {C : Type u} [Category.{v} C] [ConcreteCategory.{v} C] [HasForget₂ C Ab]
   [Abelian C] [(forget₂ C Ab).Additive] [(forget₂ C Ab).PreservesHomology]
 
-attribute [local instance] ConcreteCategory.instDFunLike ConcreteCategory.hasCoeToSort
+attribute [local instance] ConcreteCategory.instFunLike ConcreteCategory.hasCoeToSort
 
 namespace ShortComplex
 

Mathlib/Algebra/Lie/Basic.lean

@@ -307,7 +307,7 @@ attribute [coe] LieHom.toLinearMap
 instance : Coe (L₁ →ₗ⁅R⁆ L₂) (L₁ →ₗ[R] L₂) :=
   ⟨LieHom.toLinearMap⟩
 
-instance : DFunLike (L₁ →ₗ⁅R⁆ L₂) L₁ (fun _ => L₂) :=
+instance : FunLike (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] }
@@ -736,7 +736,7 @@ attribute [coe] LieModuleHom.toLinearMap
 instance : CoeOut (M →ₗ⁅R,L⁆ N) (M →ₗ[R] N) :=
   ⟨LieModuleHom.toLinearMap⟩
 
-instance : DFunLike (M →ₗ⁅R, L⁆ N) M (fun _ => N) :=
+instance : FunLike (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

@@ -219,7 +219,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 instDFunLike {σ : R →+* S} : DFunLike (M →ₛₗ[σ] M₃) M (λ _ ↦ M₃) :=
+instance instFunLike {σ : R →+* S} : FunLike (M →ₛₗ[σ] M₃) M M₃ :=
   { AddHomClass.toDFunLike 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
-  DFunLike F α fun _ => β where
+  DFunLike F α (fun _ => β) 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
-  DFunLike F α fun _ => β where
+  DFunLike F α (fun _ => β) 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 DFunLike F α fun _ => β where
+  extends DFunLike F α (fun _ => β) 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 DFunLike F α fun _ => β where
+  extends DFunLike F α (fun _ => β) 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 DFunLike F α fun _ => β where
+  extends DFunLike F α (fun _ => β) 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 : DFunLike (S₁ →◃ S₂) S₁ fun _ => S₂ where
+instance : FunLike (S₁ →◃ S₂) S₁ S₂ where
   coe := toFun
   coe_injective' | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 

Mathlib/AlgebraicTopology/TopologicalSimplex.lean

@@ -25,7 +25,7 @@ namespace SimplexCategory
 
 open Simplicial NNReal BigOperators Classical CategoryTheory
 
-attribute [local instance] ConcreteCategory.hasCoeToSort ConcreteCategory.instDFunLike
+attribute [local instance] ConcreteCategory.hasCoeToSort ConcreteCategory.instFunLike
 
 -- porting note: added, should be moved
 instance (x : SimplexCategory) : Fintype (ConcreteCategory.forget.obj x) :=

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 : DFunLike (ι →ᵇᵃ[I₀] M) (Box ι) (fun _ ↦ M) where
+instance : FunLike (ι →ᵇᵃ[I₀] M) (Box ι) M where
   coe := toFun
   coe_injective' f g h := by cases f; cases g; congr
 

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -92,10 +92,10 @@ open SchwartzSpace
 -- porting note: removed
 -- instance : Coe 𝓢(E, F) (E → F) := ⟨toFun⟩
 
-instance instDFunLike : DFunLike 𝓢(E, F) E fun _ => F where
+instance instFunLike : FunLike 𝓢(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.instDFunLike
+#align schwartz_map.fun_like SchwartzMap.instFunLike
 
 /-- Helper instance for when there's too many metavariables to apply `DFunLike.hasCoeToFun`. -/
 instance instCoeFun : CoeFun 𝓢(E, F) fun _ => E → F :=

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -356,9 +356,9 @@ theorem repr_injective :
   cases g
   congr
 
--- Porting note: `CoeFun` → `DFunLike`
+-- Porting note: `CoeFun` → `FunLike`
 /-- `b i` is the `i`th basis vector. -/
-instance instDFunLike : DFunLike (OrthonormalBasis ι 𝕜 E) ι fun _ => E where
+instance instFunLike : FunLike (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 instDFunLike (X Y : SemiNormedGroupCat₁) : DFunLike (X ⟶ Y) X (fun _ => Y) where
+instance instFunLike (X Y : SemiNormedGroupCat₁) : FunLike (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 : DFunLike (P →ᵃⁱ[𝕜] P₂) P fun _ => P₂ :=
+instance : FunLike (P →ᵃⁱ[𝕜] P₂) P P₂ :=
   { coe := fun f => f.toFun,
     coe_injective' := fun f g => by cases f; cases g; simp }