Fixes

Mathlib/Algebra/Algebra/Spectrum.lean

@@ -390,7 +390,7 @@ section CommSemiring
 
 variable {F R A B : Type*} [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B]
 
-variable [AlgHomClass F R A B]
+variable [NDFunLike F A B] [AlgHomClass F R A B]
 
 local notation "σ" => spectrum R
 
@@ -411,7 +411,7 @@ section CommRing
 
 variable {F R A B : Type*} [CommRing R] [Ring A] [Algebra R A] [Ring B] [Algebra R B]
 
-variable [AlgHomClass F R A R]
+variable [NDFunLike F A R] [AlgHomClass F R A R]
 
 local notation "σ" => spectrum R
 
@@ -431,7 +431,7 @@ end AlgHom
 
 @[simp]
 theorem AlgEquiv.spectrum_eq {F R A B : Type*} [CommSemiring R] [Ring A] [Ring B] [Algebra R A]
-    [Algebra R B] [AlgEquivClass F R A B] (f : F) (a : A) :
+    [Algebra R B] [EquivLike F A B] [AlgEquivClass F R A B] (f : F) (a : A) :
     spectrum R (f a) = spectrum R a :=
   Set.Subset.antisymm (AlgHom.spectrum_apply_subset _ _) <| by
     simpa only [AlgEquiv.coe_algHom, AlgEquiv.coe_coe_symm_apply_coe_apply] using

Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean

@@ -122,14 +122,19 @@ theorem unitization_range : (unitization s).range = Algebra.adjoin R (s : Set A)
 
 end Semiring
 
+-- Note: fixes a timeout since going through this class will cause a huge synthesis goal
+-- TODO: why is this so expensive here?
+attribute [instance 50] NonUnitalStarAlgHomClass.toNonUnitalAlgHomClass
+
 /-- A sufficient condition for injectivity of `NonUnitalSubalgebra.unitization` when the scalars
 are a commutative ring. When the scalars are a field, one should use the more natural
 `NonUnitalStarSubalgebra.unitization_injective` whose hypothesis is easier to verify. -/
 theorem _root_.AlgHomClass.unitization_injective' {F R S A : Type*} [CommRing R] [Ring A]
     [Algebra R A] [SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A]
-    (s : S) (h : ∀ r, r ≠ 0 → algebraMap R A r ∉ s) [AlgHomClass F R (Unitization R s) A] (f : F)
-    (hf : ∀ x : s, f x = x) : Function.Injective f := by
-  refine' (injective_iff_map_eq_zero _).mpr fun x hx => _
+    (s : S) (h : ∀ r, r ≠ 0 → algebraMap R A r ∉ s)
+    [NDFunLike F (Unitization R s) A] [AlgHomClass F R (Unitization R s) A]
+    (f : F) (hf : ∀ x : s, f x = x) : Function.Injective f := by
+  refine' (injective_iff_map_eq_zero f).mpr fun x hx => _
   induction' x using Unitization.ind with r a
   simp_rw [map_add, hf, ←Unitization.algebraMap_eq_inl, AlgHomClass.commutes] at hx
   rw [add_eq_zero_iff_eq_neg] at hx ⊢
@@ -142,8 +147,8 @@ theorem _root_.AlgHomClass.unitization_injective' {F R S A : Type*} [CommRing R]
 `NonUnitalSubalgebra.unitization_injective` and `NonUnitalStarSubalgebra.unitization_injective`. -/
 theorem _root_.AlgHomClass.unitization_injective {F R S A : Type*} [Field R] [Ring A]
     [Algebra R A] [SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A]
-    (s : S) (h1 : 1 ∉ s) [AlgHomClass F R (Unitization R s) A] (f : F)
-    (hf : ∀ x : s, f x = x) : Function.Injective f := by
+    (s : S) (h1 : 1 ∉ s) [NDFunLike F (Unitization R s) A] [AlgHomClass F R (Unitization R s) A]
+    (f : F) (hf : ∀ x : s, f x = x) : Function.Injective f := by
   refine AlgHomClass.unitization_injective' s (fun r hr hr' ↦ ?_) f hf
   rw [Algebra.algebraMap_eq_smul_one] at hr'
   exact h1 <| inv_smul_smul₀ hr (1 : A) ▸ SMulMemClass.smul_mem r⁻¹ hr'

