chore(Data/Finsupp): make support_single simp (leanprover-community#38860)

YaelDillies · YaelDillies · commit c315f04da499 · 2026-05-06T18:10:16.000Z
... for throth `Finsupp`, `DFinsupp` and `SkewMonoidAlgebra`, and rename the first two from `support_single_ne_zero`.
diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean
@@ -154,7 +154,7 @@ theorem support_zero [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] : (0 : ⨁ i
 @[simp]
 theorem support_of [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] (i : ι) (x : β i) (h : x ≠ 0) :
     (of _ i x).support = {i} :=
-  DFinsupp.support_single_ne_zero h
+  DFinsupp.support_single h
 
 theorem support_of_subset [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] {i : ι} {b : β i} :
     (of _ i b).support ⊆ {i} :=
diff --git a/Mathlib/Algebra/FreeAbelianGroup/Finsupp.lean b/Mathlib/Algebra/FreeAbelianGroup/Finsupp.lean
@@ -118,7 +118,7 @@ theorem support_zero : support (0 : FreeAbelianGroup X) = ∅ := by
 
 @[simp]
 theorem support_of (x : X) : support (of x) = {x} := by
-  rw [support, toFinsupp_of, Finsupp.support_single_ne_zero _ one_ne_zero]
+  rw [support, toFinsupp_of, Finsupp.support_single _ one_ne_zero]
 
 @[simp]
 theorem support_neg (a : FreeAbelianGroup X) : support (-a) = support a := by
diff --git a/Mathlib/Algebra/Group/Finsupp.lean b/Mathlib/Algebra/Group/Finsupp.lean
@@ -138,23 +138,23 @@ lemma single_add_apply (a : ι) (m₁ m₂ : M) (b : ι) :
 lemma support_single_add {a : ι} {b : M} {f : ι →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) :
     support (single a b + f) = cons a f.support ha := by
   classical
-  have H := support_single_ne_zero a hb
+  have H := support_single a hb
   rw [support_add_eq, H, cons_eq_insert, insert_eq]
   rwa [H, disjoint_singleton_left]
 
 lemma support_add_single {a : ι} {b : M} {f : ι →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) :
     support (f + single a b) = cons a f.support ha := by
   classical
-  have H := support_single_ne_zero a hb
+  have H := support_single a hb
   rw [support_add_eq, H, union_comm, cons_eq_insert, insert_eq]
   rwa [H, disjoint_singleton_right]
 
 lemma support_single_add_single [DecidableEq ι] {f₁ f₂ : ι} {g₁ g₂ : M}
     (H : f₁ ≠ f₂) (hg₁ : g₁ ≠ 0) (hg₂ : g₂ ≠ 0) :
     (single f₁ g₁ + single f₂ g₂).support = {f₁, f₂} := by
-  rw [support_add_eq, support_single_ne_zero _ hg₁, support_single_ne_zero _ hg₂]
+  rw [support_add_eq, support_single _ hg₁, support_single _ hg₂]
   · simp
-  · simp [support_single_ne_zero, *]
+  · simp [support_single, *]
 
 lemma support_single_add_single_subset [DecidableEq ι] {f₁ f₂ : ι} {g₁ g₂ : M} :
     (single f₁ g₁ + single f₂ g₂).support ⊆ {f₁, f₂} := by
@@ -257,7 +257,7 @@ lemma induction₂ {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : m
   refine f.induction zero ?_
   convert add_single using 7
   apply (addCommute_of_disjoint _).eq
-  simp_all [disjoint_iff_inter_eq_empty, eq_empty_iff_forall_notMem, single_apply]
+  simp_all
 
 @[elab_as_elim]
 lemma induction_linear {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : motive 0)
@@ -304,7 +304,7 @@ lemma induction_on_max₂ (f : ι →₀ M) (zero : motive 0)
   convert add_single using 7 with _ _ _ H
   have := fun c hc ↦ (H c hc).ne
   apply (addCommute_of_disjoint _).eq
-  simp_all [disjoint_iff_inter_eq_empty, eq_empty_iff_forall_notMem, single_apply, not_imp_not]
+  simp_all [not_imp_not]
 
 /-- A finitely supported function can be built by adding up `single a b` for decreasing `a`.
 
diff --git a/Mathlib/Algebra/Module/LinearMap/Polynomial.lean b/Mathlib/Algebra/Module/LinearMap/Polynomial.lean
@@ -97,8 +97,7 @@ lemma toMvPolynomial_isHomogeneous (M : Matrix m n R) (i : m) :
   apply MvPolynomial.IsHomogeneous.sum
   rintro j -
   apply MvPolynomial.isHomogeneous_monomial _ _
-  simp [Finsupp.degree, Finsupp.support_single_ne_zero _ one_ne_zero, Finset.sum_singleton,
-    Finsupp.single_eq_same]
+  simp
 
 lemma toMvPolynomial_totalDegree_le (M : Matrix m n R) (i : m) :
     (M.toMvPolynomial i).totalDegree ≤ 1 := by
diff --git a/Mathlib/Algebra/MonoidAlgebra/Degree.lean b/Mathlib/Algebra/MonoidAlgebra/Degree.lean
@@ -254,7 +254,7 @@ theorem supDegree_sum_le {ι} {s : Finset ι} {f : ι → R[A]} :
 
 theorem supDegree_single_ne_zero (a : A) {r : R} (hr : r ≠ 0) :
     (single a r).supDegree D = D a := by
-  rw [supDegree, Finsupp.support_single_ne_zero a hr, Finset.sup_singleton]
+  rw [supDegree, Finsupp.support_single a hr, Finset.sup_singleton]
 
 open Classical in
 theorem supDegree_single (a : A) (r : R) :
diff --git a/Mathlib/Algebra/MonoidAlgebra/Grading.lean b/Mathlib/Algebra/MonoidAlgebra/Grading.lean
@@ -154,12 +154,12 @@ theorem decomposeAux_coe {i : ι} (x : gradeBy R f i) :
     exact map_zero _
   · intro m b y hmy hb ih hmby
     have : Disjoint (Finsupp.single m b).support y.support := by
-      simpa only [Finsupp.support_single_ne_zero _ hb, Finset.disjoint_singleton_left]
+      simpa only [Finsupp.support_single _ hb, Finset.disjoint_singleton_left]
     rw [mem_gradeBy_iff, Finsupp.support_add_eq this, Finset.coe_union, Set.union_subset_iff]
       at hmby
     obtain ⟨h1, h2⟩ := hmby
     have : f m = i := by
-      rwa [Finsupp.support_single_ne_zero _ hb, Finset.coe_singleton, Set.singleton_subset_iff]
+      rwa [Finsupp.support_single _ hb, Finset.coe_singleton, Set.singleton_subset_iff]
         at h1
     subst this
     simp only [map_add, decomposeAux_single f m]
diff --git a/Mathlib/Algebra/MonoidAlgebra/Support.lean b/Mathlib/Algebra/MonoidAlgebra/Support.lean
@@ -91,7 +91,7 @@ lemma support_one_subset [One G] : (1 : k[G]).support ⊆ 1 :=
 
 @[to_additive (dont_translate := k) (attr := simp) support_one]
 lemma support_one [One G] [NeZero (1 : k)] : (1 : k[G]).support = 1 :=
-  Finsupp.support_single_ne_zero _ one_ne_zero
+  Finsupp.support_single _ one_ne_zero
 
 section Span
 
diff --git a/Mathlib/Algebra/MvPolynomial/Variables.lean b/Mathlib/Algebra/MvPolynomial/Variables.lean
@@ -88,7 +88,7 @@ theorem vars_C : (C r : MvPolynomial σ R).vars = ∅ := by
 
 @[simp]
 theorem vars_X [Nontrivial R] : (X n : MvPolynomial σ R).vars = {n} := by
-  rw [X, vars_monomial (one_ne_zero' R), Finsupp.support_single_ne_zero _ (one_ne_zero' ℕ)]
+  rw [X, vars_monomial (one_ne_zero' R), Finsupp.support_single _ (one_ne_zero' ℕ)]
 
 theorem mem_vars_iff_mem_support (i : σ) : i ∈ p.vars ↔ ∃ d ∈ p.support, i ∈ d.support := by
   classical simp only [vars_def, Multiset.mem_toFinset, mem_degrees, mem_support_iff]
@@ -218,7 +218,7 @@ theorem vars_map_of_injective (hf : Injective f) : (map f p).vars = p.vars := by
 
 theorem vars_monomial_single (i : σ) {e : ℕ} {r : R} (he : e ≠ 0) (hr : r ≠ 0) :
     (monomial (Finsupp.single i e) r).vars = {i} := by
-  rw [vars_monomial hr, Finsupp.support_single_ne_zero _ he]
+  rw [vars_monomial hr, Finsupp.support_single _ he]
 
 theorem vars_eq_support_biUnion_support [DecidableEq σ] :
     p.vars = p.support.biUnion Finsupp.support := by
diff --git a/Mathlib/Algebra/Polynomial/Basic.lean b/Mathlib/Algebra/Polynomial/Basic.lean
@@ -748,7 +748,7 @@ theorem eq_zero_of_eq_zero (h : (0 : R) = (1 : R)) (p : R[X]) : p = 0 := by
 section Fewnomials
 
 theorem support_monomial (n) {a : R} (H : a ≠ 0) : (monomial n a).support = singleton n := by
-  rw [← ofFinsupp_single, support]; exact Finsupp.support_single_ne_zero _ H
+  rw [← ofFinsupp_single, support]; exact Finsupp.support_single _ H
 
 theorem support_monomial' (n) (a : R) : (monomial n a).support ⊆ singleton n := by
   rw [← ofFinsupp_single, support]
diff --git a/Mathlib/Algebra/Polynomial/Laurent.lean b/Mathlib/Algebra/Polynomial/Laurent.lean
@@ -388,7 +388,7 @@ set_option backward.isDefEq.respectTransparency false in
 theorem support_C_mul_T_of_ne_zero {a : R} (a0 : a ≠ 0) (n : ℤ) :
     Finsupp.support (C a * T n) = {n} := by
   rw [← single_eq_C_mul_T]
-  exact support_single_ne_zero _ a0
+  exact support_single _ a0
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The support of a polynomial `f` is a finset in `ℕ`.  The lemma `toLaurent_support f`
diff --git a/Mathlib/Algebra/SkewMonoidAlgebra/Support.lean b/Mathlib/Algebra/SkewMonoidAlgebra/Support.lean
@@ -28,8 +28,10 @@ section AddCommMonoid
 
 variable [AddCommMonoid k] {a : G} {b : k}
 
-theorem support_single_ne_zero (a : G) (h : b ≠ 0) : (single a b).support = {a} :=
-  Finsupp.support_single_ne_zero _ h
+@[simp] lemma support_single (a : G) (h : b ≠ 0) : (single a b).support = {a} :=
+  Finsupp.support_single _ h
+
+@[deprecated (since := "2026-05-05")] alias support_single_ne_zero := support_single
 
 theorem support_single_subset : (single a b).support ⊆ {a} := Finsupp.support_single_subset
 
@@ -59,7 +61,7 @@ lemma support_one_subset : (1 : SkewMonoidAlgebra k G).support ⊆ 1 :=
 
 @[simp]
 lemma support_one [NeZero (1 : k)] : (1 : SkewMonoidAlgebra k G).support = 1 :=
-  Finsupp.support_single_ne_zero _ one_ne_zero
+  Finsupp.support_single _ one_ne_zero
 
 end AddCommMonoidWithOne
 
diff --git a/Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean b/Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean
@@ -159,10 +159,7 @@ lemma char_mem_charPoly (w : W) : char he hL w ∈ charPoly he hL := by
   refine ⟨AddMonoidAlgebra.single w 1, ?_⟩
   ext v
   simp only [char_apply, AddMonoidAlgebra.single]
-  rw [Finset.sum_eq_single w]
-  · simp only [Finsupp.single_eq_same, one_mul]
-  · simp [Finsupp.single_apply_ne_zero]
-  · simp
+  rw [Finset.sum_eq_single w] <;> simp
 
 /-- The family `charPoly he hL w, w : W` separates points in `V`. -/
 lemma separatesPoints_charPoly (he : Continuous e) (he' : e ≠ 1)
diff --git a/Mathlib/Data/DFinsupp/BigOperators.lean b/Mathlib/Data/DFinsupp/BigOperators.lean
@@ -116,7 +116,7 @@ theorem prod_zero_index [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decid
 theorem prod_single_index [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ]
     {i : ι} {b : β i} {h : ∀ i, β i → γ} (h_zero : h i 0 = 1) : (single i b).prod h = h i b := by
   by_cases h : b ≠ 0
-  · simp [DFinsupp.prod, support_single_ne_zero h]
+  · simp [DFinsupp.prod, support_single h]
   · rw [not_not] at h
     simp [h, h_zero]
     rfl
diff --git a/Mathlib/Data/DFinsupp/Defs.lean b/Mathlib/Data/DFinsupp/Defs.lean
@@ -892,9 +892,12 @@ instance decidableZero [∀ (i) (x : β i), Decidable (x = 0)] (f : Π₀ i, β
 theorem support_subset_iff {s : Set ι} {f : Π₀ i, β i} : ↑f.support ⊆ s ↔ ∀ i ∉ s, f i = 0 := by
   simpa [Set.subset_def] using forall_congr' fun i => not_imp_comm
 
-theorem support_single_ne_zero {i : ι} {b : β i} (hb : b ≠ 0) : (single i b).support = {i} := by
+@[simp]
+theorem support_single {i : ι} {b : β i} (hb : b ≠ 0) : (single i b).support = {i} := by
   grind
 
+@[deprecated (since := "2026-05-05")] alias support_single_ne_zero := support_single
+
 theorem support_single_subset {i : ι} {b : β i} : (single i b).support ⊆ {i} :=
   support_mk'_subset
 
diff --git a/Mathlib/Data/Finsupp/Basic.lean b/Mathlib/Data/Finsupp/Basic.lean
@@ -551,8 +551,8 @@ theorem comapDomain_single (f : α → β) (a : α) (m : M)
   rcases eq_or_ne m 0 with (rfl | hm)
   · simp_rw [single_zero, comapDomain_zero]
   · rw [eq_single_iff, comapDomain_apply, comapDomain_support, ← Finset.coe_subset, coe_preimage,
-      support_single_ne_zero _ hm, coe_singleton, coe_singleton, single_eq_same]
-    rw [support_single_ne_zero _ hm, coe_singleton] at hif
+      support_single _ hm, coe_singleton, coe_singleton, single_eq_same]
+    rw [support_single _ hm, coe_singleton] at hif
     exact ⟨fun x hx => hif hx rfl hx, rfl⟩
 
 lemma comapDomain_surjective {f : α → β} (hf : Function.Injective f) :
diff --git a/Mathlib/Data/Finsupp/Multiset.lean b/Mathlib/Data/Finsupp/Multiset.lean
@@ -92,7 +92,7 @@ theorem toFinset_toMultiset [DecidableEq α] (f : α →₀ ℕ) : f.toMultiset.
   · rw [toMultiset_zero, Multiset.toFinset_zero, support_zero]
   · intro a n f ha hn ih
     rw [toMultiset_add, Multiset.toFinset_add, ih, toMultiset_single, support_add_eq,
-      support_single_ne_zero _ hn, Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton]
+      support_single _ hn, Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton]
     refine Disjoint.mono_left support_single_subset ?_
     rwa [Finset.disjoint_singleton_left]
 
diff --git a/Mathlib/Data/Finsupp/Order.lean b/Mathlib/Data/Finsupp/Order.lean
@@ -154,7 +154,7 @@ theorem single_le_sum {α M N : Type*} [Zero M] [AddCommMonoid N]
   rcases eq_or_ne (f a) 0 with H | H
   · rw [H, single_zero, sum_zero_index]
     exact sum_nonneg' (fun i ↦ h i (f i))
-  · rw [sum, support_single_ne_zero _ H, sum_singleton, single_eq_same]
+  · rw [sum, support_single _ H, sum_singleton, single_eq_same]
     apply Finset.single_le_sum (fun i hi ↦ h i (f i))
     simpa [mem_support_iff, ne_eq] using H
 
diff --git a/Mathlib/Data/Finsupp/Single.lean b/Mathlib/Data/Finsupp/Single.lean
@@ -98,9 +98,11 @@ theorem single_of_single_apply (a a' : α) (b : M) :
   classical
   grind
 
-theorem support_single_ne_zero (a : α) (hb : b ≠ 0) : (single a b).support = {a} :=
+@[simp] lemma support_single (a : α) (hb : b ≠ 0) : (single a b).support = {a} :=
   if_neg hb
 
+@[deprecated (since := "2026-05-05")] alias support_single_ne_zero := support_single
+
 theorem support_single_subset : (single a b).support ⊆ {a} := by
   classical
   grind
@@ -160,11 +162,11 @@ lemma apply_surjective (a : α) : Surjective fun f : α →₀ M ↦ f a :=
   RightInverse.surjective fun _ ↦ single_eq_same
 
 theorem support_single_ne_bot (i : α) (h : b ≠ 0) : (single i b).support ≠ ⊥ := by
-  simpa only [support_single_ne_zero _ h] using singleton_ne_empty _
+  simpa only [support_single _ h] using singleton_ne_empty _
 
 theorem support_single_disjoint {b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : α} :
     Disjoint (single i b).support (single j b').support ↔ i ≠ j := by
-  rw [support_single_ne_zero _ hb, support_single_ne_zero _ hb', disjoint_singleton]
+  rw [support_single _ hb, support_single _ hb', disjoint_singleton]
 
 @[simp]
 theorem single_eq_zero : single a b = 0 ↔ b = 0 := by
@@ -206,14 +208,14 @@ theorem support_eq_singleton {f : α →₀ M} {a : α} :
   ⟨fun h =>
     ⟨mem_support_iff.1 <| h.symm ▸ Finset.mem_singleton_self a,
       eq_single_iff.2 ⟨subset_of_eq h, rfl⟩⟩,
-    fun h => h.2.symm ▸ support_single_ne_zero _ h.1⟩
+    fun h => h.2.symm ▸ support_single _ h.1⟩
 
 theorem support_eq_singleton' {f : α →₀ M} {a : α} :
     f.support = {a} ↔ ∃ b ≠ 0, f = single a b :=
   ⟨fun h =>
     let h := support_eq_singleton.1 h
     ⟨_, h.1, h.2⟩,
-    fun ⟨_b, hb, hf⟩ => hf.symm ▸ support_single_ne_zero _ hb⟩
+    fun ⟨_b, hb, hf⟩ => hf.symm ▸ support_single _ hb⟩
 
 theorem card_support_eq_one {f : α →₀ M} :
     #f.support = 1 ↔ ∃ a, f a ≠ 0 ∧ f = single a (f a) := by
@@ -415,7 +417,7 @@ theorem single_of_embDomain_single (l : α →₀ M) (f : α ↪ β) (a : β) (b
     (h : l.embDomain f = single a b) : ∃ x, l = single x b ∧ f x = a := by
   classical
     have h_map_support : Finset.map f l.support = {a} := by
-      rw [← support_embDomain, h, support_single_ne_zero _ hb]
+      rw [← support_embDomain, h, support_single _ hb]
     have ha : a ∈ Finset.map f l.support := by simp only [h_map_support, Finset.mem_singleton]
     rcases Finset.mem_map.1 ha with ⟨c, _hc₁, hc₂⟩
     use c
diff --git a/Mathlib/LinearAlgebra/Basis/Basic.lean b/Mathlib/LinearAlgebra/Basis/Basic.lean
@@ -63,7 +63,7 @@ theorem mem_span_image {m : M} {s : Set ι} : m ∈ span R (b '' s) ↔ ↑(b.re
 @[simp]
 theorem self_mem_span_image [Nontrivial R] {i : ι} {s : Set ι} :
     b i ∈ span R (b '' s) ↔ i ∈ s := by
-  simp [mem_span_image, Finsupp.support_single_ne_zero]
+  simp [mem_span_image, Finsupp.support_single]
 
 protected theorem mem_span (x : M) : x ∈ span R (range b) :=
   span_mono (image_subset_range _ _) (mem_span_repr_support b x)
diff --git a/Mathlib/LinearAlgebra/ConvexSpace/AffineSpace.lean b/Mathlib/LinearAlgebra/ConvexSpace/AffineSpace.lean
@@ -39,7 +39,7 @@ public def convexCombination (s : StdSimplex R P) : P :=
 public theorem convexCombination_single (x : P) :
     convexCombination (StdSimplex.single x : StdSimplex R P) = x := by
   simp only [convexCombination, StdSimplex.single]
-  rw [Finsupp.support_single_ne_zero _ one_ne_zero]
+  rw [Finsupp.support_single _ one_ne_zero]
   exact ({x} : Finset P).affineCombination_of_eq_one_of_eq_zero _ _
     (Finset.mem_singleton_self x) Finsupp.single_eq_same fun j _ hne => Finsupp.single_eq_of_ne hne
 
diff --git a/Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean b/Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
@@ -158,7 +158,7 @@ theorem Module.Basis.le_span {J : Set M} (v : Basis ι R M) (hJ : span R J = ⊤
         span_le.2 fun j hj x hx => ⟨_, ⟨⟨j, hj⟩, rfl⟩, hx⟩
       rw [hJ] at this
       replace : v.repr (v i) ∈ Finsupp.supported R R (⋃ j, S j) := this trivial
-      rw [v.repr_self, Finsupp.mem_supported, Finsupp.support_single_ne_zero _ one_ne_zero] at this
+      rw [v.repr_self, Finsupp.mem_supported, Finsupp.support_single _ one_ne_zero] at this
       · subst b
         rcases mem_iUnion.1 (this (Finset.mem_singleton_self _)) with ⟨j, hj⟩
         exact mem_iUnion.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩
diff --git a/Mathlib/LinearAlgebra/Finsupp/Supported.lean b/Mathlib/LinearAlgebra/Finsupp/Supported.lean
@@ -83,7 +83,7 @@ lemma single_mem_span_single [Nontrivial R] {a : α} {s : Set α} :
     single a 1 ∈ Submodule.span R ((single · (1 : R)) '' s) ↔ a ∈ s := by
   refine ⟨fun h => ?_, fun h => Submodule.subset_span <| Set.mem_image_of_mem _ h⟩
   rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported,
-    Finsupp.support_single_ne_zero _ (one_ne_zero' R)] at h
+    Finsupp.support_single _ (one_ne_zero' R)] at h
   simpa using h
 
 theorem span_le_supported_biUnion_support (s : Set (α →₀ M)) :
@@ -188,7 +188,7 @@ lemma codisjoint_supported_supported_iff [Nontrivial M] {s t : Set α} :
   refine ⟨fun h ↦ codisjoint_iff.mpr (eq_top_iff.mpr fun a ↦ ?_), codisjoint_supported_supported⟩
   obtain ⟨x, hx⟩ := exists_ne (0 : M)
   rw [codisjoint_iff, ← supported_union, eq_top_iff'] at h
-  simpa [Finsupp.mem_supported, Finsupp.support_single_ne_zero _ hx] using h (Finsupp.single a x)
+  simpa [Finsupp.mem_supported, Finsupp.support_single _ hx] using h (Finsupp.single a x)
 
 /-- Interpret `Finsupp.restrictSupportEquiv` as a linear equivalence between
 `supported M R s` and `s →₀ M`. -/
diff --git a/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean b/Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
@@ -182,7 +182,7 @@ variable {σ}
 
 theorem isHomogeneous_X (i : σ) : IsHomogeneous (X i : MvPolynomial σ R) 1 := by
   apply isHomogeneous_monomial
-  simp only [degree_apply, Finsupp.support_single_ne_zero _ one_ne_zero, Finset.sum_singleton,
+  simp only [degree_apply, Finsupp.support_single _ one_ne_zero, Finset.sum_singleton,
     single_eq_same]
 
 variable {R} in
diff --git a/Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean b/Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean
@@ -227,7 +227,7 @@ theorem irreducible_sumSMulXSMulY [IsDomain R]
   · simp [ι]
   · rw [hsupp, Finset.coe_map, ι.injective.injOn.pairwiseDisjoint_image]
     suffices (c.support : Set n).PairwiseDisjoint fun x ↦ {Sum.inl x, Sum.inr x} by
-      simpa [ι, Function.comp_def, Finsupp.support_add_eq, Finsupp.support_single_ne_zero]
+      simpa [ι, Function.comp_def, Finsupp.support_add_eq, Finsupp.support_single]
     simp [Set.PairwiseDisjoint, Set.Pairwise, ne_comm]
   · intro r hr
     apply h_dvd
diff --git a/Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean b/Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
@@ -255,28 +255,21 @@ theorem support_esymm'' [DecidableEq σ] [Nontrivial R] (n : ℕ) :
   simp only [← single_eq_monomial]
   refine Finsupp.support_sum_eq_biUnion (powersetCard n (univ : Finset σ)) ?_
   intro s t hst
-  rw [disjoint_left, Finsupp.support_single_ne_zero _ one_ne_zero]
-  rw [Finsupp.support_single_ne_zero _ one_ne_zero]
+  rw [disjoint_left, Finsupp.support_single _ one_ne_zero]
+  rw [Finsupp.support_single _ one_ne_zero]
   simp only [mem_singleton]
   rintro a h rfl
   have := congr_arg Finsupp.support h
-  rw [Finsupp.support_sum_eq_biUnion, Finsupp.support_sum_eq_biUnion] at this
-  · have hsingle : ∀ s : Finset σ, ∀ x : σ, x ∈ s → (Finsupp.single x 1).support = {x} := by
-      intro _ x _
-      rw [Finsupp.support_single_ne_zero x one_ne_zero]
-    have hs := biUnion_congr (of_eq_true (eq_self s)) (hsingle s)
-    have ht := biUnion_congr (of_eq_true (eq_self t)) (hsingle t)
-    rw [hs, ht] at this
-    · simp only [biUnion_singleton_eq_self] at this
-      exact absurd this hst.symm
-  all_goals intro x y; simp [Finsupp.support_single_disjoint]
+  rw [Finsupp.support_sum_eq_biUnion _ (by simp), Finsupp.support_sum_eq_biUnion _ (by simp)]
+    at this
+  simp_all
 
 theorem support_esymm' [DecidableEq σ] [Nontrivial R] (n : ℕ) : (esymm σ R n).support =
     (powersetCard n (univ : Finset σ)).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1} := by
   rw [support_esymm'']
   congr
   funext
-  exact Finsupp.support_single_ne_zero _ one_ne_zero
+  exact Finsupp.support_single _ one_ne_zero
 
 theorem support_esymm [DecidableEq σ] [Nontrivial R] (n : ℕ) : (esymm σ R n).support =
     (powersetCard n (univ : Finset σ)).image fun t => ∑ i ∈ t, Finsupp.single i 1 := by
diff --git a/Mathlib/RingTheory/MvPowerSeries/Rename.lean b/Mathlib/RingTheory/MvPowerSeries/Rename.lean
@@ -269,7 +269,7 @@ theorem killCompl_X (i : σ) : killCompl (R := R) e (X (e i)) = X i := by
 theorem killCompl_X_eq_zero {t : τ} (h : t ∉ Set.range e) :
     killCompl (R := R) e (X t) = 0 := by
   replace h : single t 1 ∉ Set.range (embDomain e) := by
-    rwa [mem_range_embDomain_iff, support_single_ne_zero _ (by simp), Finset.coe_singleton,
+    rwa [mem_range_embDomain_iff, support_single _ (by simp), Finset.coe_singleton,
       Set.singleton_subset_iff]
   simpa using killCompl_monomial_eq_zero (1 : R) h
 
