case intro.intro
α : Type ?u.150661
β : Type ?u.150664
ι : Type ?u.150667
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ Summable fun n => ‖↑n ^ k * r ^ n‖
α : Type ?u.150661
β : Type ?u.150664
ι : Type ?u.150667
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable fun n => ‖↑n ^ k * r ^ n‖
rcases exists_between hr with ⟨r', hrr', h⟩
no goals
case intro.intro
α : Type ?u.150661
β : Type ?u.150664
ι : Type ?u.150667
R : Type u_1
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ Summable fun n => ‖↑n ^ k * r ^ n‖
exact summable_of_isBigO_nat (summable_geometric_of_lt_1 ((norm_nonneg _).trans hrr'.le) h)
  (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt _ hrr').isBigO.norm_left