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

Proof state:
case mpr.intro.intro.intro
𝕜 : 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
V : Set E
s : Finset ι
r : ℝ
hr : 0 < r
hV : (s.sup p).ball 0 r ⊆ V
⊢ ∃ i, (∃ i_1 r, 0 < r ∧ i = (i_1.sup p).ball 0 r) ∧ id i ⊆ V

Tactic:
exact ⟨_, ⟨s, r, hr, rfl⟩, hV⟩

Result:
no goals

Proof state:
case mp
𝕜 : 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
V : Set E
⊢ (∃ i, (∃ i_1 r, 0 < r ∧ i = (i_1.sup p).ball 0 r) ∧ id i ⊆ V) → ∃ a b, 0 < b ∧ (a.sup p).ball 0 b ⊆ V

Tactic:
rintro ⟨-, ⟨s, r, hr, rfl⟩, hV⟩

Result:
case mp.intro.intro.intro.intro.intro
𝕜 : 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
V : Set E
s : Finset ι
r : ℝ
hr : 0 < r
hV : id ((s.sup p).ball 0 r) ⊆ V
⊢ ∃ a b, 0 < b ∧ (a.sup p).ball 0 b ⊆ V

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
⊢ (𝓝 0).HasBasis (fun sr => 0 < sr.2) fun sr => (sr.1.sup p).ball 0 sr.2

Tactic:
refine ⟨fun V => ?_⟩

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
V : Set E
⊢ V ∈ 𝓝 0 ↔ ∃ i, 0 < i.2 ∧ (i.1.sup p).ball 0 i.2 ⊆ V

Proof state:
case mpr
𝕜 : 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
V : Set E
⊢ (∃ a b, 0 < b ∧ (a.sup p).ball 0 b ⊆ V) → ∃ i, (∃ i_1 r, 0 < r ∧ i = (i_1.sup p).ball 0 r) ∧ id i ⊆ V

Tactic:
rintro ⟨s, r, hr, hV⟩

Result:
case mpr.intro.intro.intro
𝕜 : 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
V : Set E
s : Finset ι
r : ℝ
hr : 0 < r
hV : (s.sup p).ball 0 r ⊆ V
⊢ ∃ i, (∃ i_1 r, 0 < r ∧ i = (i_1.sup p).ball 0 r) ∧ id i ⊆ V

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
V : Set E
⊢ V ∈ 𝓝 0 ↔ ∃ i, 0 < i.2 ∧ (i.1.sup p).ball 0 i.2 ⊆ V

Tactic:
simp only [hp.hasBasis.mem_iff, SeminormFamily.basisSets_iff, Prod.exists]

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
V : Set E
⊢ (∃ i, (∃ i_1 r, 0 < r ∧ i = (i_1.sup p).ball 0 r) ∧ id i ⊆ V) ↔ ∃ a b, 0 < b ∧ (a.sup p).ball 0 b ⊆ V

Proof state:
case mp.intro.intro.intro.intro.intro
𝕜 : 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
V : Set E
s : Finset ι
r : ℝ
hr : 0 < r
hV : id ((s.sup p).ball 0 r) ⊆ V
⊢ ∃ a b, 0 < b ∧ (a.sup p).ball 0 b ⊆ V

Tactic:
exact ⟨s, r, hr, hV⟩

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
V : Set E
⊢ (∃ i, (∃ i_1 r, 0 < r ∧ i = (i_1.sup p).ball 0 r) ∧ id i ⊆ V) ↔ ∃ a b, 0 < b ∧ (a.sup p).ball 0 b ⊆ V

Tactic:
constructor

Result:
case mp
𝕜 : 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
V : Set E
⊢ (∃ i, (∃ i_1 r, 0 < r ∧ i = (i_1.sup p).ball 0 r) ∧ id i ⊆ V) → ∃ a b, 0 < b ∧ (a.sup p).ball 0 b ⊆ V

case mpr
𝕜 : 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
V : Set E
⊢ (∃ a b, 0 < b ∧ (a.sup p).ball 0 b ⊆ V) → ∃ i, (∃ i_1 r, 0 < r ∧ i = (i_1.sup p).ball 0 r) ∧ id i ⊆ V