α : Type ?u.248624
β : Type ?u.248627
ι : Type ?u.248630
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑(r ^ a)) ↑(1 - r)⁻¹
α : Type ?u.248624
β : Type ?u.248627
ι : Type ?u.248630
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun n => r ^ n) (1 - r)⁻¹
apply NNReal.hasSum_coe.1
α : Type ?u.248624
β : Type ?u.248627
ι : Type ?u.248630
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑r ^ a) (↑(1 - r))⁻¹
α : Type ?u.248624
β : Type ?u.248627
ι : Type ?u.248630
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑(r ^ a)) ↑(1 - r)⁻¹
push_cast
α : Type ?u.248624
β : Type ?u.248627
ι : Type ?u.248630
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑r ^ a) (↑1 - ↑r)⁻¹
α : Type ?u.248624
β : Type ?u.248627
ι : Type ?u.248630
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑r ^ a) (↑(1 - r))⁻¹
rw [NNReal.coe_sub (le_of_lt hr)]
no goals
α : Type ?u.248624
β : Type ?u.248627
ι : Type ?u.248630
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑r ^ a) (↑1 - ↑r)⁻¹
exact hasSum_geometric_of_lt_1 r.coe_nonneg hr