awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
n_1 : ℕ
x : R
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn : 2 ≤ n
hn' : ¬Even n
ihn : LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n, x ^ i)
⊢ x * ∑ i ∈ range n, x ^ i + 1 < x + 1
have neg : x * ∑ i ∈ range n, x ^ i < x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : 0 < x + 1
hn : n ≠ 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
have zero : ∀ (hn : Ne (α := ℕ) 0 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 0, x ^ i)
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : 0 < x + 1
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 0, x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
have succ : ∀ (hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), x ^ i)
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : 0 < x + 1
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 0, x ^ i)
succ : ∀ (hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
have succ₁ : ∀ (n : ℕ) (hn : n + 1 + 1 ≠ 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1 + 1), x ^ i)
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1 + 1), x ^ i)
have succ : ∀ (hx' : x < 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1 + 1), x ^ i)
Tactic: obtain hx' | hx' := lt_or_ge x 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : 0 < x + 1
n : ℕ
hn : n + 1 + 1 ≠ 0
succ : ∀ (hx' : x < 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1 + 1), x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1 + 1), x ^ i)
have succ₁ : ∀ (hx' : 0 ≤ x), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (n + 1 + 1), x ^ i)
Tactic: obtain hx' | hx' := lt_or_ge x 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
h : Odd n
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
have zero : ∀ (h : Odd (α := ℕ) 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 0, x ^ i)
Tactic: rcases n with (_ | _ | k)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
h : Odd n
zero : ∀ (h : Odd (α := ℕ) 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 0, x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
have succ : ∀ (h : Odd (HAdd.hAdd (α := ℕ) 0 1)), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), x ^ i)
Tactic: rcases n with (_ | _ | k)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
h : Odd n
zero : ∀ (h : Odd (α := ℕ) 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range 0, x ^ i)
succ : ∀ (h : Odd (HAdd.hAdd (α := ℕ) 0 1)), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
have succ₁ : ∀ (k : ℕ) (h : Odd (k + 1 + 1)), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
Tactic: rcases n with (_ | _ | k)
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : Odd (k + 1 + 1)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
have h₁ : ¬Even (k + 1 + 1)
Tactic: rw [← Nat.not_even_iff_odd] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
have succ : ∀ (hx : x + 1 < 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
Tactic: rcases lt_trichotomy (x + 1) 0 with (hx | hx | hx)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
succ : ∀ (hx : x + 1 < 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
have succ₁ : ∀ (hx : x + 1 = 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
Tactic: rcases lt_trichotomy (x + 1) 0 with (hx | hx | hx)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
succ : ∀ (hx : x + 1 < 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
succ₁ : ∀ (hx : x + 1 = 0), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
have succ₂ : ∀ (hx : 0 < x + 1), LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
Tactic: rcases lt_trichotomy (x + 1) 0 with (hx | hx | hx)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
have this : if Even k.succ.succ then LT.lt.{u_1} (α := R) (∑ i ∈ range k.succ.succ, x ^ i) 0
else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range k.succ.succ, x ^ i)
Tactic: have := geom_sum_alternating_of_lt_neg_one hx k.one_lt_succ_succ
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
k : ℕ
h : ¬Even (k + 1 + 1)
hx : x + 1 < 0
this :
  if Even k.succ.succ then LT.lt.{u_1} (α := R) (∑ i ∈ range k.succ.succ, x ^ i) 0
  else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range k.succ.succ, x ^ i)
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range (k + 1 + 1), x ^ i)
have this₁ : LT.lt.{u_1} (α := R) 1 (∑ i ∈ range k.succ.succ, x ^ i)
Tactic: simp only [h, if_false] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ Odd n ∨ 0 < x + 1
have refine_1 : ∀ (h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)), Odd n ∨ 0 < x + 1
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
refine_1 : ∀ (h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)), Odd n ∨ 0 < x + 1
⊢ LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ Odd n ∨ 0 < x + 1
have refine_2 : Odd n ∨ 0 < x + 1 → LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
⊢ Odd n ∨ 0 < x + 1
have refine_1 : Even n → ¬x + 1 ≤ 0
Tactic: rw [or_iff_not_imp_left, ← not_le, Nat.not_odd_iff_even]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i)
⊢ Even n → ¬x + 1 ≤ 0
have refine_1 : ∀ (hn : Even n) (hx : x + 1 ≤ 0), LE.le.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0
Tactic: refine fun hn hx => h.not_ge ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : x ≠ -1
hn : n ≠ 0
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0
have zero : ∀ (hn : Ne (α := ℕ) 0 0), Ne.{u_1 + 1} (α := R) (∑ i ∈ range 0, x ^ i) 0
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : x ≠ -1
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), Ne.{u_1 + 1} (α := R) (∑ i ∈ range 0, x ^ i) 0
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0
have succ : ∀ (hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0), Ne.{u_1 + 1} (α := R) (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), x ^ i) 0
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hx : x ≠ -1
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), Ne.{u_1 + 1} (α := R) (∑ i ∈ range 0, x ^ i) 0
succ : ∀ (hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0), Ne.{u_1 + 1} (α := R) (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), x ^ i) 0
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0
have succ₁ : ∀ (n : ℕ) (hn : n + 1 + 1 ≠ 0), Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : x ≠ -1
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
have succ : ∀ (hx : x + 1 ≠ 0) (n : ℕ) (hn : n + 1 + 1 ≠ 0), Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
Tactic: rw [Ne, eq_neg_iff_add_eq_zero, ← Ne] at hx
Cleared hypotheses: hx, n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
have succ : ∀ (h : x + 1 < 0), Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
Tactic: obtain h | h := hx.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
succ : ∀ (h : x + 1 < 0), Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
have succ₁ : ∀ (h : 0 < x + 1), Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
Tactic: obtain h | h := hx.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
have this : if Even n.succ.succ then LT.lt.{u_1} (α := R) (∑ i ∈ range n.succ.succ, x ^ i) 0
else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n.succ.succ, x ^ i)
Tactic: have := geom_sum_alternating_of_lt_neg_one h n.one_lt_succ_succ
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
this :
  if Even n.succ.succ then LT.lt.{u_1} (α := R) (∑ i ∈ range n.succ.succ, x ^ i) 0
  else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n.succ.succ, x ^ i)
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
have pos : Even n.succ.succ →
  ∀ (this : LT.lt.{u_1} (α := R) (∑ i ∈ range n.succ.succ, x ^ i) 0),
    Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
