From 7dcbb0701f29df5088a53c9f7281e3a022083556 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sat, 28 Mar 2026 08:44:13 -0400
Subject: [PATCH 01/27] Moved three results to recover weaker hypotheses.

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 29 ++++++++++++--------
 1 file changed, 17 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index ab33b541f87304..39498452d3c126 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -158,6 +158,23 @@ theorem coe_toStrongDual (x' : WeakDual 𝕜 E) : (toStrongDual x' : E → 𝕜)
 theorem toStrongDual_inj (x' y' : WeakDual 𝕜 E) : toStrongDual x' = toStrongDual y' ↔ x' = y' :=
   (LinearEquiv.injective toStrongDual).eq_iff
 
+section Polar
+
+variable (𝕜)
+
+/-- The polar set `polar 𝕜 s` of `s : Set E` seen as a subset of the dual of `E` with the
+weak-star topology is `WeakDual.polar 𝕜 s`. -/
+def polar (s : Set E) : Set (WeakDual 𝕜 E) := toStrongDual ⁻¹' (StrongDual.polar 𝕜) s
+
+theorem polar_def (s : Set E) : polar 𝕜 s = { f : WeakDual 𝕜 E | ∀ x ∈ s, ‖f x‖ ≤ 1 } := rfl
+
+/-- The polar `polar 𝕜 s` of a set `s : E` is a closed subset when the weak star topology
+is used. -/
+theorem isClosed_polar (s : Set E) : IsClosed (polar 𝕜 s) := by
+  simp only [polar_def, setOf_forall]
+  exact isClosed_biInter fun x hx => isClosed_Iic.preimage (WeakBilin.eval_continuous _ _).norm
+
+end Polar
 section Bornology
 
 variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
@@ -316,18 +333,6 @@ theorem isCompact_closedBall [ProperSpace 𝕜] (x' : StrongDual 𝕜 E) (r : 
 section PolarSets
 variable (𝕜)
 
-/-- The polar set `polar 𝕜 s` of `s : Set E` seen as a subset of the dual of `E` with the
-weak-star topology is `WeakDual.polar 𝕜 s`. -/
-def polar (s : Set E) : Set (WeakDual 𝕜 E) := toStrongDual ⁻¹' (StrongDual.polar 𝕜) s
-
-theorem polar_def (s : Set E) : polar 𝕜 s = { f : WeakDual 𝕜 E | ∀ x ∈ s, ‖f x‖ ≤ 1 } := rfl
-
-/-- The polar `polar 𝕜 s` of a set `s : E` is a closed subset when the weak star topology
-is used. -/
-theorem isClosed_polar (s : Set E) : IsClosed (polar 𝕜 s) := by
-  simp only [polar_def, setOf_forall]
-  exact isClosed_biInter fun x hx => isClosed_Iic.preimage (WeakBilin.eval_continuous _ _).norm
-
 /-- Polar sets of neighborhoods of the origin are bounded in the weak dual. -/
 theorem isBounded_polar {s : Set E} (s_nhds : s ∈ 𝓝 (0 : E)) : IsBounded (polar 𝕜 s) :=
   isBounded_toStrongDual_preimage_iff_isBounded.mpr

From f23769bc7e3d7e9ba197e766e5f49b63c9dc1633 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sat, 28 Mar 2026 08:48:02 -0400
Subject: [PATCH 02/27] space

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index 93e7677f9651e8..f9b934d49de3e0 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -175,6 +175,7 @@ theorem isClosed_polar (s : Set E) : IsClosed (polar 𝕜 s) := by
   exact isClosed_biInter fun x hx => isClosed_Iic.preimage (WeakBilin.eval_continuous _ _).norm
 
 end Polar
+
 section Bornology
 
 variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]

From 9742bcbb96507fc509e53f3bf17bfa22e96946ef Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sat, 28 Mar 2026 13:50:11 -0400
Subject: [PATCH 03/27] Used the "M" rename to specify when NormedSpace `E` was
 being used. (Thanks Monica!)

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 42 +++++++++-----------
 1 file changed, 19 insertions(+), 23 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index f9b934d49de3e0..a51ca07ab4ba39 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -142,40 +142,22 @@ end StrongDual
 namespace WeakDual
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
-variable {E : Type*} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E]
+variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M]
 
 /-- For vector spaces `E`, there is a canonical map `WeakDual 𝕜 E → StrongDual 𝕜 E` (the "identity"
 mapping). It is a linear equivalence. Here it is implemented as the inverse of the linear
 equivalence `StrongDual.toWeakDual` in the other direction. -/
-def toStrongDual : WeakDual 𝕜 E ≃ₗ[𝕜] StrongDual 𝕜 E :=
+def toStrongDual : WeakDual 𝕜 M ≃ₗ[𝕜] StrongDual 𝕜 M :=
   StrongDual.toWeakDual.symm
 
 @[simp]
-theorem toStrongDual_apply (x : WeakDual 𝕜 E) (y : E) : (toStrongDual x) y = x y := rfl
+theorem toStrongDual_apply (x : WeakDual 𝕜 M) (y : M) : (toStrongDual x) y = x y := rfl
 
-theorem coe_toStrongDual (x' : WeakDual 𝕜 E) : (toStrongDual x' : E → 𝕜) = x' := rfl
+theorem coe_toStrongDual (x' : WeakDual 𝕜 M) : (toStrongDual x' : M → 𝕜) = x' := rfl
 
-theorem toStrongDual_inj (x' y' : WeakDual 𝕜 E) : toStrongDual x' = toStrongDual y' ↔ x' = y' :=
+theorem toStrongDual_inj (x' y' : WeakDual 𝕜 M) : toStrongDual x' = toStrongDual y' ↔ x' = y' :=
   (LinearEquiv.injective toStrongDual).eq_iff
 
-section Polar
-
-variable (𝕜)
-
-/-- The polar set `polar 𝕜 s` of `s : Set E` seen as a subset of the dual of `E` with the
-weak-star topology is `WeakDual.polar 𝕜 s`. -/
-def polar (s : Set E) : Set (WeakDual 𝕜 E) := toStrongDual ⁻¹' (StrongDual.polar 𝕜) s
-
-theorem polar_def (s : Set E) : polar 𝕜 s = { f : WeakDual 𝕜 E | ∀ x ∈ s, ‖f x‖ ≤ 1 } := rfl
-
-/-- The polar `polar 𝕜 s` of a set `s : E` is a closed subset when the weak star topology
-is used. -/
-theorem isClosed_polar (s : Set E) : IsClosed (polar 𝕜 s) := by
-  simp only [polar_def, setOf_forall]
-  exact isClosed_biInter fun x hx => isClosed_Iic.preimage (WeakBilin.eval_continuous _ _).norm
-
-end Polar
-
 section Bornology
 
 variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
