diff --git a/Mathlib/Algebra/MonoidAlgebra/MapDomain.lean b/Mathlib/Algebra/MonoidAlgebra/MapDomain.lean index 4c26e9fb3c9cc1..5bee795c915ada 100644 --- a/Mathlib/Algebra/MonoidAlgebra/MapDomain.lean +++ b/Mathlib/Algebra/MonoidAlgebra/MapDomain.lean @@ -185,7 +185,7 @@ lemma mapDomainNonUnitalRingHom_id : mapDomainNonUnitalRingHom R (.id M) = .id R lemma mapDomainNonUnitalRingHom_comp (f : N →ₙ* O) (g : M →ₙ* N) : mapDomainNonUnitalRingHom R (f.comp g) = (mapDomainNonUnitalRingHom R f).comp (mapDomainNonUnitalRingHom R g) := by - ext; simp [Finsupp.mapDomain_comp] + ext; simp [Finsupp.mapDomain_fun_comp] variable (R) in /-- Equivalent monoids have additively isomorphic monoid algebras. diff --git a/Mathlib/Algebra/MonoidAlgebra/Module.lean b/Mathlib/Algebra/MonoidAlgebra/Module.lean index 8f8721f29c6dcf..694e7569c76862 100644 --- a/Mathlib/Algebra/MonoidAlgebra/Module.lean +++ b/Mathlib/Algebra/MonoidAlgebra/Module.lean @@ -91,7 +91,7 @@ lemma mapDomainLinearMap_single (f : M → N) (s : S) (m : M) : @[to_additive (attr := simp)] lemma mapDomainLinearMap_comp (f : M → N) (g : N → O) : mapDomainLinearMap R S (g ∘ f) = mapDomainLinearMap R S g ∘ₗ mapDomainLinearMap R S f := by - ext; simp [Finsupp.mapDomain_comp] + ext; simp [Finsupp.mapDomain_fun_comp] variable (R S) in /-- `MonoidAlgebra.mapDomain` as a linear equiv. -/ diff --git a/Mathlib/Algebra/MvPolynomial/Nilpotent.lean b/Mathlib/Algebra/MvPolynomial/Nilpotent.lean index 817993a0c2ab17..a664ea8f746594 100644 --- a/Mathlib/Algebra/MvPolynomial/Nilpotent.lean +++ b/Mathlib/Algebra/MvPolynomial/Nilpotent.lean @@ -65,7 +65,7 @@ theorem isUnit_iff : IsUnit P ↔ IsUnit (P.coeff 0) ∧ ∀ i ≠ 0, IsNilpoten simp only [ne_eq, isNilpotent_iff] at H convert! ← H (n.equivMapDomain (Equiv.optionSubtypeNe i).symm).some refine (optionEquivLeft_coeff_some_coeff_none _ _ _ _).trans ?_ - simp [Finsupp.equivMapDomain_eq_mapDomain, + simp [Finsupp.equivMapDomain_eq_mapDomain, -Equiv.optionSubtypeNe_symm_apply, coeff_rename_mapDomain _ (Equiv.optionSubtypeNe i).symm.injective] · have : IsNilpotent (P - C (P.coeff 0)) := by simp +contextual [isNilpotent_iff, apply_ite, eq_comm, h₂] diff --git a/Mathlib/Algebra/Polynomial/Laurent.lean b/Mathlib/Algebra/Polynomial/Laurent.lean index e7c7d9340ea465..d5cf2fdf7a0805 100644 --- a/Mathlib/Algebra/Polynomial/Laurent.lean +++ b/Mathlib/Algebra/Polynomial/Laurent.lean @@ -390,7 +390,8 @@ alias support_C_mul_T_of_ne_zero := support_coeff_C_mul_T_of_ne_zero shows that the support of `f.toLaurent` is the same finset, but viewed in `ℤ` under the natural inclusion `ℕ ↪ ℤ`. -/ theorem support_coeff_toLaurent (f : R[X]) : - f.toLaurent.coeff.support = f.support.map Nat.castEmbedding := by simp [Polynomial.support] + f.toLaurent.coeff.support = f.support.map Nat.castEmbedding := by + simp [-Nat.castEmbedding_apply, Polynomial.support] @[deprecated (since := "2026-06-18")] alias toLaurent_support := support_coeff_toLaurent diff --git a/Mathlib/Data/Finsupp/Basic.lean b/Mathlib/Data/Finsupp/Basic.lean index ff4e89bf70c22e..89931ac114de81 100644 --- a/Mathlib/Data/Finsupp/Basic.lean +++ b/Mathlib/Data/Finsupp/Basic.lean @@ -288,19 +288,17 @@ theorem mapDomain_notin_range {f : α → β} (x : α →₀ M) (a : β) (h : a lemma mem_range_of_mapDomain_ne_zero {f : α → β} {x : α →₀ M} {b : β} (h : mapDomain f x b ≠ 0) : b ∈ Set.range f := by contrapose! h; exact mapDomain_notin_range _ _ h -@[simp] -theorem mapDomain_id : mapDomain id v = v := - sum_single _ +-- The linter complains that `mapDomain_id` can be proved from `mapDomain_fun_id` and `id_eq` +-- but this isn't true (at least within most of mathlib) +@[to_fun (attr := simp) mapDomain_fun_id, nolint simpNF] +lemma mapDomain_id : mapDomain id v = v := sum_single _ + +lemma mapDomain_fun_comp (f : α → β) (g : β → γ) : + mapDomain (fun a ↦ g (f a)) v = mapDomain g (mapDomain f v) := by + simp [mapDomain, sum_sum_index] theorem mapDomain_comp {f : α → β} {g : β → γ} : - mapDomain (g ∘ f) v = mapDomain g (mapDomain f v) := by - refine ((sum_sum_index ?_ ?_).trans ?_).symm - · intro - exact single_zero _ - · intro - exact single_add _ - refine sum_congr fun _ _ => sum_single_index ?_ - exact single_zero _ + mapDomain (g ∘ f) v = mapDomain g (mapDomain f v) := mapDomain_fun_comp f g @[simp] theorem mapDomain_single {f : α → β} {a : α} {b : M} : mapDomain f (single a b) = single (f a) b := @@ -310,7 +308,7 @@ theorem mapDomain_single {f : α → β} {a : α} {b : M} : mapDomain f (single theorem mapDomain_zero {f : α → β} : mapDomain f (0 : α →₀ M) = (0 : β →₀ M) := sum_zero_index -theorem mapDomain_congr {f g : α → β} (h : ∀ x ∈ v.support, f x = g x) : +@[congr] theorem mapDomain_congr {f g : α → β} (h : ∀ x ∈ v.support, f x = g x) : v.mapDomain f = v.mapDomain g := Finset.sum_congr rfl fun _ H => by simp only [h _ H] @@ -1070,7 +1068,7 @@ lemma sumElim_eq_add [AddCommMonoid M] (f : α →₀ M) (g : β →₀ M) : @[simp] lemma mapDomain_swap_sumElim [AddCommMonoid M] (f : α →₀ M) (g : β →₀ M) : mapDomain Sum.swap (sumElim f g) = sumElim g f := by - simp [sumElim_eq_add, mapDomain_add, ← mapDomain_comp, Function.comp_def, add_comm] + simp [sumElim_eq_add, mapDomain_add, ← mapDomain_comp, add_comm] @[to_additive] lemma prod_sumElim {ι₁ ι₂ α M : Type*} [Zero α] [CommMonoid M] diff --git a/Mathlib/Geometry/Convex/ConvexSpace/Defs.lean b/Mathlib/Geometry/Convex/ConvexSpace/Defs.lean index 9f7e74f57e4fd9..66810c4c9304ee 100644 --- a/Mathlib/Geometry/Convex/ConvexSpace/Defs.lean +++ b/Mathlib/Geometry/Convex/ConvexSpace/Defs.lean @@ -139,7 +139,7 @@ lemma map_id (f : StdSimplex R M) : f.map id = f := by lemma map_comp (f : StdSimplex R M) (g₁ : M → N) (g₂ : N → P) : f.map (g₂ ∘ g₁) = (f.map g₁).map g₂ := by - ext; simp [mapDomain_comp] + ext; simp [← mapDomain_comp] lemma map_map (f : StdSimplex R M) (g₁ : M → N) (g₂ : N → P) : (f.map g₁).map g₂ = f.map (fun x ↦ g₂ (g₁ x)) := diff --git a/Mathlib/LinearAlgebra/Basis/Defs.lean b/Mathlib/LinearAlgebra/Basis/Defs.lean index c4ff6d939ed635..c7a2bd5096e507 100644 --- a/Mathlib/LinearAlgebra/Basis/Defs.lean +++ b/Mathlib/LinearAlgebra/Basis/Defs.lean @@ -199,7 +199,7 @@ theorem repr_reindex_apply (i' : ι') : (b.reindex e).repr x i' = b.repr x (e.sy show (Finsupp.domLCongr e : _ ≃ₗ[R] _) (b.repr x) i' = _ by simp @[simp] -theorem repr_reindex : (b.reindex e).repr x = (b.repr x).mapDomain e := +theorem repr_reindex : (b.reindex e).repr x = (b.repr x).equivMapDomain e := DFunLike.ext _ _ <| by simp [repr_reindex_apply] @[simp] @@ -479,8 +479,7 @@ theorem reindexFinsetRange_repr_self (i : ι) : b.reindexFinsetRange.repr (b i) = Finsupp.single ⟨b i, Finset.mem_image_of_mem b (Finset.mem_univ i)⟩ 1 := by ext ⟨bi, hbi⟩ - rw [reindexFinsetRange, repr_reindex, Finsupp.mapDomain_equiv_apply, reindexRange_repr_self] - simp [Finsupp.single_apply] + simp [reindexFinsetRange, reindexRange_repr_self] @[simp] theorem reindexFinsetRange_repr (x : M) (i : ι) @@ -710,8 +709,7 @@ variable (e : ι ≃ ι') @[simp] theorem sumCoords_reindex : (b.reindex e).sumCoords = b.sumCoords := by ext x - simp only [coe_sumCoords, repr_reindex] - exact Finsupp.sum_mapDomain_index (fun _ => rfl) fun _ _ _ => rfl + simp [Function.id_def] variable (S : Type*) [Semiring S] [Module S M'] variable [SMulCommClass R S M'] diff --git a/Mathlib/LinearAlgebra/Finsupp/Pi.lean b/Mathlib/LinearAlgebra/Finsupp/Pi.lean index b182855f479a7b..b8be9ce6f3c016 100644 --- a/Mathlib/LinearAlgebra/Finsupp/Pi.lean +++ b/Mathlib/LinearAlgebra/Finsupp/Pi.lean @@ -284,7 +284,7 @@ lemma map_id [Finite X] : map (_root_.id : X → X) (M := M) = _root_.id := by lemma map_comp [Finite X] [Finite Y] [Finite Z] (g : Y → Z) (f : X → Y) : map (g.comp f) (M := M) = (map g).comp (map f) := by ext s - simp [map, Finsupp.mapDomain_comp] + simp [map, Finsupp.mapDomain_fun_comp] end diff --git a/Mathlib/LinearAlgebra/Matrix/Basis.lean b/Mathlib/LinearAlgebra/Matrix/Basis.lean index 226675ca15bc1d..7bf86a6d1eb0ba 100644 --- a/Mathlib/LinearAlgebra/Matrix/Basis.lean +++ b/Mathlib/LinearAlgebra/Matrix/Basis.lean @@ -264,8 +264,7 @@ def invertibleToMatrix [DecidableEq ι] [Fintype ι] (b b' : Basis ι R₂ M₂) theorem toMatrix_reindex (b : Basis ι R M) (v : ι' → M) (e : ι ≃ ι') : (b.reindex e).toMatrix v = (b.toMatrix v).submatrix e.symm _root_.id := by ext - simp only [toMatrix_apply, repr_reindex, Matrix.submatrix_apply, _root_.id, - Finsupp.mapDomain_equiv_apply] + simp [toMatrix_apply] @[simp] theorem toMatrix_map (b : Basis ι R M) (f : M ≃ₗ[R] N) (v : ι → N) : diff --git a/Mathlib/NumberTheory/NumberField/EquivReindex.lean b/Mathlib/NumberTheory/NumberField/EquivReindex.lean index 1eaf27e1199dea..db769e85caf39e 100644 --- a/Mathlib/NumberTheory/NumberField/EquivReindex.lean +++ b/Mathlib/NumberTheory/NumberField/EquivReindex.lean @@ -70,9 +70,7 @@ theorem canonicalEmbedding_eq_basisMatrix_mulVec (α : K) : (fun i ↦ (((integralBasis K).reindex (equivReindex K).symm).repr α i : ℂ)) := by ext i rw [← (latticeBasis K).sum_repr (canonicalEmbedding K α), ← Equiv.sum_comp (equivReindex K)] - simp only [canonicalEmbedding.integralBasis_repr_apply, mulVec, dotProduct, - transpose_apply, of_apply, Fintype.sum_apply, mul_comm, Basis.repr_reindex, - Finsupp.mapDomain_equiv_apply, Equiv.symm_symm, Pi.smul_apply, smul_eq_mul] + simp [canonicalEmbedding.integralBasis_repr_apply, mulVec, dotProduct, mul_comm] theorem inverse_basisMatrix_mulVec_eq_repr [DecidableEq (K →+* ℂ)] (α : 𝓞 K) : ∀ i, ((basisMatrix K).transpose)⁻¹.mulVec (fun j => diff --git a/Mathlib/NumberTheory/NumberField/House.lean b/Mathlib/NumberTheory/NumberField/House.lean index 509517939b2428..837ecf0921b018 100644 --- a/Mathlib/NumberTheory/NumberField/House.lean +++ b/Mathlib/NumberTheory/NumberField/House.lean @@ -283,9 +283,9 @@ private theorem asiegel_remark : ‖asiegel K a‖ ≤ c₂ K * A := by _ ≤ c₂ K * A := ?_ · simp only [Int.cast_abs, ← Real.norm_eq_abs (asiegel K a kr lu)]; rfl · have remark := basis_repr_norm_le_const_mul_house K - simp only [Basis.repr_reindex, Finsupp.mapDomain_equiv_apply, - integralBasis_repr_apply, eq_intCast, Rat.cast_intCast, - Complex.norm_intCast] at remark + simp only [Basis.repr_reindex, Finsupp.equivMapDomain_apply, Equiv.symm_symm, + integralBasis_repr_apply, algebraMap_int_eq, eq_intCast, Rat.cast_intCast, + Complex.norm_intCast] at remark exact mod_cast remark ((a kr.1 lu.1 * ((newBasis K) lu.2))) kr.2 · simp only [house, map_mul, mul_assoc] gcongr diff --git a/Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean b/Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean index 7367d9ff4f49ff..fc2bda7453f749 100644 --- a/Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean +++ b/Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean @@ -429,9 +429,8 @@ instance mapCycles₁_quotientGroupMk'_epi : rw [ModuleCat.epi_iff_surjective] rintro ⟨x, hx⟩ choose! s hs using QuotientGroup.mk_surjective (s := S) - have hs₁ : QuotientGroup.mk ∘ s = id := funext hs refine ⟨⟨mapDomain s x, ?_⟩, Subtype.ext <| by - simp [mapCycles₁_hom, ← mapDomain_comp, hs₁, res, Rep.hom_id (of _)]⟩ + simp [mapCycles₁_hom, ← mapDomain_comp, hs, res, Rep.hom_id (of _)]⟩ simpa [mem_cycles₁_iff, ← (mem_cycles₁_iff _).1 hx, sum_mapDomain_index_inj (f := s) (fun x y h => by rw [← hs x, ← hs y, h])] using Finsupp.sum_congr fun a b => QuotientGroup.induction_on a fun a => by @@ -489,7 +488,7 @@ theorem H1CoresCoinfOfTrivial_exact : (d₂₁ (A.ofQuotient S)).hom y := by have := congr($((mapShortComplexH1 (QuotientGroup.mk' S) (resOfQuotientIso A S).inv).comm₁₂.symm) z) - simp_all [shortComplexH1, z, ← mapDomain_comp, Prod.map_comp_map, Rep.hom_id (res _ _)] + simp_all [shortComplexH1, z, ← mapDomain_comp, Prod.map_map, Rep.hom_id (res _ _)] let v := x - (d₂₁ _).hom z /- We have `C₁(s ∘ π)(v) = ∑ v(g)·s(π(g)) = 0`, since `C₁(π)(v) = dC₁(π)(z) - C₁(π)(dz) = 0` by previous assumptions. -/ diff --git a/Mathlib/RepresentationTheory/Intertwining.lean b/Mathlib/RepresentationTheory/Intertwining.lean index 94b70397a40b47..c0f2cfc86de9a4 100644 --- a/Mathlib/RepresentationTheory/Intertwining.lean +++ b/Mathlib/RepresentationTheory/Intertwining.lean @@ -201,8 +201,8 @@ def id : IntertwiningMap ρ ρ where @[simp] lemma toLinearMap_id : (id ρ).toLinearMap = LinearMap.id := rfl -@[simp] -lemma id_apply (v : V) : id ρ v = v := rfl +@[simp] lemma coe_id : ⇑(id ρ) = _root_.id := rfl +@[simp high] lemma id_apply (v : V) : id ρ v = v := rfl variable {ρ σ τ} in /-- Composition of intertwining maps. diff --git a/Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean b/Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean index fb4f490cda5313..bc4bbbf736efba 100644 --- a/Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean +++ b/Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean @@ -74,7 +74,7 @@ lemma mapDomainBialgHom_id : mapDomainBialgHom R (.id M) = .id R R[M] := by ext; @[to_additive (attr := simp)] lemma mapDomainBialgHom_comp (f : N →* O) (g : M →* N) : mapDomainBialgHom R (f.comp g) = (mapDomainBialgHom R f).comp (mapDomainBialgHom R g) := by - ext; simp [Finsupp.mapDomain_comp] + ext; simp [Finsupp.mapDomain_fun_comp] @[to_additive] lemma mapDomainBialgHom_mapDomainBialgHom (f : N →* O) (g : M →* N) (x : R[M]) :