Tactic: split_ifs at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : x + 1 ≠ 0
n : ℕ
hn : n + 1 + 1 ≠ 0
h : x + 1 < 0
this :
  if Even n.succ.succ then LT.lt.{u_1} (α := R) (∑ i ∈ range n.succ.succ, x ^ i) 0
  else LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n.succ.succ, x ^ i)
pos :
  Even n.succ.succ →
    ∀ (this : LT.lt.{u_1} (α := R) (∑ i ∈ range n.succ.succ, x ^ i) 0),
      Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
have neg : ¬Even n.succ.succ →
  ∀ (this : LT.lt.{u_1} (α := R) 1 (∑ i ∈ range n.succ.succ, x ^ i)),
    Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0
Tactic: split_ifs at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ x = -1 ∧ Even n
have refine : ∀ (h : Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0), x = -1 ∧ Even n
Tactic: refine ⟨fun h => ?_, @fun ⟨h, hn⟩ => by simp only [h, hn, neg_one_geom_sum, if_true]⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0
⊢ x = -1 ∧ Even n
have contrapose! : ∀ (h : ∀ (_ : x = -1), ¬Even n), Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : ∀ (_ : x = -1), ¬Even n
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0
have hx : x = -1 ∨ x ≠ -1
Tactic: have hx := eq_or_ne x (-1)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : ∀ (_ : x = -1), ¬Even n
hx : x = -1 ∨ x ≠ -1
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0
have inl : ∀ (hx : x = -1), Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : ∀ (_ : x = -1), ¬Even n
hx : x = -1 ∨ x ≠ -1
inl : ∀ (hx : x = -1), Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0
have inr : ∀ (hx : x ≠ -1), Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0
Tactic: rcases hx with hx | hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
h : ∀ (_ : x = -1), ¬Even n
hx : x = -1
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0
have inl : Ne.{u_1 + 1} (α := R) (if Even n then 0 else 1) 0
Tactic: rw [hx, neg_one_geom_sum]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw : ¬LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ ¬(Even n ∧ x + 1 < 0)
Tactic: rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm,
    or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), ← Nat.not_even_iff_odd, ←
    add_eq_zero_iff_eq_neg, not_and, not_lt, le_iff_lt_or_eq, eq_comm, ← imp_iff_not_or, or_comm,
    and_comm, Decidable.and_or_imp, or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
rw : ¬LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ ¬(Even n ∧ x + 1 < 0)
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw₁ : LE.le.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ ¬(Even n ∧ x + 1 < 0)
Tactic: rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm,
    or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), ← Nat.not_even_iff_odd, ←
    add_eq_zero_iff_eq_neg, not_and, not_lt, le_iff_lt_or_eq, eq_comm, ← imp_iff_not_or, or_comm,
    and_comm, Decidable.and_or_imp, or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
rw : ¬LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ ¬(Even n ∧ x + 1 < 0)
rw₁ : LE.le.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ ¬(Even n ∧ x + 1 < 0)
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw₂ : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∨ Eq.{u_1 + 1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ ¬(Even n ∧ x + 1 < 0)
Tactic: rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm,
    or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), ← Nat.not_even_iff_odd, ←
    add_eq_zero_iff_eq_neg, not_and, not_lt, le_iff_lt_or_eq, eq_comm, ← imp_iff_not_or, or_comm,
    and_comm, Decidable.and_or_imp, or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