@@ -337,7 +319,21 @@ theorem isCompact_closedBall [ProperSpace 𝕜] (x' : StrongDual 𝕜 E) (r : 
 -/
 
 section PolarSets
+
 variable (𝕜)
+variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M]
+
+/-- The polar set `polar 𝕜 s` of `s : Set E` seen as a subset of the dual of `E` with the
+weak-star topology is `WeakDual.polar 𝕜 s`. -/
+def polar (s : Set M) : Set (WeakDual 𝕜 M) := toStrongDual ⁻¹' (StrongDual.polar 𝕜) s
+
+theorem polar_def (s : Set M) : polar 𝕜 s = { f : WeakDual 𝕜 M | ∀ x ∈ s, ‖f x‖ ≤ 1 } := rfl
+
+/-- The polar `polar 𝕜 s` of a set `s : E` is a closed subset when the weak star topology
+is used. -/
+theorem isClosed_polar (s : Set M) : IsClosed (polar 𝕜 s) := by
+  simp only [polar_def, setOf_forall]
+  exact isClosed_biInter fun x hx => isClosed_Iic.preimage (WeakBilin.eval_continuous _ _).norm
 
 /-- Polar sets of neighborhoods of the origin are bounded in the weak dual. -/
 theorem isBounded_polar {s : Set E} (s_nhds : s ∈ 𝓝 (0 : E)) : IsBounded (polar 𝕜 s) :=

From d03bc30c4ba69ee2f53d89ccdedd5903848d8aef Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sat, 28 Mar 2026 14:12:08 -0400
Subject: [PATCH 04/27] Globalize vars

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index a51ca07ab4ba39..fa3a1e4c85077b 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -114,6 +114,10 @@ open Filter Function Bornology Metric Set Topology Filter
 ### Equivalences between `StrongDual` and `WeakDual`
 -/
 
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M]
+variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
+
 namespace StrongDual
 
 section
@@ -141,9 +145,6 @@ end StrongDual
 
 namespace WeakDual
 
-variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
-variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M]
-
 /-- For vector spaces `E`, there is a canonical map `WeakDual 𝕜 E → StrongDual 𝕜 E` (the "identity"
 mapping). It is a linear equivalence. Here it is implemented as the inverse of the linear
 equivalence `StrongDual.toWeakDual` in the other direction. -/
@@ -160,8 +161,6 @@ theorem toStrongDual_inj (x' y' : WeakDual 𝕜 M) : toStrongDual x' = toStrongD
 
 section Bornology
 
-variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
-
 /-- The bornology on `WeakDual 𝕜 F` is the norm bornology inherited from `StrongDual 𝕜 F`.
 
 Note: This is a pragmatic choice. To be precise, the bornology of a weak topology should be
@@ -197,9 +196,6 @@ i.e., that the weak-* topology is coarser (not necessarily strictly) than the to
 by the dual-norm (i.e. the operator-norm).
 -/
 
-variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
-variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
-
 namespace NormedSpace
 
 namespace Dual
@@ -321,7 +317,6 @@ theorem isCompact_closedBall [ProperSpace 𝕜] (x' : StrongDual 𝕜 E) (r : 
 section PolarSets
 
 variable (𝕜)
-variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M]
 
 /-- The polar set `polar 𝕜 s` of `s : Set E` seen as a subset of the dual of `E` with the
 weak-star topology is `WeakDual.polar 𝕜 s`. -/

From a9ecdc070f046d695c6efda1cc275f2fef45a215 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sun, 29 Mar 2026 08:31:41 -0400
Subject: [PATCH 05/27] Globalized more, and corrected breakage

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 31 ++++++++++----------
 1 file changed, 15 insertions(+), 16 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index fa3a1e4c85077b..50e30ff9bbddea 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -124,7 +124,7 @@ section
 
 variable {R : Type*} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R]
   [ContinuousConstSMul R R]
-variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module R M]
+variable [Module R M]
 
 /-- For vector spaces `M`, there is a canonical map `StrongDual R M → WeakDual R M` (the "identity"
 mapping). It is a linear equivalence. -/
@@ -362,25 +362,25 @@ end PolarSets
 
 open TopologicalSpace
 
-variable (𝕜 V : Type*) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V]
-variable [TopologicalSpace.SeparableSpace V] (K : Set (WeakDual 𝕜 V))
+variable (𝕜 V)
+variable [TopologicalSpace.SeparableSpace E] (K : Set (WeakDual 𝕜 E))
 
 /-- In a separable normed space, there exists a sequence of continuous functions that
 separates points of the weak dual. -/
-lemma exists_countable_separating : ∃ (gs : ℕ → (WeakDual 𝕜 V) → 𝕜),
+lemma exists_countable_separating : ∃ (gs : ℕ → (WeakDual 𝕜 E) → 𝕜),
     (∀ n, Continuous (gs n)) ∧ (∀ ⦃x y⦄, x ≠ y → ∃ n, gs n x ≠ gs n y) := by
-  use (fun n φ ↦ φ (denseSeq V n))
+  use (fun n φ ↦ φ (denseSeq E n))
   constructor
   · exact fun _ ↦ eval_continuous _
   · intro w y w_ne_y
     contrapose! w_ne_y
     exact DFunLike.ext'_iff.mpr <| (map_continuous w).ext_on
-      (denseRange_denseSeq V) (map_continuous y) (Set.eqOn_range.mpr (funext w_ne_y))
+      (denseRange_denseSeq E) (map_continuous y) (Set.eqOn_range.mpr (funext w_ne_y))
 
 /-- A compact subset of the weak dual of a separable normed space is metrizable. -/
 lemma metrizable_of_isCompact (K_cpt : IsCompact K) : TopologicalSpace.MetrizableSpace K := by
   have : CompactSpace K := isCompact_iff_compactSpace.mp K_cpt
-  obtain ⟨gs, gs_cont, gs_sep⟩ := exists_countable_separating 𝕜 V
+  obtain ⟨gs, gs_cont, gs_sep⟩ := exists_countable_separating 𝕜 (E := E)
   exact Metric.PiNatEmbed.TopologicalSpace.MetrizableSpace.of_countable_separating
     (fun n k ↦ gs n k) (fun n ↦ (gs_cont n).comp continuous_subtype_val)
     fun x y hxy ↦ gs_sep <| Subtype.val_injective.ne hxy
@@ -388,29 +388,28 @@ lemma metrizable_of_isCompact (K_cpt : IsCompact K) : TopologicalSpace.Metrizabl
 variable [ProperSpace 𝕜] (K_cpt : IsCompact K)
 
 /-- Bounded closed sets in the weak dual of a separable normed space are sequentially compact. -/
