refactor(analysis/locally_convex/with_seminorms): use abbreviations t…

…o allow for dot notation (#12846)

src/analysis/locally_convex/with_seminorms.lean

@@ -11,15 +11,15 @@ import analysis.seminorm
 
 ## Main definitions
 
-* `seminorm_basis_zero`: The set of open seminorm balls for a family of seminorms.
-* `seminorm_module_filter_basis`: A module filter basis formed by the open balls.
+* `seminorm_family.basis_sets`: The set of open seminorm balls for a family of seminorms.
+* `seminorm_family.module_filter_basis`: A module filter basis formed by the open balls.
 * `seminorm.is_bounded`: A linear map `f : E →ₗ[𝕜] F` is bounded iff every seminorm in `F` can be
 bounded by a finite number of seminorms in `E`.
 
 ## Main statements
 
 * `continuous_from_bounded`: A bounded linear map `f : E →ₗ[𝕜] F` is continuous.
-* `with_seminorms.to_locally_convex_space`: A space equipped with a family of seminorms is locally
+* `seminorm_family.to_locally_convex_space`: A space equipped with a family of seminorms is locally
 convex.
 
 ## TODO
@@ -40,39 +40,49 @@ section filter_basis
 
 variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E]
 
-/-- A filter basis for the neighborhood filter of 0. -/
-def seminorm_basis_zero (p : ι → seminorm 𝕜 E) : set (set E) :=
+variables (𝕜 E ι)
+
+/-- An abbreviation for indexed families of seminorms. This is mainly to allow for dot-notation. -/
+abbreviation seminorm_family := ι → seminorm 𝕜 E
+
+variables {𝕜 E ι}
+
+namespace seminorm_family
+
+/-- The sets of a filter basis for the neighborhood filter of 0. -/
+def basis_sets (p : seminorm_family 𝕜 E ι) : set (set E) :=
 ⋃ (s : finset ι) r (hr : 0 < r), singleton $ ball (s.sup p) (0 : E) r
 
-lemma seminorm_basis_zero_iff (p : ι → seminorm 𝕜 E) (U : set E) :
-  U ∈ seminorm_basis_zero p ↔ ∃ (i : finset ι) r (hr : 0 < r), U = ball (i.sup p) 0 r :=
-by simp only [seminorm_basis_zero, mem_Union, mem_singleton_iff]
+variables (p : seminorm_family 𝕜 E ι)
+
+lemma basis_sets_iff (U : set E) :
+  U ∈ p.basis_sets ↔ ∃ (i : finset ι) r (hr : 0 < r), U = ball (i.sup p) 0 r :=
+by simp only [basis_sets, mem_Union, mem_singleton_iff]
 
-lemma seminorm_basis_zero_mem (p : ι → seminorm 𝕜 E) (i : finset ι) {r : ℝ} (hr : 0 < r) :
-  (i.sup p).ball 0 r ∈ seminorm_basis_zero p :=
-(seminorm_basis_zero_iff _ _).mpr ⟨i,_,hr,rfl⟩
+lemma basis_sets_mem (i : finset ι) {r : ℝ} (hr : 0 < r) :
+  (i.sup p).ball 0 r ∈ p.basis_sets :=
+(basis_sets_iff _ _).mpr ⟨i,_,hr,rfl⟩
 
-lemma seminorm_basis_zero_singleton_mem (p : ι → seminorm 𝕜 E) (i : ι) {r : ℝ} (hr : 0 < r) :
-  (p i).ball 0 r ∈ seminorm_basis_zero p :=
-(seminorm_basis_zero_iff _ _).mpr ⟨{i},_,hr, by rw finset.sup_singleton⟩
+lemma basis_sets_singleton_mem (i : ι) {r : ℝ} (hr : 0 < r) :
+  (p i).ball 0 r ∈ p.basis_sets :=
+(basis_sets_iff _ _).mpr ⟨{i},_,hr, by rw finset.sup_singleton⟩
 
-lemma seminorm_basis_zero_nonempty (p : ι → seminorm 𝕜 E) [nonempty ι] :
-  (seminorm_basis_zero p).nonempty :=
+lemma basis_sets_nonempty [nonempty ι] : p.basis_sets.nonempty :=
 begin
   let i := classical.arbitrary ι,
