-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem IsVonNBounded.extend_scalars [NontriviallyNormedField 𝕜]
    {E : Type*} [AddCommGroup E] [Module 𝕜 E]
    (𝕝 : Type*) [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝]
    [Module 𝕝 E] [TopologicalSpace E] [ContinuousSMul 𝕝 E] [IsScalarTower 𝕜 𝕝 E]
    {s : Set E} (h : IsVonNBounded 𝕜 s) : IsVonNBounded 𝕝 s

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_6
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
𝕝 : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : NormedAlgebra 𝕜 𝕝
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
ε : ℕ → 𝕜
hε : Tendsto ε atTop (𝓝 0)
hε₀ : ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0
x : ℕ → E
hx : ∀ (n : ℕ), x n ∈ s
⊢ Tendsto ((fun x => ε x • 1) • x) atTop (𝓝 0)

Tactic:
have := h.smul_tendsto_zero (.of_forall hx) hε

Result:
case intro.intro
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_6
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
𝕝 : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : NormedAlgebra 𝕜 𝕝
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
ε : ℕ → 𝕜
hε : Tendsto ε atTop (𝓝 0)
hε₀ : ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0
x : ℕ → E
hx : ∀ (n : ℕ), x n ∈ s
this : Tendsto (ε • x) atTop (𝓝 0)
⊢ Tendsto ((fun x => ε x • 1) • x) atTop (𝓝 0)

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_6
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
𝕝 : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : NormedAlgebra 𝕜 𝕝
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
⊢ IsVonNBounded 𝕝 s

Tactic:
obtain ⟨ε, hε, hε₀⟩ : ∃ ε : ℕ → 𝕜, Tendsto ε atTop (𝓝 0) ∧ ∀ᶠ n in atTop, ε n ≠ 0 := by
  simpa only [tendsto_nhdsWithin_iff] using exists_seq_tendsto (𝓝[≠] (0 : 𝕜))

Result:
case intro.intro
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_6
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
𝕝 : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : NormedAlgebra 𝕜 𝕝
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
ε : ℕ → 𝕜
hε : Tendsto ε atTop (𝓝 0)
hε₀ : ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0
⊢ IsVonNBounded 𝕝 s

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_6
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
𝕝 : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : NormedAlgebra 𝕜 𝕝
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
ε : ℕ → 𝕜
hε : Tendsto ε atTop (𝓝 0)
hε₀ : ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0
⊢ ∀ᶠ (n : ℕ) in ?m.80114, (fun x => ε x • 1) n ≠ 0

Tactic:
simpa

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_6
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
𝕝 : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : NormedAlgebra 𝕜 𝕝
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
ε : ℕ → 𝕜
hε : Tendsto ε atTop (𝓝 0)
hε₀ : ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0
x : ℕ → E
hx : ∀ (n : ℕ), x n ∈ s
this : Tendsto (ε • x) atTop (𝓝 0)
⊢ Tendsto ((fun x => ε x • 1) • x) atTop (𝓝 0)

Tactic:
simpa only [Pi.smul_def', smul_one_smul]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_6
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
𝕝 : Type u_7
inst✝⁵ : NontriviallyNormedField 𝕝
inst✝⁴ : NormedAlgebra 𝕜 𝕝
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
inst✝ : IsScalarTower 𝕜 𝕝 E
s : Set E
h : IsVonNBounded 𝕜 s
⊢ ∃ ε, Tendsto ε atTop (𝓝 0) ∧ ∀ᶠ (n : ℕ) in atTop, ε n ≠ 0

Tactic:
simpa only [tendsto_nhdsWithin_iff] using exists_seq_tendsto (𝓝[≠] (0 : 𝕜))

Result:
no goals