no goals
α : Type ?u.41397
β : Type ?u.41400
ι : Type ?u.41403
r : ℝ≥0
hr : r < 1
⊢ Tendsto (fun a => ↑(r ^ a)) atTop (𝓝 ↑0)
simp only [NNReal.coe_pow, NNReal.coe_zero,
  _root_.tendsto_pow_atTop_nhds_0_of_lt_1 r.coe_nonneg hr]