simp [tendsto_norm_atTop_atTop.comp hf]
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝¹ : _root_.RCLike 𝕜
α : Type u_1
inst✝ : Preorder α
a : ℝ
f : α → ℝ
hf : Tendsto f atTop atTop
⊢ (fun x => a) =o[atTop] f
no goals