Mathlib/Algebra/Category/AlgebraCat/Basic.lean

@@ -57,6 +57,9 @@ instance : Category (AlgebraCat.{v} R) where
   id A := AlgHom.id R A
   comp f g := g.comp f
 
+instance {M N : AlgebraCat.{v} R} : NDFunLike (M ⟶ N) M N :=
+  AlgHom.funLike
+
 instance {M N : AlgebraCat.{v} R} : AlgHomClass (M ⟶ N) R M N :=
   AlgHom.algHomClass
 

Mathlib/Algebra/Category/AlgebraCat/Limits.lean

@@ -108,7 +108,7 @@ def limitConeIsLimit (F : J ⥤ AlgebraCatMax.{v, w} R) : IsLimit (limitCone.{v,
       forget_map_eq_coe]
     -- This used to be as below but we need `erw` after leanprover/lean4#2644
     -- simp [forget_map_eq_coe, AlgHom.map_one, Functor.mapCone_π_app]
-    erw [map_one]
+    erw [AlgHom.map_one]
     rfl
   · intro x y
     apply Subtype.ext
@@ -117,7 +117,7 @@ def limitConeIsLimit (F : J ⥤ AlgebraCatMax.{v, w} R) : IsLimit (limitCone.{v,
       forget_map_eq_coe]
     -- This used to be as below, but we need `erw` after leanprover/lean4#2644
     -- simp [forget_map_eq_coe, AlgHom.map_mul, Functor.mapCone_π_app]
-    erw [map_mul]
+    erw [AlgHom.map_mul]
     rfl
   · simp only [Functor.comp_obj, Functor.mapCone_pt, Functor.mapCone_π_app,
       forget_map_eq_coe]

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

@@ -67,7 +67,7 @@ open MonoidalCategory
 -- porting note: `CoeFun` was replaced by `FunLike`
 -- I can't seem to express the function coercion here without writing `@FunLike.coe`.
 theorem monoidalClosed_curry {M N P : ModuleCat.{u} R} (f : M ⊗ N ⟶ P) (x : M) (y : N) :
-    @FunLike.coe _ _ _ LinearMap.instFunLike
+    @FunLike.coe _ _ _ LinearMap.ndFunLike
       ((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) =
-      @FunLike.coe _ _ _ LinearMap.instFunLike (f y) x :=
+      @FunLike.coe _ _ _ LinearMap.ndFunLike (f y) x :=
   rfl
 set_option linter.uppercaseLean3 false in
 #align Module.monoidal_closed_uncurry ModuleCat.monoidalClosed_uncurry

Mathlib/Algebra/Lie/Basic.lean

@@ -564,6 +564,10 @@ instance : EquivLike (L₁ ≃ₗ⁅R⁆ L₂) L₁ L₂ :=
     coe_injective' := fun f g h₁ h₂ =>
       by cases f; cases g; simp at h₁ h₂; simp [*] }
 
+instance : NDFunLike (L₁ ≃ₗ⁅R⁆ L₂) L₁ L₂ where
+  coe f := f.toFun
+  coe_injective' := FunLike.coe_injective
+
 theorem coe_to_lieHom (e : L₁ ≃ₗ⁅R⁆ L₂) : ⇑(e : L₁ →ₗ⁅R⁆ L₂) = e :=
   rfl
 #align lie_equiv.coe_to_lie_hom LieEquiv.coe_to_lieHom

Mathlib/Algebra/Order/Hom/Basic.lean

@@ -172,7 +172,7 @@ group `α`.
 
 You should extend this class when you extend `AddGroupSeminorm`. -/
 class AddGroupSeminormClass (F α β : Type*) [AddGroup α] [OrderedAddCommMonoid β] [NDFunLike F α β]
-  extends SubadditiveHomClass F α β where
+  extends SubadditiveHomClass F α β : Prop where
   /-- The image of zero is zero. -/
   map_zero (f : F) : f 0 = 0
   /-- The map is invariant under negation of its argument. -/
@@ -184,7 +184,7 @@ class AddGroupSeminormClass (F α β : Type*) [AddGroup α] [OrderedAddCommMonoi
 You should extend this class when you extend `GroupSeminorm`. -/
 @[to_additive]
 class GroupSeminormClass (F α β : Type*) [Group α] [OrderedAddCommMonoid β] [NDFunLike F α β]
-  extends MulLEAddHomClass F α β where
+  extends MulLEAddHomClass F α β : Prop where
   /-- The image of one is zero. -/
   map_one_eq_zero (f : F) : f 1 = 0
   /-- The map is invariant under inversion of its argument. -/
@@ -196,7 +196,7 @@ class GroupSeminormClass (F α β : Type*) [Group α] [OrderedAddCommMonoid β]
 
 You should extend this class when you extend `AddGroupNorm`. -/
 class AddGroupNormClass (F α β : Type*) [AddGroup α] [OrderedAddCommMonoid β] [NDFunLike F α β]
-  extends AddGroupSeminormClass F α β where
+  extends AddGroupSeminormClass F α β : Prop where
   /-- The argument is zero if its image under the map is zero. -/
   eq_zero_of_map_eq_zero (f : F) {a : α} : f a = 0 → a = 0
 #align add_group_norm_class AddGroupNormClass
@@ -206,7 +206,7 @@ class AddGroupNormClass (F α β : Type*) [AddGroup α] [OrderedAddCommMonoid β
 You should extend this class when you extend `GroupNorm`. -/
 @[to_additive]
 class GroupNormClass (F α β : Type*) [Group α] [OrderedAddCommMonoid β] [NDFunLike F α β]
-  extends GroupSeminormClass F α β where
+  extends GroupSeminormClass F α β : Prop where
   /-- The argument is one if its image under the map is zero. -/
   eq_one_of_map_eq_zero (f : F) {a : α} : f a = 0 → a = 1
 #align group_norm_class GroupNormClass
@@ -314,30 +314,30 @@ theorem map_pos_of_ne_one [Group α] [LinearOrderedAddCommMonoid β] [GroupNormC
 
 You should extend this class when you extend `RingSeminorm`. -/
 class RingSeminormClass (F α β : Type*) [NonUnitalNonAssocRing α] [OrderedSemiring β]
-  [NDFunLike F α β] extends AddGroupSeminormClass F α β, SubmultiplicativeHomClass F α β
+  [NDFunLike F α β] extends AddGroupSeminormClass F α β, SubmultiplicativeHomClass F α β : Prop
 #align ring_seminorm_class RingSeminormClass
 
 /-- `RingNormClass F α` states that `F` is a type of `β`-valued norms on the ring `α`.
 
 You should extend this class when you extend `RingNorm`. -/
 class RingNormClass (F α β : Type*) [NonUnitalNonAssocRing α] [OrderedSemiring β] [NDFunLike F α β]
-  extends RingSeminormClass F α β, AddGroupNormClass F α β
+  extends RingSeminormClass F α β, AddGroupNormClass F α β : Prop
 #align ring_norm_class RingNormClass
 
 /-- `MulRingSeminormClass F α` states that `F` is a type of `β`-valued multiplicative seminorms
 on the ring `α`.
 
 You should extend this class when you extend `MulRingSeminorm`. -/
 class MulRingSeminormClass (F α β : Type*) [NonAssocRing α] [OrderedSemiring β] [NDFunLike F α β]
-  extends AddGroupSeminormClass F α β, MonoidWithZeroHomClass F α β
+  extends AddGroupSeminormClass F α β, MonoidWithZeroHomClass F α β : Prop
 #align mul_ring_seminorm_class MulRingSeminormClass
 
 /-- `MulRingNormClass F α` states that `F` is a type of `β`-valued multiplicative norms on the
 ring `α`.
 
 You should extend this class when you extend `MulRingNorm`. -/
 class MulRingNormClass (F α β : Type*) [NonAssocRing α] [OrderedSemiring β] [NDFunLike F α β]
-  extends MulRingSeminormClass F α β, AddGroupNormClass F α β
+  extends MulRingSeminormClass F α β, AddGroupNormClass F α β : Prop
 #align mul_ring_norm_class MulRingNormClass
 
 -- See note [out-param inheritance]

Mathlib/Analysis/Normed/Field/Basic.lean

@@ -934,6 +934,7 @@ end RingHomIsometric
 section Induced
 
 variable {F : Type*} (R S : Type*)
+variable [NDFunLike F R S]
 
 /-- A non-unital ring homomorphism from a `NonUnitalRing` to a `NonUnitalSeminormedRing`
 induces a `NonUnitalSeminormedRing` structure on the domain.
@@ -1025,7 +1026,7 @@ def NormedField.induced [Field R] [NormedField S] [NonUnitalRingHomClass F R S]
 /-- A ring homomorphism from a `Ring R` to a `SeminormedRing S` which induces the norm structure
 `SeminormedRing.induced` makes `R` satisfy `‖(1 : R)‖ = 1` whenever `‖(1 : S)‖ = 1`. -/
 theorem NormOneClass.induced {F : Type*} (R S : Type*) [Ring R] [SeminormedRing S]
-    [NormOneClass S] [RingHomClass F R S] (f : F) :
+    [NormOneClass S] [NDFunLike F R S] [RingHomClass F R S] (f : F) :
     @NormOneClass R (SeminormedRing.induced R S f).toNorm _ :=
   -- porting note: is this `let` a bad idea somehow?
   let _ : SeminormedRing R := SeminormedRing.induced R S f

Mathlib/Analysis/Normed/Group/Hom.lean

@@ -85,17 +85,15 @@ variable {f g : NormedAddGroupHom V₁ V₂}
 def ofLipschitz (f : V₁ →+ V₂) {K : ℝ≥0} (h : LipschitzWith K f) : NormedAddGroupHom V₁ V₂ :=
   f.mkNormedAddGroupHom K fun x ↦ by simpa only [map_zero, dist_zero_right] using h.dist_le_mul x 0
 
--- porting note: moved this declaration up so we could get a `FunLike` instance sooner.
-instance toAddMonoidHomClass : AddMonoidHomClass (NormedAddGroupHom V₁ V₂) V₁ V₂ where
+instance funLike : NDFunLike (NormedAddGroupHom V₁ V₂) V₁ V₂ where
   coe := toFun
   coe_injective' := fun f g h => by cases f; cases g; congr
+
+-- porting note: moved this declaration up so we could get a `FunLike` instance sooner.
+instance toAddMonoidHomClass : AddMonoidHomClass (NormedAddGroupHom V₁ V₂) V₁ V₂ where
   map_add f := f.map_add'
   map_zero f := (AddMonoidHom.mk' f.toFun f.map_add').map_zero
 
-/-- Helper instance for when there are too many metavariables to apply `FunLike.coeFun` directly. -/
-instance coeFun : CoeFun (NormedAddGroupHom V₁ V₂) fun _ => V₁ → V₂ :=
-  ⟨FunLike.coe⟩
-
 initialize_simps_projections NormedAddGroupHom (toFun → apply)
 
 theorem coe_inj (H : (f : V₁ → V₂) = g) : f = g := by

Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean

@@ -59,9 +59,11 @@ instance (M : SemiNormedGroupCat) : SeminormedAddCommGroup M :=
   M.str
 
 -- Porting Note: added
-instance toAddMonoidHomClass {V W : SemiNormedGroupCat} : AddMonoidHomClass (V ⟶ W) V W where
+instance funLike {V W : SemiNormedGroupCat} : NDFunLike (V ⟶ W) V W where
   coe := (forget SemiNormedGroupCat).map
   coe_injective' := fun f g h => by cases f; cases g; congr
+
+instance toAddMonoidHomClass {V W : SemiNormedGroupCat} : AddMonoidHomClass (V ⟶ W) V W where
   map_add f := f.map_add'
   map_zero f := (AddMonoidHom.mk' f.toFun f.map_add').map_zero
 

Mathlib/Analysis/Normed/Ring/Seminorm.lean

@@ -78,24 +78,22 @@ section NonUnitalRing
 
 variable [NonUnitalRing R]
 
-instance ringSeminormClass : RingSeminormClass (RingSeminorm R) R ℝ where
+instance funLike : NDFunLike (RingSeminorm R) R ℝ where
   coe f := f.toFun
   coe_injective' f g h := by
     cases f
     cases g
     congr
     ext x
     exact congr_fun h x
+
+instance ringSeminormClass : RingSeminormClass (RingSeminorm R) R ℝ where
   map_zero f := f.map_zero'
   map_add_le_add f := f.add_le'
   map_mul_le_mul f := f.mul_le'
   map_neg_eq_map f := f.neg'
 #align ring_seminorm.ring_seminorm_class RingSeminorm.ringSeminormClass
 
-/-- Helper instance for when there's too many metavariables to apply `FunLike.hasCoeToFun`. -/
-instance : CoeFun (RingSeminorm R) fun _ => R → ℝ :=
-  FunLike.hasCoeToFun
-
 @[simp]
 theorem toFun_eq_coe (p : RingSeminorm R) : (p.toAddGroupSeminorm : R → ℝ) = p :=
   rfl
@@ -176,29 +174,26 @@ namespace RingNorm
 
 variable [NonUnitalRing R]
 
-instance ringNormClass : RingNormClass (RingNorm R) R ℝ where
+instance funLike : NDFunLike (RingNorm R) R ℝ where
   coe f := f.toFun
   coe_injective' f g h := by
     cases f
     cases g
     congr
     ext x
     exact congr_fun h x
+
+instance ringNormClass : RingNormClass (RingNorm R) R ℝ where
   map_zero f := f.map_zero'
   map_add_le_add f := f.add_le'
   map_mul_le_mul f := f.mul_le'
   map_neg_eq_map f := f.neg'
   eq_zero_of_map_eq_zero f := f.eq_zero_of_map_eq_zero' _
 #align ring_norm.ring_norm_class RingNorm.ringNormClass
 
-/-- Helper instance for when there's too many metavariables to apply `FunLike.hasCoeToFun`. -/
-instance : CoeFun (RingNorm R) fun _ => R → ℝ :=
-  ⟨fun p => p.toFun⟩
-
--- Porting note: This is a syntactic tautology in Lean 4
--- @[simp]
--- theorem toFun_eq_coe (p : RingNorm R) : p.toFun = p := rfl
-#noalign ring_norm.to_fun_eq_coe
+-- Porting note: This is no longer `@[simp]` in Lean 4
+theorem toFun_eq_coe (p : RingNorm R) : p.toFun = p := rfl
+#align ring_norm.to_fun_eq_coe RingNorm.toFun_eq_coe
 
 @[ext]
 theorem ext {p q : RingNorm R} : (∀ x, p x = q x) → p = q :=
@@ -226,25 +221,23 @@ namespace MulRingSeminorm
 
 variable [NonAssocRing R]
 
-instance mulRingSeminormClass : MulRingSeminormClass (MulRingSeminorm R) R ℝ where
+instance funLike : NDFunLike (MulRingSeminorm R) R ℝ where
   coe f := f.toFun
   coe_injective' f g h := by
     cases f
     cases g
     congr
     ext x
     exact congr_fun h x
+
+instance mulRingSeminormClass : MulRingSeminormClass (MulRingSeminorm R) R ℝ where
   map_zero f := f.map_zero'
   map_one f := f.map_one'
   map_add_le_add f := f.add_le'
   map_mul f := f.map_mul'
   map_neg_eq_map f := f.neg'
 #align mul_ring_seminorm.mul_ring_seminorm_class MulRingSeminorm.mulRingSeminormClass
 
-/-- Helper instance for when there's too many metavariables to apply `FunLike.hasCoeToFun`. -/
-instance : CoeFun (MulRingSeminorm R) fun _ => R → ℝ :=
-  FunLike.hasCoeToFun
-
 @[simp]
 theorem toFun_eq_coe (p : MulRingSeminorm R) : (p.toAddGroupSeminorm : R → ℝ) = p :=
   rfl
@@ -283,14 +276,16 @@ namespace MulRingNorm
 
 variable [NonAssocRing R]
 
-instance mulRingNormClass : MulRingNormClass (MulRingNorm R) R ℝ where
+instance funLike : NDFunLike (MulRingNorm R) R ℝ where
   coe f := f.toFun
   coe_injective' f g h := by
     cases f
     cases g
     congr
     ext x
     exact congr_fun h x
+
+instance mulRingNormClass : MulRingNormClass (MulRingNorm R) R ℝ where
   map_zero f := f.map_zero'
   map_one f := f.map_one'
   map_add_le_add f := f.add_le'
@@ -299,14 +294,9 @@ instance mulRingNormClass : MulRingNormClass (MulRingNorm R) R ℝ where
   eq_zero_of_map_eq_zero f := f.eq_zero_of_map_eq_zero' _
 #align mul_ring_norm.mul_ring_norm_class MulRingNorm.mulRingNormClass
 
-/-- Helper instance for when there's too many metavariables to apply `FunLike.hasCoeToFun`. -/
-instance : CoeFun (MulRingNorm R) fun _ => R → ℝ :=
-  ⟨fun p => p.toFun⟩
-
--- Porting note: This is a syntactic tautology in Lean 4
--- @[simp]
--- theorem toFun_eq_coe (p : MulRingNorm R) : p.toFun = p := rfl
-#noalign mul_ring_norm.to_fun_eq_coe
+-- Porting note: This no longer in `@[simp]`-normal form in Lean 4
+theorem toFun_eq_coe (p : MulRingNorm R) : p.toFun = p := rfl
+#align mul_ring_norm.to_fun_eq_coe MulRingNorm.toFun_eq_coe
 
 @[ext]
 theorem ext {p q : MulRingNorm R} : (∀ x, p x = q x) → p = q :=

Mathlib/Analysis/NormedSpace/Basic.lean

@@ -526,7 +526,8 @@ end NormedAlgebra
 See note [reducible non-instances] -/
 @[reducible]
 def NormedAlgebra.induced {F : Type*} (α β γ : Type*) [NormedField α] [Ring β] [Algebra α β]
-    [SeminormedRing γ] [NormedAlgebra α γ] [NonUnitalAlgHomClass F α β γ] (f : F) :
+    [SeminormedRing γ] [NormedAlgebra α γ] [NDFunLike F β γ] [NonUnitalAlgHomClass F α β γ]
+    (f : F) :
     @NormedAlgebra α β _ (SeminormedRing.induced β γ f) := by
   -- Porting note: trouble with SeminormedRing β, Algebra α β, and unfolding seminorm
   refine @NormedAlgebra.mk (𝕜 := α) (𝕜' := β) _ ?_ ?_ ?_
@@ -539,7 +540,7 @@ def NormedAlgebra.induced {F : Type*} (α β γ : Type*) [NormedField α] [Ring
 -- Porting note: failed to synth NonunitalAlgHomClass
 instance Subalgebra.toNormedAlgebra {𝕜 A : Type*} [SeminormedRing A] [NormedField 𝕜]
     [NormedAlgebra 𝕜 A] (S : Subalgebra 𝕜 A) : NormedAlgebra 𝕜 S :=
-  @NormedAlgebra.induced _ 𝕜 S A _ (SubringClass.toRing S) _ _ _ _ S.val
+  @NormedAlgebra.induced _ 𝕜 S A _ (SubringClass.toRing S) _ _ _ _ _ S.val
 #align subalgebra.to_normed_algebra Subalgebra.toNormedAlgebra
 
 section RestrictScalars