-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.isVonNBounded_iff_seminorm_bounded {s : Set E} (hp : WithSeminorms p) :
    Bornology.IsVonNBounded 𝕜 s ↔ ∀ i : ι, ∃ r > 0, ∀ x ∈ s, p i x < r

Proof state:
case neg
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r
I : Finset ι
hI : ¬I.Nonempty
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
simp only [Finset.not_nonempty_iff_eq_empty.mp hI, Finset.sup_empty, coe_bot, Pi.zero_apply,
  exists_prop]

Result:
case neg
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r
I : Finset ι
hI : ¬I.Nonempty
⊢ ∃ r > 0, ∀ x ∈ s, 0 < r

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r

Tactic:
rw [hp.isVonNBounded_iff_finset_seminorm_bounded]

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r) ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r) ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r) → ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r

case mpr
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
⊢ (∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r) → ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Proof state:
case intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
i : ι
hi : i ∈ I
⊢ 0 < I.sup' ⋯ r

Tactic:
exact lt_of_lt_of_le (hr i) (Finset.le_sup' r hi)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
⊢ 0 < I.sup' hI r

Tactic:
rcases hI with ⟨i, hi⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
i : ι
hi : i ∈ I
⊢ 0 < I.sup' ⋯ r

Proof state:
case pos
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r
I : Finset ι
hI : I.Nonempty
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
choose r hr h using hi

Result:
case pos
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Proof state:
case pos
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
h' : 0 < I.sup' hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ (p i) x < I.sup' hI r

Tactic:
refine lt_of_lt_of_le (h i x hx) ?_

Result:
case pos
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
h' : 0 < I.sup' hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ r i ≤ I.sup' hI r

Proof state:
case mp
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hI : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
i : ι
⊢ ∃ r > 0, ∀ x ∈ s, (p i) x < r

Tactic:
convert hI {i}

Result:
case h.e'_2.h.h.e'_2.h.h'.h.e'_3.h.e'_5
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hI : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
i : ι
x✝ : ℝ
a✝¹ : E
a✝ : a✝¹ ∈ s
⊢ p i = {i}.sup p

Proof state:
case pos
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
I : Finset ι
hI : I.Nonempty
r : ι → ℝ
hr : ∀ (i : ι), r i > 0
h : ∀ (i : ι), ∀ x ∈ s, (p i) x < r i
h' : 0 < I.sup' hI r
x : E
hx : x ∈ s
i : ι
hi : i ∈ I
⊢ ∃ b ∈ I, r i ≤ r b

Tactic:
exact ⟨i, hi, (Eq.refl _).le⟩

Result:
no goals

Proof state:
case h.e'_2.h.h.e'_2.h.h'.h.e'_3.h.e'_5
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hI : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
i : ι
x✝ : ℝ
a✝¹ : E
a✝ : a✝¹ ∈ s
⊢ p i = {i}.sup p

Tactic:
rw [Finset.sup_singleton]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
p : SeminormFamily 𝕜 E ι
inst✝ : TopologicalSpace E
s : Set E
hp : WithSeminorms p
hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r
I : Finset ι
hI : ¬I.Nonempty
⊢ ∃ r > 0, ∀ x ∈ s, 0 < r

Tactic:
exact ⟨1, zero_lt_one, fun _ _ => zero_lt_one⟩

Result:
no goals