-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_ne_zero [LinearOrderedRing α] (hx : x ≠ -1) (hn : n ≠ 0) :
    ∑ i ∈ range n, x ^ i ≠ 0

Proof state:
case succ.succ
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
rw [Ne, eq_neg_iff_add_eq_zero, ← Ne] at hx

Result:
case succ.succ
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

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

Tactic:
exact (geom_sum_pos' h n.succ.succ_ne_zero).ne'

Result:
no goals

Proof state:
case succ.succ
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Tactic:
obtain h | h := hx.lt_or_lt

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

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

Proof state:
case succ.zero
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : 0 + 1 ≠ 0
⊢ ∑ i ∈ range (0 + 1), x ^ i ≠ 0

Tactic:
simp only [zero_add, range_one, sum_singleton, pow_zero, ne_eq, one_ne_zero, not_false_eq_true]

Result:
no goals

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

Tactic:
have := geom_sum_alternating_of_lt_neg_one h n.one_lt_succ_succ

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

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

Tactic:
exact (zero_lt_one.trans this).ne'

Result:
no goals

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

Tactic:
split_ifs at this

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

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

Proof state:
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : n ≠ 0
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
obtain _ | _ | n := n

Result:
case zero
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : 0 ≠ 0
⊢ ∑ i ∈ range 0, x ^ i ≠ 0

case succ.zero
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : 0 + 1 ≠ 0
⊢ ∑ i ∈ range (0 + 1), x ^ i ≠ 0

case succ.succ
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ ∑ i ∈ range (n + 1 + 1), x ^ i ≠ 0

Proof state:
case zero
α : Type u
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : 0 ≠ 0
⊢ ∑ i ∈ range 0, x ^ i ≠ 0

Tactic:
cases hn rfl

Result:
no goals

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

Tactic:
exact this.ne

Result:
no goals