-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
/-- If a family of seminorms is continuous, then their basis sets are neighborhoods of zero. -/
lemma basisSets_mem_nhds {𝕜 E ι : Type*} [NormedField 𝕜]
    [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (p : SeminormFamily 𝕜 E ι)
    (hp : ∀ i, Continuous (p i)) (U : Set E) (hU : U ∈ p.basisSets) : U ∈ 𝓝 (0 : E)

Proof state:
case intro.intro.intro.insert
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
r : ℝ
hr : 0 < r
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : Continuous ⇑(s✝.sup p)
⊢ Continuous ⇑((insert a✝² s✝).sup p)

Tactic:
case insert a s _ hs =>
  simp only [Finset.sup_insert, coe_sup]
  exact Continuous.max (hp a) hs

Result:
no goals

Proof state:
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
U : Set E
hU : U ∈ p.basisSets
⊢ U ∈ 𝓝 0

Tactic:
obtain ⟨s, r, hr, rfl⟩ := p.basisSets_iff.mp hU

Result:
case intro.intro.intro
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
⊢ (s.sup p).ball 0 r ∈ 𝓝 0

Proof state:
case intro.intro.intro
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
s : Finset ι
r : ℝ
hr : 0 < r
⊢ Continuous ⇑(s.sup p)

Tactic:
classical
induction s using Finset.induction_on
case empty => simpa using continuous_zero
case insert a s _ hs =>
  simp only [Finset.sup_insert, coe_sup]
  exact Continuous.max (hp a) hs

Result:
no goals

Proof state:
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
r : ℝ
hr : 0 < r
a : ι
s : Finset ι
a✝ : a ∉ s
hs : Continuous ⇑(s.sup p)
⊢ Continuous (⇑(p a) ⊔ ⇑(s.sup p))

Tactic:
exact Continuous.max (hp a) hs

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
s : Finset ι
r : ℝ
hr : 0 < r
⊢ Continuous ⇑(s.sup p)

Tactic:
induction s using Finset.induction_on

Result:
case intro.intro.intro.empty
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
r : ℝ
hr : 0 < r
⊢ Continuous ⇑(∅.sup p)

case intro.intro.intro.insert
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
r : ℝ
hr : 0 < r
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : Continuous ⇑(s✝.sup p)
⊢ Continuous ⇑((insert a✝² s✝).sup p)

Proof state:
case intro.intro.intro.empty
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
r : ℝ
hr : 0 < r
⊢ Continuous ⇑(∅.sup p)

case intro.intro.intro.insert
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
r : ℝ
hr : 0 < r
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : Continuous ⇑(s✝.sup p)
⊢ Continuous ⇑((insert a✝² s✝).sup p)

Tactic:
case empty => simpa using continuous_zero

Result:
case intro.intro.intro.insert
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
r : ℝ
hr : 0 < r
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : Continuous ⇑(s✝.sup p)
⊢ Continuous ⇑((insert a✝² s✝).sup p)

Proof state:
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
r : ℝ
hr : 0 < r
a : ι
s : Finset ι
a✝ : a ∉ s
hs : Continuous ⇑(s.sup p)
⊢ Continuous ⇑((insert a s).sup p)

Tactic:
simp only [Finset.sup_insert, coe_sup]

Result:
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
r : ℝ
hr : 0 < r
a : ι
s : Finset ι
a✝ : a ∉ s
hs : Continuous ⇑(s.sup p)
⊢ Continuous (⇑(p a) ⊔ ⇑(s.sup p))

Proof state:
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
r : ℝ
hr : 0 < r
⊢ Continuous ⇑(∅.sup p)

Tactic:
simpa using continuous_zero

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
s : Finset ι
r : ℝ
hr : 0 < r
⊢ (s.sup p).ball 0 r ∈ 𝓝 0

Tactic:
refine Seminorm.ball_mem_nhds ?_ hr

Result:
case intro.intro.intro
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
s : Finset ι
r : ℝ
hr : 0 < r
⊢ Continuous ⇑(s.sup p)

Proof state:
case intro.intro.intro
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
s : Finset ι
r : ℝ
hr : 0 < r
hU : (s.sup p).ball 0 r ∈ p.basisSets
⊢ (s.sup p).ball 0 r ∈ 𝓝 0

Tactic:
clear hU

Result:
case intro.intro.intro
𝕜 : Type u_10
E : Type u_11
ι : Type u_12
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : ∀ (i : ι), Continuous ⇑(p i)
s : Finset ι
r : ℝ
hr : 0 < r
⊢ (s.sup p).ball 0 r ∈ 𝓝 0