-theorem isSeqCompact_of_isBounded_of_isClosed {s : Set (WeakDual 𝕜 V)}
+theorem isSeqCompact_of_isBounded_of_isClosed {s : Set (WeakDual 𝕜 E)}
     (hb : IsBounded s) (hc : IsClosed s) :
     IsSeqCompact s := by
   have b_isCompact' : CompactSpace s :=
     isCompact_iff_compactSpace.mp <| isCompact_of_bounded_of_closed hb hc
   have b_isMetrizable : TopologicalSpace.MetrizableSpace s :=
-    metrizable_of_isCompact 𝕜 V s <| isCompact_of_bounded_of_closed hb hc
-  have seq_cont_phi : SeqContinuous (fun φ : s ↦ (φ : WeakDual 𝕜 V)) :=
+    metrizable_of_isCompact 𝕜 s <| isCompact_of_bounded_of_closed hb hc
+  have seq_cont_phi : SeqContinuous (fun φ : s ↦ (φ : WeakDual 𝕜 E)) :=
     continuous_iff_seqContinuous.mp continuous_subtype_val
   simpa using IsSeqCompact.range seq_cont_phi
 
 /-- The **Sequential Banach-Alaoglu theorem**: the polar set of a neighborhood `s` of the origin in
 a separable normed space `V` is a sequentially compact subset of `WeakDual 𝕜 V`. -/
-theorem isSeqCompact_polar {s : Set V} (s_nhd : s ∈ 𝓝 (0 : V)) :
+theorem isSeqCompact_polar {s : Set E} (s_nhd : s ∈ 𝓝 (0 : E)) :
     IsSeqCompact (polar 𝕜 s) :=
-  isSeqCompact_of_isBounded_of_isClosed (s := polar 𝕜 s) _ _
-    (isBounded_polar 𝕜 s_nhd) (isClosed_polar _ _)
+  isSeqCompact_of_isBounded_of_isClosed 𝕜 (isBounded_polar 𝕜 s_nhd) (isClosed_polar _ _)
+
 
 /-- The **Sequential Banach-Alaoglu theorem**: closed balls of the dual of a separable
 normed space `V` are sequentially compact in the weak-* topology. -/
-theorem isSeqCompact_closedBall (x' : StrongDual 𝕜 V) (r : ℝ) :
+theorem isSeqCompact_closedBall (x' : StrongDual 𝕜 E) (r : ℝ) :
     IsSeqCompact (toStrongDual ⁻¹' Metric.closedBall x' r) :=
-  isSeqCompact_of_isBounded_of_isClosed 𝕜 V
-    (isBounded_closedBall x' r) (isClosed_closedBall x' r)
+  isSeqCompact_of_isBounded_of_isClosed 𝕜 (isBounded_closedBall x' r) (isClosed_closedBall x' r)
 
 end WeakDual

From 1ef92ce017e75de09f3736c0b836378244a5b460 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sun, 29 Mar 2026 08:32:11 -0400
Subject: [PATCH 06/27] cleanup

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index 50e30ff9bbddea..7cbb2d1348c228 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -123,8 +123,7 @@ namespace StrongDual
 section
 
 variable {R : Type*} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R]
-  [ContinuousConstSMul R R]
-variable [Module R M]
+variable [ContinuousConstSMul R R] [Module R M]
 
 /-- For vector spaces `M`, there is a canonical map `StrongDual R M → WeakDual R M` (the "identity"
 mapping). It is a linear equivalence. -/

From e3a4440f7b4c22fecb95d3f8bad5b8daa321ae55 Mon Sep 17 00:00:00 2001
From: Jon Bannon <59937998+JonBannon@users.noreply.github.com>
Date: Sun, 29 Mar 2026 09:07:54 -0400
Subject: [PATCH 07/27] Update Mathlib/Analysis/Normed/Module/WeakDual.lean

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index 7cbb2d1348c228..b6f937f82d38ca 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -361,8 +361,7 @@ end PolarSets
 
 open TopologicalSpace
 
-variable (𝕜 V)
-variable [TopologicalSpace.SeparableSpace E] (K : Set (WeakDual 𝕜 E))
+variable (𝕜 E) [TopologicalSpace.SeparableSpace E] (K : Set (WeakDual 𝕜 E))
 
 /-- In a separable normed space, there exists a sequence of continuous functions that
 separates points of the weak dual. -/

From 4bce9a9ee595ba6c6552b90398f33da8a36aa4d5 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sun, 29 Mar 2026 09:14:44 -0400
Subject: [PATCH 08/27] Fixed spurious `V` and breakage I caused.

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index b6f937f82d38ca..45aa3d92eb869f 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -123,7 +123,8 @@ namespace StrongDual
 section
 
 variable {R : Type*} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R]
-variable [ContinuousConstSMul R R] [Module R M]
+  [ContinuousConstSMul R R]
+variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module R M]
 
 /-- For vector spaces `M`, there is a canonical map `StrongDual R M → WeakDual R M` (the "identity"
 mapping). It is a linear equivalence. -/
