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

Proof state:
case mpr.intro.intro.intro.intro.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
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
s' : Set E
hs'✝ : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
r' : ℝ
left✝ : r' > 0
h' : ∀ x ∈ s, (I.sup p) x < r'
⊢ Absorbs 𝕜 ((I.sup p).ball 0 r) s

Tactic:
simp_rw [← (I.sup p).mem_ball_zero] at h'

Result:
case mpr.intro.intro.intro.intro.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
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
s' : Set E
hs'✝ : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
r' : ℝ
left✝ : r' > 0
h' : ∀ x ∈ s, x ∈ (I.sup p).ball 0 r'
⊢ Absorbs 𝕜 ((I.sup p).ball 0 r) s

Proof state:
case mp.intro.intro.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 ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
h : ∀ (c : 𝕜), r ≤ ‖c‖ → s ⊆ c • (I.sup p).ball 0 1
a : 𝕜
ha : r < ‖a‖
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
specialize h a (le_of_lt ha)

Result:
case mp.intro.intro.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 ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
h : s ⊆ a • (I.sup p).ball 0 1
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Proof state:
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 : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r) → ∀ i ∈ p.basisSets, Absorbs 𝕜 (id i) s

Tactic:
intro h s' hs'

Result:
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
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
s' : Set E
hs' : s' ∈ p.basisSets
⊢ Absorbs 𝕜 (id s') s

Proof state:
case mpr.intro.intro.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
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
s' : Set E
hs'✝ : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
⊢ Absorbs 𝕜 (id s') s

Tactic:
rw [id, hs']

Result:
case mpr.intro.intro.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
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
s' : Set E
hs'✝ : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
⊢ Absorbs 𝕜 ((I.sup p).ball 0 r) s

Proof state:
case mp.intro.intro.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 ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
h : s ⊆ (I.sup p).ball 0 ‖a‖
⊢ ∀ x ∈ s, (I.sup p) x < ‖a‖

Tactic:
intro x hx

Result:
case mp.intro.intro.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 ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
h : s ⊆ (I.sup p).ball 0 ‖a‖
x : E
hx : x ∈ s
⊢ (I.sup p) x < ‖a‖

Proof state:
case mp.intro.intro.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 ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
h : s ⊆ (I.sup p).ball 0 ‖a‖
x : E
hx : x ∈ s
⊢ (I.sup p) x < ‖a‖

Tactic:
specialize h hx

Result:
case mp.intro.intro.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 ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
x : E
hx : x ∈ s
h : x ∈ (I.sup p).ball 0 ‖a‖
⊢ (I.sup p) x < ‖a‖

Proof state:
case mp.intro.intro.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 ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
h : s ⊆ a • (I.sup p).ball 0 1
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
rw [Seminorm.smul_ball_zero (norm_pos_iff.1 <| hr.trans ha), mul_one] at h

Result:
case mp.intro.intro.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 ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
a : 𝕜
ha : r < ‖a‖
h : s ⊆ (I.sup p).ball 0 ‖a‖
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Proof state:
case mp.intro.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 ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
h : ∀ (c : 𝕜), r ≤ ‖c‖ → s ⊆ c • (I.sup p).ball 0 1
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Tactic:
obtain ⟨a, ha⟩ := NormedField.exists_lt_norm 𝕜 r

Result:
case mp.intro.intro.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 ι
h✝ : Absorbs 𝕜 ((I.sup p).ball 0 1) s
r : ℝ
hr : r > 0
h : ∀ (c : 𝕜), r ≤ ‖c‖ → s ⊆ c • (I.sup p).ball 0 1
a : 𝕜
ha : r < ‖a‖
⊢ ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r

Proof state:
case mpr.intro.intro.intro.intro.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
h : ∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
s' : Set E
hs'✝ : s' ∈ p.basisSets
I : Finset ι
r : ℝ
hr : 0 < r
hs' : s' = (I.sup p).ball 0 r
r' : ℝ
left✝ : r' > 0
h' : ∀ x ∈ s, x ∈ (I.sup p).ball 0 r'
⊢ Absorbs 𝕜 ((I.sup p).ball 0 r) ((I.sup p).ball 0 r')

Tactic:
exact (Finset.sup I p).ball_zero_absorbs_ball_zero hr

Result:
no goals