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

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

case succ.succ
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
α : Type u
β : Type ?u.249597
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : n ≠ 0
⊢ ∑ i in range n, x ^ i ≠ 0
obtain _ | _ | n := n
case succ.succ
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
case succ.succ
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
rw [Ne.def, eq_neg_iff_add_eq_zero, ← Ne.def] at hx
case succ.succ.inl
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0

case succ.succ.inr
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : 0 < x + 1
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
case succ.succ
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
obtain h | h := hx.lt_or_lt
no goals
case zero
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : Nat.zero ≠ 0
⊢ ∑ i in range Nat.zero, x ^ i ≠ 0
cases hn rfl
no goals
case succ.zero
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x ≠ -1
hn : Nat.succ Nat.zero ≠ 0
⊢ ∑ i in range (Nat.succ Nat.zero), x ^ i ≠ 0
simp only [Nat.zero_eq, ← Nat.one_eq_succ_zero, range_one, sum_singleton, pow_zero, ne_eq,
  one_ne_zero, not_false_iff]
case succ.succ.inl
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
this :
  if Even (Nat.succ (Nat.succ n)) then ∑ i in range (Nat.succ (Nat.succ n)), x ^ i < 0
  else 1 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
case succ.succ.inl
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
have := geom_sum_alternating_of_lt_neg_one h n.one_lt_succ_succ
case succ.succ.inl.inl
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
h✝ : Even (Nat.succ (Nat.succ n))
this : ∑ i in range (Nat.succ (Nat.succ n)), x ^ i < 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0

case succ.succ.inl.inr
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
h✝ : ¬Even (Nat.succ (Nat.succ n))
this : 1 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
case succ.succ.inl
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
this :
  if Even (Nat.succ (Nat.succ n)) then ∑ i in range (Nat.succ (Nat.succ n)), x ^ i < 0
  else 1 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
split_ifs  at this
no goals
case succ.succ.inl.inl
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
h✝ : Even (Nat.succ (Nat.succ n))
this : ∑ i in range (Nat.succ (Nat.succ n)), x ^ i < 0
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
exact this.ne
no goals
case succ.succ.inl.inr
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : x + 1 < 0
h✝ : ¬Even (Nat.succ (Nat.succ n))
this : 1 < ∑ i in range (Nat.succ (Nat.succ n)), x ^ i
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
exact (zero_lt_one.trans this).ne'
no goals
case succ.succ.inr
α : Type u
β : Type ?u.249597
x : α
inst✝ : LinearOrderedRing α
hx : x + 1 ≠ 0
n : ℕ
hn : Nat.succ (Nat.succ n) ≠ 0
h : 0 < x + 1
⊢ ∑ i in range (Nat.succ (Nat.succ n)), x ^ i ≠ 0
exact (geom_sum_pos' h n.succ.succ_ne_zero).ne'