-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
/-- Let `E` be a topological vector space (over a `NontriviallyNormedField`) whose topology is
generated by some family of seminorms `p`, and let `q` be a seminorm on `E`. If `q` is continuous,
then it is uniformly controlled by *finitely many* seminorms of `p`, that is there
is some finset `s` of the index set and some `C > 0` such that `q ≤ C • s.sup p`. -/
lemma bound_of_continuous [Nonempty ι] [t : TopologicalSpace E] (hp : WithSeminorms p)
    (q : Seminorm 𝕜 E) (hq : Continuous q) :
    ∃ s : Finset ι, ∃ C : ℝ≥0, C ≠ 0 ∧ q ≤ C • s.sup p

Proof state:
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x✝ : NormedSpace 𝕜 E := NormedSpace.mk ⋯
this : Continuous ⇑q
C : ℝ
C_pos : 0 < C
hC : ∀ (x : E), q x ≤ C * ‖x‖
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
exact ⟨s, ⟨C, C_pos.le⟩, fun H ↦ C_pos.ne.symm (congr_arg NNReal.toReal H), hC⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
let _ : NormedSpace 𝕜 E := { norm_smul_le := fun a b ↦ le_of_eq (map_smul_eq_mul (s.sup p) a b) }

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x✝ : NormedSpace 𝕜 E := NormedSpace.mk ⋯
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
t : TopologicalSpace E
hp : WithSeminorms p
q : Seminorm 𝕜 E
hq : Continuous ⇑q
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
clear hp hq t

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x✝ : NormedSpace 𝕜 E := NormedSpace.mk ⋯
this : Continuous ⇑q
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
rcases bound_of_continuous_normedSpace q this with ⟨C, C_pos, hC⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x✝ : NormedSpace 𝕜 E := NormedSpace.mk ⋯
this : Continuous ⇑q
C : ℝ
C_pos : 0 < C
hC : ∀ (x : E), q x ≤ C * ‖x‖
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
t : TopologicalSpace E
hp : WithSeminorms p
q : Seminorm 𝕜 E
hq : Continuous ⇑q
V : Set E
hV : V ∈ p.basisSets
hε : id V ⊆ q.ball 0 1
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
rcases p.basisSets_iff.mp hV with ⟨s, ε, ε_pos, rfl⟩

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
t : TopologicalSpace E
hp : WithSeminorms p
q : Seminorm 𝕜 E
hq : Continuous ⇑q
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
t : TopologicalSpace E
hp : WithSeminorms p
q : Seminorm 𝕜 E
hq : Continuous ⇑q
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
rcases hp.hasBasis.mem_iff.mp (ball_mem_nhds hq one_pos) with ⟨V, hV, hε⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
t : TopologicalSpace E
hp : WithSeminorms p
q : Seminorm 𝕜 E
hq : Continuous ⇑q
V : Set E
hV : V ∈ p.basisSets
hε : id V ⊆ q.ball 0 1
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x✝ : NormedSpace 𝕜 E := NormedSpace.mk ⋯
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
have : Continuous q :=
  Seminorm.continuous (r := 1) (mem_of_superset (Metric.ball_mem_nhds _ ε_pos) hε)

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
x✝ : NormedSpace 𝕜 E := NormedSpace.mk ⋯
this : Continuous ⇑q
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p

Tactic:
let _ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
inst✝ : Nonempty ι
q : Seminorm 𝕜 E
s : Finset ι
ε : ℝ
ε_pos : 0 < ε
hV : (s.sup p).ball 0 ε ∈ p.basisSets
hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1
x✝ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup
⊢ ∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p