α : Type ?u.79820
β : Type ?u.79823
ι : Type ?u.79826
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ ∑ i in Finset.range n, (1 / 2) ^ i ≤ 2
α : Type ?u.79820
β : Type ?u.79823
ι : Type ?u.79826
n : ℕ
⊢ ∑ i in Finset.range n, (1 / 2) ^ i ≤ 2
have : ∀ i, 0 ≤ (1 / (2 : ℝ)) ^ i := by
  intro i
  apply pow_nonneg
  norm_num
case h.e'_4
α : Type ?u.79820
β : Type ?u.79823
ι : Type ?u.79826
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ 2 = ∑' (i : ℕ), (1 / 2) ^ i
α : Type ?u.79820
β : Type ?u.79823
ι : Type ?u.79826
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ ∑ i in Finset.range n, (1 / 2) ^ i ≤ 2
convert sum_le_tsum (range n) (fun i _ => this i) summable_geometric_two
no goals
case h.e'_4
α : Type ?u.79820
β : Type ?u.79823
ι : Type ?u.79826
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ 2 = ∑' (i : ℕ), (1 / 2) ^ i
exact tsum_geometric_two.symm
α : Type ?u.79820
β : Type ?u.79823
ι : Type ?u.79826
n i : ℕ
⊢ 0 ≤ (1 / 2) ^ i
α : Type ?u.79820
β : Type ?u.79823
ι : Type ?u.79826
n : ℕ
⊢ ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
intro i
case H
α : Type ?u.79820
β : Type ?u.79823
ι : Type ?u.79826
n i : ℕ
⊢ 0 ≤ 1 / 2
α : Type ?u.79820
β : Type ?u.79823
ι : Type ?u.79826
n i : ℕ
⊢ 0 ≤ (1 / 2) ^ i
apply pow_nonneg
no goals
case H
α : Type ?u.79820
β : Type ?u.79823
ι : Type ?u.79826
n i : ℕ
⊢ 0 ≤ 1 / 2
norm_num