no goals
ι : Type ?u.237721
ι' : Type ?u.237724
α : Type u_2
β : Type u_1
γ : Type ?u.237733
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
⊢ Tendsto (fun x => r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop
simp only [← tendsto_neg_atTop_iff, ← mul_neg, tendsto_const_mul_atTop_iff, neg_neg]