-  refine set.nonempty_def.mpr ⟨ball (p i) 0 1, _⟩,
-  exact seminorm_basis_zero_singleton_mem _ i zero_lt_one,
+  refine set.nonempty_def.mpr ⟨(p i).ball 0 1, _⟩,
+  exact p.basis_sets_singleton_mem i zero_lt_one,
 end
 
-lemma seminorm_basis_zero_intersect (p : ι → seminorm 𝕜 E)
-  (U V : set E) (hU : U ∈ seminorm_basis_zero p) (hV : V ∈ seminorm_basis_zero p) :
-  ∃ (z : set E) (H : z ∈ (seminorm_basis_zero p)), z ⊆ U ∩ V :=
+lemma basis_sets_intersect
+  (U V : set E) (hU : U ∈ p.basis_sets) (hV : V ∈ p.basis_sets) :
+  ∃ (z : set E) (H : z ∈ p.basis_sets), z ⊆ U ∩ V :=
 begin
   classical,
-  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨s, r₁, hr₁, hU⟩,
-  rcases (seminorm_basis_zero_iff p V).mp hV with ⟨t, r₂, hr₂, hV⟩,
+  rcases (p.basis_sets_iff U).mp hU with ⟨s, r₁, hr₁, hU⟩,
+  rcases (p.basis_sets_iff V).mp hV with ⟨t, r₂, hr₂, hV⟩,
   use ((s ∪ t).sup p).ball 0 (min r₁ r₂),
-  refine ⟨seminorm_basis_zero_mem p (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), _⟩,
+  refine ⟨p.basis_sets_mem (s ∪ t) (lt_min_iff.mpr ⟨hr₁, hr₂⟩), _⟩,
   rw [hU, hV, ball_finset_sup_eq_Inter _ _ _ (lt_min_iff.mpr ⟨hr₁, hr₂⟩),
     ball_finset_sup_eq_Inter _ _ _ hr₁, ball_finset_sup_eq_Inter _ _ _ hr₂],
   exact set.subset_inter
@@ -81,46 +91,41 @@ begin
     min_le_right _ _⟩),
 end
 
-lemma seminorm_basis_zero_zero (p : ι → seminorm 𝕜 E) (U) (hU : U ∈ seminorm_basis_zero p) :
+lemma basis_sets_zero (U) (hU : U ∈ p.basis_sets) :
   (0 : E) ∈ U :=
 begin
