no goals
ι : Type ?u.216245
ι' : Type ?u.216248
α : Type u_1
β : Type u_2
γ : Type ?u.216257
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
hr : 0 < r
⊢ Tendsto (fun x => f x * r) l atTop ↔ Tendsto f l atTop
simpa only [mul_comm] using tendsto_const_mul_atTop_of_pos hr