no goals
ι : Type ?u.210440
ι' : Type ?u.210443
α : Type u_1
β : Type ?u.210449
γ : Type ?u.210452
inst✝ : LinearOrderedSemiring α
l : Filter β
f : β → α
n : ℕ
h : Tendsto (fun x => x ^ n) atTop atTop
hn : n = 0
⊢ False
simp only [hn, pow_zero, not_tendsto_const_atTop] at h