use abbrev

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

@@ -69,7 +69,7 @@ open MonoidalCategory
 -- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
 @[simp, nolint simpNF]
 theorem monoidalClosed_curry {M N P : ModuleCat.{u} R} (f : M ⊗ N ⟶ P) (x : M) (y : N) :
-    @FunLike.coe _ _ _ LinearMap.instFunLike.toFunLike
+    @FunLike.coe _ _ _ LinearMap.instFunLike
       ((MonoidalClosed.curry f : N →ₗ[R] M →ₗ[R] P) y) x = f (x ⊗ₜ[R] y) :=
   rfl
 set_option linter.uppercaseLean3 false in
@@ -79,7 +79,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) =
-      @FunLike.coe _ _ _ LinearMap.instFunLike.toFunLike (f y) x :=
+      @FunLike.coe _ _ _ LinearMap.instFunLike (f y) x :=
   rfl
 set_option linter.uppercaseLean3 false in
 #align Module.monoidal_closed_uncurry ModuleCat.monoidalClosed_uncurry

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) :
     (@FunLike.coe (SemiRingCat.of X ⟶ SemiRingCat.of Y) _ (fun _ => (forget SemiRingCat).obj _)
-      ConcreteCategory.funLike.toFunLike (e : X →+* Y) : X → Y) = ↑e :=
+      ConcreteCategory.funLike (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) :
     (@FunLike.coe (RingCat.of X ⟶ RingCat.of Y) _ (fun _ => (forget RingCat).obj _)
-      ConcreteCategory.funLike.toFunLike (e : X →+* Y) : X → Y) = ↑e :=
+      ConcreteCategory.funLike (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) :
     (@FunLike.coe (CommSemiRingCat.of X ⟶ CommSemiRingCat.of Y) _
       (fun _ => (forget CommSemiRingCat).obj _)
-      ConcreteCategory.funLike.toFunLike (e : X →+* Y) : X → Y) = ↑e :=
+      ConcreteCategory.funLike (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) :
     (@FunLike.coe (CommRingCat.of X ⟶ CommRingCat.of Y) _ (fun _ => (forget CommRingCat).obj _)
-      ConcreteCategory.funLike.toFunLike (e : X →+* Y) : X → Y) = ↑e :=
+      ConcreteCategory.funLike (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) :
     (@FunLike.coe (MagmaCat.of X ⟶ MagmaCat.of Y) _ (fun _ => (forget MagmaCat).obj _)
-      ConcreteCategory.funLike.toFunLike (e : X →ₙ* Y) : X → Y) = ↑e :=
+      ConcreteCategory.funLike (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) :
     (@FunLike.coe (SemigroupCat.of X ⟶ SemigroupCat.of Y) _ (fun _ => (forget SemigroupCat).obj _)
-      ConcreteCategory.funLike.toFunLike (e : X →ₙ* Y) : X → Y) = ↑e :=
+      ConcreteCategory.funLike (e : X →ₙ* Y) : X → Y) = ↑e :=
   rfl
 
 /-- Typecheck a `MulHom` as a morphism in `SemigroupCat`. -/

Mathlib/Data/FunLike/Basic.lean

@@ -205,9 +205,21 @@ end Dependent
 
 section NonDependent
 
-/-! ### `FunLike F α (λ _, β)` where `β` does not depend on `a : α` -/
+/-- 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`, ....
+-/
+abbrev NDFunLike (F : Sort*) (α : outParam <| Sort*) (β : outParam <| Sort*) :=
+  FunLike F α fun _ ↦ β
+
+instance (priority := 110) hasCoeToFun {F α β} [NDFunLike F α β] : CoeFun F fun _ ↦ α → β where
+  coe := FunLike.coe
+
+/-! ### `NDFunLike F α β` where `β` does not depend on `a : α` -/
 
-variable {F α β : Sort*} [i : FunLike F α fun _ ↦ β]
+variable {F α β : Sort*} [i : NDFunLike F α β]
 
 namespace FunLike
 
@@ -221,16 +233,4 @@ 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