From aeffdb98b93eb74b14526c18115f99b170f2693a Mon Sep 17 00:00:00 2001
From: Raph-DG <raphaeldouglasgiles@gmail.com>
Date: Thu, 26 Feb 2026 13:01:52 +0100
Subject: [PATCH 01/11] Copied over the changes from the algebraic cycles repo

---
 Mathlib/Topology/LocallyFinsupp.lean | 78 ++++++++++++++++++++--------
 1 file changed, 56 insertions(+), 22 deletions(-)

diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index 1b6f5ee7a23861..c95548793050b0 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -110,6 +110,10 @@ lemma LocallyFiniteSupport.finite_inter_support_of_isCompact {W : Set X}
   rw [← lem f.support W]
   exact Finite.image Subtype.val this
 
+lemma Function.locallyFinsupp.locallyFiniteSupport [Zero Y] (f : locallyFinsupp X Y) :
+    LocallyFiniteSupport f.toFun :=
+  fun z ↦ f.supportLocallyFiniteWithinDomain' z (mem_of_subset_of_mem (fun _ a ↦ a) trivial)
+
 namespace Function.locallyFinsuppWithin
 
 /--
@@ -246,7 +250,7 @@ variable (U) in
 /--
 Functions with locally finite support within `U` form an additive subgroup of functions X → Y.
 -/
-protected def addSubgroup [AddCommGroup Y] : AddSubgroup (X → Y) where
+protected def addSubmonoid [AddMonoid Y] : AddSubmonoid (X → Y) where
   carrier := {f | f.support ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, Set.Finite (t ∩ f.support)}
   zero_mem' := by
     simp only [support_subset_iff, ne_eq, mem_setOf_eq, Pi.zero_apply, not_true_eq_false,
@@ -268,10 +272,21 @@ protected def addSubgroup [AddCommGroup Y] : AddSubgroup (X → Y) where
         mem_inter_iff, mem_support, Pi.add_apply, mem_union, true_and]
       by_contra! hCon
       simp_all
-  neg_mem' {f} hf := by
-    simp_all
 
-protected lemma memAddSubgroup [AddCommGroup Y] (D : locallyFinsuppWithin U Y) :
+protected lemma memAddSubmonoid [AddMonoid Y] (D : locallyFinsuppWithin U Y) :
+    (D : X → Y) ∈ locallyFinsuppWithin.addSubmonoid U :=
+  ⟨D.supportWithinDomain, D.supportLocallyFiniteWithinDomain⟩
+
+variable (U) in
+/--
+Functions with locally finite support within `U` form an additive subgroup of functions X → Y.
+-/
+protected def addSubgroup [AddGroup Y] : AddSubgroup (X → Y) where
+  carrier := {f | f.support ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, Set.Finite (t ∩ f.support)}
+  __ := locallyFinsuppWithin.addSubmonoid U
+  neg_mem' {f} hf := by simp_all
+
+protected lemma memAddSubgroup [AddGroup Y] (D : locallyFinsuppWithin U Y) :
     (D : X → Y) ∈ locallyFinsuppWithin.addSubgroup U :=
   ⟨D.supportWithinDomain, D.supportLocallyFiniteWithinDomain⟩
 
@@ -279,40 +294,59 @@ protected lemma memAddSubgroup [AddCommGroup Y] (D : locallyFinsuppWithin U Y) :
 Assign a function with locally finite support within `U` to a function in the subgroup.
 -/
 @[simps]
-def mk_of_mem [AddCommGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U) :
+def mk_of_mem [AddMonoid Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubmonoid U) :
     locallyFinsuppWithin U Y := ⟨f, hf.1, hf.2⟩
 
-instance [AddCommGroup Y] : Zero (locallyFinsuppWithin U Y) where
+instance [AddMonoid Y] : Zero (locallyFinsuppWithin U Y) where
   zero := mk_of_mem 0 <| zero_mem _
 