@@ -378,7 +379,7 @@ lemma exists_countable_separating : ∃ (gs : ℕ → (WeakDual 𝕜 E) → 𝕜
 /-- A compact subset of the weak dual of a separable normed space is metrizable. -/
 lemma metrizable_of_isCompact (K_cpt : IsCompact K) : TopologicalSpace.MetrizableSpace K := by
   have : CompactSpace K := isCompact_iff_compactSpace.mp K_cpt
-  obtain ⟨gs, gs_cont, gs_sep⟩ := exists_countable_separating 𝕜 (E := E)
+  obtain ⟨gs, gs_cont, gs_sep⟩ := exists_countable_separating 𝕜 E
   exact Metric.PiNatEmbed.TopologicalSpace.MetrizableSpace.of_countable_separating
     (fun n k ↦ gs n k) (fun n ↦ (gs_cont n).comp continuous_subtype_val)
     fun x y hxy ↦ gs_sep <| Subtype.val_injective.ne hxy
@@ -392,7 +393,7 @@ theorem isSeqCompact_of_isBounded_of_isClosed {s : Set (WeakDual 𝕜 E)}
   have b_isCompact' : CompactSpace s :=
     isCompact_iff_compactSpace.mp <| isCompact_of_bounded_of_closed hb hc
   have b_isMetrizable : TopologicalSpace.MetrizableSpace s :=
-    metrizable_of_isCompact 𝕜 s <| isCompact_of_bounded_of_closed hb hc
+    metrizable_of_isCompact 𝕜 E s <| isCompact_of_bounded_of_closed hb hc
   have seq_cont_phi : SeqContinuous (fun φ : s ↦ (φ : WeakDual 𝕜 E)) :=
     continuous_iff_seqContinuous.mp continuous_subtype_val
   simpa using IsSeqCompact.range seq_cont_phi
@@ -401,13 +402,14 @@ theorem isSeqCompact_of_isBounded_of_isClosed {s : Set (WeakDual 𝕜 E)}
 a separable normed space `V` is a sequentially compact subset of `WeakDual 𝕜 V`. -/
 theorem isSeqCompact_polar {s : Set E} (s_nhd : s ∈ 𝓝 (0 : E)) :
     IsSeqCompact (polar 𝕜 s) :=
-  isSeqCompact_of_isBounded_of_isClosed 𝕜 (isBounded_polar 𝕜 s_nhd) (isClosed_polar _ _)
-
+  isSeqCompact_of_isBounded_of_isClosed (s := polar 𝕜 s) _ _
+    (isBounded_polar 𝕜 s_nhd) (isClosed_polar _ _)
 
 /-- The **Sequential Banach-Alaoglu theorem**: closed balls of the dual of a separable
 normed space `V` are sequentially compact in the weak-* topology. -/
 theorem isSeqCompact_closedBall (x' : StrongDual 𝕜 E) (r : ℝ) :
     IsSeqCompact (toStrongDual ⁻¹' Metric.closedBall x' r) :=
-  isSeqCompact_of_isBounded_of_isClosed 𝕜 (isBounded_closedBall x' r) (isClosed_closedBall x' r)
+  isSeqCompact_of_isBounded_of_isClosed 𝕜 E
+    (isBounded_closedBall x' r) (isClosed_closedBall x' r)
 
 end WeakDual

From 00997777d6504203bb5adbef0682fccb4560af4c Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sun, 29 Mar 2026 12:33:22 -0400
Subject: [PATCH 09/27] Globalized "all" variables.

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index 45aa3d92eb869f..0bacdd4211ca9b 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -114,18 +114,15 @@ open Filter Function Bornology Metric Set Topology Filter
 ### Equivalences between `StrongDual` and `WeakDual`
 -/
 
-variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
-variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M]
+variable {R : Type*} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R]
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [ContinuousConstSMul R R]
+variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M] [Module R M]
 variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
 
 namespace StrongDual
 
 section
 
-variable {R : Type*} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R]
-  [ContinuousConstSMul R R]
-variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module R M]
-
 /-- For vector spaces `M`, there is a canonical map `StrongDual R M → WeakDual R M` (the "identity"
 mapping). It is a linear equivalence. -/
 def toWeakDual : StrongDual R M ≃ₗ[R] WeakDual R M :=

From 85ce1a53faf6fec0d97104801a038ba4f6908d7b Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Sun, 29 Mar 2026 12:38:31 -0400
Subject: [PATCH 10/27] Somehow STILL missed some changes.

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index 0bacdd4211ca9b..400cf7af42dd17 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -399,14 +399,12 @@ theorem isSeqCompact_of_isBounded_of_isClosed {s : Set (WeakDual 𝕜 E)}
 a separable normed space `V` is a sequentially compact subset of `WeakDual 𝕜 V`. -/
 theorem isSeqCompact_polar {s : Set E} (s_nhd : s ∈ 𝓝 (0 : E)) :
     IsSeqCompact (polar 𝕜 s) :=
-  isSeqCompact_of_isBounded_of_isClosed (s := polar 𝕜 s) _ _
-    (isBounded_polar 𝕜 s_nhd) (isClosed_polar _ _)
+  isSeqCompact_of_isBounded_of_isClosed 𝕜 _ (isBounded_polar 𝕜 s_nhd) (isClosed_polar _ _)
 
 /-- The **Sequential Banach-Alaoglu theorem**: closed balls of the dual of a separable
 normed space `V` are sequentially compact in the weak-* topology. -/
 theorem isSeqCompact_closedBall (x' : StrongDual 𝕜 E) (r : ℝ) :
     IsSeqCompact (toStrongDual ⁻¹' Metric.closedBall x' r) :=
-  isSeqCompact_of_isBounded_of_isClosed 𝕜 E
-    (isBounded_closedBall x' r) (isClosed_closedBall x' r)
+  isSeqCompact_of_isBounded_of_isClosed 𝕜 _ (isBounded_closedBall x' r) (isClosed_closedBall x' r)
 
 end WeakDual

From 4295dfcd6a70095c71e32156b644e23b4eabd928 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Mon, 30 Mar 2026 06:49:46 -0400
Subject: [PATCH 11/27] De-globalized R.

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index 400cf7af42dd17..919eef1cec3289 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -114,15 +114,17 @@ open Filter Function Bornology Metric Set Topology Filter
 ### Equivalences between `StrongDual` and `WeakDual`
 -/
 
-variable {R : Type*} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R]
-variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [ContinuousConstSMul R R]
-variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M] [Module R M]
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M]
 variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
 
 namespace StrongDual
 
 section
 
+variable {R : Type*} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R]
+variable [ContinuousConstSMul R R] [Module R M]
+
 /-- For vector spaces `M`, there is a canonical map `StrongDual R M → WeakDual R M` (the "identity"
 mapping). It is a linear equivalence. -/
 def toWeakDual : StrongDual R M ≃ₗ[R] WeakDual R M :=

From fa8f04ab70bafd96a72d233f3ebb44f979563fee Mon Sep 17 00:00:00 2001
From: Jon Bannon <59937998+JonBannon@users.noreply.github.com>
Date: Mon, 30 Mar 2026 10:52:07 -0400
Subject: [PATCH 12/27] Update Mathlib/Analysis/Normed/Module/WeakDual.lean

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index 919eef1cec3289..9cc255bf639ae0 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -115,7 +115,7 @@ open Filter Function Bornology Metric Set Topology Filter
 -/
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
-variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module 𝕜 M]
+variable {M : Type*} [AddCommGroup M] [TopologicalSpace M] [Module 𝕜 M]
 variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
 
 namespace StrongDual

From a025839c3593c12a9a45449081a0901fc13a407d Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Mon, 30 Mar 2026 11:01:19 -0400
Subject: [PATCH 13/27] Attempt to handle AddCommMonoid mask correctly...

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index 9cc255bf639ae0..c1a8f0394c516f 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -114,16 +114,17 @@ open Filter Function Bornology Metric Set Topology Filter
 ### Equivalences between `StrongDual` and `WeakDual`
 -/
 
-variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
-variable {M : Type*} [AddCommGroup M] [TopologicalSpace M] [Module 𝕜 M]
-variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
+variable {𝕜 M E R : Type*}
+variable [NontriviallyNormedField 𝕜]
+variable [AddCommGroup M] [TopologicalSpace M] [Module 𝕜 M]
+variable [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
 
 namespace StrongDual
 
 section
 
-variable {R : Type*} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R]
-variable [ContinuousConstSMul R R] [Module R M]
+variable [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R]
+variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module R M] [ContinuousConstSMul R R]
 
 /-- For vector spaces `M`, there is a canonical map `StrongDual R M → WeakDual R M` (the "identity"
 mapping). It is a linear equivalence. -/

