no goals
α : Type u_2
R : Type u_1
l : Filter α
f✝ : α → R
r : R
inst✝¹ : LinearOrderedAddCommGroup R
inst✝ : Archimedean R
f : α → ℕ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x • r) l atBot
simpa using hf.atTop_nsmul_const (neg_pos.2 hr)