𝕜 : Type u_1
𝕜₂ : Type ?u.189437
𝕝 : Type ?u.189440
𝕝₂ : Type ?u.189443
E : Type u_2
F : Type ?u.189449
G : Type ?u.189452
ι : Type u_3
ι' : Type ?u.189458
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : TopologicalAddGroup E
⊢ Filter.HasBasis (𝓝 x) (fun sr => 0 < sr.snd) fun sr => ball (Finset.sup sr.fst p) x sr.snd
𝕜 : Type u_1
𝕜₂ : Type ?u.189437
𝕝 : Type ?u.189440
𝕝₂ : Type ?u.189443
E : Type u_2
F : Type ?u.189449
G : Type ?u.189452
ι : Type u_3
ι' : Type ?u.189458
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
⊢ Filter.HasBasis (𝓝 x) (fun sr => 0 < sr.snd) fun sr => ball (Finset.sup sr.fst p) x sr.snd
haveI : TopologicalAddGroup E := hp.topologicalAddGroup
𝕜 : Type u_1
𝕜₂ : Type ?u.189437
𝕝 : Type ?u.189440
𝕝₂ : Type ?u.189443
E : Type u_2
F : Type ?u.189449
G : Type ?u.189452
ι : Type u_3
ι' : Type ?u.189458
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : TopologicalAddGroup E
⊢ Filter.HasBasis (Filter.map ((fun x x_1 => x + x_1) x) (𝓝 0)) (fun sr => 0 < sr.snd) fun sr =>
    ball (Finset.sup sr.fst p) x sr.snd
𝕜 : Type u_1
𝕜₂ : Type ?u.189437
𝕝 : Type ?u.189440
𝕝₂ : Type ?u.189443
E : Type u_2
F : Type ?u.189449
G : Type ?u.189452
ι : Type u_3
ι' : Type ?u.189458
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : TopologicalAddGroup E
⊢ Filter.HasBasis (𝓝 x) (fun sr => 0 < sr.snd) fun sr => ball (Finset.sup sr.fst p) x sr.snd
rw [← map_add_left_nhds_zero]
case h.e'_5.h
𝕜 : Type u_1
𝕜₂ : Type ?u.189437
𝕝 : Type ?u.189440
𝕝₂ : Type ?u.189443
E : Type u_2
F : Type ?u.189449
G : Type ?u.189452
ι : Type u_3
ι' : Type ?u.189458
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : TopologicalAddGroup E
sr : Finset ι × ℝ
⊢ ball (Finset.sup sr.fst p) x sr.snd = (fun x x_1 => x + x_1) x '' ball (Finset.sup sr.fst p) 0 sr.snd
case h.e'_5
𝕜 : Type u_1
𝕜₂ : Type ?u.189437
𝕝 : Type ?u.189440
𝕝₂ : Type ?u.189443
E : Type u_2
F : Type ?u.189449
G : Type ?u.189452
ι : Type u_3
ι' : Type ?u.189458
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : TopologicalAddGroup E
⊢ (fun sr => ball (Finset.sup sr.fst p) x sr.snd) = fun i =>
    (fun x x_1 => x + x_1) x '' ball (Finset.sup i.fst p) 0 i.snd
ext sr : 1
case h.e'_5.h
𝕜 : Type u_1
𝕜₂ : Type ?u.189437
𝕝 : Type ?u.189440
𝕝₂ : Type ?u.189443
E : Type u_2
F : Type ?u.189449
G : Type ?u.189452
ι : Type u_3
ι' : Type ?u.189458
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this✝ : TopologicalAddGroup E
sr : Finset ι × ℝ
this : ball (Finset.sup sr.fst p) (x +ᵥ 0) sr.snd = x +ᵥ ball (Finset.sup sr.fst p) 0 sr.snd
⊢ ball (Finset.sup sr.fst p) x sr.snd = (fun x x_1 => x + x_1) x '' ball (Finset.sup sr.fst p) 0 sr.snd
case h.e'_5.h
𝕜 : Type u_1
𝕜₂ : Type ?u.189437
𝕝 : Type ?u.189440
𝕝₂ : Type ?u.189443
E : Type u_2
F : Type ?u.189449
G : Type ?u.189452
ι : Type u_3
ι' : Type ?u.189458
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : TopologicalAddGroup E
sr : Finset ι × ℝ
⊢ ball (Finset.sup sr.fst p) x sr.snd = (fun x x_1 => x + x_1) x '' ball (Finset.sup sr.fst p) 0 sr.snd
have : (sr.fst.sup p).ball (x +ᵥ (0 : E)) sr.snd = x +ᵥ (sr.fst.sup p).ball 0 sr.snd :=
  Eq.symm (Seminorm.vadd_ball (sr.fst.sup p))
no goals
case h.e'_5.h
𝕜 : Type u_1
𝕜₂ : Type ?u.189437
𝕝 : Type ?u.189440
𝕝₂ : Type ?u.189443
E : Type u_2
F : Type ?u.189449
G : Type ?u.189452
ι : Type u_3
ι' : Type ?u.189458
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this✝ : TopologicalAddGroup E
sr : Finset ι × ℝ
this : ball (Finset.sup sr.fst p) (x +ᵥ 0) sr.snd = x +ᵥ ball (Finset.sup sr.fst p) 0 sr.snd
⊢ ball (Finset.sup sr.fst p) x sr.snd = (fun x x_1 => x + x_1) x '' ball (Finset.sup sr.fst p) 0 sr.snd
rwa [vadd_eq_add, add_zero] at this