-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem isBounded_iff_subset_smul_ball {s : Set E} :
    Bornology.IsBounded s ↔ ∃ a : 𝕜, s ⊆ a • Metric.ball (0 : E) 1

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.ball 0 1) → Bornology.IsVonNBounded 𝕜 s

Tactic:
rintro ⟨a, ha⟩

Result:
case mpr.intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ a • Metric.ball 0 1
⊢ Bornology.IsVonNBounded 𝕜 s

Proof state:
case mp.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
ρ : ℝ
left✝ : ρ > 0
hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ c • Metric.ball 0 1
a : 𝕜
ha : ρ < ‖a‖
⊢ ∃ a, s ⊆ a • Metric.ball 0 1

Tactic:
exact ⟨a, hρball a ha.le⟩

Result:
no goals

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

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

Result:
case mp.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
ρ : ℝ
left✝ : ρ > 0
hρball : ∀ (c : 𝕜), ρ ≤ ‖c‖ → s ⊆ c • Metric.ball 0 1
a : 𝕜
ha : ρ < ‖a‖
⊢ ∃ a, s ⊆ a • Metric.ball 0 1

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsBounded s ↔ ∃ a, s ⊆ a • Metric.ball 0 1

Tactic:
rw [← isVonNBounded_iff 𝕜]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ a, s ⊆ a • Metric.ball 0 1

Proof state:
case mp
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
⊢ ∃ a, s ⊆ a • Metric.ball 0 1

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

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

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s ↔ ∃ a, s ⊆ a • Metric.ball 0 1

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s → ∃ a, s ⊆ a • Metric.ball 0 1

case mpr
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ (∃ a, s ⊆ a • Metric.ball 0 1) → Bornology.IsVonNBounded 𝕜 s

Proof state:
case mpr.intro
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
a : 𝕜
ha : s ⊆ a • Metric.ball 0 1
⊢ Bornology.IsVonNBounded 𝕜 s

Tactic:
exact ((isVonNBounded_ball 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha

Result:
no goals

Proof state:
case mp
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ Bornology.IsVonNBounded 𝕜 s → ∃ a, s ⊆ a • Metric.ball 0 1

Tactic:
intro h

Result:
case mp
𝕜 : Type u_1
E : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
h : Bornology.IsVonNBounded 𝕜 s
⊢ ∃ a, s ⊆ a • Metric.ball 0 1