𝕜 : Type u_2
𝕜₂ : Type ?u.451403
𝕝 : Type ?u.451406
𝕝₂ : Type ?u.451409
E : Type u_1
F : Type ?u.451415
G : Type ?u.451418
ι : Type u_3
ι' : Type ?u.451424
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ (𝓝 0 = ⨅ (i : ι), Filter.comap (↑(p i)) (𝓝 0)) ↔ 𝓝 0 = ⨅ (i : ι), 𝓝 0
𝕜 : Type u_2
𝕜₂ : Type ?u.451403
𝕝 : Type ?u.451406
𝕝₂ : Type ?u.451409
E : Type u_1
F : Type ?u.451415
G : Type ?u.451418
ι : Type u_3
ι' : Type ?u.451424
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ u = ⨅ (i : ι), PseudoMetricSpace.toUniformSpace
rw [p.withSeminorms_iff_nhds_eq_iInf,
  UniformAddGroup.ext_iff inferInstance (uniformAddGroup_iInf fun i => inferInstance),
  toTopologicalSpace_iInf, nhds_iInf]
𝕜 : Type u_2
𝕜₂ : Type ?u.451403
𝕝 : Type ?u.451406
𝕝₂ : Type ?u.451409
E : Type u_1
F : Type ?u.451415
G : Type ?u.451418
ι : Type u_3
ι' : Type ?u.451424
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ (𝓝 0 = ⨅ (i : ι), Filter.comap (↑(p i)) (𝓝 0)) = (𝓝 0 = ⨅ (i : ι), 𝓝 0)
𝕜 : Type u_2
𝕜₂ : Type ?u.451403
𝕝 : Type ?u.451406
𝕝₂ : Type ?u.451409
E : Type u_1
F : Type ?u.451415
G : Type ?u.451418
ι : Type u_3
ι' : Type ?u.451424
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ (𝓝 0 = ⨅ (i : ι), Filter.comap (↑(p i)) (𝓝 0)) ↔ 𝓝 0 = ⨅ (i : ι), 𝓝 0
refine Eq.to_iff ?_
case e_a.e_s
𝕜 : Type u_2
𝕜₂ : Type ?u.451403
𝕝 : Type ?u.451406
𝕝₂ : Type ?u.451409
E : Type u_1
F : Type ?u.451415
G : Type ?u.451418
ι : Type u_3
ι' : Type ?u.451424
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ (fun i => Filter.comap (↑(p i)) (𝓝 0)) = fun i => 𝓝 0
𝕜 : Type u_2
𝕜₂ : Type ?u.451403
𝕝 : Type ?u.451406
𝕝₂ : Type ?u.451409
E : Type u_1
F : Type ?u.451415
G : Type ?u.451418
ι : Type u_3
ι' : Type ?u.451424
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ (𝓝 0 = ⨅ (i : ι), Filter.comap (↑(p i)) (𝓝 0)) = (𝓝 0 = ⨅ (i : ι), 𝓝 0)
congr
case e_a.e_s.h
𝕜 : Type u_2
𝕜₂ : Type ?u.451403
𝕝 : Type ?u.451406
𝕝₂ : Type ?u.451409
E : Type u_1
F : Type ?u.451415
G : Type ?u.451418
ι : Type u_3
ι' : Type ?u.451424
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ Filter.comap (↑(p i)) (𝓝 0) = 𝓝 0
case e_a.e_s
𝕜 : Type u_2
𝕜₂ : Type ?u.451403
𝕝 : Type ?u.451406
𝕝₂ : Type ?u.451409
E : Type u_1
F : Type ?u.451415
G : Type ?u.451418
ι : Type u_3
ι' : Type ?u.451424
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ (fun i => Filter.comap (↑(p i)) (𝓝 0)) = fun i => 𝓝 0
funext i
no goals
case e_a.e_s.h
𝕜 : Type u_2
𝕜₂ : Type ?u.451403
𝕝 : Type ?u.451406
𝕝₂ : Type ?u.451409
E : Type u_1
F : Type ?u.451415
G : Type ?u.451418
ι : Type u_3
ι' : Type ?u.451424
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ Filter.comap (↑(p i)) (𝓝 0) = 𝓝 0
exact @comap_norm_nhds_zero _ (p i).toAddGroupSeminorm.toSeminormedAddGroup