no goals
ι : Type ?u.221463
ι' : Type ?u.221466
α : Type u_1
β : Type u_2
γ : Type ?u.221475
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x / r) l atTop
simpa only [div_eq_mul_inv] using hf.atTop_mul_const (inv_pos.2 hr)