-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_alternating_of_le_neg_one [StrictOrderedRing α] (hx : x + 1 ≤ 0) (n : ℕ) :
    if Even n then (∑ i ∈ range n, x ^ i) ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i

Proof state:
case zero
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
⊢ if Even 0 then ∑ i ∈ range 0, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range 0, x ^ i

Tactic:
simp only [range_zero, sum_empty, le_refl, ite_true, Even.zero]

Result:
no goals

Proof state:
case pos
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i ∈ range n, x ^ i ≤ 0
⊢ 0 ≤ x * ∑ i ∈ range n, x ^ i

Tactic:
exact mul_nonneg_of_nonpos_of_nonpos hx0 ih

Result:
no goals

Proof state:
case neg
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1

Tactic:
rw [if_pos h]

Result:
case neg
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ 0

Proof state:
case neg
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i ≤ x

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonpos_left ih hx0

Result:
no goals

Proof state:
case neg
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i + 1 ≤ 0

Tactic:
refine (add_le_add_right ?_ _).trans hx

Result:
case neg
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ x * ∑ i ∈ range n, x ^ i ≤ x

Proof state:
case pos
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i ∈ range n, x ^ i ≤ 0
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1

Tactic:
rw [if_neg (not_not_intro h), le_add_iff_nonneg_left]

Result:
case pos
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i ∈ range n, x ^ i ≤ 0
⊢ 0 ≤ x * ∑ i ∈ range n, x ^ i

Proof state:
case succ
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
ih : if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i
⊢ if Even (n + 1) then ∑ i ∈ range (n + 1), x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range (n + 1), x ^ i

Tactic:
simp only [Nat.even_add_one, geom_sum_succ]

Result:
case succ
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
ih : if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1

Proof state:
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
n : ℕ
⊢ if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i

Tactic:
have hx0 : x ≤ 0 := (le_add_of_nonneg_right zero_le_one).trans hx

Result:
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
n : ℕ
hx0 : x ≤ 0
⊢ if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i

Proof state:
case succ
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
ih : if Even n then ∑ i ∈ range n, x ^ i ≤ 0 else 1 ≤ ∑ i ∈ range n, x ^ i
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1

Tactic:
split_ifs at ih with h

Result:
case pos
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : Even n
ih : ∑ i ∈ range n, x ^ i ≤ 0
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1

case neg
α : Type u
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 ≤ 0
hx0 : x ≤ 0
n : ℕ
h : ¬Even n
ih : 1 ≤ ∑ i ∈ range n, x ^ i
⊢ if ¬Even n then x * ∑ i ∈ range n, x ^ i + 1 ≤ 0 else 1 ≤ x * ∑ i ∈ range n, x ^ i + 1