no goals
ι : Type ?u.246385
ι' : Type ?u.246388
α : Type u_2
β : Type u_1
γ : Type ?u.246397
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
h : Tendsto f l atTop
⊢ Tendsto (fun x => f x * r) l atBot ↔ r < 0
simp only [mul_comm _ r, tendsto_const_mul_atBot_iff_neg h]