no goals
α : Type u_2
R : Type u_1
l : Filter α
f : α → R
r : R
inst✝¹ : LinearOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto (fun x => f x * r) l atTop
simpa only [mul_neg, tendsto_neg_atBot_iff] using hf.atBot_mul_const' (neg_pos.2 hr)