-- 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:
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

Tactic:
rw [bE.1.tendsto_left_iff] 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 : ∀ t ∈ 𝓝 0, ∃ i, True ∧ Set.MapsTo (fun x => ↑n • x) (b i) t
⊢ ∃ i, True ∧ b i ⊆ (↑n)⁻¹ • b n

Proof state:
case intro.intro.intro.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)
r : ℝ
hr : r > 0
h' : ∀ (c : 𝕜'), r ≤ ‖c‖ → (⇑f '' Set.range fun n => ↑n • u n) ⊆ c • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
⊢ False

Tactic:
have h'' : f (u n) ∈ V := by
  simp only [Set.image_subset_iff] at h'
  specialize h' (n : 𝕜') h1 (Set.mem_range_self n)
  simp only [Set.mem_preimage, LinearMap.map_smulₛₗ, map_natCast] at h'
  rcases h' with ⟨y, hy, h'⟩
  apply_fun fun y : F => (n : 𝕜')⁻¹ • y at h'
  simp only [hn', inv_smul_smul₀, Ne, Nat.cast_eq_zero, not_false_iff] at h'
  rwa [← h']

Result:
case intro.intro.intro.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)
r : ℝ
hr : r > 0
h' : ∀ (c : 𝕜'), r ≤ ‖c‖ → (⇑f '' Set.range fun n => ↑n • u n) ⊆ c • V
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h'' : f (u n) ∈ V
⊢ False

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
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h' : ∀ (c : 𝕜'), r ≤ ‖c‖ → (Set.range fun n => ↑n • u n) ⊆ ⇑f ⁻¹' (c • V)
⊢ f (u n) ∈ V

Tactic:
specialize h' (n : 𝕜') h1 (Set.mem_range_self n)

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
n : ℕ
hn : r < ↑n
h1 : r ≤ ‖↑n‖
hn' : ¬n = 0
h' : ↑n • u n ∈ ⇑f ⁻¹' (↑n • V)
⊢ f (u n) ∈ V

Proof state:
case refine_1
𝕜 : 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 : ℕ
a✝ : True
⊢ ∃ i', i' ≠ 0 ∧ (↑i')⁻¹ • b i' ⊆ b n

Tactic:
use n + 1

Result:
case h
𝕜 : 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 : ℕ
a✝ : True
⊢ n + 1 ≠ 0 ∧ (↑(n + 1))⁻¹ • b (n + 1) ⊆ b n