exact tendsto_natCast_atTop_atTop.const_mul_atTop (by positivity)
case hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ Tendsto (fun x => δ / 2 * ↑x) atTop atTop
no goals