no goals
ι : Type ?u.242288
ι' : Type ?u.242291
α : Type u_2
β : Type u_1
γ : Type ?u.242300
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : NeBot l
h : Tendsto f l atBot
⊢ Tendsto (fun x => r * f x) l atBot ↔ 0 < r
simp [tendsto_const_mul_atBot_iff, h, h.not_tendsto disjoint_atBot_atTop]