simpa using ((continuous_ofReal.tendsto 1).mono_left nhdsWithin_le_nhds).const_cpow
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
ψ : W21
hx : 0 < x
C : ℝ
hC : ∀ (u : ℝ), ‖𝓕 ψ.toFun u‖ ≤ C / (1 + u ^ 2)
this : 0 ≤ C
n : ℕ
h : ¬n = 0
⊢ Tendsto (fun k => ↑n ^ ↑k) (𝓝[>] 1) (𝓝 ↑n)
no goals