-  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨ι', r, hr, hU⟩,
+  rcases (p.basis_sets_iff U).mp hU with ⟨ι', r, hr, hU⟩,
   rw [hU, mem_ball_zero, (ι'.sup p).zero],
   exact hr,
 end
 
-lemma seminorm_basis_zero_add (p : ι → seminorm 𝕜 E) (U) (hU : U ∈ seminorm_basis_zero p) :
-  ∃ (V : set E) (H : V ∈ (seminorm_basis_zero p)), V + V ⊆ U :=
+lemma basis_sets_add (U) (hU : U ∈ p.basis_sets) :
+  ∃ (V : set E) (H : V ∈ p.basis_sets), V + V ⊆ U :=
 begin
-  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨s, r, hr, hU⟩,
+  rcases (p.basis_sets_iff U).mp hU with ⟨s, r, hr, hU⟩,
   use (s.sup p).ball 0 (r/2),
-  refine ⟨seminorm_basis_zero_mem p s (div_pos hr zero_lt_two), _⟩,
+  refine ⟨p.basis_sets_mem s (div_pos hr zero_lt_two), _⟩,
   refine set.subset.trans (ball_add_ball_subset (s.sup p) (r/2) (r/2) 0 0) _,
   rw [hU, add_zero, add_halves'],
 end
 
-lemma seminorm_basis_zero_neg (p : ι → seminorm 𝕜 E) (U) (hU' : U ∈ seminorm_basis_zero p) :
-  ∃ (V : set E) (H : V ∈ (seminorm_basis_zero p)), V ⊆ (λ (x : E), -x) ⁻¹' U :=
+lemma basis_sets_neg (U) (hU' : U ∈ p.basis_sets) :
+  ∃ (V : set E) (H : V ∈ p.basis_sets), V ⊆ (λ (x : E), -x) ⁻¹' U :=
 begin
-  rcases (seminorm_basis_zero_iff p U).mp hU' with ⟨s, r, hr, hU⟩,
+  rcases (p.basis_sets_iff U).mp hU' with ⟨s, r, hr, hU⟩,
   rw [hU, neg_preimage, neg_ball (s.sup p), neg_zero],
   exact ⟨U, hU', eq.subset hU⟩,
 end
 
 /-- The `add_group_filter_basis` induced by the filter basis `seminorm_basis_zero`. -/
-def seminorm_add_group_filter_basis [nonempty ι]
-  (p : ι → seminorm 𝕜 E) : add_group_filter_basis E :=
-add_group_filter_basis_of_comm (seminorm_basis_zero p)
-  (seminorm_basis_zero_nonempty p)
-  (seminorm_basis_zero_intersect p)
-  (seminorm_basis_zero_zero p)
-  (seminorm_basis_zero_add p)
-  (seminorm_basis_zero_neg p)
-
-lemma seminorm_basis_zero_smul_right (p : ι → seminorm 𝕜 E) (v : E) (U : set E)
-  (hU : U ∈ seminorm_basis_zero p) : ∀ᶠ (x : 𝕜) in 𝓝 0, x • v ∈ U :=
+protected def add_group_filter_basis [nonempty ι] : add_group_filter_basis E :=
+add_group_filter_basis_of_comm p.basis_sets p.basis_sets_nonempty
+  p.basis_sets_intersect p.basis_sets_zero p.basis_sets_add p.basis_sets_neg
+
+lemma basis_sets_smul_right (v : E) (U : set E)
+  (hU : U ∈ p.basis_sets) : ∀ᶠ (x : 𝕜) in 𝓝 0, x • v ∈ U :=
 begin
-  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨s, r, hr, hU⟩,
+  rcases (p.basis_sets_iff U).mp hU with ⟨s, r, hr, hU⟩,
   rw [hU, filter.eventually_iff],
   simp_rw [(s.sup p).mem_ball_zero, (s.sup p).smul],
   by_cases h : 0 < (s.sup p) v,
@@ -133,38 +138,40 @@ end
 
 variables [nonempty ι]
 
-lemma seminorm_basis_zero_smul (p : ι → seminorm 𝕜 E) (U) (hU : U ∈ seminorm_basis_zero p) :
+lemma basis_sets_smul (U) (hU : U ∈ p.basis_sets) :
   ∃ (V : set 𝕜) (H : V ∈ 𝓝 (0 : 𝕜)) (W : set E)
-  (H : W ∈ (seminorm_add_group_filter_basis p).sets), V • W ⊆ U :=
+  (H : W ∈ p.add_group_filter_basis.sets), V • W ⊆ U :=
 begin
-  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨s, r, hr, hU⟩,
+  rcases (p.basis_sets_iff U).mp hU with ⟨s, r, hr, hU⟩,
   refine ⟨metric.ball 0 r.sqrt, metric.ball_mem_nhds 0 (real.sqrt_pos.mpr hr), _⟩,
-  refine ⟨(s.sup p).ball 0 r.sqrt, seminorm_basis_zero_mem p s (real.sqrt_pos.mpr hr), _⟩,
+  refine ⟨(s.sup p).ball 0 r.sqrt, p.basis_sets_mem s (real.sqrt_pos.mpr hr), _⟩,
   refine set.subset.trans (ball_smul_ball (s.sup p) r.sqrt r.sqrt) _,
   rw [hU, real.mul_self_sqrt (le_of_lt hr)],
 end
 
-lemma seminorm_basis_zero_smul_left (p : ι → seminorm 𝕜 E) (x : 𝕜) (U : set E)
-  (hU : U ∈ seminorm_basis_zero p) : ∃ (V : set E)
-  (H : V ∈ (seminorm_add_group_filter_basis p).sets), V ⊆ (λ (y : E), x • y) ⁻¹' U :=
+lemma basis_sets_smul_left (x : 𝕜) (U : set E)
+  (hU : U ∈ p.basis_sets) : ∃ (V : set E)
+  (H : V ∈ p.add_group_filter_basis.sets), V ⊆ (λ (y : E), x • y) ⁻¹' U :=
 begin
-  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨s, r, hr, hU⟩,
+  rcases (p.basis_sets_iff U).mp hU with ⟨s, r, hr, hU⟩,
   rw hU,
   by_cases h : x ≠ 0,
   { rw [(s.sup p).smul_ball_preimage 0 r x h, smul_zero],
     use (s.sup p).ball 0 (r / ∥x∥),
-    exact ⟨seminorm_basis_zero_mem p s (div_pos hr (norm_pos_iff.mpr h)), subset.rfl⟩ },
-  refine ⟨(s.sup p).ball 0 r, seminorm_basis_zero_mem p s hr, _⟩,
+    exact ⟨p.basis_sets_mem s (div_pos hr (norm_pos_iff.mpr h)), subset.rfl⟩ },
+  refine ⟨(s.sup p).ball 0 r, p.basis_sets_mem s hr, _⟩,
   simp only [not_ne_iff.mp h, subset_def, mem_ball_zero, hr, mem_univ, seminorm.zero,
     implies_true_iff, preimage_const_of_mem, zero_smul],
 end
 
 /-- The `module_filter_basis` induced by the filter basis `seminorm_basis_zero`. -/
-def seminorm_module_filter_basis (p : ι → seminorm 𝕜 E) : module_filter_basis 𝕜 E :=
-{ to_add_group_filter_basis := seminorm_add_group_filter_basis p,
-  smul' := seminorm_basis_zero_smul p,
-  smul_left' := seminorm_basis_zero_smul_left p,
-  smul_right' := seminorm_basis_zero_smul_right p }
+protected def module_filter_basis : module_filter_basis 𝕜 E :=
+{ to_add_group_filter_basis := p.add_group_filter_basis,
+  smul' := p.basis_sets_smul,
+  smul_left' := p.basis_sets_smul_left,
+  smul_right' := p.basis_sets_smul_right }
+
+end seminorm_family
 
 end filter_basis
 
@@ -174,6 +181,8 @@ namespace seminorm
 
 variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [add_comm_group F] [module 𝕜 F]
 
+-- Todo: This should be phrased entirely in terms of the von Neumann bornology.
+
 /-- The proposition that a linear map is bounded between spaces with families of seminorms. -/
 def is_bounded (p : ι → seminorm 𝕜 E) (q : ι' → seminorm 𝕜 F) (f : E →ₗ[𝕜] F) : Prop :=
   ∀ i, ∃ s : finset ι, ∃ C : ℝ≥0, C ≠ 0 ∧ (q i).comp f ≤ C • s.sup p
@@ -187,12 +196,9 @@ lemma const_is_bounded (ι : Type*) [nonempty ι]
   {p : seminorm 𝕜 E} {q : ι' → seminorm 𝕜 F} (f : E →ₗ[𝕜] F) :
   is_bounded (λ _ : ι, p) q f ↔ ∀ i, ∃ C : ℝ≥0, C ≠ 0 ∧ (q i).comp f ≤ C • p :=
 begin
-  dunfold is_bounded,
-  split,
-  { intros h i,
-    rcases h i with ⟨s, C, hC, h⟩,
+  split; intros h i,
+  { rcases h i with ⟨s, C, hC, h⟩,
     exact ⟨C, hC, le_trans h (smul_le_smul (finset.sup_le (λ _ _, le_rfl)) le_rfl)⟩ },
-  intros h i,
   use [{classical.arbitrary ι}],
   simp only [h, finset.sup_singleton],
 end
@@ -220,7 +226,7 @@ begin
     exact finset.sup_mono (finset.subset_bUnion_of_mem fₛ hi),
   end,
   refine le_trans (comp_mono f (finset_sup_le_sum q s')) _,
-  simp_rw [←pullback_apply, add_monoid_hom.map_sum, pullback_apply], --improve this
+  simp_rw [←pullback_apply, add_monoid_hom.map_sum, pullback_apply],
   refine le_trans (finset.sum_le_sum hs) _,
   rw [finset.sum_const, smul_assoc],
   exact le_rfl,
@@ -235,11 +241,12 @@ section topology
 variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [nonempty ι]
 
 /-- The proposition that the topology of `E` is induced by a family of seminorms `p`. -/
-class with_seminorms (p : ι → seminorm 𝕜 E) [t : topological_space E] : Prop :=
-(topology_eq_with_seminorms : t = (seminorm_module_filter_basis p).topology)
+class with_seminorms (p : seminorm_family 𝕜 E ι) [t : topological_space E] : Prop :=
+(topology_eq_with_seminorms : t = p.module_filter_basis.topology)
 
-lemma with_seminorms_eq (p : ι → seminorm 𝕜 E) [t : topological_space E] [with_seminorms p] :
-  t = ((seminorm_module_filter_basis p).topology) := with_seminorms.topology_eq_with_seminorms
+lemma seminorm_family.with_seminorms_eq (p : seminorm_family 𝕜 E ι) [t : topological_space E]
+  [with_seminorms p] : t = p.module_filter_basis.topology :=
+with_seminorms.topology_eq_with_seminorms
 
 end topology
 
@@ -249,21 +256,21 @@ variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E]
 variables [topological_space E] [topological_add_group E]
 variables [nonempty ι]
 
-lemma with_seminorms_of_nhds (p : ι → seminorm 𝕜 E)
-  (h : 𝓝 (0 : E) = (seminorm_module_filter_basis p).to_filter_basis.filter) :
+lemma seminorm_family.with_seminorms_of_nhds (p : seminorm_family 𝕜 E ι)
+  (h : 𝓝 (0 : E) = p.module_filter_basis.to_filter_basis.filter) :
   with_seminorms p :=
 begin
   refine ⟨topological_add_group.ext (by apply_instance)
-    ((seminorm_add_group_filter_basis _).is_topological_add_group) _⟩,
+    (p.add_group_filter_basis.is_topological_add_group) _⟩,
   rw add_group_filter_basis.nhds_zero_eq,
   exact h,
 end
 
-lemma with_seminorms_of_has_basis (p : ι → seminorm 𝕜 E) (h : (𝓝 (0 : E)).has_basis
-  (λ (s : set E), s ∈ (seminorm_basis_zero p)) id) :
+lemma seminorm_family.with_seminorms_of_has_basis (p : seminorm_family 𝕜 E ι)
+  (h : (𝓝 (0 : E)).has_basis (λ (s : set E), s ∈ p.basis_sets) id) :
   with_seminorms p :=
-with_seminorms_of_nhds p $ filter.has_basis.eq_of_same_basis h
-  ((seminorm_add_group_filter_basis p).to_filter_basis.has_basis)
+p.with_seminorms_of_nhds $ filter.has_basis.eq_of_same_basis h
+  p.add_group_filter_basis.to_filter_basis.has_basis
 
 end topological_add_group
 
@@ -273,15 +280,15 @@ section normed_space
 instance norm_with_seminorms (𝕜 E) [normed_field 𝕜] [semi_normed_group E] [normed_space 𝕜 E] :
   with_seminorms (λ (_ : fin 1), norm_seminorm 𝕜 E) :=
 begin
-  let p := λ _ : fin 1, norm_seminorm 𝕜 E,
+  let p : seminorm_family 𝕜 E (fin 1) := λ _, norm_seminorm 𝕜 E,
   refine ⟨topological_add_group.ext normed_top_group
-    ((seminorm_add_group_filter_basis _).is_topological_add_group) _⟩,
+    (p.add_group_filter_basis.is_topological_add_group) _⟩,
   refine filter.has_basis.eq_of_same_basis metric.nhds_basis_ball _,
   rw ←ball_norm_seminorm 𝕜 E,
-  refine filter.has_basis.to_has_basis (seminorm_add_group_filter_basis p).nhds_zero_has_basis _
-    (λ r hr, ⟨(norm_seminorm 𝕜 E).ball 0 r, seminorm_basis_zero_singleton_mem p 0 hr, rfl.subset⟩),
-  rintros U (hU : U ∈ seminorm_basis_zero p),
-  rcases (seminorm_basis_zero_iff p U).mp hU with ⟨s, r, hr, hU⟩,
+  refine filter.has_basis.to_has_basis p.add_group_filter_basis.nhds_zero_has_basis _
+    (λ r hr, ⟨(norm_seminorm 𝕜 E).ball 0 r, p.basis_sets_singleton_mem 0 hr, rfl.subset⟩),
+  rintros U (hU : U ∈ p.basis_sets),
+  rcases (p.basis_sets_iff U).mp hU with ⟨s, r, hr, hU⟩,
   use [r, hr],
   rw [hU, id.def],
   by_cases h : s.nonempty,
@@ -299,23 +306,22 @@ namespace seminorm
 variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [add_comm_group F] [module 𝕜 F]
 variables [nonempty ι] [nonempty ι']
 
-lemma continuous_from_bounded (p : ι → seminorm 𝕜 E) (q : ι' → seminorm 𝕜 F)
+lemma continuous_from_bounded (p : seminorm_family 𝕜 E ι) (q : seminorm_family 𝕜 F ι')
   [uniform_space E] [uniform_add_group E] [with_seminorms p]
   [uniform_space F] [uniform_add_group F] [with_seminorms q]
   (f : E →ₗ[𝕜] F) (hf : seminorm.is_bounded p q f) : continuous f :=
 begin
   refine uniform_continuous.continuous _,
   refine add_monoid_hom.uniform_continuous_of_continuous_at_zero f.to_add_monoid_hom _,
-  rw [f.to_add_monoid_hom_coe, continuous_at_def, f.map_zero, with_seminorms_eq p],
+  rw [f.to_add_monoid_hom_coe, continuous_at_def, f.map_zero, p.with_seminorms_eq],
   intros U hU,
-  rw [with_seminorms_eq q, add_group_filter_basis.nhds_zero_eq, filter_basis.mem_filter_iff] at hU,
-  rcases hU with ⟨V, hV : V ∈ seminorm_basis_zero q, hU⟩,
-  rcases (seminorm_basis_zero_iff q V).mp hV with ⟨s₂, r, hr, hV⟩,
+  rw [q.with_seminorms_eq, add_group_filter_basis.nhds_zero_eq, filter_basis.mem_filter_iff] at hU,
+  rcases hU with ⟨V, hV : V ∈ q.basis_sets, hU⟩,
+  rcases (q.basis_sets_iff V).mp hV with ⟨s₂, r, hr, hV⟩,
   rw hV at hU,
-  rw [(seminorm_add_group_filter_basis p).nhds_zero_eq, filter_basis.mem_filter_iff],
+  rw [p.add_group_filter_basis.nhds_zero_eq, filter_basis.mem_filter_iff],
   rcases (seminorm.is_bounded_sup hf s₂) with ⟨C, s₁, hC, hf⟩,
-  refine ⟨(s₁.sup p).ball 0 (r/C),
-    seminorm_basis_zero_mem p _ (div_pos hr (nnreal.coe_pos.mpr hC)), _⟩,
+  refine ⟨(s₁.sup p).ball 0 (r/C), p.basis_sets_mem _ (div_pos hr (nnreal.coe_pos.mpr hC)), _⟩,
   refine subset.trans _ (preimage_mono hU),
   simp_rw [←linear_map.map_zero f, ←ball_comp],
   refine subset.trans _ (ball_antitone hf),
@@ -353,11 +359,11 @@ variables [nonempty ι] [normed_field 𝕜] [normed_space ℝ 𝕜]
   [add_comm_group E] [module 𝕜 E] [module ℝ E] [is_scalar_tower ℝ 𝕜 E] [topological_space E]
   [topological_add_group E]
 
-lemma with_seminorms.to_locally_convex_space (p : ι → seminorm 𝕜 E) [with_seminorms p] :
+lemma seminorm_family.to_locally_convex_space (p : seminorm_family 𝕜 E ι) [with_seminorms p] :
   locally_convex_space ℝ E :=
 begin
-  apply of_basis_zero ℝ E id (λ s, s ∈ seminorm_basis_zero p),
-  { rw [with_seminorms_eq p, add_group_filter_basis.nhds_eq _, add_group_filter_basis.N_zero],
+  apply of_basis_zero ℝ E id (λ s, s ∈ p.basis_sets),
+  { rw [p.with_seminorms_eq, add_group_filter_basis.nhds_eq _, add_group_filter_basis.N_zero],
     exact filter_basis.has_basis _ },
   { intros s hs,
     change s ∈ set.Union _ at hs,
@@ -376,7 +382,7 @@ variables (𝕜) [normed_field 𝕜] [normed_space ℝ 𝕜] [semi_normed_group
 slightly weaker instance version. -/
 lemma normed_space.to_locally_convex_space' [normed_space 𝕜 E] [module ℝ E]
   [is_scalar_tower ℝ 𝕜 E] : locally_convex_space ℝ E :=
-with_seminorms.to_locally_convex_space (λ _ : fin 1, norm_seminorm 𝕜 E)
+seminorm_family.to_locally_convex_space (λ _ : fin 1, norm_seminorm 𝕜 E)
 
 /-- See `normed_space.to_locally_convex_space'` for a slightly stronger version which is not an
 instance. -/