refactor(Data/Finsupp): use single in uniqueEquiv (#37755)

In essence, this changes `(Finsupp.uniqueEquiv i).symm m` from having support `univ.filter (fun _ ↦ m ≠ 0)` to having support `if m = 0 then {i} else ∅`. These are equal, but having the RHS be `single 1 r` is much more useful in practice. Similarly for `MonoidAlgebra`. To avoid simp getting stuck after rewriting with `uniqueEquiv_symm_apply`, add `uniqueEquiv_symm_apply_apply` and tag it with `simp↓ high`.

Also rename `Equiv.finsuppUnique` to `Finsupp.uniqueEquiv` and change the `Unique ι` argument into `Subsingleton ι` and `i : ι`. Similarly for `AddEquiv` and `LinearEquiv`.

Author: YaelDillies

Mathlib/Algebra/FreeAlgebra/Cardinality.lean

@@ -36,7 +36,7 @@ theorem cardinalMk_eq_max_lift [Nonempty X] [Nontrivial R] :
 
 @[simp]
 theorem cardinalMk_eq_lift [IsEmpty X] : #(FreeAlgebra R X) = Cardinal.lift.{v} #R := by
-  have := lift_mk_eq'.2 ⟨show (FreeMonoid X →₀ R) ≃ R from Equiv.finsuppUnique⟩
+  have := lift_mk_eq'.2 ⟨show (FreeMonoid X →₀ R) ≃ R from Finsupp.uniqueEquiv 1⟩
   rw [lift_id'.{u, v}, lift_umax] at this
   rwa [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra]
 

Mathlib/Algebra/Group/Finsupp.lean

@@ -77,7 +77,19 @@ noncomputable def addEquivFunOnFinite {ι : Type*} [Finite ι] :
 
 /-- If `M` is the trivial monoid, then the monoid of finitely supported functions `ι →₀ M` is
 is isomorphic to `M`. -/
-@[simps!]
+@[simps! apply symm_apply]
+noncomputable def uniqueAddEquiv (i : ι) [Subsingleton ι] : (ι →₀ M) ≃+ M where
+  toEquiv := uniqueEquiv i
+  map_add' _ _ := rfl
+
+-- We want this lemma to fire before `uniqueAddEquiv_symm_apply`.
+@[simp↓ high] lemma uniqueAddEquiv_symm_apply_apply (i : ι) [Subsingleton ι] (m : M) (j : ι) :
+    (uniqueAddEquiv i).symm m j = m := by simp [Subsingleton.elim j i]
+
+set_option linter.deprecated false in
+/-- If `M` is the trivial monoid, then the monoid of finitely supported functions `ι →₀ M` is
+is isomorphic to `M`. -/
+@[simps!, deprecated uniqueAddEquiv (since := "2026-05-06")]
 noncomputable def _root_.AddEquiv.finsuppUnique {ι : Type*} [Unique ι] : (ι →₀ M) ≃+ M where
   toEquiv := .finsuppUnique
   map_add' _ _ := rfl
@@ -161,6 +173,8 @@ lemma support_single_add_single_subset [DecidableEq ι] {f₁ f₂ : ι} {g₁ g
   refine subset_trans Finsupp.support_add <| union_subset_iff.mpr ⟨?_, ?_⟩ <;>
   exact subset_trans Finsupp.support_single_subset (by simp)
 
+set_option linter.deprecated false in
+@[deprecated uniqueAddEquiv_symm_apply (since := "2026-05-06")]
 lemma _root_.AddEquiv.finsuppUnique_symm {M : Type*} [AddZeroClass M] (d : M) :
     AddEquiv.finsuppUnique.symm d = single () d := by ext; simp [AddEquiv.finsuppUnique]
 

Mathlib/Algebra/MonoidAlgebra/Defs.lean

@@ -634,12 +634,24 @@ instance isLocalHom_singleOneRingHom : IsLocalHom (singleOneRingHom (R := R) (M
 set_option backward.isDefEq.respectTransparency false in
 variable (M) in
 /-- The trivial monoid algebra is the base ring. -/
-@[to_additive (dont_translate := R) (attr := simps! apply symm_apply)
+@[to_additive (dont_translate := R) (attr := simps! apply)
 /-- The trivial additive monoid algebra is the base ring. -/]
-def uniqueRingEquiv [Unique M] : R[M] ≃+* R where
-  toAddEquiv := .finsuppUnique
-  map_mul' x y :=
-    (mul_apply ..).trans <| by simp [Finsupp.sum_unique, Unique.eq_default, MonoidAlgebra]
+def uniqueRingEquiv [Subsingleton M] : R[M] ≃+* R where
+  toAddEquiv := Finsupp.uniqueAddEquiv 1
+  map_mul' x y := by
+    let : Unique M := ⟨⟨1⟩, fun _ ↦ Subsingleton.elim _ _⟩
+    refine (mul_apply ..).trans ?_
+    simp [Finsupp.sum_unique, Unique.eq_default, MonoidAlgebra]
+
+variable (M) in
+@[to_additive (dont_translate := R) (attr := simp)]
+lemma uniqueRingEquiv_symm_apply [Subsingleton M] (r : R) :
+    (uniqueRingEquiv M).symm r = single 1 r := rfl
+
+-- We want this lemma to fire before `uniqueRingEquiv_symm_apply`.
+@[to_additive (dont_translate := R) (attr := simp↓ high)]
+lemma uniqueRingEquiv_symm_apply_apply [Subsingleton M] (r : R) (m : M) :
+    (uniqueRingEquiv M).symm r m = r := by simp [Subsingleton.elim m 1]
 
 /-- A product monoid algebra is a nested monoid algebra. -/
 @[to_additive (dont_translate := R)

Mathlib/Data/Finsupp/Defs.lean

@@ -213,13 +213,6 @@ theorem equivFunOnFinite_symm_coe {α} [Finite α] (f : α →₀ M) : equivFunO
 @[simp]
 lemma coe_equivFunOnFinite_symm {α} [Finite α] (f : α → M) : ⇑(equivFunOnFinite.symm f) = f := rfl
 
-/--
-If `α` has a unique term, the type of finitely supported functions `α →₀ β` is equivalent to `β`.
--/
-@[simps!]
-noncomputable def _root_.Equiv.finsuppUnique {ι : Type*} [Unique ι] : (ι →₀ M) ≃ M :=
-  Finsupp.equivFunOnFinite.trans (Equiv.funUnique ι M)
-
 @[ext]
 theorem unique_ext [Unique α] {f g : α →₀ M} (h : f default = g default) : f = g :=
   ext fun a => by rwa [Unique.eq_default a]

Mathlib/Data/Finsupp/Single.lean

@@ -240,6 +240,26 @@ theorem card_support_le_one' [Nonempty α] {f : α →₀ M} :
     #f.support ≤ 1 ↔ ∃ a b, f = single a b := by
   simp only [card_le_one_iff_subset_singleton, support_subset_singleton']
 
+/-- If `α` has a unique term, then finitely supported functions `α →₀ M` are in bijection with `M`.
+-/
+@[simps]
+noncomputable def uniqueEquiv (a : α) [Subsingleton α] : (α →₀ M) ≃ M where
+  toFun f := f a
+  invFun := single a
+  left_inv f := by ext b; simp [Subsingleton.elim b a]
+  right_inv x := by simp
+
+-- We want this lemma to fire before `uniqueEquiv_symm_apply`.
+@[simp↓ high] lemma uniqueEquiv_symm_apply_apply (a : α) [Subsingleton α] (m : M) (b : α) :
+    (uniqueEquiv a).symm m b = m := by simp [Subsingleton.elim b a]
+
+/--
+If `α` has a unique term, the type of finitely supported functions `α →₀ β` is equivalent to `β`.
+-/
+@[simps!, deprecated uniqueEquiv (since := "2026-05-06")]
+noncomputable def _root_.Equiv.finsuppUnique {ι : Type*} [Unique ι] : (ι →₀ M) ≃ M :=
+  Finsupp.equivFunOnFinite.trans (Equiv.funUnique ι M)
+
 @[simp]
 theorem equivFunOnFinite_single [DecidableEq α] [Finite α] (x : α) (m : M) :
     Finsupp.equivFunOnFinite (Finsupp.single x m) = Pi.single x m := by

Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean

@@ -247,7 +247,7 @@ theorem eq_bot_of_rank_le_one (h : Module.rank F S ≤ 1) [Module.Free F S] : S
     rw [← b.mk_eq_rank'', eq_one_iff_unique, ← unique_iff_subsingleton_and_nonempty] at h1
     obtain ⟨h1⟩ := h1
     obtain ⟨y, hy⟩ := (bijective_algebraMap_of_linearEquiv (b.repr ≪≫ₗ
-      Finsupp.LinearEquiv.finsuppUnique _ _ _).symm).surjective ⟨x, hx⟩
+      Finsupp.uniqueLinearEquiv _ _ default).symm).surjective ⟨x, hx⟩
     exact ⟨y, congr(Subtype.val $(hy))⟩
   haveI := mk_eq_zero_iff.1 (b.mk_eq_rank''.symm ▸ Cardinal.lt_one_iff.1 (h.lt_of_ne h1))
   haveI := b.repr.toEquiv.subsingleton

Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean

@@ -129,9 +129,9 @@ noncomputable def basisSingleton (ι : Type*) [Unique ι] (h : finrank K V = 1)
       map_smul' := by simp [mul_div]
       left_inv := fun w => by
         apply_fun b.repr using b.repr.toEquiv.injective
-        apply_fun Equiv.finsuppUnique
+        apply_fun Finsupp.uniqueEquiv default
         simp only [map_smulₛₗ, Finsupp.coe_smul, Finsupp.single_eq_same,
-          smul_eq_mul, Pi.smul_apply, Equiv.finsuppUnique_apply]
+          smul_eq_mul, Pi.smul_apply, Finsupp.uniqueEquiv_apply]
         exact div_mul_cancel₀ _ h
       right_inv := fun f => by
         ext

Mathlib/LinearAlgebra/Finsupp/Pi.lean

@@ -31,35 +31,46 @@ open Set LinearMap Submodule
 
 namespace Finsupp
 
-section LinearEquiv.finsuppUnique
+section uniqueLinearEquiv
 
-variable (R : Type*) {S : Type*} (M : Type*)
+variable (R : Type*) {S α : Type*} (M : Type*)
 variable [AddCommMonoid M] [Semiring R] [Module R M]
-variable (α : Type*) [Unique α]
 
 /-- If `α` has a unique term, then the type of finitely supported functions `α →₀ M` is
 `R`-linearly equivalent to `M`. -/
-noncomputable def LinearEquiv.finsuppUnique : (α →₀ M) ≃ₗ[R] M :=
+@[simps! apply symm_apply]
+noncomputable def uniqueLinearEquiv [Subsingleton α] (a : α) : (α →₀ M) ≃ₗ[R] M where
+  toAddEquiv := uniqueAddEquiv a
+  map_smul' _ _ := rfl
+
+-- We want this lemma to fire before `uniqueRingEquiv_symm_apply`.
+@[simp↓ high] lemma uniqueLinearEquiv_symm_apply_apply (a : α) [Subsingleton α] (m : M) (b : α) :
+    (uniqueLinearEquiv R M a).symm m b = m := by simp [Subsingleton.elim b a]
+
+/-- If `α` has a unique term, then the type of finitely supported functions `α →₀ M` is
+`R`-linearly equivalent to `M`. -/
+@[deprecated uniqueLinearEquiv (since := "2026-05-06")]
+noncomputable def LinearEquiv.finsuppUnique (α : Type*) [Unique α] : (α →₀ M) ≃ₗ[R] M :=
   { Finsupp.equivFunOnFinite.trans (Equiv.funUnique α M) with
     map_add' := fun _ _ => rfl
     map_smul' := fun _ _ => rfl }
 
 variable {R M}
 
-@[simp]
-theorem LinearEquiv.finsuppUnique_apply (f : α →₀ M) :
+set_option linter.deprecated false in
+@[deprecated uniqueLinearEquiv_apply (since := "2026-05-06")]
+theorem LinearEquiv.finsuppUnique_apply (α : Type*) [Unique α] (f : α →₀ M) :
     LinearEquiv.finsuppUnique R M α f = f default :=
   rfl
 
-variable {α}
-
-@[simp]
-theorem LinearEquiv.finsuppUnique_symm_apply (m : M) :
+set_option linter.deprecated false in
+@[deprecated uniqueLinearEquiv_symm_apply (since := "2026-05-06")]
+theorem LinearEquiv.finsuppUnique_symm_apply (α : Type*) [Unique α] (m : M) :
     (LinearEquiv.finsuppUnique R M α).symm m = Finsupp.single default m := by
   ext; simp [LinearEquiv.finsuppUnique, Equiv.funUnique, single, Pi.single,
     equivFunOnFinite, Function.update]
 
-end LinearEquiv.finsuppUnique
+end uniqueLinearEquiv
 
 variable {α : Type*} {M : Type*} {N : Type*} {P : Type*} {R : Type*} {S : Type*}
 variable [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M]

Mathlib/RepresentationTheory/Action.lean

@@ -81,7 +81,7 @@ variable (k G) in
 @[simps toLinearMap]
 def ε : (trivial k G k).IntertwiningMap (linearize k G (MonoidalCategoryStruct.tensorUnit
     (Action (Type w) G))) where
-  __ := Finsupp.LinearEquiv.finsuppUnique k k PUnit |>.symm.toLinearMap
+  __ := Finsupp.uniqueLinearEquiv k k PUnit.unit |>.symm.toLinearMap
   isIntertwining' g := by ext1; simp [linearize_single _]
 
 lemma ε_one : ε k G 1 = Finsupp.single PUnit.unit 1 := by
@@ -93,7 +93,7 @@ variable (k G) in
 /-- The unit of the linearize functor. -/
 @[simps toLinearMap]
 def η : (linearize k G (𝟙_ (Action (Type u) G))).IntertwiningMap (trivial k G k) where
-  __ := (Finsupp.LinearEquiv.finsuppUnique k k PUnit).toLinearMap
+  __ := (Finsupp.uniqueLinearEquiv k k PUnit.unit).toLinearMap
   isIntertwining' g := by ext; simp [linearize_single _]
 
 lemma η_single (x : PUnit) : η k G (Finsupp.single x 1) = 1 := by

Mathlib/RepresentationTheory/Equiv.lean

@@ -34,8 +34,7 @@ variable (k G) in
 /-- If there exists `G`-action on a trivial monoid `H` then the induced representation
   on `k[H]` is equivalent to the trivial representation. -/
 def ofMulActionSubsingletonEquivTrivial : (ofMulAction k G H).Equiv (trivial k G k) :=
-  letI : Unique H := uniqueOfSubsingleton 1
-  .mk (Finsupp.LinearEquiv.finsuppUnique _ _ _) fun g ↦ by
+  .mk (Finsupp.uniqueLinearEquiv _ _ 1) fun g ↦ by
     ext a; simp [Subsingleton.elim (g • a) a]
 
 @[simp]
@@ -45,9 +44,7 @@ lemma ofMulActionSubsingletonEquivTrivial_apply (f : H →₀ k) :
 @[simp]
 lemma ofMulActionSubsingletonEquivTrivial_symm_apply (r : k) :
     (ofMulActionSubsingletonEquivTrivial k G H).symm.toIntertwiningMap.toLinearMap r =
-      Finsupp.single 1 r := by
-  letI : Unique H := uniqueOfSubsingleton 1
-  simp [ofMulActionSubsingletonEquivTrivial, Subsingleton.elim (1 : H) (default : H)]
+      Finsupp.single 1 r := rfl
 
 variable (k G) in
 /-- The equivalence of representations between `(Fin 1 → G) →₀ k` and `G →₀ k`. -/