rw : ¬LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ ¬(Even n ∧ x + 1 < 0)
rw₁ : LE.le.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ ¬(Even n ∧ x + 1 < 0)
rw₂ :
  LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∨ Eq.{u_1 + 1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ ¬(Even n ∧ x + 1 < 0)
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw₃ : LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∨ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ ¬(Even n ∧ x + 1 < 0)
Tactic: rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm,
    or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), ← Nat.not_even_iff_odd, ←
    add_eq_zero_iff_eq_neg, not_and, not_lt, le_iff_lt_or_eq, eq_comm, ← imp_iff_not_or, or_comm,
    and_comm, Decidable.and_or_imp, or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
rw : ¬LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ ¬(Even n ∧ x + 1 < 0)
rw₁ : LE.le.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ ¬(Even n ∧ x + 1 < 0)
rw₂ :
  LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∨ Eq.{u_1 + 1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ ¬(Even n ∧ x + 1 < 0)
rw₃ :
  LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∨ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ ¬(Even n ∧ x + 1 < 0)
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw₄ : (Odd n ∨ 0 < x + 1) ∨ x = -1 ∧ Even n ↔ ¬(Even n ∧ x + 1 < 0)
Tactic: rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm,
    or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), ← Nat.not_even_iff_odd, ←
    add_eq_zero_iff_eq_neg, not_and, not_lt, le_iff_lt_or_eq, eq_comm, ← imp_iff_not_or, or_comm,
    and_comm, Decidable.and_or_imp, or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
rw : ¬LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ ¬(Even n ∧ x + 1 < 0)
rw₁ : LE.le.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ ¬(Even n ∧ x + 1 < 0)
rw₂ :
  LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∨ Eq.{u_1 + 1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ ¬(Even n ∧ x + 1 < 0)
rw₃ :
  LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∨ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ ¬(Even n ∧ x + 1 < 0)
rw₄ : (Odd n ∨ 0 < x + 1) ∨ x = -1 ∧ Even n ↔ ¬(Even n ∧ x + 1 < 0)
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw₅ : (¬Even n ∨ 0 < x + 1) ∨ x = -1 ∧ Even n ↔ ¬(Even n ∧ x + 1 < 0)
Tactic: rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm,
    or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), ← Nat.not_even_iff_odd, ←
    add_eq_zero_iff_eq_neg, not_and, not_lt, le_iff_lt_or_eq, eq_comm, ← imp_iff_not_or, or_comm,
    and_comm, Decidable.and_or_imp, or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
rw : ¬LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ ¬(Even n ∧ x + 1 < 0)
rw₁ : LE.le.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ ¬(Even n ∧ x + 1 < 0)
rw₂ :
  LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∨ Eq.{u_1 + 1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ ¬(Even n ∧ x + 1 < 0)
rw₃ :
  LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∨ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ ¬(Even n ∧ x + 1 < 0)
rw₄ : (Odd n ∨ 0 < x + 1) ∨ x = -1 ∧ Even n ↔ ¬(Even n ∧ x + 1 < 0)
rw₅ : (¬Even n ∨ 0 < x + 1) ∨ x = -1 ∧ Even n ↔ ¬(Even n ∧ x + 1 < 0)
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw₆ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ ¬(Even n ∧ x + 1 < 0)
Tactic: rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm,
    or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), ← Nat.not_even_iff_odd, ←
    add_eq_zero_iff_eq_neg, not_and, not_lt, le_iff_lt_or_eq, eq_comm, ← imp_iff_not_or, or_comm,
    and_comm, Decidable.and_or_imp, or_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
rw : ¬LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ ¬(Even n ∧ x + 1 < 0)
rw₁ : LE.le.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ ¬(Even n ∧ x + 1 < 0)
rw₂ :
  LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∨ Eq.{u_1 + 1} (α := R) 0 (∑ i ∈ range n, x ^ i) ↔ ¬(Even n ∧ x + 1 < 0)
rw₃ :
  LT.lt.{u_1} (α := R) 0 (∑ i ∈ range n, x ^ i) ∨ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ ¬(Even n ∧ x + 1 < 0)
rw₄ : (Odd n ∨ 0 < x + 1) ∨ x = -1 ∧ Even n ↔ ¬(Even n ∧ x + 1 < 0)
rw₅ : (¬Even n ∨ 0 < x + 1) ∨ x = -1 ∧ Even n ↔ ¬(Even n ∧ x + 1 < 0)
rw₆ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ ¬(Even n ∧ x + 1 < 0)
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw₇ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → ¬x + 1 < 0
Tactic: rw [← not_iff_not, not_lt, le_iff_lt_or_eq, eq_comm,
    or_congr (geom_sum_pos_iff hn) (geom_sum_eq_zero_iff_neg_one hn), ← Nat.not_even_iff_odd, ←
    add_eq_zero_iff_eq_neg, not_and, not_lt, le_iff_lt_or_eq, eq_comm, ← imp_iff_not_or, or_comm,
    and_comm, Decidable.and_or_imp, or_comm]