-- Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean
theorem LinearMap.continuousAt_zero_of_locally_bounded (f : E →ₛₗ[σ] F)
    (hf : ∀ s, IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (f '' s)) : ContinuousAt f 0

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : RCLike 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i => b i
bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → f (u ia) ∉ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : r > 0
h' : ∀ (c : 𝕜'), r ≤ ‖c‖ → (⇑f '' Set.range fun n => ↑n • u n) ⊆ c • V
n : ℕ
hn : r < ↑n
⊢ r ≤ ‖↑n‖

Tactic:
rw [RCLike.norm_natCast]

Result:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : RCLike 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i => b i
bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → f (u ia) ∉ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
r : ℝ
hr : r > 0
h' : ∀ (c : 𝕜'), r ≤ ‖c‖ → (⇑f '' Set.range fun n => ↑n • u n) ⊆ c • V
n : ℕ
hn : r < ↑n
⊢ r ≤ ↑n

Proof state:
case intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : RCLike 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i => b i
bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
h : ∃ ib, (ib ∈ 𝓝 0 ∧ Balanced 𝕜' ib) ∧ ∀ (ia : ℕ), ia ≠ 0 → ∃ x ∈ (↑ia)⁻¹ • b ia, f x ∉ _root_.id ib
⊢ False

Tactic:
rcases h with ⟨V, ⟨hV, -⟩, h⟩

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : RCLike 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i => b i
bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
h : ∀ (ia : ℕ), ia ≠ 0 → ∃ x ∈ (↑ia)⁻¹ • b ia, f x ∉ _root_.id V
hV : V ∈ 𝓝 0
⊢ False

Proof state:
case refine_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : RCLike 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
h : ¬ContinuousAt (⇑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i => b i
n : ℕ
hn : n ≠ 0
hcont : ContinuousAt (fun x => ↑n • x) 0
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n

Tactic:
simp only [ContinuousAt, map_zero, smul_zero] at hcont

Result:
case refine_2
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : RCLike 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
h : ¬ContinuousAt (⇑f) 0
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i => b i
n : ℕ
hn : n ≠ 0
hcont : Tendsto (fun x => ↑n • x) (𝓝 0) (𝓝 0)
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : RCLike 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i => b i
bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → f (u ia) ∉ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
⊢ False

Tactic:
have h_bounded : IsVonNBounded 𝕜 (Set.range fun n : ℕ => (n : 𝕜) • u n) :=
  h_tendsto.cauchySeq.totallyBounded_range.isVonNBounded 𝕜

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : UniformSpace E
inst✝⁹ : UniformAddGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : UniformSpace F
inst✝⁶ : FirstCountableTopology E
inst✝⁵ : RCLike 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : RCLike 𝕜'
inst✝¹ : Module 𝕜' F
inst✝ : ContinuousSMul 𝕜' F
σ : 𝕜 →+* 𝕜'
f : E →ₛₗ[σ] F
hf : ∀ (s : Set E), IsVonNBounded 𝕜 s → IsVonNBounded 𝕜' (⇑f '' s)
b : ℕ → Set E
bE1 : ∀ (i : ℕ), b i ∈ 𝓝 0 ∧ Balanced 𝕜 (b i)
bE : (𝓝 0).HasAntitoneBasis fun i => b i
bE' : (𝓝 0).HasBasis (fun x => x ≠ 0) fun n => (↑n)⁻¹ • b n
V : Set F
hV : V ∈ 𝓝 0
u : ℕ → E
hu : ∀ (ia : ℕ), ia ≠ 0 → u ia ∈ (↑ia)⁻¹ • b ia
hu' : ∀ (ia : ℕ), ia ≠ 0 → f (u ia) ∉ V
h_tendsto : Tendsto (fun n => ↑n • u n) atTop (𝓝 0)
h_bounded : IsVonNBounded 𝕜 (Set.range fun n => ↑n • u n)
⊢ False