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 : 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)
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 → 0 ≤ x + 1
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)
rw₇ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → ¬x + 1 < 0
rw₈ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 ≤ x + 1
⊢ 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 → 0 < x + 1 ∨ 0 = x + 1
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)
rw₇ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → ¬x + 1 < 0
rw₈ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 ≤ x + 1
rw₉ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw₁₀ : (¬Even n ∨ 0 < x + 1) ∨ 0 = x + 1 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
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)
rw₇ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → ¬x + 1 < 0
rw₈ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 ≤ x + 1
rw₉ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₀ : (¬Even n ∨ 0 < x + 1) ∨ 0 = x + 1 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw₁₁ : (Even n → 0 < x + 1) ∨ 0 = x + 1 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
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)
rw₇ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → ¬x + 1 < 0
rw₈ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 ≤ x + 1
rw₉ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₀ : (¬Even n ∨ 0 < x + 1) ∨ 0 = x + 1 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₁ : (Even n → 0 < x + 1) ∨ 0 = x + 1 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw₁₂ : 0 = x + 1 ∧ Even n ∨ (Even n → 0 < x + 1) ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
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)
rw₇ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → ¬x + 1 < 0
rw₈ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 ≤ x + 1
rw₉ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₀ : (¬Even n ∨ 0 < x + 1) ∨ 0 = x + 1 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₁ : (Even n → 0 < x + 1) ∨ 0 = x + 1 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₂ : 0 = x + 1 ∧ Even n ∨ (Even n → 0 < x + 1) ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw₁₃ : Even n ∧ 0 = x + 1 ∨ (Even n → 0 < x + 1) ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
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)
rw₇ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → ¬x + 1 < 0
rw₈ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 ≤ x + 1
rw₉ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₀ : (¬Even n ∨ 0 < x + 1) ∨ 0 = x + 1 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₁ : (Even n → 0 < x + 1) ∨ 0 = x + 1 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₂ : 0 = x + 1 ∧ Even n ∨ (Even n → 0 < x + 1) ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₃ : Even n ∧ 0 = x + 1 ∨ (Even n → 0 < x + 1) ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw₁₄ : Even n → 0 = x + 1 ∨ 0 < x + 1 ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
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)
rw₇ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → ¬x + 1 < 0
rw₈ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 ≤ x + 1
rw₉ : (¬Even n ∨ 0 < x + 1) ∨ x + 1 = 0 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₀ : (¬Even n ∨ 0 < x + 1) ∨ 0 = x + 1 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₁ : (Even n → 0 < x + 1) ∨ 0 = x + 1 ∧ Even n ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₂ : 0 = x + 1 ∧ Even n ∨ (Even n → 0 < x + 1) ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₃ : Even n ∧ 0 = x + 1 ∨ (Even n → 0 < x + 1) ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
rw₁₄ : Even n → 0 = x + 1 ∨ 0 < x + 1 ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
⊢ LT.lt.{u_1} (α := R) (∑ i ∈ range n, x ^ i) 0 ↔ Even n ∧ x + 1 < 0
have rw₁₅ : Even n → 0 < x + 1 ∨ 0 = x + 1 ↔ Even n → 0 < x + 1 ∨ 0 = x + 1
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:
a b n : ℕ
⊢ (b - 1) * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
have rw : b * ∑ i ∈ range n.succ, a / b ^ i - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
  ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
