From 59c46b509141d1e80362d7a0551717bdd7b25144 Mon Sep 17 00:00:00 2001 From: Vierkantor Date: Thu, 23 Nov 2023 15:28:46 +0000 Subject: [PATCH] Fixes --- Mathlib/Algebra/Algebra/Spectrum.lean | 6 +-- .../Algebra/Subalgebra/Unitization.lean | 15 ++++-- .../Algebra/Category/AlgebraCat/Basic.lean | 3 ++ .../Algebra/Category/AlgebraCat/Limits.lean | 4 +- .../Category/ModuleCat/Monoidal/Closed.lean | 4 +- Mathlib/Algebra/Lie/Basic.lean | 4 ++ Mathlib/Algebra/Order/Hom/Basic.lean | 16 +++---- Mathlib/Analysis/Normed/Field/Basic.lean | 3 +- Mathlib/Analysis/Normed/Group/Hom.lean | 10 ++-- .../Normed/Group/SemiNormedGroupCat.lean | 4 +- Mathlib/Analysis/Normed/Ring/Seminorm.lean | 46 ++++++++----------- Mathlib/Analysis/NormedSpace/Basic.lean | 5 +- .../Analysis/NormedSpace/LinearIsometry.lean | 15 +++--- Mathlib/Analysis/NormedSpace/Star/Basic.lean | 2 +- Mathlib/Analysis/Seminorm.lean | 10 ++-- Mathlib/Data/Complex/Exponential.lean | 4 +- Mathlib/Data/MvPolynomial/Division.lean | 2 +- Mathlib/Data/Polynomial/AlgebraMap.lean | 3 +- .../RotationNumber/TranslationNumber.lean | 4 +- Mathlib/FieldTheory/RatFunc.lean | 15 +++--- Mathlib/GroupTheory/Exponent.lean | 3 +- Mathlib/LinearAlgebra/Eigenspace/Basic.lean | 2 +- Mathlib/LinearAlgebra/FiniteDimensional.lean | 2 +- .../LinearAlgebra/QuadraticForm/Basic.lean | 2 +- .../TensorProduct/RightExactness.lean | 8 ++-- .../MeasureTheory/MeasurableSpace/Basic.lean | 5 ++ .../LegendreSymbol/MulCharacter.lean | 6 ++- Mathlib/RingTheory/Artinian.lean | 3 +- .../RingTheory/Derivation/ToSquareZero.lean | 5 +- Mathlib/RingTheory/Ideal/Prod.lean | 8 ++-- .../RingTheory/Ideal/QuotientOperations.lean | 13 ++---- Mathlib/RingTheory/Nilpotent.lean | 10 ++-- Mathlib/RingTheory/Polynomial/Basic.lean | 2 +- .../Topology/Algebra/ContinuousAffineMap.lean | 9 ++-- .../Topology/Algebra/InfiniteSum/Basic.lean | 13 +++--- .../Topology/Algebra/Module/Alternating.lean | 4 +- .../Algebra/Module/CharacterSpace.lean | 8 ++-- .../Topology/Algebra/Module/Multilinear.lean | 5 +- Mathlib/Topology/Algebra/Module/WeakDual.lean | 4 -- Mathlib/Topology/Algebra/StarSubalgebra.lean | 9 +++- Mathlib/Topology/Homotopy/HomotopyGroup.lean | 2 +- .../Topology/Instances/RealVectorSpace.lean | 3 +- 42 files changed, 164 insertions(+), 137 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Spectrum.lean b/Mathlib/Algebra/Algebra/Spectrum.lean index 7b7906e1571abf..b50797689903fb 100644 --- a/Mathlib/Algebra/Algebra/Spectrum.lean +++ b/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 diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean b/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean index 9792a9232f75c3..407753c51da3ed 100644 --- a/Mathlib/Algebra/Algebra/Subalgebra/Unitization.lean +++ b/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' diff --git a/Mathlib/Algebra/Category/AlgebraCat/Basic.lean b/Mathlib/Algebra/Category/AlgebraCat/Basic.lean index 9c910e9de3b6ee..d00eb35c4f70dd 100644 --- a/Mathlib/Algebra/Category/AlgebraCat/Basic.lean +++ b/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 diff --git a/Mathlib/Algebra/Category/AlgebraCat/Limits.lean b/Mathlib/Algebra/Category/AlgebraCat/Limits.lean index 3fce38163c59ac..c372ce0f50fc31 100644 --- a/Mathlib/Algebra/Category/AlgebraCat/Limits.lean +++ b/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] diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean index b58421dd4d2b1c..8d28386bd7cd0e 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean +++ b/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 diff --git a/Mathlib/Algebra/Lie/Basic.lean b/Mathlib/Algebra/Lie/Basic.lean index 441ab5d2e19a52..3205e41e7b8862 100644 --- a/Mathlib/Algebra/Lie/Basic.lean +++ b/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 diff --git a/Mathlib/Algebra/Order/Hom/Basic.lean b/Mathlib/Algebra/Order/Hom/Basic.lean index 4aaa3ea5f96032..44c7cc07e3e909 100644 --- a/Mathlib/Algebra/Order/Hom/Basic.lean +++ b/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,14 +314,14 @@ 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 @@ -329,7 +329,7 @@ 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 @@ -337,7 +337,7 @@ 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] diff --git a/Mathlib/Analysis/Normed/Field/Basic.lean b/Mathlib/Analysis/Normed/Field/Basic.lean index 3e2df65f094d9e..d56ce9c33e2016 100644 --- a/Mathlib/Analysis/Normed/Field/Basic.lean +++ b/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 diff --git a/Mathlib/Analysis/Normed/Group/Hom.lean b/Mathlib/Analysis/Normed/Group/Hom.lean index 462b117c6022d4..10784ef48d30e3 100644 --- a/Mathlib/Analysis/Normed/Group/Hom.lean +++ b/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 diff --git a/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean b/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean index 628a23e7cc11f4..99d109a14f2457 100644 --- a/Mathlib/Analysis/Normed/Group/SemiNormedGroupCat.lean +++ b/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 diff --git a/Mathlib/Analysis/Normed/Ring/Seminorm.lean b/Mathlib/Analysis/Normed/Ring/Seminorm.lean index 7f494e762968fc..f67a431f1c055f 100644 --- a/Mathlib/Analysis/Normed/Ring/Seminorm.lean +++ b/Mathlib/Analysis/Normed/Ring/Seminorm.lean @@ -78,7 +78,7 @@ 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 @@ -86,16 +86,14 @@ instance ringSeminormClass : RingSeminormClass (RingSeminorm R) R ℝ where 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,7 +174,7 @@ 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 @@ -184,6 +182,8 @@ instance ringNormClass : RingNormClass (RingNorm R) R ℝ where 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' @@ -191,14 +191,9 @@ instance ringNormClass : RingNormClass (RingNorm R) R ℝ where 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,7 +221,7 @@ 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 @@ -234,6 +229,8 @@ instance mulRingSeminormClass : MulRingSeminormClass (MulRingSeminorm R) R ℝ w 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' @@ -241,10 +238,6 @@ instance mulRingSeminormClass : MulRingSeminormClass (MulRingSeminorm R) R ℝ w 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,7 +276,7 @@ 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 @@ -291,6 +284,8 @@ instance mulRingNormClass : MulRingNormClass (MulRingNorm R) R ℝ where 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 := diff --git a/Mathlib/Analysis/NormedSpace/Basic.lean b/Mathlib/Analysis/NormedSpace/Basic.lean index 6eea6485dc2c86..c0d3d8abf21a9b 100644 --- a/Mathlib/Analysis/NormedSpace/Basic.lean +++ b/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 diff --git a/Mathlib/Analysis/NormedSpace/LinearIsometry.lean b/Mathlib/Analysis/NormedSpace/LinearIsometry.lean index 64815cc752a59d..a468425539aa82 100644 --- a/Mathlib/Analysis/NormedSpace/LinearIsometry.lean +++ b/Mathlib/Analysis/NormedSpace/LinearIsometry.lean @@ -142,20 +142,15 @@ theorem toLinearMap_inj {f g : E →ₛₗᵢ[σ₁₂] E₂} : f.toLinearMap = toLinearMap_injective.eq_iff #align linear_isometry.to_linear_map_inj LinearIsometry.toLinearMap_inj -instance : SemilinearIsometryClass (E →ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂ where +instance : NDFunLike (E →ₛₗᵢ[σ₁₂] E₂) E E₂ where coe f := f.toFun coe_injective' _ _ h := toLinearMap_injective (FunLike.coe_injective h) + +instance : SemilinearIsometryClass (E →ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂ where map_add f := map_add f.toLinearMap map_smulₛₗ f := map_smulₛₗ f.toLinearMap norm_map f := f.norm_map' --- porting note: These helper instances are unhelpful in Lean 4, so omitting: --- /-- Helper instance for when there's too many metavariables to apply `FunLike.has_coe_to_fun` --- directly. --- -/ --- instance : CoeFun (E →ₛₗᵢ[σ₁₂] E₂) fun _ => E → E₂ := --- ⟨fun f => f.toFun⟩ - @[simp] theorem coe_toLinearMap : ⇑f.toLinearMap = f := rfl @@ -543,7 +538,7 @@ theorem toLinearEquiv_inj {f g : E ≃ₛₗᵢ[σ₁₂] E₂} : f.toLinearEqui toLinearEquiv_injective.eq_iff #align linear_isometry_equiv.to_linear_equiv_inj LinearIsometryEquiv.toLinearEquiv_inj -instance : SemilinearIsometryEquivClass (E ≃ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂ where +instance : EquivLike (E ≃ₛₗᵢ[σ₁₂] E₂) E E₂ where coe e := e.toFun inv e := e.invFun coe_injective' f g h₁ h₂ := by @@ -555,6 +550,8 @@ instance : SemilinearIsometryEquivClass (E ≃ₛₗᵢ[σ₁₂] E₂) σ₁₂ congr left_inv e := e.left_inv right_inv e := e.right_inv + +instance : SemilinearIsometryEquivClass (E ≃ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂ where map_add f := map_add f.toLinearEquiv map_smulₛₗ e := map_smulₛₗ e.toLinearEquiv norm_map e := e.norm_map' diff --git a/Mathlib/Analysis/NormedSpace/Star/Basic.lean b/Mathlib/Analysis/NormedSpace/Star/Basic.lean index cdb579d99aa64a..5bc27af1fd1a46 100644 --- a/Mathlib/Analysis/NormedSpace/Star/Basic.lean +++ b/Mathlib/Analysis/NormedSpace/Star/Basic.lean @@ -317,7 +317,7 @@ namespace StarSubalgebra instance toNormedAlgebra {𝕜 A : Type*} [NormedField 𝕜] [StarRing 𝕜] [SeminormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [StarModule 𝕜 A] (S : StarSubalgebra 𝕜 A) : NormedAlgebra 𝕜 S := - @NormedAlgebra.induced _ 𝕜 S A _ (SubringClass.toRing S) S.algebra _ _ _ S.subtype + @NormedAlgebra.induced _ 𝕜 S A _ (SubringClass.toRing S) S.algebra _ _ _ _ S.subtype #align star_subalgebra.to_normed_algebra StarSubalgebra.toNormedAlgebra instance to_cstarRing {R A} [CommRing R] [StarRing R] [NormedRing A] [StarRing A] [CstarRing A] diff --git a/Mathlib/Analysis/Seminorm.lean b/Mathlib/Analysis/Seminorm.lean index f2bb0a774471c7..c7acda447a680d 100644 --- a/Mathlib/Analysis/Seminorm.lean +++ b/Mathlib/Analysis/Seminorm.lean @@ -59,7 +59,7 @@ attribute [nolint docBlame] Seminorm.toAddGroupSeminorm You should extend this class when you extend `Seminorm`. -/ class SeminormClass (F : Type*) (𝕜 E : outParam <| Type*) [SeminormedRing 𝕜] [AddGroup E] - [SMul 𝕜 E] extends AddGroupSeminormClass F E ℝ where + [SMul 𝕜 E] [NDFunLike F E ℝ] extends AddGroupSeminormClass F E ℝ : Prop where /-- The seminorm of a scalar multiplication is the product of the absolute value of the scalar and the original seminorm. -/ map_smul_eq_mul (f : F) (a : 𝕜) (x : E) : f (a • x) = ‖a‖ * f x @@ -117,22 +117,20 @@ section SMul variable [SMul 𝕜 E] -instance instSeminormClass : SeminormClass (Seminorm 𝕜 E) 𝕜 E where +instance instFunLike : NDFunLike (Seminorm 𝕜 E) E ℝ where coe f := f.toFun coe_injective' f g h := by rcases f with ⟨⟨_⟩⟩ rcases g with ⟨⟨_⟩⟩ congr + +instance instSeminormClass : SeminormClass (Seminorm 𝕜 E) 𝕜 E where map_zero f := f.map_zero' map_add_le_add f := f.add_le' map_neg_eq_map f := f.neg' map_smul_eq_mul f := f.smul' #align seminorm.seminorm_class Seminorm.instSeminormClass -/-- Helper instance for when there's too many metavariables to apply `FunLike.hasCoeToFun`. -/ -instance instCoeFun : CoeFun (Seminorm 𝕜 E) fun _ => E → ℝ := - FunLike.hasCoeToFun - @[ext] theorem ext {p q : Seminorm 𝕜 E} (h : ∀ x, (p : E → ℝ) x = q x) : p = q := FunLike.ext p q h diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean index 27616587f1ad91..d02eb5da74eee0 100644 --- a/Mathlib/Data/Complex/Exponential.lean +++ b/Mathlib/Data/Complex/Exponential.lean @@ -538,7 +538,7 @@ theorem exp_multiset_sum (s : Multiset ℂ) : exp s.sum = (s.map exp).prod := theorem exp_sum {α : Type*} (s : Finset α) (f : α → ℂ) : exp (∑ x in s, f x) = ∏ x in s, exp (f x) := - @map_prod (Multiplicative ℂ) α ℂ _ _ _ _ expMonoidHom f s + map_prod (β := Multiplicative ℂ) expMonoidHom f s #align complex.exp_sum Complex.exp_sum theorem exp_nat_mul (x : ℂ) : ∀ n : ℕ, exp (n * x) = exp x ^ n @@ -1156,7 +1156,7 @@ theorem exp_multiset_sum (s : Multiset ℝ) : exp s.sum = (s.map exp).prod := theorem exp_sum {α : Type*} (s : Finset α) (f : α → ℝ) : exp (∑ x in s, f x) = ∏ x in s, exp (f x) := - @map_prod (Multiplicative ℝ) α ℝ _ _ _ _ expMonoidHom f s + map_prod (β := Multiplicative ℝ) expMonoidHom f s #align real.exp_sum Real.exp_sum nonrec theorem exp_nat_mul (x : ℝ) (n : ℕ) : exp (n * x) = exp x ^ n := diff --git a/Mathlib/Data/MvPolynomial/Division.lean b/Mathlib/Data/MvPolynomial/Division.lean index 634ae6990b14a2..4f5be172677908 100644 --- a/Mathlib/Data/MvPolynomial/Division.lean +++ b/Mathlib/Data/MvPolynomial/Division.lean @@ -70,7 +70,7 @@ theorem divMonomial_zero (x : MvPolynomial σ R) : x /ᵐᵒⁿᵒᵐⁱᵃˡ 0 theorem add_divMonomial (x y : MvPolynomial σ R) (s : σ →₀ ℕ) : (x + y) /ᵐᵒⁿᵒᵐⁱᵃˡ s = x /ᵐᵒⁿᵒᵐⁱᵃˡ s + y /ᵐᵒⁿᵒᵐⁱᵃˡ s := - map_add _ _ _ + map_add (N := _ →₀ _) _ _ _ #align mv_polynomial.add_div_monomial MvPolynomial.add_divMonomial theorem divMonomial_add (a b : σ →₀ ℕ) (x : MvPolynomial σ R) : diff --git a/Mathlib/Data/Polynomial/AlgebraMap.lean b/Mathlib/Data/Polynomial/AlgebraMap.lean index 9ec2c525cbf9b2..df2b82a6230d3e 100644 --- a/Mathlib/Data/Polynomial/AlgebraMap.lean +++ b/Mathlib/Data/Polynomial/AlgebraMap.lean @@ -281,7 +281,8 @@ theorem eval_unique (φ : R[X] →ₐ[R] A) (p) : φ p = eval₂ (algebraMap R A rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id] #align polynomial.eval_unique Polynomial.eval_unique -theorem aeval_algHom_apply {F : Type*} [AlgHomClass F R A B] (f : F) (x : A) (p : R[X]) : +theorem aeval_algHom_apply {F : Type*} [NDFunLike F A B] [AlgHomClass F R A B] + (f : F) (x : A) (p : R[X]) : aeval (f x) p = f (aeval x p) := by refine' Polynomial.induction_on p (by simp [AlgHomClass.commutes]) (fun p q hp hq => _) (by simp [AlgHomClass.commutes]) diff --git a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean index 320e0c9ba1773e..096d507277bf42 100644 --- a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean +++ b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean @@ -133,9 +133,11 @@ structure CircleDeg1Lift extends ℝ →o ℝ : Type where namespace CircleDeg1Lift -instance : OrderHomClass CircleDeg1Lift ℝ ℝ where +instance : NDFunLike CircleDeg1Lift ℝ ℝ where coe f := f.toFun coe_injective' | ⟨⟨_, _⟩, _⟩, ⟨⟨_, _⟩, _⟩, rfl => rfl + +instance : OrderHomClass CircleDeg1Lift ℝ ℝ where map_rel f _ _ h := f.monotone' h @[simp] theorem coe_mk (f h) : ⇑(mk f h) = f := rfl diff --git a/Mathlib/FieldTheory/RatFunc.lean b/Mathlib/FieldTheory/RatFunc.lean index 643ca0dd850d03..5ba5b0f86d907a 100644 --- a/Mathlib/FieldTheory/RatFunc.lean +++ b/Mathlib/FieldTheory/RatFunc.lean @@ -598,6 +598,7 @@ variable {K} section LiftHom variable {G₀ L R S F : Type*} [CommGroupWithZero G₀] [Field L] [CommRing R] [CommRing S] +variable [NDFunLike F R[X] S[X]] /-- Lift a monoid homomorphism that maps polynomials `φ : R[X] →* S[X]` to a `RatFunc R →* RatFunc S`, @@ -689,7 +690,6 @@ theorem coe_mapRingHom_eq_coe_map [RingHomClass F R[X] S[X]] (φ : F) (hφ : R[X rfl #align ratfunc.coe_map_ring_hom_eq_coe_map RatFunc.coe_mapRingHom_eq_coe_map -set_option maxHeartbeats 300000 in -- TODO: Generalize to `FunLike` classes, /-- Lift a monoid with zero homomorphism `R[X] →*₀ G₀` to a `RatFunc R →*₀ G₀` on the condition that `φ` maps non zero divisors to non zero divisors, @@ -846,7 +846,8 @@ theorem algebraMap_apply {R : Type*} [CommSemiring R] [Algebra R K[X]] (x : R) : rfl #align ratfunc.algebra_map_apply RatFunc.algebraMap_apply -theorem map_apply_div_ne_zero {R F : Type*} [CommRing R] [IsDomain R] [MonoidHomClass F K[X] R[X]] +theorem map_apply_div_ne_zero {R F : Type*} [CommRing R] [IsDomain R] + [NDFunLike F K[X] R[X]] [MonoidHomClass F K[X] R[X]] (φ : F) (hφ : K[X]⁰ ≤ R[X]⁰.comap φ) (p q : K[X]) (hq : q ≠ 0) : map φ hφ (algebraMap _ _ p / algebraMap _ _ q) = algebraMap _ _ (φ p) / algebraMap _ _ (φ q) := by @@ -856,7 +857,8 @@ theorem map_apply_div_ne_zero {R F : Type*} [CommRing R] [IsDomain R] [MonoidHom #align ratfunc.map_apply_div_ne_zero RatFunc.map_apply_div_ne_zero @[simp] -theorem map_apply_div {R F : Type*} [CommRing R] [IsDomain R] [MonoidWithZeroHomClass F K[X] R[X]] +theorem map_apply_div {R F : Type*} [CommRing R] [IsDomain R] + [NDFunLike F K[X] R[X]] [MonoidWithZeroHomClass F K[X] R[X]] (φ : F) (hφ : K[X]⁰ ≤ R[X]⁰.comap φ) (p q : K[X]) : map φ hφ (algebraMap _ _ p / algebraMap _ _ q) = algebraMap _ _ (φ p) / algebraMap _ _ (φ q) := by @@ -1333,12 +1335,13 @@ theorem denom_add_dvd (x y : RatFunc K) : denom (x + y) ∣ denom x * denom y := · exact algebraMap_ne_zero (denom_ne_zero y) #align ratfunc.denom_add_dvd RatFunc.denom_add_dvd -theorem map_denom_ne_zero {L F : Type*} [Zero L] [ZeroHomClass F K[X] L] (φ : F) - (hφ : Function.Injective φ) (f : RatFunc K) : φ f.denom ≠ 0 := fun H => +theorem map_denom_ne_zero {L F : Type*} [Zero L] [NDFunLike F K[X] L] [ZeroHomClass F K[X] L] + (φ : F) (hφ : Function.Injective φ) (f : RatFunc K) : φ f.denom ≠ 0 := fun H => (denom_ne_zero f) ((map_eq_zero_iff φ hφ).mp H) #align ratfunc.map_denom_ne_zero RatFunc.map_denom_ne_zero -theorem map_apply {R F : Type*} [CommRing R] [IsDomain R] [MonoidHomClass F K[X] R[X]] (φ : F) +theorem map_apply {R F : Type*} [CommRing R] [IsDomain R] + [NDFunLike F K[X] R[X]] [MonoidHomClass F K[X] R[X]] (φ : F) (hφ : K[X]⁰ ≤ R[X]⁰.comap φ) (f : RatFunc K) : map φ hφ f = algebraMap _ _ (φ f.num) / algebraMap _ _ (φ f.denom) := by rw [← num_div_denom f, map_apply_div_ne_zero, num_div_denom f] diff --git a/Mathlib/GroupTheory/Exponent.lean b/Mathlib/GroupTheory/Exponent.lean index cea2702876a3c8..746427214046e5 100644 --- a/Mathlib/GroupTheory/Exponent.lean +++ b/Mathlib/GroupTheory/Exponent.lean @@ -424,7 +424,8 @@ theorem Monoid.exponent_pi_eq_zero {ι : Type*} {M : ι → Type*} [∀ i, Monoi /-- If `f : M₁ →⋆ M₂` is surjective, then the exponent of `M₂` divides the exponent of `M₁`. -/ @[to_additive] -theorem MonoidHom.exponent_dvd {F M₁ M₂ : Type*} [Monoid M₁] [Monoid M₂] [MonoidHomClass F M₁ M₂] +theorem MonoidHom.exponent_dvd {F M₁ M₂ : Type*} [Monoid M₁] [Monoid M₂] + [NDFunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] {f : F} (hf : Function.Surjective f) : exponent M₂ ∣ exponent M₁ := by refine Monoid.exponent_dvd_of_forall_pow_eq_one M₂ _ fun m₂ ↦ ?_ obtain ⟨m₁, rfl⟩ := hf m₂ diff --git a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean index 81b691bc98ce34..f176a86bba281e 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean @@ -337,7 +337,7 @@ lemma disjoint_generalizedEigenspace [NoZeroSMulDivisors R M] · ext; simp [smul_sub, sub_sub, smul_comm μ₁, add_sub_left_comm] all_goals ext ⟨x, _, _⟩; simpa [LinearMap.restrict_apply, LinearMap.pow_restrict _] using ‹_› have hf₁₂ : f₂ - f₁ = algebraMap R (End R p) (μ₁ - μ₂) := by ext; simp [sub_smul] - rw [hf₁₂, IsNilpotent.map_iff (NoZeroSMulDivisors.algebraMap_injective _ _), + rw [hf₁₂, IsNilpotent.map_iff (NoZeroSMulDivisors.algebraMap_injective R (End R p)), isNilpotent_iff_eq_zero, sub_eq_zero] at this contradiction diff --git a/Mathlib/LinearAlgebra/FiniteDimensional.lean b/Mathlib/LinearAlgebra/FiniteDimensional.lean index 99d2725ee88d68..ef9529989520f6 100644 --- a/Mathlib/LinearAlgebra/FiniteDimensional.lean +++ b/Mathlib/LinearAlgebra/FiniteDimensional.lean @@ -371,7 +371,7 @@ theorem _root_.Submodule.eq_top_of_finrank_eq [FiniteDimensional K V] {S : Submo span_image] have := bS.span_eq rw [bS_eq, Basis.coe_ofVectorSpace, Subtype.range_coe] at this - rw [this, map_top (Submodule.subtype S), range_subtype] + rw [this, Submodule.map_top (Submodule.subtype S), range_subtype] #align finite_dimensional.eq_top_of_finrank_eq Submodule.eq_top_of_finrank_eq #align submodule.eq_top_of_finrank_eq Submodule.eq_top_of_finrank_eq diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 6ade80c39662c1..3941e29248f676 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -123,7 +123,7 @@ theorem polar_add_left_iff {f : M → R} {x x' y : M} : add_right_comm (f (x + y)), add_left_inj] #align quadratic_form.polar_add_left_iff QuadraticForm.polar_add_left_iff -theorem polar_comp {F : Type*} [CommRing S] [AddMonoidHomClass F R S] +theorem polar_comp {F : Type*} [CommRing S] [NDFunLike F R S] [AddMonoidHomClass F R S] (f : M → R) (g : F) (x y : M) : polar (g ∘ f) x y = g (polar f x y) := by simp only [polar, Pi.smul_apply, Function.comp_apply, map_sub] diff --git a/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean b/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean index 9397932378d0f3..541072ebcdc69c 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean @@ -460,7 +460,8 @@ lemma Ideal.map_includeLeft_eq (I : Ideal A) : Submodule.mem_toAddSubmonoid, Submodule.restrictScalars_mem] rw [this] apply Ideal.mul_mem_left - apply Ideal.mem_map_of_mem + -- Note: adding `includeLeft` as a hint fixes a timeout + apply Ideal.mem_map_of_mem includeLeft exact Submodule.coe_mem a simp only [Submodule.coe_restrictScalars, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul] @@ -527,7 +528,8 @@ lemma Ideal.map_includeRight_eq (I : Ideal B) : simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, Submodule.mem_toAddSubmonoid, Submodule.restrictScalars_mem] apply Ideal.mul_mem_left - apply Ideal.mem_map_of_mem + -- Note: adding `includeRight` as a hint fixes a timeout + apply Ideal.mem_map_of_mem includeRight exact Submodule.coe_mem b simp only [Submodule.coe_restrictScalars, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul] @@ -580,7 +582,7 @@ theorem Algebra.TensorProduct.map_ker (hf : Function.Surjective f) (hg : Functio simp only [← AlgHom.coe_ker] -- apply one step of exactness rw [← Algebra.TensorProduct.lTensor_ker _ hg, RingHom.ker_eq_comap_bot (map (AlgHom.id R A) g)] - rw [← Ideal.comap_map_of_surjective _ (lTensor.surjective A hg)] + rw [← Ideal.comap_map_of_surjective (map (AlgHom.id R A) g) (lTensor.surjective A hg)] -- apply the other step of exactness rw [Algebra.TensorProduct.rTensor_ker _ hf] apply congr_arg₂ _ rfl diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean index ba5a37cd8ba250..36ae6fc87c85ed 100644 --- a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean +++ b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean @@ -1300,6 +1300,11 @@ instance instEquivLike : EquivLike (α ≃ᵐ β) α β where right_inv e := e.toEquiv.right_inv coe_injective' _ _ he _ := toEquiv_injective <| FunLike.ext' he +/-- Helper instance for when the `EquivLike` instance is too hard to find. -/ +instance instFunLike : NDFunLike (α ≃ᵐ β) α β where + coe e := e.toEquiv + coe_injective' := FunLike.coe_injective + @[simp] theorem coe_toEquiv (e : α ≃ᵐ β) : (e.toEquiv : α → β) = e := rfl diff --git a/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean b/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean index d9bef5da10fd87..43dca7575d1927 100644 --- a/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean +++ b/Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean @@ -77,7 +77,7 @@ instance funLike : FunLike (MulChar R R') R (fun _ => R') := /-- This is the corresponding extension of `MonoidHomClass`. -/ class MulCharClass (F : Type*) (R R' : outParam <| Type*) [CommMonoid R] - [CommMonoidWithZero R'] extends MonoidHomClass F R R' where + [CommMonoidWithZero R'] [NDFunLike F R R'] extends MonoidHomClass F R R' : Prop where map_nonunit : ∀ (χ : F) {a : R} (_ : ¬IsUnit a), χ a = 0 #align mul_char_class MulCharClass @@ -132,9 +132,11 @@ theorem ext' {χ χ' : MulChar R R'} (h : ∀ a, χ a = χ' a) : χ = χ' := by exact MonoidHom.ext h #align mul_char.ext' MulChar.ext' -instance : MulCharClass (MulChar R R') R R' where +instance : NDFunLike (MulChar R R') R R' where coe χ := χ.toMonoidHom.toFun coe_injective' _ _ h := ext' fun a => congr_fun h a + +instance : MulCharClass (MulChar R R') R R' where map_mul χ := χ.map_mul' map_one χ := χ.map_one' map_nonunit χ := χ.map_nonunit' _ diff --git a/Mathlib/RingTheory/Artinian.lean b/Mathlib/RingTheory/Artinian.lean index f38041754f91ef..2749a61a97c8c8 100644 --- a/Mathlib/RingTheory/Artinian.lean +++ b/Mathlib/RingTheory/Artinian.lean @@ -408,7 +408,8 @@ theorem isArtinian_span_of_finite (R) {M} [Ring R] [AddCommGroup M] [Module R M] isArtinian_of_fg_of_artinian _ (Submodule.fg_def.mpr ⟨A, hA, rfl⟩) #align is_artinian_span_of_finite isArtinian_span_of_finite -theorem Function.Surjective.isArtinianRing {R} [Ring R] {S} [Ring S] {F} [RingHomClass F R S] +theorem Function.Surjective.isArtinianRing {R} [Ring R] {S} [Ring S] {F} + [NDFunLike F R S] [RingHomClass F R S] {f : F} (hf : Function.Surjective f) [H : IsArtinianRing R] : IsArtinianRing S := by rw [isArtinianRing_iff, isArtinian_iff_wellFounded] at H ⊢ exact (Ideal.orderEmbeddingOfSurjective f hf).wellFounded H diff --git a/Mathlib/RingTheory/Derivation/ToSquareZero.lean b/Mathlib/RingTheory/Derivation/ToSquareZero.lean index f8c32321e3b400..20de7426e0f758 100644 --- a/Mathlib/RingTheory/Derivation/ToSquareZero.lean +++ b/Mathlib/RingTheory/Derivation/ToSquareZero.lean @@ -85,7 +85,10 @@ def liftOfDerivationToSquareZero (f : Derivation R A I) : A →ₐ[R] B := { ((I.restrictScalars R).subtype.comp f.toLinearMap + (IsScalarTower.toAlgHom R A B).toLinearMap : A →ₗ[R] B) with toFun := fun x => f x + algebraMap A B x - map_one' := by dsimp; rw [map_one, f.map_one_eq_zero, Submodule.coe_zero, zero_add] + map_one' := by + dsimp + -- Note: added the `(algebraMap _ _)` hint because otherwise it would match `f 1` + rw [map_one (algebraMap _ _), f.map_one_eq_zero, Submodule.coe_zero, zero_add] map_mul' := fun x y => by have : (f x : B) * f y = 0 := by rw [← Ideal.mem_bot, ← hI, pow_two] diff --git a/Mathlib/RingTheory/Ideal/Prod.lean b/Mathlib/RingTheory/Ideal/Prod.lean index 981efa1608843d..a1113635a0270e 100644 --- a/Mathlib/RingTheory/Ideal/Prod.lean +++ b/Mathlib/RingTheory/Ideal/Prod.lean @@ -121,9 +121,10 @@ theorem isPrime_of_isPrime_prod_top {I : Ideal R} (h : (Ideal.prod I (⊤ : Idea theorem isPrime_of_isPrime_prod_top' {I : Ideal S} (h : (Ideal.prod (⊤ : Ideal R) I).IsPrime) : I.IsPrime := by - apply @isPrime_of_isPrime_prod_top _ R + apply isPrime_of_isPrime_prod_top (S := R) rw [← map_prodComm_prod] - exact map_isPrime_of_equiv _ + -- Note: couldn't synthesize the right instances without the `R` and `S` hints + exact map_isPrime_of_equiv (RingEquiv.prodComm (R := R) (S := S)) #align ideal.is_prime_of_is_prime_prod_top' Ideal.isPrime_of_isPrime_prod_top' theorem isPrime_ideal_prod_top {I : Ideal R} [h : I.IsPrime] : (prod I (⊤ : Ideal S)).IsPrime := by @@ -141,7 +142,8 @@ theorem isPrime_ideal_prod_top {I : Ideal R} [h : I.IsPrime] : (prod I (⊤ : Id theorem isPrime_ideal_prod_top' {I : Ideal S} [h : I.IsPrime] : (prod (⊤ : Ideal R) I).IsPrime := by letI : IsPrime (prod I (⊤ : Ideal R)) := isPrime_ideal_prod_top rw [← map_prodComm_prod] - apply map_isPrime_of_equiv _ + -- Note: couldn't synthesize the right instances without the `R` and `S` hints + exact map_isPrime_of_equiv (RingEquiv.prodComm (R := S) (S := R)) #align ideal.is_prime_ideal_prod_top' Ideal.isPrime_ideal_prod_top' theorem ideal_prod_prime_aux {I : Ideal R} {J : Ideal S} : diff --git a/Mathlib/RingTheory/Ideal/QuotientOperations.lean b/Mathlib/RingTheory/Ideal/QuotientOperations.lean index 4f8bb42d92710e..718b4cf641f25a 100644 --- a/Mathlib/RingTheory/Ideal/QuotientOperations.lean +++ b/Mathlib/RingTheory/Ideal/QuotientOperations.lean @@ -154,7 +154,7 @@ lemma ker_Pi_Quotient_mk {ι : Type*} (I : ι → Ideal R) : theorem bot_quotient_isMaximal_iff (I : Ideal R) : (⊥ : Ideal (R ⧸ I)).IsMaximal ↔ I.IsMaximal := ⟨fun hI => @mk_ker _ _ I ▸ - @comap_isMaximal_of_surjective _ _ _ _ _ _ (Quotient.mk I) Quotient.mk_surjective ⊥ hI, + comap_isMaximal_of_surjective (Quotient.mk I) Quotient.mk_surjective (K := ⊥) (H := hI), fun hI => by skip letI := Quotient.field I @@ -211,7 +211,6 @@ lemma quotientInfToPiQuotient_surj [Fintype ι] {I : ι → Ideal R} replace he : ∀ j, j ≠ i → e ∈ I j := by simpa using he refine ⟨e, ?_, ?_⟩ · simp [eq_sub_of_add_eq' hue, map_sub, eq_zero_iff_mem.mpr hu] - rfl · exact fun j hj ↦ eq_zero_iff_mem.mpr (he j hj) choose e he using key use mk _ (∑ i, f i*e i) @@ -478,12 +477,10 @@ theorem quotientMap_comp_mk {J : Ideal R} {I : Ideal S} {f : R →+* S} (H : J def quotientEquiv (I : Ideal R) (J : Ideal S) (f : R ≃+* S) (hIJ : J = I.map (f : R →+* S)) : R ⧸ I ≃+* S ⧸ J := { - quotientMap J (↑f) - (by - rw [hIJ] - exact - @le_comap_map _ S _ _ _ _ _ - _) with + quotientMap J (↑f) (by + rw [hIJ] + exact le_comap_map) + with invFun := quotientMap I (↑f.symm) (by diff --git a/Mathlib/RingTheory/Nilpotent.lean b/Mathlib/RingTheory/Nilpotent.lean index 727a2537c7cfe0..6ea3bbbd83d6c1 100644 --- a/Mathlib/RingTheory/Nilpotent.lean +++ b/Mathlib/RingTheory/Nilpotent.lean @@ -73,13 +73,14 @@ theorem isNilpotent_neg_iff [Ring R] : IsNilpotent (-x) ↔ IsNilpotent x := #align is_nilpotent_neg_iff isNilpotent_neg_iff theorem IsNilpotent.map [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type*} - [MonoidWithZeroHomClass F R S] (hr : IsNilpotent r) (f : F) : IsNilpotent (f r) := by + [NDFunLike F R S] [MonoidWithZeroHomClass F R S] (hr : IsNilpotent r) (f : F) : + IsNilpotent (f r) := by use hr.choose rw [← map_pow, hr.choose_spec, map_zero] #align is_nilpotent.map IsNilpotent.map lemma IsNilpotent.map_iff [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type*} - [MonoidWithZeroHomClass F R S] {f : F} (hf : Function.Injective f) : + [NDFunLike F R S] [MonoidWithZeroHomClass F R S] {f : F} (hf : Function.Injective f) : IsNilpotent (f r) ↔ IsNilpotent r := ⟨fun ⟨k, hk⟩ ↦ ⟨k, (map_eq_zero_iff f hf).mp <| by rwa [map_pow]⟩, fun h ↦ h.map f⟩ @@ -127,7 +128,8 @@ theorem isNilpotent_iff_eq_zero [MonoidWithZero R] [IsReduced R] : IsNilpotent x #align is_nilpotent_iff_eq_zero isNilpotent_iff_eq_zero theorem isReduced_of_injective [MonoidWithZero R] [MonoidWithZero S] {F : Type*} - [MonoidWithZeroHomClass F R S] (f : F) (hf : Function.Injective f) [IsReduced S] : + [NDFunLike F R S] [MonoidWithZeroHomClass F R S] + (f : F) (hf : Function.Injective f) [IsReduced S] : IsReduced R := by constructor intro x hx @@ -137,7 +139,7 @@ theorem isReduced_of_injective [MonoidWithZero R] [MonoidWithZero S] {F : Type*} #align is_reduced_of_injective isReduced_of_injective theorem RingHom.ker_isRadical_iff_reduced_of_surjective {S F} [CommSemiring R] [CommRing S] - [RingHomClass F R S] {f : F} (hf : Function.Surjective f) : + [NDFunLike F R S] [RingHomClass F R S] {f : F} (hf : Function.Surjective f) : (RingHom.ker f).IsRadical ↔ IsReduced S := by simp_rw [isReduced_iff, hf.forall, IsNilpotent, ← map_pow, ← RingHom.mem_ker] rfl diff --git a/Mathlib/RingTheory/Polynomial/Basic.lean b/Mathlib/RingTheory/Polynomial/Basic.lean index 873224e280a7cf..fc9081c3cf19e2 100644 --- a/Mathlib/RingTheory/Polynomial/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Basic.lean @@ -679,7 +679,7 @@ theorem isPrime_map_C_iff_isPrime (P : Ideal R) : -- `(Quotient.isDomain_iff_prime (map C P : Ideal R[X]))` constructor · intro H - have := @comap_isPrime R R[X] (R →+* R[X]) _ _ _ C (map C P) H + have := comap_isPrime C (map C P) convert this using 1 ext x simp only [mem_comap, mem_map_C_iff] diff --git a/Mathlib/Topology/Algebra/ContinuousAffineMap.lean b/Mathlib/Topology/Algebra/ContinuousAffineMap.lean index 2a3ec5062b95de..6f6b9d13026ccb 100644 --- a/Mathlib/Topology/Algebra/ContinuousAffineMap.lean +++ b/Mathlib/Topology/Algebra/ContinuousAffineMap.lean @@ -59,15 +59,12 @@ theorem to_affineMap_injective {f g : P →A[R] Q} (h : (f : P →ᵃ[R] Q) = (g congr #align continuous_affine_map.to_affine_map_injective ContinuousAffineMap.to_affineMap_injective -instance : ContinuousMapClass (P →A[R] Q) P Q where +instance : NDFunLike (P →A[R] Q) P Q where coe f := f.toAffineMap coe_injective' _ _ h := to_affineMap_injective <| FunLike.coe_injective h - map_continuous := cont -/-- Helper instance for when there's too many metavariables to apply -`FunLike.hasCoeToFun` directly. -/ -instance : CoeFun (P →A[R] Q) fun _ ↦ P → Q := - FunLike.hasCoeToFun +instance : ContinuousMapClass (P →A[R] Q) P Q where + map_continuous := cont theorem toFun_eq_coe (f : P →A[R] Q) : f.toFun = ⇑f := rfl #align continuous_affine_map.to_fun_eq_coe ContinuousAffineMap.toFun_eq_coe diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean index dc430ad6c00d9b..2bca814dc97466 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean @@ -273,7 +273,7 @@ theorem Equiv.summable_iff_of_support {g : γ → α} (e : support f ≃ support #align equiv.summable_iff_of_support Equiv.summable_iff_of_support protected theorem HasSum.map [AddCommMonoid γ] [TopologicalSpace γ] (hf : HasSum f a) {G} - [AddMonoidHomClass G α γ] (g : G) (hg : Continuous g) : HasSum (g ∘ f) (g a) := + [NDFunLike G α γ] [AddMonoidHomClass G α γ] (g : G) (hg : Continuous g) : HasSum (g ∘ f) (g a) := have : (g ∘ fun s : Finset β => ∑ b in s, f b) = fun s : Finset β => ∑ b in s, g (f b) := funext <| map_sum g _ show Tendsto (fun s : Finset β => ∑ b in s, g (f b)) atTop (𝓝 (g a)) from @@ -281,12 +281,13 @@ protected theorem HasSum.map [AddCommMonoid γ] [TopologicalSpace γ] (hf : HasS #align has_sum.map HasSum.map protected theorem Summable.map [AddCommMonoid γ] [TopologicalSpace γ] (hf : Summable f) {G} - [AddMonoidHomClass G α γ] (g : G) (hg : Continuous g) : Summable (g ∘ f) := + [NDFunLike G α γ] [AddMonoidHomClass G α γ] (g : G) (hg : Continuous g) : Summable (g ∘ f) := (hf.hasSum.map g hg).summable #align summable.map Summable.map protected theorem Summable.map_iff_of_leftInverse [AddCommMonoid γ] [TopologicalSpace γ] {G G'} - [AddMonoidHomClass G α γ] [AddMonoidHomClass G' γ α] (g : G) (g' : G') (hg : Continuous g) + [NDFunLike G α γ] [AddMonoidHomClass G α γ] [NDFunLike G' γ α] [AddMonoidHomClass G' γ α] + (g : G) (g' : G') (hg : Continuous g) (hg' : Continuous g') (hinv : Function.LeftInverse g' g) : Summable (g ∘ f) ↔ Summable f := ⟨fun h => by have := h.map _ hg' @@ -295,9 +296,9 @@ protected theorem Summable.map_iff_of_leftInverse [AddCommMonoid γ] [Topologica /-- A special case of `Summable.map_iff_of_leftInverse` for convenience -/ protected theorem Summable.map_iff_of_equiv [AddCommMonoid γ] [TopologicalSpace γ] {G} - [AddEquivClass G α γ] (g : G) (hg : Continuous g) - (hg' : Continuous (AddEquivClass.toEquivLike.inv g : γ → α)) : Summable (g ∘ f) ↔ Summable f := - Summable.map_iff_of_leftInverse g (g : α ≃+ γ).symm hg hg' (AddEquivClass.toEquivLike.left_inv g) + [EquivLike G α γ] [AddEquivClass G α γ] (g : G) (hg : Continuous g) + (hg' : Continuous (EquivLike.inv g : γ → α)) : Summable (g ∘ f) ↔ Summable f := + Summable.map_iff_of_leftInverse g (g : α ≃+ γ).symm hg hg' (EquivLike.left_inv g) #align summable.map_iff_of_equiv Summable.map_iff_of_equiv /-- If `f : ℕ → α` has sum `a`, then the partial sums `∑_{i=0}^{n-1} f i` converge to `a`. -/ diff --git a/Mathlib/Topology/Algebra/Module/Alternating.lean b/Mathlib/Topology/Algebra/Module/Alternating.lean index eca13578da0351..7051a666717e30 100644 --- a/Mathlib/Topology/Algebra/Module/Alternating.lean +++ b/Mathlib/Topology/Algebra/Module/Alternating.lean @@ -66,9 +66,11 @@ theorem range_toContinuousMultilinearMap : {f | ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f v = 0} := Set.ext fun f => ⟨fun ⟨g, hg⟩ => hg ▸ g.2, fun h => ⟨⟨f, h⟩, rfl⟩⟩ -instance continuousMapClass : ContinuousMapClass (M [Λ^ι]→L[R] N) (ι → M) N where +instance funLike : NDFunLike (M [Λ^ι]→L[R] N) (ι → M) N where coe f := f.toFun coe_injective' _ _ h := toContinuousMultilinearMap_injective <| FunLike.ext' h + +instance continuousMapClass : ContinuousMapClass (M [Λ^ι]→L[R] N) (ι → M) N where map_continuous f := f.cont initialize_simps_projections ContinuousAlternatingMap (toFun → apply) diff --git a/Mathlib/Topology/Algebra/Module/CharacterSpace.lean b/Mathlib/Topology/Algebra/Module/CharacterSpace.lean index 5657965d5b749f..d2e21f0fa01d87 100644 --- a/Mathlib/Topology/Algebra/Module/CharacterSpace.lean +++ b/Mathlib/Topology/Algebra/Module/CharacterSpace.lean @@ -54,10 +54,12 @@ section NonUnitalNonAssocSemiring variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] -/-- Elements of the character space are continuous linear maps. -/ -instance instContinuousLinearMapClass : ContinuousLinearMapClass (characterSpace 𝕜 A) 𝕜 A 𝕜 where +instance instFunLike : NDFunLike (characterSpace 𝕜 A) A 𝕜 where coe φ := ((φ : WeakDual 𝕜 A) : A → 𝕜) coe_injective' φ ψ h := by ext1; apply FunLike.ext; exact congr_fun h + +/-- Elements of the character space are continuous linear maps. -/ +instance instContinuousLinearMapClass : ContinuousLinearMapClass (characterSpace 𝕜 A) 𝕜 A 𝕜 where map_smulₛₗ φ := (φ : WeakDual 𝕜 A).map_smul map_add φ := (φ : WeakDual 𝕜 A).map_add map_continuous φ := (φ : WeakDual 𝕜 A).cont @@ -87,7 +89,7 @@ theorem coe_toClm (φ : characterSpace 𝕜 A) : ⇑(toClm φ) = φ := /-- Elements of the character space are non-unital algebra homomorphisms. -/ instance instNonUnitalAlgHomClass : NonUnitalAlgHomClass (characterSpace 𝕜 A) 𝕜 A 𝕜 := { CharacterSpace.instContinuousLinearMapClass with - map_smul := fun φ => map_smul φ + map_smul := fun φ => map_smulₛₗ φ map_zero := fun φ => map_zero φ map_mul := fun φ => φ.prop.2 } diff --git a/Mathlib/Topology/Algebra/Module/Multilinear.lean b/Mathlib/Topology/Algebra/Module/Multilinear.lean index 35baa053296e6c..02981ecd81dc21 100644 --- a/Mathlib/Topology/Algebra/Module/Multilinear.lean +++ b/Mathlib/Topology/Algebra/Module/Multilinear.lean @@ -76,10 +76,13 @@ theorem toMultilinearMap_injective : | ⟨f, hf⟩, ⟨g, hg⟩, h => by subst h; rfl #align continuous_multilinear_map.to_multilinear_map_injective ContinuousMultilinearMap.toMultilinearMap_injective -instance continuousMapClass : ContinuousMapClass (ContinuousMultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂ +instance funLike : NDFunLike (ContinuousMultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂ where coe f := f.toFun coe_injective' _ _ h := toMultilinearMap_injective <| MultilinearMap.coe_injective h + +instance continuousMapClass : ContinuousMapClass (ContinuousMultilinearMap R M₁ M₂) (∀ i, M₁ i) M₂ + where map_continuous := ContinuousMultilinearMap.cont #align continuous_multilinear_map.continuous_map_class ContinuousMultilinearMap.continuousMapClass diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean index 4c85b71e622e31..a39ba28cf0321d 100644 --- a/Mathlib/Topology/Algebra/Module/WeakDual.lean +++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean @@ -179,10 +179,6 @@ instance instTopologicalAddGroup [ContinuousAdd 𝕜] : TopologicalAddGroup (Wea refine' cast (congr_arg _ _) (eval_continuous B (-y)) ext x simp only [map_neg, Function.comp_apply, LinearMap.neg_apply] - -- Porting note: mathlib3 proof was done here - rw [← (B x).neg_apply] - congr - exact (map_neg B x).symm end Ring diff --git a/Mathlib/Topology/Algebra/StarSubalgebra.lean b/Mathlib/Topology/Algebra/StarSubalgebra.lean index a0673a707e56ed..d100bb35de092b 100644 --- a/Mathlib/Topology/Algebra/StarSubalgebra.lean +++ b/Mathlib/Topology/Algebra/StarSubalgebra.lean @@ -170,7 +170,8 @@ theorem _root_.StarAlgHom.ext_topologicalClosure [T2Space B] {S : StarSubalgebra #align star_alg_hom.ext_topological_closure StarAlgHom.ext_topologicalClosure theorem _root_.StarAlgHomClass.ext_topologicalClosure [T2Space B] {F : Type*} - {S : StarSubalgebra R A} [StarAlgHomClass F R S.topologicalClosure B] {φ ψ : F} + {S : StarSubalgebra R A} [NDFunLike F S.topologicalClosure B] + [StarAlgHomClass F R S.topologicalClosure B] {φ ψ : F} (hφ : Continuous φ) (hψ : Continuous ψ) (h : ∀ x : S, φ (inclusion (le_topologicalClosure S) x) = ψ ((inclusion (le_topologicalClosure S)) x)) : φ = ψ := by @@ -252,8 +253,12 @@ theorem closedEmbedding_coe (x : A) : ClosedEmbedding ((↑) : elementalStarAlge #align elemental_star_algebra.closed_embedding_coe elementalStarAlgebra.closedEmbedding_coe theorem starAlgHomClass_ext [T2Space B] {F : Type*} {a : A} - [StarAlgHomClass F R (elementalStarAlgebra R a) B] {φ ψ : F} (hφ : Continuous φ) + [NDFunLike F (elementalStarAlgebra R a) B] [StarAlgHomClass F R (elementalStarAlgebra R a) B] + {φ ψ : F} (hφ : Continuous φ) (hψ : Continuous ψ) (h : φ ⟨a, self_mem R a⟩ = ψ ⟨a, self_mem R a⟩) : φ = ψ := by + -- Note: help with unfolding `elementalStarAlgebra` + have : StarAlgHomClass F R (↥(topologicalClosure (adjoin R {a}))) B := + inferInstanceAs (StarAlgHomClass F R (elementalStarAlgebra R a) B) refine StarAlgHomClass.ext_topologicalClosure hφ hψ fun x => ?_ apply adjoin_induction' x ?_ ?_ ?_ ?_ ?_ exacts [fun y hy => by simpa only [Set.mem_singleton_iff.mp hy] using h, fun r => by diff --git a/Mathlib/Topology/Homotopy/HomotopyGroup.lean b/Mathlib/Topology/Homotopy/HomotopyGroup.lean index 978727379c757f..9c69dfb4e67b19 100644 --- a/Mathlib/Topology/Homotopy/HomotopyGroup.lean +++ b/Mathlib/Topology/Homotopy/HomotopyGroup.lean @@ -258,7 +258,7 @@ def loopHomeo (i : N) : Ω^ N X x ≃ₜ Ω (Ω^ { j // j ≠ i } X x) const where toFun := toLoop i invFun := fromLoop i - left_inv p := by ext; exact congr_arg p (Equiv.apply_symm_apply _ _) + left_inv p := by ext; exact congr_arg p (by dsimp; exact Equiv.apply_symm_apply _ _) right_inv := to_from i continuous_toFun := continuous_toLoop i continuous_invFun := continuous_fromLoop i diff --git a/Mathlib/Topology/Instances/RealVectorSpace.lean b/Mathlib/Topology/Instances/RealVectorSpace.lean index 8ccbee96baa268..d8db3f19ce0049 100644 --- a/Mathlib/Topology/Instances/RealVectorSpace.lean +++ b/Mathlib/Topology/Instances/RealVectorSpace.lean @@ -20,7 +20,8 @@ variable {E : Type*} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [Conti {F : Type*} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [ContinuousSMul ℝ F] [T2Space F] /-- A continuous additive map between two vector spaces over `ℝ` is `ℝ`-linear. -/ -theorem map_real_smul {G} [AddMonoidHomClass G E F] (f : G) (hf : Continuous f) (c : ℝ) (x : E) : +theorem map_real_smul {G} [NDFunLike G E F] [AddMonoidHomClass G E F] (f : G) (hf : Continuous f) + (c : ℝ) (x : E) : f (c • x) = c • f x := suffices (fun c : ℝ => f (c • x)) = fun c : ℝ => c • f x from congr_fun this c Rat.denseEmbedding_coe_real.dense.equalizer (hf.comp <| continuous_id.smul continuous_const)