From db45164229c8b3a1545d2ac6b6bd8952ee559c3a Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Mon, 30 Mar 2026 11:15:10 -0400
Subject: [PATCH 14/27] Variable suggestions implemented. (I opted for
 `ContinuousConstSMul R R` before `M` decls.)

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index c1a8f0394c516f..3fe00148a65353 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -114,7 +114,7 @@ open Filter Function Bornology Metric Set Topology Filter
 ### Equivalences between `StrongDual` and `WeakDual`
 -/
 
-variable {𝕜 M E R : Type*}
+variable {𝕜 M E : Type*}
 variable [NontriviallyNormedField 𝕜]
 variable [AddCommGroup M] [TopologicalSpace M] [Module 𝕜 M]
 variable [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
@@ -123,8 +123,8 @@ namespace StrongDual
 
 section
 
-variable [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R]
-variable {M : Type*} [AddCommMonoid M] [TopologicalSpace M] [Module R M] [ContinuousConstSMul R R]
+variable {R M : Type*} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R]
+variable [ContinuousConstSMul R R] [AddCommMonoid M] [TopologicalSpace M] [Module R M]
 
 /-- For vector spaces `M`, there is a canonical map `StrongDual R M → WeakDual R M` (the "identity"
 mapping). It is a linear equivalence. -/

From a6de12b5e20cb0e325c5acde49fc3e85574aef48 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Tue, 31 Mar 2026 10:28:53 -0400
Subject: [PATCH 15/27] Tried to implement these changes, globalizing variables
 in the new file.

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 39 +-------------------
 1 file changed, 1 insertion(+), 38 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index 3fe00148a65353..c543339d89980c 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -11,6 +11,7 @@ public import Mathlib.Topology.Algebra.Module.WeakDual
 public import Mathlib.Topology.MetricSpace.PiNat
 public import Mathlib.Analysis.Normed.Operator.BanachSteinhaus
 public import Mathlib.Analysis.LocallyConvex.WeakDual
+public import Mathlib.Topology.Algebra.Module.WeakDual
 
 /-!
 # Weak dual of normed space
@@ -119,46 +120,8 @@ variable [NontriviallyNormedField 𝕜]
 variable [AddCommGroup M] [TopologicalSpace M] [Module 𝕜 M]
 variable [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
 
-namespace StrongDual
-
-section
-
-variable {R M : Type*} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R]
-variable [ContinuousConstSMul R R] [AddCommMonoid M] [TopologicalSpace M] [Module R M]
-
-/-- For vector spaces `M`, there is a canonical map `StrongDual R M → WeakDual R M` (the "identity"
-mapping). It is a linear equivalence. -/
-def toWeakDual : StrongDual R M ≃ₗ[R] WeakDual R M :=
-  LinearEquiv.refl R (StrongDual R M)
-
-theorem coe_toWeakDual (x' : StrongDual R M) : (toWeakDual x' : M → R) = x' := rfl
-
-@[simp]
-theorem toWeakDual_apply (x' : StrongDual R M) (y : M) : (toWeakDual x') y = x' y := rfl
-
-theorem toWeakDual_inj (x' y' : StrongDual R M) : toWeakDual x' = toWeakDual y' ↔ x' = y' :=
-  (LinearEquiv.injective toWeakDual).eq_iff
-
-end
-
-end StrongDual
-
 namespace WeakDual
 
-/-- For vector spaces `E`, there is a canonical map `WeakDual 𝕜 E → StrongDual 𝕜 E` (the "identity"
-mapping). It is a linear equivalence. Here it is implemented as the inverse of the linear
-equivalence `StrongDual.toWeakDual` in the other direction. -/
-def toStrongDual : WeakDual 𝕜 M ≃ₗ[𝕜] StrongDual 𝕜 M :=
-  StrongDual.toWeakDual.symm
-
-@[simp]
-theorem toStrongDual_apply (x : WeakDual 𝕜 M) (y : M) : (toStrongDual x) y = x y := rfl
-
-theorem coe_toStrongDual (x' : WeakDual 𝕜 M) : (toStrongDual x' : M → 𝕜) = x' := rfl
-
-theorem toStrongDual_inj (x' y' : WeakDual 𝕜 M) : toStrongDual x' = toStrongDual y' ↔ x' = y' :=
-  (LinearEquiv.injective toStrongDual).eq_iff
-
 section Bornology
 
 /-- The bornology on `WeakDual 𝕜 F` is the norm bornology inherited from `StrongDual 𝕜 F`.

From c834d4484196b96b6d6efdf768a4523ba0aaa6f2 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Tue, 31 Mar 2026 10:29:02 -0400
Subject: [PATCH 16/27] Ditto

---
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 74 ++++++++++++-------
 1 file changed, 49 insertions(+), 25 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index b75634ddc7e2d2..9c056168de65af 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -55,22 +55,53 @@ open Filter
 open Topology
 
 variable {α 𝕜 𝕝 E F : Type*}