Tactic: rw [Nat.sub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
        Nat.div_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
a b n : ℕ
rw :
  b * ∑ i ∈ range n.succ, a / b ^ i - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
⊢ (b - 1) * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
have rw₁ : (∑ i ∈ range n.succ, a / b ^ i) * b - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
  ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
Tactic: rw [Nat.sub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
        Nat.div_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
a b n : ℕ
rw :
  b * ∑ i ∈ range n.succ, a / b ^ i - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₁ :
  (∑ i ∈ range n.succ, a / b ^ i) * b - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
⊢ (b - 1) * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
have rw₂ : ∑ i ∈ range n.succ, a / b ^ i * b - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
  ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
Tactic: rw [Nat.sub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
        Nat.div_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
a b n : ℕ
rw :
  b * ∑ i ∈ range n.succ, a / b ^ i - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₁ :
  (∑ i ∈ range n.succ, a / b ^ i) * b - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₂ :
  ∑ i ∈ range n.succ, a / b ^ i * b - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
⊢ (b - 1) * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
have rw₃ : HSub.hSub (α := ℕ) (∑ i ∈ range n.succ, a / b ^ i * b) (∑ i ∈ range n.succ, a / b ^ i) =
  ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
Tactic: rw [Nat.sub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
        Nat.div_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
a b n : ℕ
rw :
  b * ∑ i ∈ range n.succ, a / b ^ i - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₁ :
  (∑ i ∈ range n.succ, a / b ^ i) * b - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₂ :
  ∑ i ∈ range n.succ, a / b ^ i * b - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₃ :
  HSub.hSub (α := ℕ) (∑ i ∈ range n.succ, a / b ^ i * b) (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
⊢ (b - 1) * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
have rw₄ : ∑ k ∈ range n, a / b ^ (k + 1) * b + a / HPow.hPow (β := ℕ) b 0 * b - ∑ i ∈ range n.succ, a / b ^ i =
  ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
Tactic: rw [Nat.sub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
        Nat.div_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
a b n : ℕ
rw :
  b * ∑ i ∈ range n.succ, a / b ^ i - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₁ :
  (∑ i ∈ range n.succ, a / b ^ i) * b - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₂ :
  ∑ i ∈ range n.succ, a / b ^ i * b - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₃ :
  HSub.hSub (α := ℕ) (∑ i ∈ range n.succ, a / b ^ i * b) (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₄ :
  ∑ k ∈ range n, a / b ^ (k + 1) * b + a / HPow.hPow (β := ℕ) b 0 * b - ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
⊢ (b - 1) * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
have rw₅ : ∑ k ∈ range n, a / b ^ (k + 1) * b + a / HPow.hPow (β := ℕ) b 0 * b - (∑ x ∈ range n, a / b ^ x + a / b ^ n) =
  ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
Tactic: rw [Nat.sub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
        Nat.div_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
a b n : ℕ
rw :
  b * ∑ i ∈ range n.succ, a / b ^ i - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₁ :
  (∑ i ∈ range n.succ, a / b ^ i) * b - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₂ :
  ∑ i ∈ range n.succ, a / b ^ i * b - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₃ :
  HSub.hSub (α := ℕ) (∑ i ∈ range n.succ, a / b ^ i * b) (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₄ :
  ∑ k ∈ range n, a / b ^ (k + 1) * b + a / HPow.hPow (β := ℕ) b 0 * b - ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₅ :
  ∑ k ∈ range n, a / b ^ (k + 1) * b + a / HPow.hPow (β := ℕ) b 0 * b - (∑ x ∈ range n, a / b ^ x + a / b ^ n) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
⊢ (b - 1) * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
have rw₆ : ∑ k ∈ range n, a / b ^ (k + 1) * b + a / 1 * b - (∑ x ∈ range n, a / b ^ x + a / b ^ n) =
  ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
Tactic: rw [Nat.sub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
        Nat.div_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
a b n : ℕ
rw :
  b * ∑ i ∈ range n.succ, a / b ^ i - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₁ :
  (∑ i ∈ range n.succ, a / b ^ i) * b - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₂ :
  ∑ i ∈ range n.succ, a / b ^ i * b - HMul.hMul (α := ℕ) 1 (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₃ :
  HSub.hSub (α := ℕ) (∑ i ∈ range n.succ, a / b ^ i * b) (∑ i ∈ range n.succ, a / b ^ i) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₄ :
  ∑ k ∈ range n, a / b ^ (k + 1) * b + a / HPow.hPow (β := ℕ) b 0 * b - ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₅ :
  ∑ k ∈ range n, a / b ^ (k + 1) * b + a / HPow.hPow (β := ℕ) b 0 * b - (∑ x ∈ range n, a / b ^ x + a / b ^ n) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
rw₆ :
  ∑ k ∈ range n, a / b ^ (k + 1) * b + a / 1 * b - (∑ x ∈ range n, a / b ^ x + a / b ^ n) =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
⊢ (b - 1) * ∑ i ∈ range n.succ, a / b ^ i =
    ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
have rw₇ : ∑ k ∈ range n, a / b ^ (k + 1) * b + a * b - (∑ x ∈ range n, a / b ^ x + a / b ^ n) =
  ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
Tactic: rw [Nat.sub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
        Nat.div_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
a b n : ℕ
⊢ ∑ i ∈ range n, a / b ^ (i + 1) * b + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n) ≤
    ∑ i ∈ range n, a / b ^ i + a * b - (∑ i ∈ range n, a / b ^ i + a / b ^ n)
have h : ∀ (i : ℕ) (hi : i ∈ range n), a / b ^ (i + 1) * b ≤ a / b ^ i
Tactic: gcongr with i hi
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
a b n i : ℕ
hi : i ∈ range n
⊢ a / b ^ (i + 1) * b ≤ a / b ^ i
have h : a / b ^ i / b * b ≤ a / b ^ i
Tactic: rw [pow_succ, ← Nat.div_div_eq_div_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i ∈ range n, a / b ^ i ≤ a * b / (b - 1)
have refine : (∑ i ∈ range n, a / b ^ i) * (b - 1) ≤ a * b
Tactic: refine (Nat.le_div_iff_mul_le <| tsub_pos_of_lt hb).2 ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ (∑ i ∈ range 0, a / b ^ i) * (b - 1) ≤ a * b
have zero : 0 ≤ a * b
Tactic: rw [sum_range_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (∑ i ∈ range (n + 1), a / b ^ i) * (b - 1) ≤ a * b
have succ : (b - 1) * ∑ i ∈ range (n + 1), a / b ^ i ≤ a * b
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i ∈ Ico 1 n, a / b ^ i ≤ a / (b - 1)
have zero : ∑ i ∈ Ico 1 0, a / b ^ i ≤ a / (b - 1)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
zero : ∑ i ∈ Ico 1 0, a / b ^ i ≤ a / (b - 1)
⊢ ∑ i ∈ Ico 1 n, a / b ^ i ≤ a / (b - 1)
have succ : ∀ (n : ℕ), ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a / (b - 1)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.GeomSum (goal)
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a / (b - 1)
have succ : a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)
Tactic: rw [← add_le_add_iff_left a]