case zero
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
h : Odd Nat.zero
⊢ 0 < ∑ i in range Nat.zero, x ^ i

case succ.zero
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
h : Odd (Nat.succ Nat.zero)
⊢ 0 < ∑ i in range (Nat.succ Nat.zero), x ^ i

case succ.succ
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : Odd (Nat.succ (Nat.succ k))
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
α : Type u
β : Type ?u.244183
n : ℕ
x : α
inst✝ : LinearOrderedRing α
h : Odd n
⊢ 0 < ∑ i in range n, x ^ i
rcases n with (_ | _ | k)
case succ.succ
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
case succ.succ
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : Odd (Nat.succ (Nat.succ k))
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
rw [Nat.odd_iff_not_even] at h
case succ.succ.inl
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 < 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i

case succ.succ.inr.inl
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 = 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i

case succ.succ.inr.inr
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : 0 < x + 1
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
case succ.succ
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
rcases lt_trichotomy (x + 1) 0 with (hx | hx | hx)
no goals
case zero
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
h : Odd Nat.zero
⊢ 0 < ∑ i in range Nat.zero, x ^ i
exact ((show ¬Odd 0 by decide) h).elim
no goals
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
h : Odd Nat.zero
⊢ ¬Odd 0
decide
no goals
case succ.zero
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
h : Odd (Nat.succ Nat.zero)
⊢ 0 < ∑ i in range (Nat.succ Nat.zero), x ^ i
simp only [Nat.zero_eq, ← Nat.one_eq_succ_zero, geom_sum_one, zero_lt_one]
case succ.succ.inl
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 < 0
this :
  if Even (Nat.succ (Nat.succ k)) then ∑ i in range (Nat.succ (Nat.succ k)), x ^ i < 0
  else 1 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
case succ.succ.inl
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 < 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
have := geom_sum_alternating_of_lt_neg_one hx k.one_lt_succ_succ
case succ.succ.inl
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 < 0
this : 1 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
case succ.succ.inl
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 < 0
this :
  if Even (Nat.succ (Nat.succ k)) then ∑ i in range (Nat.succ (Nat.succ k)), x ^ i < 0
  else 1 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
simp only [h, if_false] at this
no goals
case succ.succ.inl
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 < 0
this : 1 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
exact zero_lt_one.trans this
no goals
case succ.succ.inr.inl
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : x + 1 = 0
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
simp only [eq_neg_of_add_eq_zero_left hx, h, neg_one_geom_sum, if_false, zero_lt_one]
no goals
case succ.succ.inr.inr
α : Type u
β : Type ?u.244183
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (Nat.succ (Nat.succ k))
hx : 0 < x + 1
⊢ 0 < ∑ i in range (Nat.succ (Nat.succ k)), x ^ i
exact geom_sum_pos' hx k.succ.succ_ne_zero