chore(Data/Finsupp): make mapDomain_congr congr

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.

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. -/

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₂]

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
 

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]

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)) :=

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']

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
 

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) :

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 =>

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

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. -/

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.

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]) :