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.

Author: Vierkantor

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