-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem norm_withSeminorms (𝕜 E) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
    WithSeminorms fun _ : Fin 1 => normSeminorm 𝕜 E

Proof state:
case right
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (normSeminorm 𝕜 E).ball 0 r ⊆ id U

Tactic:
rw [hU, id]

Result:
case right
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (normSeminorm 𝕜 E).ball 0 r ⊆ (s.sup p).ball 0 r

Proof state:
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ (𝓝 0).HasBasis (fun x => 0 < x) (Metric.ball 0)

Tactic:
rw [← ball_normSeminorm 𝕜 E]

Result:
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ (𝓝 0).HasBasis (fun x => 0 < x) ((normSeminorm 𝕜 E).ball 0)

Proof state:
case neg
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : ¬s.Nonempty
⊢ (normSeminorm 𝕜 E).ball 0 r ⊆ (s.sup p).ball 0 r

Tactic:
rw [Finset.not_nonempty_iff_eq_empty.mp h, Finset.sup_empty, ball_bot _ hr]

Result:
case neg
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : ¬s.Nonempty
⊢ (normSeminorm 𝕜 E).ball 0 r ⊆ univ

Proof state:
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ WithSeminorms fun x => normSeminorm 𝕜 E

Tactic:
let p : SeminormFamily 𝕜 E (Fin 1) := fun _ => normSeminorm 𝕜 E

Result:
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ WithSeminorms fun x => normSeminorm 𝕜 E

Proof state:
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ ∀ i ∈ p.addGroupFilterBasis, ∃ i', 0 < i' ∧ (normSeminorm 𝕜 E).ball 0 i' ⊆ id i

Tactic:
rintro U (hU : U ∈ p.basisSets)

Result:
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU : U ∈ p.basisSets
⊢ ∃ i', 0 < i' ∧ (normSeminorm 𝕜 E).ball 0 i' ⊆ id U

Proof state:
case pos
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : s.Nonempty
⊢ (normSeminorm 𝕜 E).ball 0 r ⊆ (s.sup p).ball 0 r

Tactic:
rw [Finset.sup_const h]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : ¬s.Nonempty
⊢ (normSeminorm 𝕜 E).ball 0 r ⊆ univ

Tactic:
exact Set.subset_univ _

Result:
no goals

Proof state:
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ (𝓝 0).HasBasis (fun x => 0 < x) ((normSeminorm 𝕜 E).ball 0)

Tactic:
refine
  Filter.HasBasis.to_hasBasis p.addGroupFilterBasis.nhds_zero_hasBasis ?_ fun r hr =>
    ⟨(normSeminorm 𝕜 E).ball 0 r, p.basisSets_singleton_mem 0 hr, rfl.subset⟩

Result:
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ ∀ i ∈ p.addGroupFilterBasis, ∃ i', 0 < i' ∧ (normSeminorm 𝕜 E).ball 0 i' ⊆ id i

Proof state:
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ WithSeminorms fun x => normSeminorm 𝕜 E

Tactic:
refine
  ⟨SeminormedAddCommGroup.toIsTopologicalAddGroup.ext
      p.addGroupFilterBasis.isTopologicalAddGroup ?_⟩

Result:
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
⊢ 𝓝 0 = 𝓝 0

Proof state:
case intro.intro.intro
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ i', 0 < i' ∧ (normSeminorm 𝕜 E).ball 0 i' ⊆ id U

Tactic:
use r, hr

Result:
case right
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (normSeminorm 𝕜 E).ball 0 r ⊆ id U

Proof state:
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU : U ∈ p.basisSets
⊢ ∃ i', 0 < i' ∧ (normSeminorm 𝕜 E).ball 0 i' ⊆ id U

Tactic:
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩

Result:
case intro.intro.intro
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ ∃ i', 0 < i' ∧ (normSeminorm 𝕜 E).ball 0 i' ⊆ id U

Proof state:
case right
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
⊢ (normSeminorm 𝕜 E).ball 0 r ⊆ (s.sup p).ball 0 r

Tactic:
by_cases h : s.Nonempty

Result:
case pos
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : s.Nonempty
⊢ (normSeminorm 𝕜 E).ball 0 r ⊆ (s.sup p).ball 0 r

case neg
𝕜 : Type u_10
E : Type u_11
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : SeminormFamily 𝕜 E (Fin 1) := fun x => normSeminorm 𝕜 E
U : Set E
hU✝ : U ∈ p.basisSets
s : Finset (Fin 1)
r : ℝ
hr : 0 < r
hU : U = (s.sup p).ball 0 r
h : ¬s.Nonempty
⊢ (normSeminorm 𝕜 E).ball 0 r ⊆ (s.sup p).ball 0 r