-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.hasBasis_ball (hp : WithSeminorms p) {x : E} :
    (𝓝 (x : E)).HasBasis
    (fun sr : Finset ι × ℝ => 0 < sr.2) fun sr => (sr.1.sup p).ball x sr.2

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
⊢ (𝓝 x).HasBasis (fun sr => 0 < sr.2) fun sr => (sr.1.sup p).ball x sr.2

Tactic:
have : IsTopologicalAddGroup E := hp.topologicalAddGroup

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
⊢ (𝓝 x).HasBasis (fun sr => 0 < sr.2) fun sr => (sr.1.sup p).ball x sr.2

Proof state:
case h.e'_5.h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
sr : Finset ι × ℝ
⊢ (sr.1.sup p).ball x sr.2 = (fun x_1 => x + x_1) '' (sr.1.sup p).ball 0 sr.2

Tactic:
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))

Result:
case h.e'_5.h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this✝ : IsTopologicalAddGroup E
sr : Finset ι × ℝ
this : (sr.1.sup p).ball (x +ᵥ 0) sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2
⊢ (sr.1.sup p).ball x sr.2 = (fun x_1 => x + x_1) '' (sr.1.sup p).ball 0 sr.2

Proof state:
case h.e'_5
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
⊢ (fun sr => (sr.1.sup p).ball x sr.2) = fun i => (fun x_1 => x + x_1) '' (i.1.sup p).ball 0 i.2

Tactic:
ext sr : 1

Result:
case h.e'_5.h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
sr : Finset ι × ℝ
⊢ (sr.1.sup p).ball x sr.2 = (fun x_1 => x + x_1) '' (sr.1.sup p).ball 0 sr.2

Proof state:
case h.e'_5.h
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this✝ : IsTopologicalAddGroup E
sr : Finset ι × ℝ
this : (sr.1.sup p).ball (x +ᵥ 0) sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2
⊢ (sr.1.sup p).ball x sr.2 = (fun x_1 => x + x_1) '' (sr.1.sup p).ball 0 sr.2

Tactic:
rwa [vadd_eq_add, add_zero] at this

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
⊢ (𝓝 x).HasBasis (fun sr => 0 < sr.2) fun sr => (sr.1.sup p).ball x sr.2

Tactic:
rw [← map_add_left_nhds_zero]

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
this : IsTopologicalAddGroup E
⊢ (Filter.map (fun x_1 => x + x_1) (𝓝 0)).HasBasis (fun sr => 0 < sr.2) fun sr => (sr.1.sup p).ball x sr.2