case refine'_1
α : Type u
β : Type ?u.247460
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : 0 < ∑ i in range n, x ^ i
⊢ Odd n ∨ 0 < x + 1

case refine'_2
α : Type u
β : Type ?u.247460
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ Odd n ∨ 0 < x + 1 → 0 < ∑ i in range n, x ^ i
α : Type u
β : Type ?u.247460
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ 0 < ∑ i in range n, x ^ i ↔ Odd n ∨ 0 < x + 1
refine' ⟨fun h => _, _⟩
case refine'_1
α : Type u
β : Type ?u.247460
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : 0 < ∑ i in range n, x ^ i
⊢ Even n → ¬x + 1 ≤ 0
case refine'_1
α : Type u
β : Type ?u.247460
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : 0 < ∑ i in range n, x ^ i
⊢ Odd n ∨ 0 < x + 1
rw [or_iff_not_imp_left, ← not_le, ← Nat.even_iff_not_odd]
case refine'_1
α : Type u
β : Type ?u.247460
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
h : 0 < ∑ i in range n, x ^ i
hn : Even n
hx : x + 1 ≤ 0
⊢ ∑ i in range n, x ^ i ≤ 0
case refine'_1
α : Type u
β : Type ?u.247460
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : 0 < ∑ i in range n, x ^ i
⊢ Even n → ¬x + 1 ≤ 0
refine' fun hn hx => h.not_le _
no goals
case refine'_1
α : Type u
β : Type ?u.247460
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
h : 0 < ∑ i in range n, x ^ i
hn : Even n
hx : x + 1 ≤ 0
⊢ ∑ i in range n, x ^ i ≤ 0
simpa [if_pos hn] using geom_sum_alternating_of_le_neg_one hx n
case refine'_2.inl
α : Type u
β : Type ?u.247460
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
hn : Odd n
⊢ 0 < ∑ i in range n, x ^ i

case refine'_2.inr
α : Type u
β : Type ?u.247460
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
hx' : 0 < x + 1
⊢ 0 < ∑ i in range n, x ^ i
case refine'_2
α : Type u
β : Type ?u.247460
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ Odd n ∨ 0 < x + 1 → 0 < ∑ i in range n, x ^ i
rintro (hn | hx')
no goals
case refine'_2.inl
α : Type u
β : Type ?u.247460
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
hn : Odd n
⊢ 0 < ∑ i in range n, x ^ i
exact hn.geom_sum_pos
no goals
case refine'_2.inr
α : Type u
β : Type ?u.247460
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
hx' : 0 < x + 1
⊢ 0 < ∑ i in range n, x ^ i
exact geom_sum_pos' hx' hn