case inl
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0∞
hr : r < 1
⊢ (∑' (n : ℕ), r ^ n) = (1 - r)⁻¹

case inr
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0∞
hr : 1 ≤ r
⊢ (∑' (n : ℕ), r ^ n) = (1 - r)⁻¹
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0∞
⊢ (∑' (n : ℕ), r ^ n) = (1 - r)⁻¹
cases' lt_or_le r 1 with hr hr
case inl.intro.intro
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ (∑' (n : ℕ), ↑r ^ n) = (1 - ↑r)⁻¹
case inl
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0∞
hr : r < 1
⊢ (∑' (n : ℕ), r ^ n) = (1 - r)⁻¹
rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
case inl.intro.intro
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0
hr' hr : r < 1
⊢ (∑' (n : ℕ), ↑(r ^ n)) = (1 - ↑r)⁻¹
case inl.intro.intro
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ (∑' (n : ℕ), ↑r ^ n) = (1 - ↑r)⁻¹
norm_cast at *
case h.e'_3
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0
hr' hr : r < 1
⊢ (1 - ↑r)⁻¹ = ↑(1 - r)⁻¹
case inl.intro.intro
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0
hr' hr : r < 1
⊢ (∑' (n : ℕ), ↑(r ^ n)) = (1 - ↑r)⁻¹
convert ENNReal.tsum_coe_eq (NNReal.hasSum_geometric hr)
no goals
case h.e'_3
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0
hr' hr : r < 1
⊢ (1 - ↑r)⁻¹ = ↑(1 - r)⁻¹
rw [ENNReal.coe_inv <| ne_of_gt <| tsub_pos_iff_lt.2 hr, coe_sub, coe_one]
case inr
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∀ (b : ℝ≥0∞), b < ⊤ → ∃ i, b < ∑ a in Finset.range i, r ^ a
case inr
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0∞
hr : 1 ≤ r
⊢ (∑' (n : ℕ), r ^ n) = (1 - r)⁻¹
rw [tsub_eq_zero_iff_le.mpr hr, ENNReal.inv_zero, ENNReal.tsum_eq_iSup_nat, iSup_eq_top]
case inr
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
⊢ ↑n ≤ ∑ a in Finset.range n, r ^ a
case inr
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∀ (b : ℝ≥0∞), b < ⊤ → ∃ i, b < ∑ a in Finset.range i, r ^ a
refine' fun a ha =>
  (ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp fun n hn => lt_of_lt_of_le hn _
no goals
case inr
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
⊢ ↑n ≤ ∑ a in Finset.range n, r ^ a
calc
  (n : ℝ≥0∞) = ∑ i in range n, 1 := by rw [sum_const, nsmul_one, card_range]
  _ ≤ ∑ i in range n, r ^ i := by gcongr; apply one_le_pow_of_one_le' hr
no goals
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
⊢ ↑n = ∑ i in Finset.range n, 1
rw [sum_const, nsmul_one, card_range]
case h
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
i✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ 1 ≤ r ^ i✝
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
⊢ ∑ i in Finset.range n, 1 ≤ ∑ i in Finset.range n, r ^ i
gcongr
no goals
case h
α : Type ?u.250475
β : Type ?u.250478
ι : Type ?u.250481
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
i✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ 1 ≤ r ^ i✝
apply one_le_pow_of_one_le' hr