no goals
ι : Type ?u.230840
ι' : Type ?u.230843
α : Type u_1
β : Type u_2
γ : Type ?u.230852
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atTop
simpa only [neg_mul, tendsto_neg_atTop_iff] using tendsto_const_mul_atTop_of_pos (neg_pos.2 hr)