-instance [AddCommGroup Y] : Add (locallyFinsuppWithin U Y) where
-  add D₁ D₂ := mk_of_mem (D₁ + D₂) <| add_mem D₁.memAddSubgroup D₂.memAddSubgroup
+instance [AddMonoid Y] : Add (locallyFinsuppWithin U Y) where
+  add D₁ D₂ := mk_of_mem (D₁ + D₂) <| add_mem D₁.memAddSubmonoid D₂.memAddSubmonoid
 
-instance [AddCommGroup Y] : Neg (locallyFinsuppWithin U Y) where
-  neg D := mk_of_mem (-D) <| neg_mem D.memAddSubgroup
+instance [AddMonoid Y] : SMul ℕ (locallyFinsuppWithin U Y) where
+  smul n D := mk_of_mem (n • D) <| nsmul_mem D.memAddSubmonoid n
 
-instance [AddCommGroup Y] : Sub (locallyFinsuppWithin U Y) where
-  sub D₁ D₂ := mk_of_mem (D₁ - D₂) <| sub_mem D₁.memAddSubgroup D₂.memAddSubgroup
+/--
+Assign a function with locally finite support within `U` to a function in the subgroup.
+-/
+@[simps]
+def mk_of_mem' [AddGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U) :
+    locallyFinsuppWithin U Y := ⟨f, hf.1, hf.2⟩
 
-instance [AddCommGroup Y] : SMul ℕ (locallyFinsuppWithin U Y) where
-  smul n D := mk_of_mem (n • D) <| nsmul_mem D.memAddSubgroup n
+instance [AddGroup Y] : Neg (locallyFinsuppWithin U Y) where
+  neg D := mk_of_mem' (-D) <| neg_mem D.memAddSubgroup
 
-instance [AddCommGroup Y] : SMul ℤ (locallyFinsuppWithin U Y) where
-  smul n D := mk_of_mem (n • D) <| zsmul_mem D.memAddSubgroup n
+instance [AddGroup Y] : Sub (locallyFinsuppWithin U Y) where
+  sub D₁ D₂ := mk_of_mem' (D₁ - D₂) <| sub_mem D₁.memAddSubgroup D₂.memAddSubgroup
 
-@[simp] lemma coe_zero [AddCommGroup Y] :
+instance [AddGroup Y] : SMul ℤ (locallyFinsuppWithin U Y) where
+  smul n D := mk_of_mem' (n • D) <| zsmul_mem D.memAddSubgroup n
+
+@[simp] lemma coe_zero [AddMonoid Y] :
     ((0 : locallyFinsuppWithin U Y) : X → Y) = 0 := rfl
-@[simp] lemma coe_add [AddCommGroup Y] (D₁ D₂ : locallyFinsuppWithin U Y) :
+@[simp] lemma coe_add [AddMonoid Y] (D₁ D₂ : locallyFinsuppWithin U Y) :
     (↑(D₁ + D₂) : X → Y) = D₁ + D₂ := rfl
-@[simp] lemma coe_neg [AddCommGroup Y] (D : locallyFinsuppWithin U Y) :
+@[simp] lemma coe_neg [AddGroup Y] (D : locallyFinsuppWithin U Y) :
     (↑(-D) : X → Y) = -(D : X → Y) := rfl
-@[simp] lemma coe_sub [AddCommGroup Y] (D₁ D₂ : locallyFinsuppWithin U Y) :
+@[simp] lemma coe_sub [AddGroup Y] (D₁ D₂ : locallyFinsuppWithin U Y) :
     (↑(D₁ - D₂) : X → Y) = D₁ - D₂ := rfl
-@[simp] lemma coe_nsmul [AddCommGroup Y] (D : locallyFinsuppWithin U Y) (n : ℕ) :
+@[simp] lemma coe_nsmul [AddMonoid Y] (D : locallyFinsuppWithin U Y) (n : ℕ) :
     (↑(n • D) : X → Y) = n • (D : X → Y) := rfl
-@[simp] lemma coe_zsmul [AddCommGroup Y] (D : locallyFinsuppWithin U Y) (n : ℤ) :
+@[simp] lemma coe_zsmul [AddGroup Y] (D : locallyFinsuppWithin U Y) (n : ℤ) :
     (↑(n • D) : X → Y) = n • (D : X → Y) := rfl
 
