-- Mathlib/Algebra/GeomSum.lean
theorem Odd.geom_sum_pos [LinearOrderedRing α] (h : Odd n) : 0 < ∑ i ∈ range n, x ^ i

Proof state:
case succ.succ.inl
α : Type u
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
this : if Even k.succ.succ then ∑ i ∈ range k.succ.succ, x ^ i < 0 else 1 < ∑ i ∈ range k.succ.succ, x ^ i
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
simp only [h, if_false] at this

Result:
case succ.succ.inl
α : Type u
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
this : 1 < ∑ i ∈ range k.succ.succ, x ^ i
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Proof state:
case zero
α : Type u
x : α
inst✝ : LinearOrderedRing α
h : Odd 0
⊢ 0 < ∑ i ∈ range 0, x ^ i

Tactic:
exact (Nat.not_odd_zero h).elim

Result:
no goals

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

Tactic:
simp only [eq_neg_of_add_eq_zero_left hx, h, neg_one_geom_sum, if_false, zero_lt_one]

Result:
no goals

Proof state:
case succ.succ
α : Type u
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : Odd (k + 1 + 1)
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
rw [← Nat.not_even_iff_odd] at h

Result:
case succ.succ
α : Type u
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (k + 1 + 1)
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Proof state:
case succ.succ
α : Type u
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (k + 1 + 1)
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
rcases lt_trichotomy (x + 1) 0 with (hx | hx | hx)

Result:
case succ.succ.inl
α : Type u
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

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

case succ.succ.inr.inr
α : Type u
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (k + 1 + 1)
hx : 0 < x + 1
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Proof state:
case succ.succ.inl
α : Type u
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
this : 1 < ∑ i ∈ range k.succ.succ, x ^ i
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
exact zero_lt_one.trans this

Result:
no goals

Proof state:
case succ.zero
α : Type u
x : α
inst✝ : LinearOrderedRing α
h : Odd (0 + 1)
⊢ 0 < ∑ i ∈ range (0 + 1), x ^ i

Tactic:
simp only [zero_add, range_one, sum_singleton, pow_zero, zero_lt_one]

Result:
no goals

Proof state:
case succ.succ.inr.inr
α : Type u
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (k + 1 + 1)
hx : 0 < x + 1
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
exact geom_sum_pos' hx k.succ.succ_ne_zero

Result:
no goals

Proof state:
case succ.succ.inl
α : Type u
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Tactic:
have := geom_sum_alternating_of_lt_neg_one hx k.one_lt_succ_succ

Result:
case succ.succ.inl
α : Type u
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
this : if Even k.succ.succ then ∑ i ∈ range k.succ.succ, x ^ i < 0 else 1 < ∑ i ∈ range k.succ.succ, x ^ i
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i

Proof state:
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
h : Odd n
⊢ 0 < ∑ i ∈ range n, x ^ i

Tactic:
rcases n with (_ | _ | k)

Result:
case zero
α : Type u
x : α
inst✝ : LinearOrderedRing α
h : Odd 0
⊢ 0 < ∑ i ∈ range 0, x ^ i

case succ.zero
α : Type u
x : α
inst✝ : LinearOrderedRing α
h : Odd (0 + 1)
⊢ 0 < ∑ i ∈ range (0 + 1), x ^ i

case succ.succ
α : Type u
x : α
inst✝ : LinearOrderedRing α
k : ℕ
h : Odd (k + 1 + 1)
⊢ 0 < ∑ i ∈ range (k + 1 + 1), x ^ i