-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isVonNBounded_iff {s : Set E} : Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s

Tactic:
refine ⟨fun h ↦ ?_, isVonNBounded_of_isBounded _⟩

Result:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
⊢ Bornology.IsBounded s

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
⊢ Bornology.IsBounded s

Tactic:
rcases (h (Metric.ball_mem_nhds 0 zero_lt_one)).exists_pos with ⟨ρ, hρ, hρball⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : ρ > 0
hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ c • Metric.ball 0 1
⊢ Bornology.IsBounded s

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : ρ > 0
hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ c • Metric.ball 0 1
⊢ Bornology.IsBounded s

Tactic:
rcases NormedField.exists_lt_norm 𝕜 ρ with ⟨a, ha⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : ρ > 0
hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ c • Metric.ball 0 1
a : 𝕜
ha : ρ < ‖a‖
⊢ Bornology.IsBounded s

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : ρ > 0
hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ c • Metric.ball 0 1
a : 𝕜
ha : ρ < ‖a‖
⊢ Bornology.IsBounded s

Tactic:
specialize hρball a ha.le

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : ρ > 0
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ a • Metric.ball 0 1
⊢ Bornology.IsBounded s

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : ρ > 0
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ a • Metric.ball 0 1
⊢ Bornology.IsBounded s

Tactic:
rw [← ball_normSeminorm 𝕜 E, Seminorm.smul_ball_zero (norm_pos_iff.1 <| hρ.trans ha),
  ball_normSeminorm] at hρball

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : ρ > 0
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ Metric.ball 0 (‖a‖ * 1)
⊢ Bornology.IsBounded s

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
ρ : ℝ
hρ : ρ > 0
a : 𝕜
ha : ρ < ‖a‖
hρball : s ⊆ Metric.ball 0 (‖a‖ * 1)
⊢ Bornology.IsBounded s

Tactic:
exact Metric.isBounded_ball.subset hρball

Result:
no goals