+instance [AddMonoid Y] : AddMonoid (locallyFinsuppWithin U Y) :=
+  Injective.addMonoid (M₁ := locallyFinsuppWithin U Y) (M₂ := X → Y)
+    _ coe_injective coe_zero coe_add coe_nsmul
+
+instance [AddCommMonoid Y] : AddCommMonoid (locallyFinsuppWithin U Y) :=
+  Injective.addCommMonoid (M₁ := locallyFinsuppWithin U Y) (M₂ := X → Y)
+    _ coe_injective coe_zero coe_add coe_nsmul
+
+instance [AddGroup Y] : AddGroup (locallyFinsuppWithin U Y) :=
+  Injective.addGroup (M₁ := locallyFinsuppWithin U Y) (M₂ := X → Y)
+    _ coe_injective coe_zero coe_add coe_neg coe_sub coe_nsmul coe_zsmul
+
 instance [AddCommGroup Y] : AddCommGroup (locallyFinsuppWithin U Y) :=
   Injective.addCommGroup (M₁ := locallyFinsuppWithin U Y) (M₂ := X → Y)
     _ coe_injective coe_zero coe_add coe_neg coe_sub coe_nsmul coe_zsmul

From fe8a862371ad9b4ab93030b998e8357c6194d2d2 Mon Sep 17 00:00:00 2001
From: Raph-DG <raphaeldouglasgiles@gmail.com>
Date: Thu, 26 Feb 2026 13:11:36 +0100
Subject: [PATCH 02/11] Changed some docstrings

---
 Mathlib/Topology/LocallyFinsupp.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index c95548793050b0..9b1edb4699fd7b 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -248,7 +248,7 @@ defined pointwise.
 
 variable (U) in
 /--
-Functions with locally finite support within `U` form an additive subgroup of functions X → Y.
+Functions with locally finite support within `U` form an additive submonoid of functions `X → Y`.
 -/
 protected def addSubmonoid [AddMonoid Y] : AddSubmonoid (X → Y) where
   carrier := {f | f.support ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, Set.Finite (t ∩ f.support)}
@@ -279,7 +279,7 @@ protected lemma memAddSubmonoid [AddMonoid Y] (D : locallyFinsuppWithin U Y) :
 
 variable (U) in
 /--
-Functions with locally finite support within `U` form an additive subgroup of functions X → Y.
+Functions with locally finite support within `U` form an additive subgroup of functions `X → Y`.
 -/
 protected def addSubgroup [AddGroup Y] : AddSubgroup (X → Y) where
   carrier := {f | f.support ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, Set.Finite (t ∩ f.support)}

From 8989ec29b42b4395a6b671b2030805302873d0f1 Mon Sep 17 00:00:00 2001
From: Raphael Douglas Giles <77658801+Raph-DG@users.noreply.github.com>
Date: Thu, 5 Mar 2026 19:12:52 +0100
Subject: [PATCH 03/11] Update Mathlib/Topology/LocallyFinsupp.lean

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
---
 Mathlib/Topology/LocallyFinsupp.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index 9b1edb4699fd7b..1c2d7e52f0801c 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -112,7 +112,7 @@ lemma LocallyFiniteSupport.finite_inter_support_of_isCompact {W : Set X}
 
 lemma Function.locallyFinsupp.locallyFiniteSupport [Zero Y] (f : locallyFinsupp X Y) :
     LocallyFiniteSupport f.toFun :=
