From 7fd1166fbdea3e7fac91e5d8612125f444f494e2 Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Wed, 14 Dec 2022 12:14:35 +0100
Subject: [PATCH 01/17] feat(analysis/locally_convex): hausdorff locally convex
 spaces

---
 .../locally_convex/with_seminorms.lean        | 86 +++++++++++++++++++
 src/analysis/seminorm.lean                    | 16 ++++
 2 files changed, 102 insertions(+)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index 6fb325e9d33b3..90614c6e08d0e 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -289,6 +289,92 @@ begin
   rw (congr_fun (congr_arg (@nhds E) hp.1) 0),
   exact add_group_filter_basis.nhds_zero_has_basis _,
 end
+
+/-- The `x`-neighbourhoods of a space whose topology is induced by a family of seminorms
+are exactly the sets which contain seminorm balls around `x`.-/
+lemma with_seminorms.mem_nhds_iff [t : topological_space E]  {p : seminorm_family 𝕜 E ι}
+(hp : with_seminorms p) (x : E) (U : set E):
+U ∈ nhds x ↔ ∃ (i : finset ι) (ε > 0), (i.sup p).ball x ε ⊆ U :=
+begin
+  rw [hp.with_seminorms_eq, (p.add_group_filter_basis.nhds_has_basis x).mem_iff' U],
+  split,
+  { rintros ⟨ V, V_in_basis, V_sub_U⟩,
+    rcases p.basis_sets_iff.mp V_in_basis with ⟨ i_set, ε , ε_pos, hr ⟩,
+    simp_rw [hr, singleton_add_ball _ ε_pos, add_zero] at V_sub_U,
+    exact ⟨ i_set, ε, ε_pos, V_sub_U ⟩ },
+  { rintros ⟨ i_set, ε, ε_pos, V_sub_U ⟩ ,
+    refine ⟨ (i_set.sup p).ball 0 ε , p.basis_sets_iff.mpr ⟨ i_set, ε, ε_pos , rfl ⟩, _ ⟩,
+    simp_rw [singleton_add_ball ε ε_pos, add_zero],
+    exact V_sub_U }
+end
+
+/-- The open sets of a space whose topology is induced by a family of seminorms
+are exactly the sets which contain seminorm balls around all of their points.-/
+lemma with_seminorms.is_open_iff_mem_balls [t : topological_space E]
+{p : seminorm_family 𝕜 E ι} (hp : with_seminorms p) (U : set E):
+is_open U ↔ ∀ (x ∈ U), ∃ (i : finset ι) (ε > 0), (i.sup p).ball x ε ⊆ U :=
+by simp_rw [←with_seminorms.mem_nhds_iff hp _ U, is_open_iff_mem_nhds]
+
+/-- A space whose topology is induced by a family of seminorms is Hausdorff iff
+the family of seminorms is separating. -/
+theorem with_seminorms.t2_iff_separating [t : topological_space E]
+{p : seminorm_family 𝕜 E ι}  (hp : with_seminorms p) :
+t2_space E ↔ ∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0 :=
+begin
+  split,
+  { intros E_t2 x x_ne_zero,
+    rcases @t2_separation E t E_t2 x 0 x_ne_zero
+      with ⟨u, v, u_open, v_open, x_in_u, zero_in_v, u_v_disj⟩,
+    rcases (with_seminorms.is_open_iff_mem_balls hp v).mp v_open 0 zero_in_v
+      with ⟨i_set, ε, ε_pos, ball_in_v ⟩,
+    have sup_p_x_ne_zero : (i_set.sup p) x ≠ 0,
+    { intro assump,
+      refine (set.singleton_nonempty x).not_subset_empty (u_v_disj _ _);
+        rw [set.le_eq_subset, set.singleton_subset_iff],
+      { exact (x_in_u) },
+      { refine (ball_in_v _),
+        rwa [seminorm.mem_ball, sub_zero, assump] } },
+    rw seminorm.finset_sup_apply at sup_p_x_ne_zero,
+    by_contra',
+    simp_rw this at sup_p_x_ne_zero,
+    apply sup_p_x_ne_zero,
+    simp_rw nnreal.coe_eq_zero,
+    by_cases i_set.nonempty,
+    { simp_rw [← real.to_nnreal_of_nonneg (le_refl 0), finset.sup_const h _ , real.to_nnreal_zero] },
+    { rw finset.not_nonempty_iff_eq_empty at h,
+      rw [h, finset.sup_empty],
+      exact bot_eq_zero } },
+  { rw t2_iff_nhds,
+    intros h x y x_y_nhds_ne_bot,
+    rw filter.inf_ne_bot_iff at x_y_nhds_ne_bot,
+    by_contra x_neq_y,
+    cases h (x - y) (sub_ne_zero.mpr x_neq_y) with i p_i_x_sub_y_ne_zero,
+    let ε := (p i) (x - y),
+    let sx := (p i).ball x (ε/2),
+    let sy := (p i).ball y (ε/2),
+    have ε_div_2_pos : ε/2 > 0 := by norm_num [div_pos, (ne.symm p_i_x_sub_y_ne_zero).lt_of_le],
+    have sx_nhds_x : sx ∈ nhds x :=
+      (with_seminorms.mem_nhds_iff hp x sx).mpr ⟨ {i}, ε/2, ε_div_2_pos, by rw finset.sup_singleton ⟩,
+    have sy_nhds_y : sy ∈ nhds y :=
+      (with_seminorms.mem_nhds_iff hp y sy).mpr ⟨ {i}, ε/2, ε_div_2_pos, by rw finset.sup_singleton ⟩,
+    cases set.nonempty_def.mp (x_y_nhds_ne_bot sx_nhds_x sy_nhds_y) with z z_in_inter,
+    have seminorm_symm := seminorm.neg' (p i) (x - z),
+    obtain ⟨ lt1, lt2 ⟩ := (set.mem_inter_iff _ _ _).mp z_in_inter,
+    rw seminorm.mem_ball at lt1 lt2,
+    have : (p i).to_fun = (p i) := rfl,
+    rw this at seminorm_symm,
+    have : ε < ε,
+    { calc
+      ε   = p i (x - y)                : rfl
+      ... = p i ((x - z) + (z - y))    : by rw ← sub_add_sub_cancel
+      ... ≤ p i (x - z) + p i (z - y)  : by apply seminorm.add_le'
+      ... = p i (z - x) + p i (z - y)  : by rw [←seminorm_symm, neg_sub]
+      ... < ε / 2 + ε / 2              : by apply add_lt_add lt1 lt2
+      ... = ε                          : by rw add_halves },
+    rwa lt_self_iff_false ε at this }
+end
+
+
 end topology
 
 section topological_add_group
diff --git a/src/analysis/seminorm.lean b/src/analysis/seminorm.lean
index a06e236385dc4..9acb630bf980e 100644
--- a/src/analysis/seminorm.lean
+++ b/src/analysis/seminorm.lean
@@ -609,6 +609,22 @@ begin
   exact (map_add_le_add p _ _).trans (add_le_add hy₁ hy₂)
 end
 
+/- Can this be done more neatly with `seminorm.ball_comp`?
+Alternatively, can this be done using/imitating the ball-addition-lemmas
+in normed_space/pointwise? -/
+/-- The image of a ball under addition with a singleton is another ball. -/
+lemma singleton_add_ball {p : seminorm 𝕜 E} {x y : E} (ε : ℝ) (ε_pos : ε > 0):
+  (λ (z : E), x + z) '' p.ball y ε = p.ball (x + y) ε :=
+begin
+  apply le_antisymm,
+  { rintros w ⟨w', w'_in_ball, w'h⟩,
+    rwa [seminorm.mem_ball, ← w'h, add_sub_add_left_eq_sub] },
+  { intros w w_in_ball,
+    refine set.mem_image_iff_bex.mpr ⟨ w - x , _ ⟩,
+    rw [seminorm.mem_ball, sub_sub, add_sub, add_sub_cancel'],
+    exact ⟨ w_in_ball , rfl ⟩ }
+end
+
 end has_smul
 
 section module

From 89f49e1377f312d54201e4d0dffacd2ac20314a1 Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Wed, 14 Dec 2022 12:40:08 +0100
Subject: [PATCH 02/17] style(analysis/locally_convex): shorten lines

Shorten all lines to less than 100 chars to pass linter.
---
 src/analysis/locally_convex/with_seminorms.lean | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index 90614c6e08d0e..444c841d6b0ba 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -340,7 +340,7 @@ begin
     apply sup_p_x_ne_zero,
     simp_rw nnreal.coe_eq_zero,
     by_cases i_set.nonempty,
-    { simp_rw [← real.to_nnreal_of_nonneg (le_refl 0), finset.sup_const h _ , real.to_nnreal_zero] },
+    { simp_rw [←real.to_nnreal_of_nonneg (le_refl 0), finset.sup_const h _ , real.to_nnreal_zero] },
     { rw finset.not_nonempty_iff_eq_empty at h,
       rw [h, finset.sup_empty],
       exact bot_eq_zero } },
@@ -354,9 +354,11 @@ begin
     let sy := (p i).ball y (ε/2),
     have ε_div_2_pos : ε/2 > 0 := by norm_num [div_pos, (ne.symm p_i_x_sub_y_ne_zero).lt_of_le],
     have sx_nhds_x : sx ∈ nhds x :=
-      (with_seminorms.mem_nhds_iff hp x sx).mpr ⟨ {i}, ε/2, ε_div_2_pos, by rw finset.sup_singleton ⟩,
+      (with_seminorms.mem_nhds_iff hp x sx).mpr
+      ⟨ {i}, ε/2, ε_div_2_pos, by rw finset.sup_singleton ⟩,
     have sy_nhds_y : sy ∈ nhds y :=
-      (with_seminorms.mem_nhds_iff hp y sy).mpr ⟨ {i}, ε/2, ε_div_2_pos, by rw finset.sup_singleton ⟩,
+      (with_seminorms.mem_nhds_iff hp y sy).mpr
+      ⟨ {i}, ε/2, ε_div_2_pos, by rw finset.sup_singleton ⟩,
     cases set.nonempty_def.mp (x_y_nhds_ne_bot sx_nhds_x sy_nhds_y) with z z_in_inter,
     have seminorm_symm := seminorm.neg' (p i) (x - z),
     obtain ⟨ lt1, lt2 ⟩ := (set.mem_inter_iff _ _ _).mp z_in_inter,

From 051b86e31b0f90a873bec61fa845ef8a029cfc12 Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Wed, 14 Dec 2022 14:19:09 +0100
Subject: [PATCH 03/17] style(analysis/locally_convex): moritz suggestions

Implemented stylistic suggestions from Moritz Doll.
---
 .../locally_convex/with_seminorms.lean        | 53 +++++++++----------
 src/analysis/seminorm.lean                    |  4 +-
 2 files changed, 26 insertions(+), 31 deletions(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index 444c841d6b0ba..3271fffc0adee 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -293,40 +293,40 @@ end
 /-- The `x`-neighbourhoods of a space whose topology is induced by a family of seminorms
 are exactly the sets which contain seminorm balls around `x`.-/
 lemma with_seminorms.mem_nhds_iff [t : topological_space E]  {p : seminorm_family 𝕜 E ι}
-(hp : with_seminorms p) (x : E) (U : set E):
-U ∈ nhds x ↔ ∃ (i : finset ι) (ε > 0), (i.sup p).ball x ε ⊆ U :=
+  (hp : with_seminorms p) (x : E) (U : set E):
+  U ∈ nhds x ↔ ∃ (i : finset ι) (ε > 0), (i.sup p).ball x ε ⊆ U :=
 begin
   rw [hp.with_seminorms_eq, (p.add_group_filter_basis.nhds_has_basis x).mem_iff' U],
   split,
-  { rintros ⟨ V, V_in_basis, V_sub_U⟩,
-    rcases p.basis_sets_iff.mp V_in_basis with ⟨ i_set, ε , ε_pos, hr ⟩,
+  { rintros ⟨V, V_in_basis, V_sub_U⟩,
+    rcases p.basis_sets_iff.mp V_in_basis with ⟨i_set, ε, ε_pos, hr⟩,
     simp_rw [hr, singleton_add_ball _ ε_pos, add_zero] at V_sub_U,
-    exact ⟨ i_set, ε, ε_pos, V_sub_U ⟩ },
-  { rintros ⟨ i_set, ε, ε_pos, V_sub_U ⟩ ,
-    refine ⟨ (i_set.sup p).ball 0 ε , p.basis_sets_iff.mpr ⟨ i_set, ε, ε_pos , rfl ⟩, _ ⟩,
-    simp_rw [singleton_add_ball ε ε_pos, add_zero],
+    exact ⟨_, _, ε_pos, V_sub_U⟩ },
+  { rintros ⟨i_set, ε, ε_pos, V_sub_U⟩,
+    refine ⟨(i_set.sup p).ball 0 ε, p.basis_sets_iff.mpr ⟨_, _, ε_pos, rfl⟩, _⟩,
+    simp_rw [singleton_add_ball _ ε_pos, add_zero],
     exact V_sub_U }
 end
 
 /-- The open sets of a space whose topology is induced by a family of seminorms
 are exactly the sets which contain seminorm balls around all of their points.-/
 lemma with_seminorms.is_open_iff_mem_balls [t : topological_space E]
-{p : seminorm_family 𝕜 E ι} (hp : with_seminorms p) (U : set E):
-is_open U ↔ ∀ (x ∈ U), ∃ (i : finset ι) (ε > 0), (i.sup p).ball x ε ⊆ U :=
+  {p : seminorm_family 𝕜 E ι} (hp : with_seminorms p) (U : set E):
+  is_open U ↔ ∀ (x ∈ U), ∃ (i : finset ι) (ε > 0), (i.sup p).ball x ε ⊆ U :=
 by simp_rw [←with_seminorms.mem_nhds_iff hp _ U, is_open_iff_mem_nhds]
 
 /-- A space whose topology is induced by a family of seminorms is Hausdorff iff
 the family of seminorms is separating. -/
 theorem with_seminorms.t2_iff_separating [t : topological_space E]
-{p : seminorm_family 𝕜 E ι}  (hp : with_seminorms p) :
-t2_space E ↔ ∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0 :=
+  {p : seminorm_family 𝕜 E ι}  (hp : with_seminorms p) :
+  t2_space E ↔ ∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0 :=
 begin
   split,
   { intros E_t2 x x_ne_zero,
     rcases @t2_separation E t E_t2 x 0 x_ne_zero
       with ⟨u, v, u_open, v_open, x_in_u, zero_in_v, u_v_disj⟩,
     rcases (with_seminorms.is_open_iff_mem_balls hp v).mp v_open 0 zero_in_v
-      with ⟨i_set, ε, ε_pos, ball_in_v ⟩,
+      with ⟨i_set, ε, ε_pos, ball_in_v⟩,
     have sup_p_x_ne_zero : (i_set.sup p) x ≠ 0,
     { intro assump,
       refine (set.singleton_nonempty x).not_subset_empty (u_v_disj _ _);
@@ -340,7 +340,7 @@ begin
     apply sup_p_x_ne_zero,
     simp_rw nnreal.coe_eq_zero,
     by_cases i_set.nonempty,
-    { simp_rw [←real.to_nnreal_of_nonneg (le_refl 0), finset.sup_const h _ , real.to_nnreal_zero] },
+    { simp_rw [←real.to_nnreal_of_nonneg (le_refl 0), finset.sup_const h _, real.to_nnreal_zero] },
     { rw finset.not_nonempty_iff_eq_empty at h,
       rw [h, finset.sup_empty],
       exact bot_eq_zero } },
@@ -348,31 +348,26 @@ begin
     intros h x y x_y_nhds_ne_bot,
     rw filter.inf_ne_bot_iff at x_y_nhds_ne_bot,
     by_contra x_neq_y,
-    cases h (x - y) (sub_ne_zero.mpr x_neq_y) with i p_i_x_sub_y_ne_zero,
+    cases h (x - y) (sub_ne_zero.mpr x_neq_y) with i pi_nonzero,
     let ε := (p i) (x - y),
     let sx := (p i).ball x (ε/2),
     let sy := (p i).ball y (ε/2),
-    have ε_div_2_pos : ε/2 > 0 := by norm_num [div_pos, (ne.symm p_i_x_sub_y_ne_zero).lt_of_le],
+    have ε_div_2_pos := div_pos ((ne.symm pi_nonzero).lt_of_le (map_nonneg _ _)) zero_lt_two,
     have sx_nhds_x : sx ∈ nhds x :=
-      (with_seminorms.mem_nhds_iff hp x sx).mpr
-      ⟨ {i}, ε/2, ε_div_2_pos, by rw finset.sup_singleton ⟩,
+      (with_seminorms.mem_nhds_iff hp _ _).mpr ⟨_, _, ε_div_2_pos, by rw finset.sup_singleton⟩,
     have sy_nhds_y : sy ∈ nhds y :=
-      (with_seminorms.mem_nhds_iff hp y sy).mpr
-      ⟨ {i}, ε/2, ε_div_2_pos, by rw finset.sup_singleton ⟩,
+      (with_seminorms.mem_nhds_iff hp _ _).mpr ⟨_, _, ε_div_2_pos, by rw finset.sup_singleton⟩,
     cases set.nonempty_def.mp (x_y_nhds_ne_bot sx_nhds_x sy_nhds_y) with z z_in_inter,
-    have seminorm_symm := seminorm.neg' (p i) (x - z),
-    obtain ⟨ lt1, lt2 ⟩ := (set.mem_inter_iff _ _ _).mp z_in_inter,
+    obtain ⟨lt1, lt2⟩ := (set.mem_inter_iff _ _ _).mp z_in_inter,
     rw seminorm.mem_ball at lt1 lt2,
-    have : (p i).to_fun = (p i) := rfl,
-    rw this at seminorm_symm,
     have : ε < ε,
     { calc
       ε   = p i (x - y)                : rfl
-      ... = p i ((x - z) + (z - y))    : by rw ← sub_add_sub_cancel
-      ... ≤ p i (x - z) + p i (z - y)  : by apply seminorm.add_le'
-      ... = p i (z - x) + p i (z - y)  : by rw [←seminorm_symm, neg_sub]
-      ... < ε / 2 + ε / 2              : by apply add_lt_add lt1 lt2
-      ... = ε                          : by rw add_halves },
+      ... = p i ((x - z) + (z - y))    : by rw ←sub_add_sub_cancel
+      ... ≤ p i (x - z) + p i (z - y)  : seminorm.add_le' _ _ _
+      ... = p i (z - x) + p i (z - y)  : by rw [←map_neg_eq_map, neg_sub]
+      ... < ε/2 + ε/2                  : add_lt_add lt1 lt2
+      ... = ε                          : add_halves _ },
     rwa lt_self_iff_false ε at this }
 end
 
diff --git a/src/analysis/seminorm.lean b/src/analysis/seminorm.lean
index 9acb630bf980e..979a51c4772ab 100644
--- a/src/analysis/seminorm.lean
+++ b/src/analysis/seminorm.lean
@@ -620,9 +620,9 @@ begin
   { rintros w ⟨w', w'_in_ball, w'h⟩,
     rwa [seminorm.mem_ball, ← w'h, add_sub_add_left_eq_sub] },
   { intros w w_in_ball,
-    refine set.mem_image_iff_bex.mpr ⟨ w - x , _ ⟩,
+    refine set.mem_image_iff_bex.mpr ⟨w - x , _⟩,
     rw [seminorm.mem_ball, sub_sub, add_sub, add_sub_cancel'],
-    exact ⟨ w_in_ball , rfl ⟩ }
+    exact ⟨w_in_ball , rfl⟩ }
 end
 
 end has_smul

From a219f2f330a05f60d1ae1b03a22ff25a68a7ad2e Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Wed, 14 Dec 2022 21:57:34 +0100
Subject: [PATCH 04/17] style(analysis/locally_convex): fix linter issues

Remove double arguments, should now pass linter
---
 src/analysis/locally_convex/with_seminorms.lean | 15 ++++++---------
 src/analysis/seminorm.lean                      | 10 +++++-----
 2 files changed, 11 insertions(+), 14 deletions(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index 3271fffc0adee..1ebd1577ced5d 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -292,38 +292,35 @@ end
 
 /-- The `x`-neighbourhoods of a space whose topology is induced by a family of seminorms
 are exactly the sets which contain seminorm balls around `x`.-/
-lemma with_seminorms.mem_nhds_iff [t : topological_space E]  {p : seminorm_family 𝕜 E ι}
-  (hp : with_seminorms p) (x : E) (U : set E):
+lemma with_seminorms.mem_nhds_iff (hp : with_seminorms p) (x : E) (U : set E):
   U ∈ nhds x ↔ ∃ (i : finset ι) (ε > 0), (i.sup p).ball x ε ⊆ U :=
 begin
   rw [hp.with_seminorms_eq, (p.add_group_filter_basis.nhds_has_basis x).mem_iff' U],
   split,
   { rintros ⟨V, V_in_basis, V_sub_U⟩,
     rcases p.basis_sets_iff.mp V_in_basis with ⟨i_set, ε, ε_pos, hr⟩,
-    simp_rw [hr, singleton_add_ball _ ε_pos, add_zero] at V_sub_U,
+    simp_rw [hr, seminorm.singleton_add_ball _, add_zero] at V_sub_U,
     exact ⟨_, _, ε_pos, V_sub_U⟩ },
   { rintros ⟨i_set, ε, ε_pos, V_sub_U⟩,
     refine ⟨(i_set.sup p).ball 0 ε, p.basis_sets_iff.mpr ⟨_, _, ε_pos, rfl⟩, _⟩,
-    simp_rw [singleton_add_ball _ ε_pos, add_zero],
+    simp_rw [seminorm.singleton_add_ball _, add_zero],
     exact V_sub_U }
 end
 
 /-- The open sets of a space whose topology is induced by a family of seminorms
 are exactly the sets which contain seminorm balls around all of their points.-/
-lemma with_seminorms.is_open_iff_mem_balls [t : topological_space E]
-  {p : seminorm_family 𝕜 E ι} (hp : with_seminorms p) (U : set E):
+lemma with_seminorms.is_open_iff_mem_balls (hp : with_seminorms p) (U : set E):
   is_open U ↔ ∀ (x ∈ U), ∃ (i : finset ι) (ε > 0), (i.sup p).ball x ε ⊆ U :=
 by simp_rw [←with_seminorms.mem_nhds_iff hp _ U, is_open_iff_mem_nhds]
 
 /-- A space whose topology is induced by a family of seminorms is Hausdorff iff
 the family of seminorms is separating. -/
-theorem with_seminorms.t2_iff_separating [t : topological_space E]
-  {p : seminorm_family 𝕜 E ι}  (hp : with_seminorms p) :
+theorem with_seminorms.t2_iff_separating (hp : with_seminorms p) :
   t2_space E ↔ ∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0 :=
 begin
   split,
   { intros E_t2 x x_ne_zero,
-    rcases @t2_separation E t E_t2 x 0 x_ne_zero
+    rcases @t2_separation E _inst_5 E_t2 x 0 x_ne_zero
       with ⟨u, v, u_open, v_open, x_in_u, zero_in_v, u_v_disj⟩,
     rcases (with_seminorms.is_open_iff_mem_balls hp v).mp v_open 0 zero_in_v
       with ⟨i_set, ε, ε_pos, ball_in_v⟩,
diff --git a/src/analysis/seminorm.lean b/src/analysis/seminorm.lean
index 979a51c4772ab..26475f32c66a7 100644
--- a/src/analysis/seminorm.lean
+++ b/src/analysis/seminorm.lean
@@ -613,16 +613,16 @@ end
 Alternatively, can this be done using/imitating the ball-addition-lemmas
 in normed_space/pointwise? -/
 /-- The image of a ball under addition with a singleton is another ball. -/
-lemma singleton_add_ball {p : seminorm 𝕜 E} {x y : E} (ε : ℝ) (ε_pos : ε > 0):
-  (λ (z : E), x + z) '' p.ball y ε = p.ball (x + y) ε :=
+lemma singleton_add_ball (p : seminorm 𝕜 E):
+  (λ (z : E), x + z) '' p.ball y r = p.ball (x + y) r :=
 begin
   apply le_antisymm,
   { rintros w ⟨w', w'_in_ball, w'h⟩,
-    rwa [seminorm.mem_ball, ← w'h, add_sub_add_left_eq_sub] },
+    rwa [mem_ball, ← w'h, add_sub_add_left_eq_sub] },
   { intros w w_in_ball,
     refine set.mem_image_iff_bex.mpr ⟨w - x , _⟩,
-    rw [seminorm.mem_ball, sub_sub, add_sub, add_sub_cancel'],
-    exact ⟨w_in_ball , rfl⟩ }
+    rw [mem_ball, sub_sub, add_sub, add_sub_cancel'],
+    exact ⟨w_in_ball, rfl⟩ }
 end
 
 end has_smul

From 3e3716539b9157d24993e63fba9d4c2a67ae8e5a Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Wed, 14 Dec 2022 22:01:45 +0100
Subject: [PATCH 05/17] style(analysis/locally_convex): remove instance
 reference

---
 src/analysis/locally_convex/with_seminorms.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index 1ebd1577ced5d..a8264d18710f8 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -320,7 +320,7 @@ theorem with_seminorms.t2_iff_separating (hp : with_seminorms p) :
 begin
   split,
   { intros E_t2 x x_ne_zero,
-    rcases @t2_separation E _inst_5 E_t2 x 0 x_ne_zero
+    rcases @t2_separation E _ E_t2 x 0 x_ne_zero
       with ⟨u, v, u_open, v_open, x_in_u, zero_in_v, u_v_disj⟩,
     rcases (with_seminorms.is_open_iff_mem_balls hp v).mp v_open 0 zero_in_v
       with ⟨i_set, ε, ε_pos, ball_in_v⟩,

From 0b1832c20802c635884baa27f406c676f9228173 Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Thu, 15 Dec 2022 08:44:04 +0100
Subject: [PATCH 06/17] style(analysis/locally_convex): remove by_contra

Make first implication of t2_iff_separating into a shorter, direct proof
---
 .../locally_convex/with_seminorms.lean        | 22 ++++++++-----------
 1 file changed, 9 insertions(+), 13 deletions(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index a8264d18710f8..e491fdc558af5 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -319,10 +319,10 @@ theorem with_seminorms.t2_iff_separating (hp : with_seminorms p) :
   t2_space E ↔ ∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0 :=
 begin
   split,
-  { intros E_t2 x x_ne_zero,
-    rcases @t2_separation E _ E_t2 x 0 x_ne_zero
-      with ⟨u, v, u_open, v_open, x_in_u, zero_in_v, u_v_disj⟩,
-    rcases (with_seminorms.is_open_iff_mem_balls hp v).mp v_open 0 zero_in_v
+  { introI t2,
+    intros x x_ne_zero,
+    rcases t2_separation x_ne_zero with ⟨u, v, u_open, v_open, x_in_u, zero_in_v, u_v_disj⟩,
+    rcases (with_seminorms.is_open_iff_mem_balls hp _).mp v_open 0 zero_in_v
       with ⟨i_set, ε, ε_pos, ball_in_v⟩,
     have sup_p_x_ne_zero : (i_set.sup p) x ≠ 0,
     { intro assump,
@@ -332,15 +332,11 @@ begin
       { refine (ball_in_v _),
         rwa [seminorm.mem_ball, sub_zero, assump] } },
     rw seminorm.finset_sup_apply at sup_p_x_ne_zero,
-    by_contra',
-    simp_rw this at sup_p_x_ne_zero,
-    apply sup_p_x_ne_zero,
-    simp_rw nnreal.coe_eq_zero,
-    by_cases i_set.nonempty,
-    { simp_rw [←real.to_nnreal_of_nonneg (le_refl 0), finset.sup_const h _, real.to_nnreal_zero] },
-    { rw finset.not_nonempty_iff_eq_empty at h,
-      rw [h, finset.sup_empty],
-      exact bot_eq_zero } },
+    have := (ne.symm sup_p_x_ne_zero).lt_of_le,
+    simp only [nnreal.zero_le_coe, nnreal.coe_pos,
+      finset.lt_sup_iff, exists_prop, forall_true_left] at this,
+    rcases this with ⟨i, i_in_set, p_i_pos⟩,
+    use ⟨i, ne_of_gt p_i_pos⟩ },
   { rw t2_iff_nhds,
     intros h x y x_y_nhds_ne_bot,
     rw filter.inf_ne_bot_iff at x_y_nhds_ne_bot,

From c2f66baaba66c8fccccaddd4b330ff98584b7dc2 Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Thu, 15 Dec 2022 19:58:23 +0100
Subject: [PATCH 07/17] style(analysis/locally_convex): max' suggestions 2

Split up iff into two implications; make proofs largely direct
---
 .../locally_convex/with_seminorms.lean        | 108 +++++++++---------
 src/analysis/seminorm.lean                    |  12 +-
 2 files changed, 58 insertions(+), 62 deletions(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index e491fdc558af5..ef31e1c19cf07 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -293,16 +293,16 @@ end
 /-- The `x`-neighbourhoods of a space whose topology is induced by a family of seminorms
 are exactly the sets which contain seminorm balls around `x`.-/
 lemma with_seminorms.mem_nhds_iff (hp : with_seminorms p) (x : E) (U : set E):
-  U ∈ nhds x ↔ ∃ (i : finset ι) (ε > 0), (i.sup p).ball x ε ⊆ U :=
+  U ∈ nhds x ↔ ∃ (s : finset ι) (r > 0), (s.sup p).ball x r ⊆ U :=
 begin
   rw [hp.with_seminorms_eq, (p.add_group_filter_basis.nhds_has_basis x).mem_iff' U],
   split,
-  { rintros ⟨V, V_in_basis, V_sub_U⟩,
-    rcases p.basis_sets_iff.mp V_in_basis with ⟨i_set, ε, ε_pos, hr⟩,
-    simp_rw [hr, seminorm.singleton_add_ball _, add_zero] at V_sub_U,
-    exact ⟨_, _, ε_pos, V_sub_U⟩ },
-  { rintros ⟨i_set, ε, ε_pos, V_sub_U⟩,
-    refine ⟨(i_set.sup p).ball 0 ε, p.basis_sets_iff.mpr ⟨_, _, ε_pos, rfl⟩, _⟩,
+  { rintros ⟨V, V_basis, hVU⟩,
+    rcases p.basis_sets_iff.mp V_basis with ⟨i_set, r, r_pos, V_ball⟩,
+    simp_rw [V_ball, seminorm.singleton_add_ball _, add_zero] at hVU,
+    exact ⟨_, _, r_pos, hVU⟩ },
+  { rintros ⟨i_set, r, r_pos, V_sub_U⟩,
+    refine ⟨(i_set.sup p).ball 0 r, p.basis_sets_iff.mpr ⟨_, _, r_pos, rfl⟩, _⟩,
     simp_rw [seminorm.singleton_add_ball _, add_zero],
     exact V_sub_U }
 end
@@ -310,60 +310,56 @@ end
 /-- The open sets of a space whose topology is induced by a family of seminorms
 are exactly the sets which contain seminorm balls around all of their points.-/
 lemma with_seminorms.is_open_iff_mem_balls (hp : with_seminorms p) (U : set E):
-  is_open U ↔ ∀ (x ∈ U), ∃ (i : finset ι) (ε > 0), (i.sup p).ball x ε ⊆ U :=
+  is_open U ↔ ∀ (x ∈ U), ∃ (s : finset ι) (r > 0), (s.sup p).ball x r ⊆ U :=
 by simp_rw [←with_seminorms.mem_nhds_iff hp _ U, is_open_iff_mem_nhds]
 
-/-- A space whose topology is induced by a family of seminorms is Hausdorff iff
-the family of seminorms is separating. -/
-theorem with_seminorms.t2_iff_separating (hp : with_seminorms p) :
-  t2_space E ↔ ∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0 :=
+/-- A separating family of seminorms induces a T₂ topology. -/
+lemma with_seminorms.t2_of_separating (hp : with_seminorms p) :
+  (∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0) → t2_space E :=
 begin
-  split,
-  { introI t2,
-    intros x x_ne_zero,
-    rcases t2_separation x_ne_zero with ⟨u, v, u_open, v_open, x_in_u, zero_in_v, u_v_disj⟩,
-    rcases (with_seminorms.is_open_iff_mem_balls hp _).mp v_open 0 zero_in_v
-      with ⟨i_set, ε, ε_pos, ball_in_v⟩,
-    have sup_p_x_ne_zero : (i_set.sup p) x ≠ 0,
-    { intro assump,
-      refine (set.singleton_nonempty x).not_subset_empty (u_v_disj _ _);
-        rw [set.le_eq_subset, set.singleton_subset_iff],
-      { exact (x_in_u) },
-      { refine (ball_in_v _),
-        rwa [seminorm.mem_ball, sub_zero, assump] } },
-    rw seminorm.finset_sup_apply at sup_p_x_ne_zero,
-    have := (ne.symm sup_p_x_ne_zero).lt_of_le,
-    simp only [nnreal.zero_le_coe, nnreal.coe_pos,
-      finset.lt_sup_iff, exists_prop, forall_true_left] at this,
-    rcases this with ⟨i, i_in_set, p_i_pos⟩,
-    use ⟨i, ne_of_gt p_i_pos⟩ },
-  { rw t2_iff_nhds,
-    intros h x y x_y_nhds_ne_bot,
-    rw filter.inf_ne_bot_iff at x_y_nhds_ne_bot,
-    by_contra x_neq_y,
-    cases h (x - y) (sub_ne_zero.mpr x_neq_y) with i pi_nonzero,
-    let ε := (p i) (x - y),
-    let sx := (p i).ball x (ε/2),
-    let sy := (p i).ball y (ε/2),
-    have ε_div_2_pos := div_pos ((ne.symm pi_nonzero).lt_of_le (map_nonneg _ _)) zero_lt_two,
-    have sx_nhds_x : sx ∈ nhds x :=
-      (with_seminorms.mem_nhds_iff hp _ _).mpr ⟨_, _, ε_div_2_pos, by rw finset.sup_singleton⟩,
-    have sy_nhds_y : sy ∈ nhds y :=
-      (with_seminorms.mem_nhds_iff hp _ _).mpr ⟨_, _, ε_div_2_pos, by rw finset.sup_singleton⟩,
-    cases set.nonempty_def.mp (x_y_nhds_ne_bot sx_nhds_x sy_nhds_y) with z z_in_inter,
-    obtain ⟨lt1, lt2⟩ := (set.mem_inter_iff _ _ _).mp z_in_inter,
-    rw seminorm.mem_ball at lt1 lt2,
-    have : ε < ε,
-    { calc
-      ε   = p i (x - y)                : rfl
-      ... = p i ((x - z) + (z - y))    : by rw ←sub_add_sub_cancel
-      ... ≤ p i (x - z) + p i (z - y)  : seminorm.add_le' _ _ _
-      ... = p i (z - x) + p i (z - y)  : by rw [←map_neg_eq_map, neg_sub]
-      ... < ε/2 + ε/2                  : add_lt_add lt1 lt2
-      ... = ε                          : add_halves _ },
-    rwa lt_self_iff_false ε at this }
+  rw t2_space_iff_nhds,
+  intros h x y hxy,
+  cases h (x - y) (sub_ne_zero.mpr hxy) with i pi_nonzero,
+  let r := p i (x - y),
+  have r_div_2_pos : p i (x - y) / 2 > 0 := by positivity,
+  have mem_nhds : ∀ x, (p i).ball x (r/2) ∈ nhds x :=
+    λ x, (with_seminorms.mem_nhds_iff hp _ _).mpr ⟨_, _, r_div_2_pos, by rw finset.sup_singleton⟩,
+  use [(p i).ball x (r/2) , mem_nhds x, (p i).ball y (r/2), mem_nhds y],
+  intros W W_sub_xball W_sub_yball,
+  by_contra W_nonemp,
+  rw [le_bot_iff, bot_eq_empty, ←ne.def, ←nonempty_iff_ne_empty] at W_nonemp,
+  cases W_nonemp with z z_in_W,
+  have : r < r,
+  { calc
+    r   = p i (x - y)               : rfl
+    ... = p i ((x - z) + (z - y))   : by rw ←sub_add_sub_cancel
+    ... ≤ p i (x - z) + p i (z - y) : seminorm.add_le' _ _ _
+    ... = p i (z - x) + p i (z - y) : by rw [←map_neg_eq_map, neg_sub]
+    ... < r/2 + r/2                 : add_lt_add (W_sub_xball z_in_W) (W_sub_yball z_in_W)
+    ... = r                         : add_halves _ },
+  rwa lt_self_iff_false r at this
 end
 
+/-- A family of seminorms inducing a T₂ topology is separating. -/
+lemma with_seminorms.separating_of_t2 [t2_space E] (hp : with_seminorms p) (x : E) (hx : x ≠ 0) :
+  ∃ i, p i x ≠ 0 :=
+begin
+  rcases t2_separation hx with ⟨U, V, hU, hV, hxU, h0V, UV_disj⟩,
+  rcases (with_seminorms.is_open_iff_mem_balls hp _).mp hV 0 h0V with ⟨s, r, r_pos, ball_V⟩,
+  have hpx_nezero : (s.sup p) x ≠ 0,
+  { intro hsup_px,
+    refine (set.singleton_nonempty x).not_subset_empty (UV_disj _ _);
+      rw [set.le_eq_subset, set.singleton_subset_iff],
+    { exact (hxU) },
+    { refine (ball_V _),
+      rwa [seminorm.mem_ball, sub_zero, hsup_px] } },
+  rw seminorm.finset_sup_apply at hpx_nezero,
+  have := (ne.symm hpx_nezero).lt_of_le,
+  simp only [nnreal.zero_le_coe, nnreal.coe_pos,
+    finset.lt_sup_iff, exists_prop, forall_true_left] at this,
+  rcases this with ⟨i, his, hpix_pos⟩,
+  use ⟨i, ne_of_gt hpix_pos⟩
+end
 
 end topology
 
diff --git a/src/analysis/seminorm.lean b/src/analysis/seminorm.lean
index 26475f32c66a7..bbe01e2522e1f 100644
--- a/src/analysis/seminorm.lean
+++ b/src/analysis/seminorm.lean
@@ -611,18 +611,18 @@ end
 
 /- Can this be done more neatly with `seminorm.ball_comp`?
 Alternatively, can this be done using/imitating the ball-addition-lemmas
-in normed_space/pointwise? -/
+in `normed_space/pointwise`? -/
 /-- The image of a ball under addition with a singleton is another ball. -/
 lemma singleton_add_ball (p : seminorm 𝕜 E):
   (λ (z : E), x + z) '' p.ball y r = p.ball (x + y) r :=
 begin
   apply le_antisymm,
-  { rintros w ⟨w', w'_in_ball, w'h⟩,
-    rwa [mem_ball, ← w'h, add_sub_add_left_eq_sub] },
-  { intros w w_in_ball,
-    refine set.mem_image_iff_bex.mpr ⟨w - x , _⟩,
+  { rintros z₀ ⟨z₁, hz₁, hz₁z₀⟩,
+    rwa [mem_ball, ←hz₁z₀, add_sub_add_left_eq_sub] },
+  { intros z hz,
+    refine set.mem_image_iff_bex.mpr ⟨z - x, _⟩,
     rw [mem_ball, sub_sub, add_sub, add_sub_cancel'],
-    exact ⟨w_in_ball, rfl⟩ }
+    exact ⟨hz, rfl⟩ }
 end
 
 end has_smul

From bd0ab94ac1609883fb833f2ed61c452514ab0dc1 Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@googlemail.com>
Date: Thu, 15 Dec 2022 23:08:40 +0100
Subject: [PATCH 08/17] Apply suggestions from code review

Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
---
 src/analysis/locally_convex/with_seminorms.lean | 10 +++++-----
 src/analysis/seminorm.lean                      |  4 ++--
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index ef31e1c19cf07..f2357b3b12af9 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -292,7 +292,7 @@ end
 
 /-- The `x`-neighbourhoods of a space whose topology is induced by a family of seminorms
 are exactly the sets which contain seminorm balls around `x`.-/
-lemma with_seminorms.mem_nhds_iff (hp : with_seminorms p) (x : E) (U : set E):
+lemma with_seminorms.mem_nhds_iff (hp : with_seminorms p) (x : E) (U : set E) :
   U ∈ nhds x ↔ ∃ (s : finset ι) (r > 0), (s.sup p).ball x r ⊆ U :=
 begin
   rw [hp.with_seminorms_eq, (p.add_group_filter_basis.nhds_has_basis x).mem_iff' U],
@@ -309,16 +309,16 @@ end
 
 /-- The open sets of a space whose topology is induced by a family of seminorms
 are exactly the sets which contain seminorm balls around all of their points.-/
-lemma with_seminorms.is_open_iff_mem_balls (hp : with_seminorms p) (U : set E):
+lemma with_seminorms.is_open_iff_mem_balls (hp : with_seminorms p) (U : set E) :
   is_open U ↔ ∀ (x ∈ U), ∃ (s : finset ι) (r > 0), (s.sup p).ball x r ⊆ U :=
 by simp_rw [←with_seminorms.mem_nhds_iff hp _ U, is_open_iff_mem_nhds]
 
 /-- A separating family of seminorms induces a T₂ topology. -/
-lemma with_seminorms.t2_of_separating (hp : with_seminorms p) :
-  (∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0) → t2_space E :=
+lemma with_seminorms.t2_of_separating (hp : with_seminorms p)
+  (h : ∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0) : t2_space E :=
 begin
   rw t2_space_iff_nhds,
-  intros h x y hxy,
+  intros x y hxy,
   cases h (x - y) (sub_ne_zero.mpr hxy) with i pi_nonzero,
   let r := p i (x - y),
   have r_div_2_pos : p i (x - y) / 2 > 0 := by positivity,
diff --git a/src/analysis/seminorm.lean b/src/analysis/seminorm.lean
index bbe01e2522e1f..cef53a66c5dca 100644
--- a/src/analysis/seminorm.lean
+++ b/src/analysis/seminorm.lean
@@ -613,11 +613,11 @@ end
 Alternatively, can this be done using/imitating the ball-addition-lemmas
 in `normed_space/pointwise`? -/
 /-- The image of a ball under addition with a singleton is another ball. -/
-lemma singleton_add_ball (p : seminorm 𝕜 E):
+lemma singleton_add_ball (p : seminorm 𝕜 E) :
   (λ (z : E), x + z) '' p.ball y r = p.ball (x + y) r :=
 begin
   apply le_antisymm,
-  { rintros z₀ ⟨z₁, hz₁, hz₁z₀⟩,
+  { rintros _ ⟨_, _, hz₁z₀⟩,
     rwa [mem_ball, ←hz₁z₀, add_sub_add_left_eq_sub] },
   { intros z hz,
     refine set.mem_image_iff_bex.mpr ⟨z - x, _⟩,

From 452fce6da16b5867bfd37c077cd35acaddfc433d Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@googlemail.com>
Date: Fri, 16 Dec 2022 00:00:09 +0100
Subject: [PATCH 09/17] Apply suggestions from code review

Co-authored-by: Moritz Doll <moritz.doll@googlemail.com>
---
 .../locally_convex/with_seminorms.lean         | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index f2357b3b12af9..3198adb9d7f9b 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -298,11 +298,11 @@ begin
   rw [hp.with_seminorms_eq, (p.add_group_filter_basis.nhds_has_basis x).mem_iff' U],
   split,
   { rintros ⟨V, V_basis, hVU⟩,
-    rcases p.basis_sets_iff.mp V_basis with ⟨i_set, r, r_pos, V_ball⟩,
+    rcases p.basis_sets_iff.mp V_basis with ⟨_, _, r_pos, V_ball⟩,
     simp_rw [V_ball, seminorm.singleton_add_ball _, add_zero] at hVU,
     exact ⟨_, _, r_pos, hVU⟩ },
-  { rintros ⟨i_set, r, r_pos, V_sub_U⟩,
-    refine ⟨(i_set.sup p).ball 0 r, p.basis_sets_iff.mpr ⟨_, _, r_pos, rfl⟩, _⟩,
+  { rintros ⟨s, r, r_pos, V_sub_U⟩,
+    refine ⟨(s.sup p).ball 0 r, p.basis_sets_iff.mpr ⟨_, _, r_pos, rfl⟩, _⟩,
     simp_rw [seminorm.singleton_add_ball _, add_zero],
     exact V_sub_U }
 end
@@ -314,8 +314,8 @@ lemma with_seminorms.is_open_iff_mem_balls (hp : with_seminorms p) (U : set E) :
 by simp_rw [←with_seminorms.mem_nhds_iff hp _ U, is_open_iff_mem_nhds]
 
 /-- A separating family of seminorms induces a T₂ topology. -/
-lemma with_seminorms.t2_of_separating (hp : with_seminorms p)
-  (h : ∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0) : t2_space E :=
+lemma with_seminorms.t2_of_separating (hp : with_seminorms p) (h : ∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0) :
+  t2_space E :=
 begin
   rw t2_space_iff_nhds,
   intros x y hxy,
@@ -323,7 +323,7 @@ begin
   let r := p i (x - y),
   have r_div_2_pos : p i (x - y) / 2 > 0 := by positivity,
   have mem_nhds : ∀ x, (p i).ball x (r/2) ∈ nhds x :=
-    λ x, (with_seminorms.mem_nhds_iff hp _ _).mpr ⟨_, _, r_div_2_pos, by rw finset.sup_singleton⟩,
+  λ x, (with_seminorms.mem_nhds_iff hp _ _).mpr ⟨_, _, r_div_2_pos, by rw finset.sup_singleton⟩,
   use [(p i).ball x (r/2) , mem_nhds x, (p i).ball y (r/2), mem_nhds y],
   intros W W_sub_xball W_sub_yball,
   by_contra W_nonemp,
@@ -350,11 +350,11 @@ begin
   { intro hsup_px,
     refine (set.singleton_nonempty x).not_subset_empty (UV_disj _ _);
       rw [set.le_eq_subset, set.singleton_subset_iff],
-    { exact (hxU) },
-    { refine (ball_V _),
+    { exact hxU },
+    { refine ball_V _,
       rwa [seminorm.mem_ball, sub_zero, hsup_px] } },
   rw seminorm.finset_sup_apply at hpx_nezero,
-  have := (ne.symm hpx_nezero).lt_of_le,
+  have := hpx_nezero.symm.lt_of_le,
   simp only [nnreal.zero_le_coe, nnreal.coe_pos,
     finset.lt_sup_iff, exists_prop, forall_true_left] at this,
   rcases this with ⟨i, his, hpix_pos⟩,

From efa9d886217e64f8c2a31f13a006e5964bc03c42 Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Fri, 16 Dec 2022 08:59:26 +0100
Subject: [PATCH 10/17] Review changes

---
 src/analysis/seminorm.lean | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/analysis/seminorm.lean b/src/analysis/seminorm.lean
index cef53a66c5dca..9d3cd85661ec2 100644
--- a/src/analysis/seminorm.lean
+++ b/src/analysis/seminorm.lean
@@ -609,6 +609,10 @@ begin
   exact (map_add_le_add p _ _).trans (add_le_add hy₁ hy₂)
 end
 
+lemma sub_mem_ball (p : seminorm 𝕜 E) (x₁ x₂ y : E) (r : ℝ) :
+  x₁ - x₂ ∈ p.ball y r ↔ x₁ ∈ p.ball (x₂ + y) r :=
+by simp_rw [mem_ball, sub_sub]
+
 /- Can this be done more neatly with `seminorm.ball_comp`?
 Alternatively, can this be done using/imitating the ball-addition-lemmas
 in `normed_space/pointwise`? -/
@@ -619,10 +623,8 @@ begin
   apply le_antisymm,
   { rintros _ ⟨_, _, hz₁z₀⟩,
     rwa [mem_ball, ←hz₁z₀, add_sub_add_left_eq_sub] },
-  { intros z hz,
-    refine set.mem_image_iff_bex.mpr ⟨z - x, _⟩,
-    rw [mem_ball, sub_sub, add_sub, add_sub_cancel'],
-    exact ⟨hz, rfl⟩ }
+  { exact λ z hz, ⟨z - x, ⟨(p.sub_mem_ball _ _ _ _).mpr hz, add_eq_of_eq_sub' rfl⟩⟩ }
+
 end
 
 end has_smul

From 170848059357700342ebb7e1ea33d17a77f4aa70 Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@googlemail.com>
Date: Sat, 17 Dec 2022 11:22:00 +0100
Subject: [PATCH 11/17] Apply suggestions from code review
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
---
 .../locally_convex/with_seminorms.lean        | 56 ++++++-------------
 1 file changed, 18 insertions(+), 38 deletions(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index 3198adb9d7f9b..f04b94161162f 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -310,55 +310,35 @@ end
 /-- The open sets of a space whose topology is induced by a family of seminorms
 are exactly the sets which contain seminorm balls around all of their points.-/
 lemma with_seminorms.is_open_iff_mem_balls (hp : with_seminorms p) (U : set E) :
-  is_open U ↔ ∀ (x ∈ U), ∃ (s : finset ι) (r > 0), (s.sup p).ball x r ⊆ U :=
+  is_open U ↔ ∀ x ∈ U, ∃ (s : finset ι) (r > 0), (s.sup p).ball x r ⊆ U :=
 by simp_rw [←with_seminorms.mem_nhds_iff hp _ U, is_open_iff_mem_nhds]
 
 /-- A separating family of seminorms induces a T₂ topology. -/
-lemma with_seminorms.t2_of_separating (hp : with_seminorms p) (h : ∀ x, (x ≠ 0) → ∃ i, p i x ≠ 0) :
+lemma with_seminorms.t2_of_separating (hp : with_seminorms p) (h : ∀ x ≠ 0, ∃ i, p i x ≠ 0) :
   t2_space E :=
 begin
-  rw t2_space_iff_nhds,
-  intros x y hxy,
-  cases h (x - y) (sub_ne_zero.mpr hxy) with i pi_nonzero,
-  let r := p i (x - y),
-  have r_div_2_pos : p i (x - y) / 2 > 0 := by positivity,
-  have mem_nhds : ∀ x, (p i).ball x (r/2) ∈ nhds x :=
-  λ x, (with_seminorms.mem_nhds_iff hp _ _).mpr ⟨_, _, r_div_2_pos, by rw finset.sup_singleton⟩,
-  use [(p i).ball x (r/2) , mem_nhds x, (p i).ball y (r/2), mem_nhds y],
-  intros W W_sub_xball W_sub_yball,
-  by_contra W_nonemp,
-  rw [le_bot_iff, bot_eq_empty, ←ne.def, ←nonempty_iff_ne_empty] at W_nonemp,
-  cases W_nonemp with z z_in_W,
-  have : r < r,
-  { calc
-    r   = p i (x - y)               : rfl
-    ... = p i ((x - z) + (z - y))   : by rw ←sub_add_sub_cancel
-    ... ≤ p i (x - z) + p i (z - y) : seminorm.add_le' _ _ _
-    ... = p i (z - x) + p i (z - y) : by rw [←map_neg_eq_map, neg_sub]
-    ... < r/2 + r/2                 : add_lt_add (W_sub_xball z_in_W) (W_sub_yball z_in_W)
-    ... = r                         : add_halves _ },
-  rwa lt_self_iff_false r at this
+  haveI : topological_add_group E := hp.topological_add_group,
+  suffices : t1_space E,
+  { haveI := this,
+    exact topological_add_group.t2_space E },
+  refine topological_add_group.t1_space _ _,
+  rw [← is_open_compl_iff, hp.is_open_iff_mem_balls],
+  rintros x (hx : x ≠ 0),
+  cases h x hx with i pi_nonzero,
+  refine ⟨{i}, p i x, by positivity, subset_compl_singleton_iff.mpr _⟩,
+  rw [finset.sup_singleton, mem_ball, zero_sub, map_neg_eq_map, not_lt]
 end
 
 /-- A family of seminorms inducing a T₂ topology is separating. -/
 lemma with_seminorms.separating_of_t2 [t2_space E] (hp : with_seminorms p) (x : E) (hx : x ≠ 0) :
   ∃ i, p i x ≠ 0 :=
 begin
-  rcases t2_separation hx with ⟨U, V, hU, hV, hxU, h0V, UV_disj⟩,
-  rcases (with_seminorms.is_open_iff_mem_balls hp _).mp hV 0 h0V with ⟨s, r, r_pos, ball_V⟩,
-  have hpx_nezero : (s.sup p) x ≠ 0,
-  { intro hsup_px,
-    refine (set.singleton_nonempty x).not_subset_empty (UV_disj _ _);
-      rw [set.le_eq_subset, set.singleton_subset_iff],
-    { exact hxU },
-    { refine ball_V _,
-      rwa [seminorm.mem_ball, sub_zero, hsup_px] } },
-  rw seminorm.finset_sup_apply at hpx_nezero,
-  have := hpx_nezero.symm.lt_of_le,
-  simp only [nnreal.zero_le_coe, nnreal.coe_pos,
-    finset.lt_sup_iff, exists_prop, forall_true_left] at this,
-  rcases this with ⟨i, his, hpix_pos⟩,
-  use ⟨i, ne_of_gt hpix_pos⟩
+  have := ((t1_space_tfae E).out 0 9).mp infer_instance,
+  by_contra' h,
+  refine hx (this _),
+  rw hp.has_basis_zero_ball.specializes_iff,
+  rintros ⟨s, r⟩ (hr : 0 < r),
+  simp only [ball_finset_sup_eq_Inter _ _ _ hr, mem_Inter₂, mem_ball_zero, h, hr, forall_true_iff],
 end
 
 end topology

From cee0dc2ebc60d83f0dd311692fc6692949d59a35 Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Sat, 17 Dec 2022 11:25:49 +0100
Subject: [PATCH 12/17] added with_seminorms.topological_add_group

---
 src/analysis/locally_convex/with_seminorms.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index f04b94161162f..cae07e7bc78ec 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -283,6 +283,12 @@ lemma with_seminorms.with_seminorms_eq {p : seminorm_family 𝕜 E ι} [t : topo
 variables [topological_space E]
 variables {p : seminorm_family 𝕜 E ι}
 
+lemma with_seminorms.topological_add_group (hp : with_seminorms p) : topological_add_group E :=
+begin
+  rw hp.with_seminorms_eq,
+  exact add_group_filter_basis.is_topological_add_group _
+end
+
 lemma with_seminorms.has_basis (hp : with_seminorms p) : (𝓝 (0 : E)).has_basis
   (λ (s : set E), s ∈ p.basis_sets) id :=
 begin

From 835483048ce9842d3923a6a98790cbc81249ad7b Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Sat, 17 Dec 2022 11:28:29 +0100
Subject: [PATCH 13/17] add has_basis_zero_ball and has_basis_ball

---
 .../locally_convex/with_seminorms.lean        | 22 +++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index cae07e7bc78ec..90289672542b2 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -296,6 +296,28 @@ begin
   exact add_group_filter_basis.nhds_zero_has_basis _,
 end
 
+lemma with_seminorms.has_basis_zero_ball (hp : with_seminorms p) : (𝓝 (0 : E)).has_basis
+  (λ sr : finset ι × ℝ, 0 < sr.2) (λ sr, (sr.1.sup p).ball 0 sr.2) :=
+begin
+  refine ⟨λ V, _⟩,
+  simp only [hp.has_basis.mem_iff, seminorm_family.basis_sets_iff, prod.exists],
+  split,
+  { rintros ⟨-, ⟨s, r, hr, rfl⟩, hV⟩,
+    exact ⟨s, r, hr, hV⟩ },
+  { rintros ⟨s, r, hr, hV⟩,
+    exact ⟨_, ⟨s, r, hr, rfl⟩, hV⟩ }
+end
+
+lemma with_seminorms.has_basis_ball (hp : with_seminorms p) {x : E} : (𝓝 (x : E)).has_basis
+  (λ sr : finset ι × ℝ, 0 < sr.2) (λ sr, (sr.1.sup p).ball x sr.2) :=
+begin
+  haveI : topological_add_group E := hp.topological_add_group,
+  rw [← map_add_left_nhds_zero],
+  convert (hp.has_basis_zero_ball.map ((+) x)),
+  ext sr : 1,
+  rw [seminorm.singleton_add_ball, add_zero]
+end
+
 /-- The `x`-neighbourhoods of a space whose topology is induced by a family of seminorms
 are exactly the sets which contain seminorm balls around `x`.-/
 lemma with_seminorms.mem_nhds_iff (hp : with_seminorms p) (x : E) (U : set E) :

From 5b994eb1839e34dfa5e13dd8b6a550c44054bbe8 Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Sat, 17 Dec 2022 20:36:40 +0100
Subject: [PATCH 14/17] shorter mem_nhds_iff

---
 src/analysis/locally_convex/with_seminorms.lean | 13 +------------
 1 file changed, 1 insertion(+), 12 deletions(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index 90289672542b2..b2bad14b82137 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -322,18 +322,7 @@ end
 are exactly the sets which contain seminorm balls around `x`.-/
 lemma with_seminorms.mem_nhds_iff (hp : with_seminorms p) (x : E) (U : set E) :
   U ∈ nhds x ↔ ∃ (s : finset ι) (r > 0), (s.sup p).ball x r ⊆ U :=
-begin
-  rw [hp.with_seminorms_eq, (p.add_group_filter_basis.nhds_has_basis x).mem_iff' U],
-  split,
-  { rintros ⟨V, V_basis, hVU⟩,
-    rcases p.basis_sets_iff.mp V_basis with ⟨_, _, r_pos, V_ball⟩,
-    simp_rw [V_ball, seminorm.singleton_add_ball _, add_zero] at hVU,
-    exact ⟨_, _, r_pos, hVU⟩ },
-  { rintros ⟨s, r, r_pos, V_sub_U⟩,
-    refine ⟨(s.sup p).ball 0 r, p.basis_sets_iff.mpr ⟨_, _, r_pos, rfl⟩, _⟩,
-    simp_rw [seminorm.singleton_add_ball _, add_zero],
-    exact V_sub_U }
-end
+by rw [hp.has_basis_ball.mem_iff, prod.exists]
 
 /-- The open sets of a space whose topology is induced by a family of seminorms
 are exactly the sets which contain seminorm balls around all of their points.-/

From b14c97c3edbf46b17019c59b213640162c5dfe7b Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Sat, 17 Dec 2022 22:47:37 +0100
Subject: [PATCH 15/17] replace singleton_add_ball with vadd_ball

---
 .../locally_convex/with_seminorms.lean        |  4 +++-
 src/analysis/seminorm.lean                    | 21 +++++++++++--------
 2 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index b2bad14b82137..b4fee7ee8b341 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -315,7 +315,9 @@ begin
   rw [← map_add_left_nhds_zero],
   convert (hp.has_basis_zero_ball.map ((+) x)),
   ext sr : 1,
-  rw [seminorm.singleton_add_ball, add_zero]
+  have : (sr.fst.sup p).ball (x +ᵥ 0) sr.snd = x +ᵥ (sr.fst.sup p).ball 0 sr.snd
+    := eq.symm (seminorm.vadd_ball (sr.fst.sup p)),
+  rwa [vadd_eq_add, add_zero] at this,
 end
 
 /-- The `x`-neighbourhoods of a space whose topology is induced by a family of seminorms
diff --git a/src/analysis/seminorm.lean b/src/analysis/seminorm.lean
index 9d3cd85661ec2..1fce620c351c3 100644
--- a/src/analysis/seminorm.lean
+++ b/src/analysis/seminorm.lean
@@ -6,6 +6,7 @@ Authors: Jean Lo, Yaël Dillies, Moritz Doll
 import data.real.pointwise
 import analysis.convex.function
 import analysis.locally_convex.basic
+import analysis.normed.group.add_torsor
 
 /-!
 # Seminorms
@@ -613,18 +614,20 @@ lemma sub_mem_ball (p : seminorm 𝕜 E) (x₁ x₂ y : E) (r : ℝ) :
   x₁ - x₂ ∈ p.ball y r ↔ x₁ ∈ p.ball (x₂ + y) r :=
 by simp_rw [mem_ball, sub_sub]
 
-/- Can this be done more neatly with `seminorm.ball_comp`?
-Alternatively, can this be done using/imitating the ball-addition-lemmas
-in `normed_space/pointwise`? -/
 /-- The image of a ball under addition with a singleton is another ball. -/
-lemma singleton_add_ball (p : seminorm 𝕜 E) :
-  (λ (z : E), x + z) '' p.ball y r = p.ball (x + y) r :=
+lemma vadd_ball (p : seminorm 𝕜 E) :
+  x +ᵥ p.ball y r = p.ball (x +ᵥ y) r :=
 begin
-  apply le_antisymm,
-  { rintros _ ⟨_, _, hz₁z₀⟩,
-    rwa [mem_ball, ←hz₁z₀, add_sub_add_left_eq_sub] },
-  { exact λ z hz, ⟨z - x, ⟨(p.sub_mem_ball _ _ _ _).mpr hz, add_eq_of_eq_sub' rfl⟩⟩ }
+  letI := add_group_seminorm.to_seminormed_add_comm_group p.to_add_group_seminorm,
+  exact vadd_ball x y r,
+end
 
+/-- The image of a closed ball under addition with a singleton is another closed ball. -/
+lemma vadd_closed_ball (p : seminorm 𝕜 E) :
+  x +ᵥ p.closed_ball y r = p.closed_ball (x +ᵥ y) r :=
+begin
+  letI := add_group_seminorm.to_seminormed_add_comm_group p.to_add_group_seminorm,
+  exact vadd_closed_ball x y r,
 end
 
 end has_smul

From b0d008fe2e7bf79d9086ae6d23bbfe370feb864e Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Sun, 18 Dec 2022 15:50:42 +0100
Subject: [PATCH 16/17] reduce to t1, add remark of equivalence to t2

---
 .../locally_convex/with_seminorms.lean        | 29 ++++++++++++-------
 1 file changed, 19 insertions(+), 10 deletions(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index b4fee7ee8b341..6fbec3724f53a 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -332,14 +332,14 @@ lemma with_seminorms.is_open_iff_mem_balls (hp : with_seminorms p) (U : set E) :
   is_open U ↔ ∀ x ∈ U, ∃ (s : finset ι) (r > 0), (s.sup p).ball x r ⊆ U :=
 by simp_rw [←with_seminorms.mem_nhds_iff hp _ U, is_open_iff_mem_nhds]
 
-/-- A separating family of seminorms induces a T₂ topology. -/
-lemma with_seminorms.t2_of_separating (hp : with_seminorms p) (h : ∀ x ≠ 0, ∃ i, p i x ≠ 0) :
-  t2_space E :=
-begin
-  haveI : topological_add_group E := hp.topological_add_group,
-  suffices : t1_space E,
-  { haveI := this,
-    exact topological_add_group.t2_space E },
+/- Note that through the following lemma, one also immediately has that separating families
+of seminorms induce T₂ and T₃ topologies by `topological_add_group.t2_space`
+and `topological_add_group.t3_space` -/
+/-- A separating family of seminorms induces a T₁ topology. -/
+lemma with_seminorms.t1_of_separating (hp : with_seminorms p) (h : ∀ x ≠ 0, ∃ i, p i x ≠ 0) :
+  t1_space E :=
+begin
+  haveI := hp.topological_add_group,
   refine topological_add_group.t1_space _ _,
   rw [← is_open_compl_iff, hp.is_open_iff_mem_balls],
   rintros x (hx : x ≠ 0),
@@ -348,8 +348,8 @@ begin
   rw [finset.sup_singleton, mem_ball, zero_sub, map_neg_eq_map, not_lt]
 end
 
-/-- A family of seminorms inducing a T₂ topology is separating. -/
-lemma with_seminorms.separating_of_t2 [t2_space E] (hp : with_seminorms p) (x : E) (hx : x ≠ 0) :
+/-- A family of seminorms inducing a T₁ topology is separating. -/
+lemma with_seminorms.separating_of_t1 [t1_space E] (hp : with_seminorms p) (x : E) (hx : x ≠ 0) :
   ∃ i, p i x ≠ 0 :=
 begin
   have := ((t1_space_tfae E).out 0 9).mp infer_instance,
@@ -360,6 +360,15 @@ begin
   simp only [ball_finset_sup_eq_Inter _ _ _ hr, mem_Inter₂, mem_ball_zero, h, hr, forall_true_iff],
 end
 
+/-- A family of seminorms is separating iff it induces a T₁ topology. -/
+lemma with_seminorms.separating_iff_t1 (hp : with_seminorms p) :
+  (∀ x ≠ 0, ∃ i, p i x ≠ 0) ↔ t1_space E :=
+begin
+  refine ⟨with_seminorms.t1_of_separating hp, _⟩,
+  introI,
+  exact with_seminorms.separating_of_t1 hp,
+end
+
 end topology
 
 section topological_add_group

From dafdca8fcc3f5e45d9a0a6b0fa80ea6cc4b47f09 Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Sun, 18 Dec 2022 15:53:27 +0100
Subject: [PATCH 17/17] typo in docstring

---
 src/analysis/locally_convex/with_seminorms.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analysis/locally_convex/with_seminorms.lean b/src/analysis/locally_convex/with_seminorms.lean
index 6fbec3724f53a..0294d199c1771 100644
--- a/src/analysis/locally_convex/with_seminorms.lean
+++ b/src/analysis/locally_convex/with_seminorms.lean
@@ -332,7 +332,7 @@ lemma with_seminorms.is_open_iff_mem_balls (hp : with_seminorms p) (U : set E) :
   is_open U ↔ ∀ x ∈ U, ∃ (s : finset ι) (r > 0), (s.sup p).ball x r ⊆ U :=
 by simp_rw [←with_seminorms.mem_nhds_iff hp _ U, is_open_iff_mem_nhds]
 
-/- Note that through the following lemma, one also immediately has that separating families
+/- Note that through the following lemmas, one also immediately has that separating families
 of seminorms induce T₂ and T₃ topologies by `topological_add_group.t2_space`
 and `topological_add_group.t3_space` -/
 /-- A separating family of seminorms induces a T₁ topology. -/