theorem ENNReal.Tendsto.rpow {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a : ENNReal} {n : ℝ} (hm : Filter.Tendsto m f (nhds a)) : Filter.Tendsto (fun (x : α) => m x ^ n) f (nhds (a ^ n))

theorem ENNReal.div_div_div_cancel_left {a b c : ENNReal} (ha : a ≠ 0) (ha' : a ≠ ⊤) (hc : c ≠ ⊤) : a / b / (a / c) = c / b