chore(analysis/locally_convex/with_seminorms): fix namespaces for dot-notation (#16771)

Some lemmas where in the wrong namespaces.

Author: mcdoll

src/analysis/locally_convex/weak_dual.lean

@@ -135,6 +135,6 @@ variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [add_comm_group
 variables [nonempty ι] [normed_space ℝ 𝕜] [module ℝ E] [is_scalar_tower ℝ 𝕜 E]
 
 instance {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} : locally_convex_space ℝ (weak_bilin B) :=
-seminorm_family.to_locally_convex_space (B.weak_bilin_with_seminorms)
+(B.weak_bilin_with_seminorms).to_locally_convex_space
 
 end locally_convex

src/analysis/locally_convex/with_seminorms.lean

@@ -271,7 +271,7 @@ variables [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [nonempty ι]
 structure with_seminorms (p : seminorm_family 𝕜 E ι) [t : topological_space E] : Prop :=
 (topology_eq_with_seminorms : t = p.module_filter_basis.topology)
 
-lemma seminorm_family.with_seminorms_eq {p : seminorm_family 𝕜 E ι} [t : topological_space E]
+lemma with_seminorms.with_seminorms_eq {p : seminorm_family 𝕜 E ι} [t : topological_space E]
   (hp : with_seminorms p) : t = p.module_filter_basis.topology := hp.1
 
 variables [topological_space E]
@@ -493,7 +493,7 @@ 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 seminorm_family.to_locally_convex_space {p : seminorm_family 𝕜 E ι} (hp : with_seminorms p) :
+lemma with_seminorms.to_locally_convex_space {p : seminorm_family 𝕜 E ι} (hp : with_seminorms p) :
   locally_convex_space ℝ E :=
 begin
   apply of_basis_zero ℝ E id (λ s, s ∈ p.basis_sets),
@@ -516,7 +516,7 @@ variables (𝕜) [normed_field 𝕜] [normed_space ℝ 𝕜] [seminormed_add_com
 slightly weaker instance version. -/
 lemma normed_space.to_locally_convex_space' [normed_space 𝕜 E] [module ℝ E]
   [is_scalar_tower ℝ 𝕜 E] : locally_convex_space ℝ E :=
-seminorm_family.to_locally_convex_space (norm_with_seminorms 𝕜 E)
+(norm_with_seminorms 𝕜 E).to_locally_convex_space
 
 /-- See `normed_space.to_locally_convex_space'` for a slightly stronger version which is not an
 instance. -/

src/analysis/schwartz_space.lean

@@ -22,7 +22,7 @@ natural numbers `k` and `n` we have uniform bounds `∥x∥^k * ∥iterated_fder
 This approach completely avoids using partial derivatives as well as polynomials.
 We construct the topology on the Schwartz space by a family of seminorms, which are the best
 constants in the above estimates, which is by abstract theory from
-`seminorm_family.module_filter_basis` and `seminorm_family.to_locally_convex_space` turns the
+`seminorm_family.module_filter_basis` and `with_seminorms.to_locally_convex_space` turns the
 Schwartz space into a locally convex topological vector space.
 
 ## Main definitions
@@ -375,22 +375,21 @@ variables {𝕜 E F}
 
 instance : has_continuous_smul 𝕜 𝓢(E, F) :=
 begin
-  rw seminorm_family.with_seminorms_eq (schwartz_with_seminorms 𝕜 E F),
+  rw (schwartz_with_seminorms 𝕜 E F).with_seminorms_eq,
   exact (schwartz_seminorm_family 𝕜 E F).module_filter_basis.has_continuous_smul,
 end
 
 instance : topological_add_group 𝓢(E, F) :=
-(schwartz_seminorm_family ℝ E F).module_filter_basis.to_add_group_filter_basis
-  .is_topological_add_group
+(schwartz_seminorm_family ℝ E F).add_group_filter_basis.is_topological_add_group
 
 instance : uniform_space 𝓢(E, F) :=
-(schwartz_seminorm_family ℝ E F).module_filter_basis.to_add_group_filter_basis.uniform_space
+(schwartz_seminorm_family ℝ E F).add_group_filter_basis.uniform_space
 
 instance : uniform_add_group 𝓢(E, F) :=
-(schwartz_seminorm_family ℝ E F).module_filter_basis.to_add_group_filter_basis.uniform_add_group
+(schwartz_seminorm_family ℝ E F).add_group_filter_basis.uniform_add_group
 
 instance : locally_convex_space ℝ 𝓢(E, F) :=
-seminorm_family.to_locally_convex_space (schwartz_with_seminorms ℝ E F)
+(schwartz_with_seminorms ℝ E F).to_locally_convex_space
 
 end topology