no goals
ι : Type ?u.252223
ι' : Type ?u.252226
α : Type u_1
β : Type ?u.252232
γ : Type ?u.252235
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r c : α
n : ℕ
⊢ Tendsto (fun x => c * x ^ n) atTop atBot ↔ n ≠ 0 ∧ c < 0
simp only [← tendsto_neg_atTop_iff, ← neg_mul, tendsto_const_mul_pow_atTop_iff, neg_pos]