no goals
ι : Type ?u.218886
ι' : Type ?u.218889
α : Type u_2
β : Type u_1
γ : Type ?u.218898
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
inst✝ : NeBot l
h : Tendsto f l atTop
⊢ Tendsto (fun x => f x * r) l atTop ↔ 0 < r
simp only [mul_comm _ r, tendsto_const_mul_atTop_iff_pos h]