-  fun z ↦ f.supportLocallyFiniteWithinDomain' z (mem_of_subset_of_mem (fun _ a ↦ a) trivial)
+  (f.supportLocallyFiniteWithinDomain' · (by trivial))
 
 namespace Function.locallyFinsuppWithin
 

From 21cfb9bc98e6f2866c5538b40fb64dfc911602c6 Mon Sep 17 00:00:00 2001
From: Raphael Douglas Giles <77658801+Raph-DG@users.noreply.github.com>
Date: Thu, 5 Mar 2026 19:13:10 +0100
Subject: [PATCH 04/11] Update Mathlib/Topology/LocallyFinsupp.lean

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
---
 Mathlib/Topology/LocallyFinsupp.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index 1c2d7e52f0801c..b62e4097767d15 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -294,7 +294,7 @@ protected lemma memAddSubgroup [AddGroup Y] (D : locallyFinsuppWithin U Y) :
 Assign a function with locally finite support within `U` to a function in the subgroup.
 -/
 @[simps]
-def mk_of_mem [AddMonoid Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubmonoid U) :
+def mk_of_mem_addSubmonoid [AddMonoid Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubmonoid U) :
     locallyFinsuppWithin U Y := ⟨f, hf.1, hf.2⟩
 
 instance [AddMonoid Y] : Zero (locallyFinsuppWithin U Y) where

From 077cba8549509dd86a37d018426235d2410ff743 Mon Sep 17 00:00:00 2001
From: Raphael Douglas Giles <77658801+Raph-DG@users.noreply.github.com>
Date: Thu, 5 Mar 2026 19:16:35 +0100
Subject: [PATCH 05/11] Update Mathlib/Topology/LocallyFinsupp.lean

Co-authored-by: Dagur Asgeirsson <dagurtomas@gmail.com>
---
 Mathlib/Topology/LocallyFinsupp.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index b62e4097767d15..b0798b23921b79 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -310,7 +310,7 @@ instance [AddMonoid Y] : SMul ℕ (locallyFinsuppWithin U Y) where
 Assign a function with locally finite support within `U` to a function in the subgroup.
 -/
 @[simps]
-def mk_of_mem' [AddGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U) :
+def mk_of_mem_addSubgroup [AddGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U) :
     locallyFinsuppWithin U Y := ⟨f, hf.1, hf.2⟩
 
 instance [AddGroup Y] : Neg (locallyFinsuppWithin U Y) where

From 57dfffc52736a58b9a61d0898ee3bd0ff889c7ae Mon Sep 17 00:00:00 2001
From: Raph-DG <raphaeldouglasgiles@gmail.com>
Date: Thu, 5 Mar 2026 20:03:08 +0100
Subject: [PATCH 06/11] Made name changes consistent and added in depricated
 lemma

---
 Mathlib/Topology/LocallyFinsupp.lean | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index b0798b23921b79..a54ca537073428 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -294,17 +294,23 @@ protected lemma memAddSubgroup [AddGroup Y] (D : locallyFinsuppWithin U Y) :
 Assign a function with locally finite support within `U` to a function in the subgroup.
 -/
 @[simps]
-def mk_of_mem_addSubmonoid [AddMonoid Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubmonoid U) :
+def mk_of_mem_addSubmonoid [AddMonoid Y] (f : X → Y)
+    (hf : f ∈ locallyFinsuppWithin.addSubmonoid U) :
     locallyFinsuppWithin U Y := ⟨f, hf.1, hf.2⟩
 
+@[deprecated mk_of_mem_addSubmonoid (since := "2026-03-05")]
+def mk_of_mem [AddMonoid Y] (f : X → Y)
+    (hf : f ∈ locallyFinsuppWithin.addSubmonoid U) :
+    locallyFinsuppWithin U Y := mk_of_mem_addSubmonoid f hf
+
 instance [AddMonoid Y] : Zero (locallyFinsuppWithin U Y) where
-  zero := mk_of_mem 0 <| zero_mem _
+  zero := mk_of_mem_addSubmonoid 0 <| zero_mem _
 
 instance [AddMonoid Y] : Add (locallyFinsuppWithin U Y) where
-  add D₁ D₂ := mk_of_mem (D₁ + D₂) <| add_mem D₁.memAddSubmonoid D₂.memAddSubmonoid
+  add D₁ D₂ := mk_of_mem_addSubmonoid (D₁ + D₂) <| add_mem D₁.memAddSubmonoid D₂.memAddSubmonoid
 
 instance [AddMonoid Y] : SMul ℕ (locallyFinsuppWithin U Y) where
-  smul n D := mk_of_mem (n • D) <| nsmul_mem D.memAddSubmonoid n
+  smul n D := mk_of_mem_addSubmonoid (n • D) <| nsmul_mem D.memAddSubmonoid n
 
 /--
 Assign a function with locally finite support within `U` to a function in the subgroup.
@@ -314,13 +320,13 @@ def mk_of_mem_addSubgroup [AddGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppW
     locallyFinsuppWithin U Y := ⟨f, hf.1, hf.2⟩
 
 instance [AddGroup Y] : Neg (locallyFinsuppWithin U Y) where
-  neg D := mk_of_mem' (-D) <| neg_mem D.memAddSubgroup
+  neg D := mk_of_mem_addSubgroup (-D) <| neg_mem D.memAddSubgroup
 
 instance [AddGroup Y] : Sub (locallyFinsuppWithin U Y) where
-  sub D₁ D₂ := mk_of_mem' (D₁ - D₂) <| sub_mem D₁.memAddSubgroup D₂.memAddSubgroup
+  sub D₁ D₂ := mk_of_mem_addSubgroup (D₁ - D₂) <| sub_mem D₁.memAddSubgroup D₂.memAddSubgroup
 
 instance [AddGroup Y] : SMul ℤ (locallyFinsuppWithin U Y) where
-  smul n D := mk_of_mem' (n • D) <| zsmul_mem D.memAddSubgroup n
+  smul n D := mk_of_mem_addSubgroup (n • D) <| zsmul_mem D.memAddSubgroup n
 
 @[simp] lemma coe_zero [AddMonoid Y] :
     ((0 : locallyFinsuppWithin U Y) : X → Y) = 0 := rfl

From 2733fd8224bcc7475b0078f7216fc0d9943775e9 Mon Sep 17 00:00:00 2001
From: Raph-DG <raphaeldouglasgiles@gmail.com>
Date: Thu, 5 Mar 2026 20:40:14 +0100
Subject: [PATCH 07/11] Added a docstring

---
 Mathlib/Topology/LocallyFinsupp.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index a54ca537073428..deae4b4c6daf51 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -298,6 +298,9 @@ def mk_of_mem_addSubmonoid [AddMonoid Y] (f : X → Y)
     (hf : f ∈ locallyFinsuppWithin.addSubmonoid U) :
     locallyFinsuppWithin U Y := ⟨f, hf.1, hf.2⟩
 
+/--
+Deprecated spelling of `mk_of_mem_addSubmonoid`.
+-/
 @[deprecated mk_of_mem_addSubmonoid (since := "2026-03-05")]
 def mk_of_mem [AddMonoid Y] (f : X → Y)
     (hf : f ∈ locallyFinsuppWithin.addSubmonoid U) :

From 23caa082cf08bda6d8503788fe140f882c5cbd4f Mon Sep 17 00:00:00 2001
From: Raph-DG <raphaeldouglasgiles@gmail.com>
Date: Fri, 6 Mar 2026 10:26:09 +0100
Subject: [PATCH 08/11] Changed the alias

---
 Mathlib/Topology/LocallyFinsupp.lean | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index deae4b4c6daf51..18d97d09925855 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -298,14 +298,6 @@ def mk_of_mem_addSubmonoid [AddMonoid Y] (f : X → Y)
     (hf : f ∈ locallyFinsuppWithin.addSubmonoid U) :
     locallyFinsuppWithin U Y := ⟨f, hf.1, hf.2⟩
 
-/--
-Deprecated spelling of `mk_of_mem_addSubmonoid`.
--/
-@[deprecated mk_of_mem_addSubmonoid (since := "2026-03-05")]
-def mk_of_mem [AddMonoid Y] (f : X → Y)
-    (hf : f ∈ locallyFinsuppWithin.addSubmonoid U) :
-    locallyFinsuppWithin U Y := mk_of_mem_addSubmonoid f hf
-
 instance [AddMonoid Y] : Zero (locallyFinsuppWithin U Y) where
   zero := mk_of_mem_addSubmonoid 0 <| zero_mem _
 
@@ -322,6 +314,8 @@ Assign a function with locally finite support within `U` to a function in the su
 def mk_of_mem_addSubgroup [AddGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U) :
     locallyFinsuppWithin U Y := ⟨f, hf.1, hf.2⟩
 
+@[deprecated] alias mk_of_mem := mk_of_mem_addSubgroup
+
 instance [AddGroup Y] : Neg (locallyFinsuppWithin U Y) where
   neg D := mk_of_mem_addSubgroup (-D) <| neg_mem D.memAddSubgroup
 

From 722a27586d889bf1faebbdb3bab16ae6e0ab753d Mon Sep 17 00:00:00 2001
From: Raph-DG <raphaeldouglasgiles@gmail.com>
Date: Fri, 6 Mar 2026 10:44:00 +0100
Subject: [PATCH 09/11] Added some arguments to the alias

---
 Mathlib/Topology/LocallyFinsupp.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index 18d97d09925855..40c78a3615351e 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -314,7 +314,8 @@ Assign a function with locally finite support within `U` to a function in the su
 def mk_of_mem_addSubgroup [AddGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U) :
     locallyFinsuppWithin U Y := ⟨f, hf.1, hf.2⟩
 
-@[deprecated] alias mk_of_mem := mk_of_mem_addSubgroup
+@[deprecated] alias mk_of_mem [AddGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U)
+    := mk_of_mem_addSubgroup
 
 instance [AddGroup Y] : Neg (locallyFinsuppWithin U Y) where
   neg D := mk_of_mem_addSubgroup (-D) <| neg_mem D.memAddSubgroup

From e6ad9f583d037daed7dc1b3e9998582dec10f506 Mon Sep 17 00:00:00 2001
From: Raph-DG <raphaeldouglasgiles@gmail.com>
Date: Fri, 6 Mar 2026 10:48:39 +0100
Subject: [PATCH 10/11] Changed alias back

---
 Mathlib/Topology/LocallyFinsupp.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index 40c78a3615351e..18d97d09925855 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -314,8 +314,7 @@ Assign a function with locally finite support within `U` to a function in the su
 def mk_of_mem_addSubgroup [AddGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U) :
     locallyFinsuppWithin U Y := ⟨f, hf.1, hf.2⟩
 
-@[deprecated] alias mk_of_mem [AddGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U)
-    := mk_of_mem_addSubgroup
+@[deprecated] alias mk_of_mem := mk_of_mem_addSubgroup
 
 instance [AddGroup Y] : Neg (locallyFinsuppWithin U Y) where
   neg D := mk_of_mem_addSubgroup (-D) <| neg_mem D.memAddSubgroup

From 12133112391f272fe4d00f20dda581a82139368e Mon Sep 17 00:00:00 2001
From: Raph-DG <raphaeldouglasgiles@gmail.com>
Date: Fri, 6 Mar 2026 10:50:38 +0100
Subject: [PATCH 11/11] Added in a date for the deprecation

---
 Mathlib/Topology/LocallyFinsupp.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/LocallyFinsupp.lean b/Mathlib/Topology/LocallyFinsupp.lean
index 18d97d09925855..eea21ef429ac82 100644
--- a/Mathlib/Topology/LocallyFinsupp.lean
+++ b/Mathlib/Topology/LocallyFinsupp.lean
@@ -314,7 +314,7 @@ Assign a function with locally finite support within `U` to a function in the su
 def mk_of_mem_addSubgroup [AddGroup Y] (f : X → Y) (hf : f ∈ locallyFinsuppWithin.addSubgroup U) :
     locallyFinsuppWithin U Y := ⟨f, hf.1, hf.2⟩
 
-@[deprecated] alias mk_of_mem := mk_of_mem_addSubgroup
+@[deprecated (since := "2026-03-06")] alias mk_of_mem := mk_of_mem_addSubgroup
 
 instance [AddGroup Y] : Neg (locallyFinsuppWithin U Y) where
   neg D := mk_of_mem_addSubgroup (-D) <| neg_mem D.memAddSubgroup