+section CommSemiring
+
+variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
+variable [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
 
 /-- The weak star topology is the topology coarsest topology on `E →L[𝕜] 𝕜` such that all
 functionals `fun v => v x` are continuous. -/
 def WeakDual (𝕜 E : Type*) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
-    [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :=
-  WeakBilin (topDualPairing 𝕜 E)
+  [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
+  := WeakBilin (topDualPairing 𝕜 E)
 deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd, Inhabited,
   FunLike, ContinuousLinearMapClass
 
+namespace StrongDual
+
+/-- For vector spaces `E`, there is a canonical map `StrongDual 𝕜 E → WeakDual 𝕜 E` (the "identity"
+mapping). It is a linear equivalence. -/
+def toWeakDual : StrongDual 𝕜 E ≃ₗ[𝕜] WeakDual 𝕜 E :=
+  LinearEquiv.refl 𝕜 (StrongDual 𝕜 E)
+
+theorem coe_toWeakDual (x' : StrongDual 𝕜 E) : (toWeakDual x' : E → 𝕜) = x' := rfl
+
+@[simp]
+theorem toWeakDual_apply (x' : StrongDual 𝕜 E) (y : E) : (toWeakDual x') y = x' y := rfl
+
+theorem toWeakDual_inj (x' y' : StrongDual 𝕜 E) : toWeakDual x' = toWeakDual y' ↔ x' = y' :=
+  (LinearEquiv.injective toWeakDual).eq_iff
+
+end StrongDual
+
 namespace WeakDual
 
-section Semiring
+/-- For vector spaces `E`, there is a canonical map `WeakDual 𝕜 E → StrongDual 𝕜 E` (the "identity"
+mapping). It is a linear equivalence. Here it is implemented as the inverse of the linear
+equivalence `StrongDual.toWeakDual` in the other direction. -/
+def toStrongDual : WeakDual 𝕜 E ≃ₗ[𝕜] StrongDual 𝕜 E :=
+  StrongDual.toWeakDual.symm
 
-variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
-variable [ContinuousConstSMul 𝕜 𝕜]
-variable [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
+@[simp]
+theorem toStrongDual_apply (x : WeakDual 𝕜 E) (y : E) : (toStrongDual x) y = x y := rfl
+
+theorem coe_toStrongDual (x' : WeakDual 𝕜 E) : (toStrongDual x' : E → 𝕜) = x' := rfl
+
+theorem toStrongDual_inj (x' y' : WeakDual 𝕜 E) : toStrongDual x' = toStrongDual y' ↔ x' = y' :=
+  (LinearEquiv.injective toStrongDual).eq_iff
+
+section Semiring
 
 /-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
 multiplication on `𝕜`, then it acts on `WeakDual 𝕜 E`. -/
@@ -117,19 +148,6 @@ instance instT2Space [T2Space 𝕜] : T2Space (WeakDual 𝕜 E) :=
 
 end Semiring
 
-section Ring
-
-variable [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜]
-variable [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
-
-instance instAddCommGroup : AddCommGroup (WeakDual 𝕜 E) :=
-  inferInstanceAs <| AddCommGroup (WeakBilin (topDualPairing 𝕜 E))
-
-instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakDual 𝕜 E) :=
-  WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E)
-
-end Ring
-
 end WeakDual
 
 /-- The weak topology is the topology coarsest topology on `E` such that all functionals
@@ -141,10 +159,6 @@ deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd
 
 section Semiring
 
-variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
-variable [ContinuousConstSMul 𝕜 𝕜]
-variable [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
-
 namespace WeakSpace
 
 instance instModule' [CommSemiring 𝕝] [Module 𝕝 E] : Module 𝕝 (WeakSpace 𝕜 E) :=
@@ -216,13 +230,23 @@ theorem tendsto_iff_forall_eval_tendsto_topDualPairing {l : Filter α} {f : α 
 
 end Semiring
 
+end CommSemiring
 section Ring
 
-namespace WeakSpace
-
 variable [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜]
 variable [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
 
+namespace WeakDual
+
+instance instAddCommGroup : AddCommGroup (WeakDual 𝕜 E) :=
+  inferInstanceAs <| AddCommGroup (WeakBilin (topDualPairing 𝕜 E))
+
+instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakDual 𝕜 E) :=
+  WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E)
+
+end WeakDual
+namespace WeakSpace
+
 instance instAddCommGroup : AddCommGroup (WeakSpace 𝕜 E) :=
   inferInstanceAs <| AddCommGroup (WeakBilin (topDualPairing 𝕜 E).flip)
 

From 091e6d03da384e71bb26e957133cea0de7846bd1 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Tue, 31 Mar 2026 10:29:58 -0400
Subject: [PATCH 17/27] Import was already there transitively, oops!

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index c543339d89980c..9776dd0f36ea2b 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -11,7 +11,6 @@ public import Mathlib.Topology.Algebra.Module.WeakDual
 public import Mathlib.Topology.MetricSpace.PiNat
 public import Mathlib.Analysis.Normed.Operator.BanachSteinhaus
 public import Mathlib.Analysis.LocallyConvex.WeakDual
-public import Mathlib.Topology.Algebra.Module.WeakDual
 
 /-!
 # Weak dual of normed space

From c78112bb4ae5823e550d42a720f1c57d6b66827f Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Tue, 31 Mar 2026 10:31:00 -0400
Subject: [PATCH 18/27] Moved heading

---
 Mathlib/Analysis/Normed/Module/WeakDual.lean  | 4 ----
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 4 ++++
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Analysis/Normed/Module/WeakDual.lean b/Mathlib/Analysis/Normed/Module/WeakDual.lean
index 9776dd0f36ea2b..a342711fc41c2f 100644
--- a/Mathlib/Analysis/Normed/Module/WeakDual.lean
+++ b/Mathlib/Analysis/Normed/Module/WeakDual.lean
@@ -110,10 +110,6 @@ noncomputable section
 
 open Filter Function Bornology Metric Set Topology Filter
 
-/-!
-### Equivalences between `StrongDual` and `WeakDual`
--/
-
 variable {𝕜 M E : Type*}
 variable [NontriviallyNormedField 𝕜]
 variable [AddCommGroup M] [TopologicalSpace M] [Module 𝕜 M]
diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index 9c056168de65af..5fa53f4114ab5f 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -68,6 +68,10 @@ def WeakDual (𝕜 E : Type*) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [Conti
 deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd, Inhabited,
   FunLike, ContinuousLinearMapClass
 
+/-!
+### Equivalences between `StrongDual` and `WeakDual`
+-/
+
 namespace StrongDual
 
 /-- For vector spaces `E`, there is a canonical map `StrongDual 𝕜 E → WeakDual 𝕜 E` (the "identity"

From dc1426b0b9e9726c9e59e0c89359d637ee9e6202 Mon Sep 17 00:00:00 2001
From: Jon Bannon <59937998+JonBannon@users.noreply.github.com>
Date: Tue, 31 Mar 2026 10:50:38 -0400
Subject: [PATCH 19/27] Update Mathlib/Topology/Algebra/Module/WeakDual.lean

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
---
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index 5fa53f4114ab5f..7af982c3ba418d 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -55,6 +55,7 @@ open Filter
 open Topology
 
 variable {α 𝕜 𝕝 E F : Type*}
+
 section CommSemiring
 
 variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]

From 750b718fcc29893b51a56feab31c46842aad13c0 Mon Sep 17 00:00:00 2001
From: Jon Bannon <59937998+JonBannon@users.noreply.github.com>
Date: Tue, 31 Mar 2026 10:51:12 -0400
Subject: [PATCH 20/27] Update Mathlib/Topology/Algebra/Module/WeakDual.lean

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
---
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index 7af982c3ba418d..950ce211b9e276 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -61,9 +61,10 @@ section CommSemiring
 variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
 variable [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
 
+variable (𝕜 E) in
 /-- The weak star topology is the topology coarsest topology on `E →L[𝕜] 𝕜` such that all
 functionals `fun v => v x` are continuous. -/
-def WeakDual (𝕜 E : Type*) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
+def WeakDual
   [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
   := WeakBilin (topDualPairing 𝕜 E)
 deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd, Inhabited,

From 8e457ee777c56c68373d4aba06f9cbb0e2c65e08 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Tue, 31 Mar 2026 10:51:59 -0400
Subject: [PATCH 21/27] Monica changes.

---
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index 950ce211b9e276..77931e2117a693 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -251,6 +251,7 @@ instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakDual 𝕜 E) :=
   WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E)
 
 end WeakDual
+
 namespace WeakSpace
 
 instance instAddCommGroup : AddCommGroup (WeakSpace 𝕜 E) :=

From a9d48f8f7ecf388cf5cd3967311b1954ca57f84b Mon Sep 17 00:00:00 2001
From: Jon Bannon <59937998+JonBannon@users.noreply.github.com>
Date: Tue, 31 Mar 2026 11:12:17 -0400
Subject: [PATCH 22/27] Update Mathlib/Topology/Algebra/Module/WeakDual.lean

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
---
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index 77931e2117a693..573b03f8c28b0c 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -237,6 +237,7 @@ theorem tendsto_iff_forall_eval_tendsto_topDualPairing {l : Filter α} {f : α 
 end Semiring
 
 end CommSemiring
+
 section Ring
 
 variable [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜]

From 21a4096043143e47410e16d391f526cfc38bfc08 Mon Sep 17 00:00:00 2001
From: Jon Bannon <59937998+JonBannon@users.noreply.github.com>
Date: Tue, 31 Mar 2026 11:47:43 -0400
Subject: [PATCH 23/27] Update Mathlib/Topology/Algebra/Module/WeakDual.lean

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>
---
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index 573b03f8c28b0c..c53705778c1ef0 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -64,9 +64,7 @@ variable [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [Topo
 variable (𝕜 E) in
 /-- The weak star topology is the topology coarsest topology on `E →L[𝕜] 𝕜` such that all
 functionals `fun v => v x` are continuous. -/
-def WeakDual
-  [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
-  := WeakBilin (topDualPairing 𝕜 E)
+def WeakDual := WeakBilin (topDualPairing 𝕜 E)
 deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd, Inhabited,
   FunLike, ContinuousLinearMapClass
 

From 52cce0e5bbba48ad0e885f15b199d4a228aa01a7 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Tue, 31 Mar 2026 21:41:52 -0400
Subject: [PATCH 24/27] Hopefully undid section mess!

---
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 62 ++++++++++---------
 1 file changed, 33 insertions(+), 29 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index c53705778c1ef0..cab2b45b12c663 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -56,21 +56,17 @@ open Topology
 
 variable {α 𝕜 𝕝 E F : Type*}
 
-section CommSemiring
-
-variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
-variable [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
-
-variable (𝕜 E) in
 /-- The weak star topology is the topology coarsest topology on `E →L[𝕜] 𝕜` such that all
 functionals `fun v => v x` are continuous. -/
-def WeakDual := WeakBilin (topDualPairing 𝕜 E)
+def WeakDual (𝕜 E) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜]
+     [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] := WeakBilin (topDualPairing 𝕜 E)
 deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd, Inhabited,
   FunLike, ContinuousLinearMapClass
 
-/-!
-### Equivalences between `StrongDual` and `WeakDual`
--/
+section Equivalences
+
+variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
+variable [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
 
 namespace StrongDual
 
@@ -105,8 +101,16 @@ theorem coe_toStrongDual (x' : WeakDual 𝕜 E) : (toStrongDual x' : E → 𝕜)
 theorem toStrongDual_inj (x' y' : WeakDual 𝕜 E) : toStrongDual x' = toStrongDual y' ↔ x' = y' :=
   (LinearEquiv.injective toStrongDual).eq_iff
 
+end WeakDual
+
+end Equivalences
+
+namespace WeakDual
 section Semiring
 
+variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
+variable [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
+
 /-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
 multiplication on `𝕜`, then it acts on `WeakDual 𝕜 E`. -/
 instance instMulAction (M) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜]
@@ -152,6 +156,19 @@ instance instT2Space [T2Space 𝕜] : T2Space (WeakDual 𝕜 E) :=
 
 end Semiring
 
+section Ring
+
+variable [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜]
+variable [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
+
+instance instAddCommGroup : AddCommGroup (WeakDual 𝕜 E) :=
+  inferInstanceAs <| AddCommGroup (WeakBilin (topDualPairing 𝕜 E))
+
+instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakDual 𝕜 E) :=
+  WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E)
+
+end Ring
+
 end WeakDual
 
 /-- The weak topology is the topology coarsest topology on `E` such that all functionals
@@ -161,9 +178,11 @@ def WeakSpace (𝕜 E) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAd
   WeakBilin (topDualPairing 𝕜 E).flip
 deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd
 
+namespace WeakSpace
 section Semiring
 
-namespace WeakSpace
+variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
+variable [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
 
 instance instModule' [CommSemiring 𝕝] [Module 𝕝 E] : Module 𝕝 (WeakSpace 𝕜 E) :=
   inferInstanceAs <| Module 𝕝 (WeakBilin (topDualPairing 𝕜 E).flip)
@@ -191,8 +210,6 @@ theorem map_apply (f : E →L[𝕜] F) (x : E) : WeakSpace.map f x = f x :=
 theorem coe_map (f : E →L[𝕜] F) : (WeakSpace.map f : E → F) = f :=
   rfl
 
-end WeakSpace
-
 variable (𝕜 E) in
 /-- There is a canonical map `E → WeakSpace 𝕜 E` (the "identity"
 mapping). It is a linear equivalence. -/
@@ -222,7 +239,7 @@ theorem isOpenMap_toWeakSpace_symm : IsOpenMap (toWeakSpace 𝕜 E).symm :=
     (toWeakSpace 𝕜 E).left_inv (toWeakSpace 𝕜 E).right_inv
 
 /-- A set in `E` which is open in the weak topology is open. -/
-theorem WeakSpace.isOpen_of_isOpen (V : Set E)
+theorem isOpen_of_isOpen (V : Set E)
     (hV : IsOpen ((toWeakSpaceCLM 𝕜 E) '' V : Set (WeakSpace 𝕜 E))) : IsOpen V := by
   simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV
 
@@ -234,31 +251,18 @@ theorem tendsto_iff_forall_eval_tendsto_topDualPairing {l : Filter α} {f : α 
 
 end Semiring
 
-end CommSemiring
-
 section Ring
 
 variable [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜]
 variable [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
 
-namespace WeakDual
-
-instance instAddCommGroup : AddCommGroup (WeakDual 𝕜 E) :=
-  inferInstanceAs <| AddCommGroup (WeakBilin (topDualPairing 𝕜 E))
-
-instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakDual 𝕜 E) :=
-  WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E)
-
-end WeakDual
-
-namespace WeakSpace
-
 instance instAddCommGroup : AddCommGroup (WeakSpace 𝕜 E) :=
   inferInstanceAs <| AddCommGroup (WeakBilin (topDualPairing 𝕜 E).flip)
 
 instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakSpace 𝕜 E) :=
   WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E).flip
 
-end WeakSpace
 
 end Ring
+
+end WeakSpace

From e3a8157b002392b7b6ff90523d99a582b77ad750 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Tue, 31 Mar 2026 21:42:56 -0400
Subject: [PATCH 25/27] stupid space

---
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index cab2b45b12c663..3145664c75ce8a 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -262,7 +262,6 @@ instance instAddCommGroup : AddCommGroup (WeakSpace 𝕜 E) :=
 instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakSpace 𝕜 E) :=
   WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E).flip
 
-
 end Ring
 
 end WeakSpace

From d8fbcab6414d59caf60cb8a8a3a69a993dbc05b9 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 1 Apr 2026 09:42:26 -0400
Subject: [PATCH 26/27] Manual rollback.

---
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 25 +++++++++++++------
 1 file changed, 17 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index 3145664c75ce8a..8dc06be492d250 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -58,8 +58,9 @@ variable {α 𝕜 𝕝 E F : Type*}
 
 /-- The weak star topology is the topology coarsest topology on `E →L[𝕜] 𝕜` such that all
 functionals `fun v => v x` are continuous. -/
-def WeakDual (𝕜 E) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜]
-     [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] := WeakBilin (topDualPairing 𝕜 E)
+def WeakDual (𝕜 E : Type*) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
+    [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :=
+  WeakBilin (topDualPairing 𝕜 E)
 deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd, Inhabited,
   FunLike, ContinuousLinearMapClass
 
@@ -106,10 +107,12 @@ end WeakDual
 end Equivalences
 
 namespace WeakDual
+
 section Semiring
 
 variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
-variable [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
+variable [ContinuousConstSMul 𝕜 𝕜]
+variable [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
 
 /-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
 multiplication on `𝕜`, then it acts on `WeakDual 𝕜 E`. -/
@@ -178,11 +181,13 @@ def WeakSpace (𝕜 E) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAd
   WeakBilin (topDualPairing 𝕜 E).flip
 deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd
 
-namespace WeakSpace
 section Semiring
 
 variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
-variable [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
+variable [ContinuousConstSMul 𝕜 𝕜]
+variable [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
+
+namespace WeakSpace
 
 instance instModule' [CommSemiring 𝕝] [Module 𝕝 E] : Module 𝕝 (WeakSpace 𝕜 E) :=
   inferInstanceAs <| Module 𝕝 (WeakBilin (topDualPairing 𝕜 E).flip)
@@ -210,6 +215,8 @@ theorem map_apply (f : E →L[𝕜] F) (x : E) : WeakSpace.map f x = f x :=
 theorem coe_map (f : E →L[𝕜] F) : (WeakSpace.map f : E → F) = f :=
   rfl
 
+end WeakSpace
+
 variable (𝕜 E) in
 /-- There is a canonical map `E → WeakSpace 𝕜 E` (the "identity"
 mapping). It is a linear equivalence. -/
@@ -239,7 +246,7 @@ theorem isOpenMap_toWeakSpace_symm : IsOpenMap (toWeakSpace 𝕜 E).symm :=
     (toWeakSpace 𝕜 E).left_inv (toWeakSpace 𝕜 E).right_inv
 
 /-- A set in `E` which is open in the weak topology is open. -/
-theorem isOpen_of_isOpen (V : Set E)
+theorem WeakSpace.isOpen_of_isOpen (V : Set E)
     (hV : IsOpen ((toWeakSpaceCLM 𝕜 E) '' V : Set (WeakSpace 𝕜 E))) : IsOpen V := by
   simpa [Set.image_image] using isOpenMap_toWeakSpace_symm _ hV
 
@@ -253,6 +260,8 @@ end Semiring
 
 section Ring
 
+namespace WeakSpace
+
 variable [CommRing 𝕜] [TopologicalSpace 𝕜] [IsTopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜]
 variable [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
 
@@ -262,6 +271,6 @@ instance instAddCommGroup : AddCommGroup (WeakSpace 𝕜 E) :=
 instance instIsTopologicalAddGroup : IsTopologicalAddGroup (WeakSpace 𝕜 E) :=
   WeakBilin.instIsTopologicalAddGroup (topDualPairing 𝕜 E).flip
 
-end Ring
-
 end WeakSpace
+
+end Ring

From 9c01996cf75db2cd8129fd8019a447c64cd29745 Mon Sep 17 00:00:00 2001
From: Jon Bannon <jbannon@siena.edu>
Date: Wed, 1 Apr 2026 10:16:42 -0400
Subject: [PATCH 27/27] Fix, essentially matches Monica's file.

---
 Mathlib/Topology/Algebra/Module/WeakDual.lean | 21 ++++++-------------
 1 file changed, 6 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Topology/Algebra/Module/WeakDual.lean b/Mathlib/Topology/Algebra/Module/WeakDual.lean
index 8dc06be492d250..4014452fca1bb6 100644
--- a/Mathlib/Topology/Algebra/Module/WeakDual.lean
+++ b/Mathlib/Topology/Algebra/Module/WeakDual.lean
@@ -64,13 +64,11 @@ def WeakDual (𝕜 E : Type*) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [Conti
 deriving AddCommMonoid, Module 𝕜, TopologicalSpace, ContinuousAdd, Inhabited,
   FunLike, ContinuousLinearMapClass
 
-section Equivalences
+namespace StrongDual
 
 variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
 variable [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
 
-namespace StrongDual
-
 /-- For vector spaces `E`, there is a canonical map `StrongDual 𝕜 E → WeakDual 𝕜 E` (the "identity"
 mapping). It is a linear equivalence. -/
 def toWeakDual : StrongDual 𝕜 E ≃ₗ[𝕜] WeakDual 𝕜 E :=
@@ -88,6 +86,11 @@ end StrongDual
 
 namespace WeakDual
 
+section Semiring
+
+variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
+variable [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
+
 /-- For vector spaces `E`, there is a canonical map `WeakDual 𝕜 E → StrongDual 𝕜 E` (the "identity"
 mapping). It is a linear equivalence. Here it is implemented as the inverse of the linear
 equivalence `StrongDual.toWeakDual` in the other direction. -/
@@ -102,18 +105,6 @@ theorem coe_toStrongDual (x' : WeakDual 𝕜 E) : (toStrongDual x' : E → 𝕜)
 theorem toStrongDual_inj (x' y' : WeakDual 𝕜 E) : toStrongDual x' = toStrongDual y' ↔ x' = y' :=
   (LinearEquiv.injective toStrongDual).eq_iff
 
-end WeakDual
-
-end Equivalences
-
-namespace WeakDual
-
-section Semiring
-
-variable [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
-variable [ContinuousConstSMul 𝕜 𝕜]
-variable [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
-
 /-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
 multiplication on `𝕜`, then it acts on `WeakDual 𝕜 E`. -/
 instance instMulAction (M) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜]