no goals
ι : Type ?u.215087
ι' : Type ?u.215090
α : Type u_1
β : Type u_2
γ : Type ?u.215099
inst✝ : LinearOrderedSemifield α
l : Filter β
f : β → α
r c : α
n : ℕ
hr : 0 < r
h : Tendsto f l atTop
⊢ Tendsto (fun x => r⁻¹ * (r * f x)) l atTop
simpa only [inv_mul_cancel_left₀ hr.ne']