case zero
α : Type u
β : Type ?u.241921
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : Nat.zero ≠ 0
⊢ 0 < ∑ i in range Nat.zero, x ^ i

case succ.zero
α : Type u
β : Type ?u.241921
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : Nat.succ Nat.zero ≠ 0
⊢ 0 < ∑ i in range (Nat.succ Nat.zero), x ^ i

case succ.succ
α : Type u
β : Type ?u.241921
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
α : Type u
β : Type ?u.241921
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : n ≠ 0
⊢ 0 < ∑ i in range n, x ^ i
obtain _ | _ | n := n
case succ.succ.inl
α : Type u
β : Type ?u.241921
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
hx' : x < 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i

case succ.succ.inr
α : Type u
β : Type ?u.241921
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
case succ.succ
α : Type u
β : Type ?u.241921
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
obtain hx' | hx' := lt_or_le x 0
no goals
case zero
α : Type u
β : Type ?u.241921
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : Nat.zero ≠ 0
⊢ 0 < ∑ i in range Nat.zero, x ^ i
cases hn rfl
no goals
case succ.zero
α : Type u
β : Type ?u.241921
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
hn : Nat.succ Nat.zero ≠ 0
⊢ 0 < ∑ i in range (Nat.succ Nat.zero), x ^ i
simp only [Nat.zero_eq, ← Nat.one_eq_succ_zero, range_one, sum_singleton, pow_zero, zero_lt_one]
no goals
case succ.succ.inl
α : Type u
β : Type ?u.241921
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
hx' : x < 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
exact (geom_sum_pos_and_lt_one hx' hx n.one_lt_succ_succ).1
no goals
case succ.succ.inr
α : Type u
β : Type ?u.241921
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
hx' : 0 ≤ x
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
exact geom_sum_pos hx' (by simp only [Nat.succ_ne_zero, Ne.def, not_false_iff])
no goals
α : Type u
β : Type ?u.241921
x : α
inst✝ : LinearOrderedRing α
hx : 0 < x + 1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
hx' : 0 ≤ x
⊢ Nat.succ (Nat.succ n) ≠ 0
simp only [Nat.succ_ne_zero, Ne.def, not_false_iff]