∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔
    0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.atBot