case pos
α : Type ?u.120365
β : Type ?u.120368
ι : Type ?u.120371
k : ℕ
r : ℝ
hr : abs r < 1
h0 : r = 0
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)

case neg
α : Type ?u.120365
β : Type ?u.120368
ι : Type ?u.120371
k : ℕ
r : ℝ
hr : abs r < 1
h0 : ¬r = 0
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)
α : Type ?u.120365
β : Type ?u.120368
ι : Type ?u.120371
k : ℕ
r : ℝ
hr : abs r < 1
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)
by_cases h0 : r = 0
case neg
α : Type ?u.120365
β : Type ?u.120368
ι : Type ?u.120371
k : ℕ
r : ℝ
hr : abs r < 1
h0 : ¬r = 0
hr' : 1 < (abs r)⁻¹
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)
case neg
α : Type ?u.120365
β : Type ?u.120368
ι : Type ?u.120371
k : ℕ
r : ℝ
hr : abs r < 1
h0 : ¬r = 0
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)
have hr' : 1 < (|r|)⁻¹ := one_lt_inv (abs_pos.2 h0) hr
case neg
α : Type ?u.120365
β : Type ?u.120368
ι : Type ?u.120371
k : ℕ
r : ℝ
hr : abs r < 1
h0 : ¬r = 0
hr' : 1 < (abs r)⁻¹
⊢ Tendsto (fun e => ‖↑e ^ k * r ^ e‖) atTop (𝓝 0)
case neg
α : Type ?u.120365
β : Type ?u.120368
ι : Type ?u.120371
k : ℕ
r : ℝ
hr : abs r < 1
h0 : ¬r = 0
hr' : 1 < (abs r)⁻¹
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)
rw [tendsto_zero_iff_norm_tendsto_zero]
no goals
case neg
α : Type ?u.120365
β : Type ?u.120368
ι : Type ?u.120371
k : ℕ
r : ℝ
hr : abs r < 1
h0 : ¬r = 0
hr' : 1 < (abs r)⁻¹
⊢ Tendsto (fun e => ‖↑e ^ k * r ^ e‖) atTop (𝓝 0)
simpa [div_eq_mul_inv] using tendsto_pow_const_div_const_pow_of_one_lt k hr'
no goals
case pos
α : Type ?u.120365
β : Type ?u.120368
ι : Type ?u.120371
k : ℕ
r : ℝ
hr : abs r < 1
h0 : r = 0
⊢ Tendsto (fun n => ↑n ^ k * r ^ n) atTop (𝓝 0)
exact tendsto_const_nhds.congr'
  (mem_atTop_sets.2 ⟨1, fun n hn ↦ by simp [zero_lt_one.trans_le hn, h0]⟩)
no goals
α : Type ?u.120365
β : Type ?u.120368
ι : Type ?u.120371
k : ℕ
r : ℝ
hr : abs r < 1
h0 : r = 0
n : ℕ
hn : n ≥ 1
⊢ n ∈ {x | (fun x => 0 = (fun n => ↑n ^ k * r ^ n) x) x}
simp [zero_lt_one.trans_le hn, h0]