awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
x : R
hx : x ≠ -1
hn : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), x ^ i) 0

Tactic:
simp only [zero_add, range_one, sum_singleton, pow_zero, ne_eq, one_ne_zero, not_false_eq_true]

Premises used: zero_add, ne_eq, pow_zero, Finset.sum_singleton, Finset.range_one, one_ne_zero, not_false_eq_true
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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
succ : ∀ (hx : x + 1 ≠ 0) (n : ℕ) (hn : n + 1 + 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

Tactic:
rw [Ne, eq_neg_iff_add_eq_zero, ← Ne] at hx

Premises used: Ne, eq_neg_iff_add_eq_zero
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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
succ₁ : ∀ (h : 0 < x + 1), 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

Tactic:
obtain h | h := hx.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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
⊢ 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
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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
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
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0

Tactic:
split_ifs at this
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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
h_1 : 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:
this.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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
h_1 : 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:
exact this.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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
h_1 : ¬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:
(zero_lt_one.trans this).ne'

Premises used: LT.lt.ne', zero_lt_one, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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
h_1 : ¬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:
exact (zero_lt_one.trans this).ne'

Premises used: LT.lt.ne', zero_lt_one, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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 : 0 < x + 1
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0

Tactic:
(geom_sum_pos' h n.succ.succ_ne_zero).ne'

Premises used: LT.lt.ne', Nat.succ_ne_zero, Nat.succ, geom_sum_pos'
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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 : 0 < x + 1
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1 + 1), x ^ i) 0

Tactic:
exact (geom_sum_pos' h n.succ.succ_ne_zero).ne'

Premises used: LT.lt.ne', Nat.succ_ne_zero, Nat.succ, geom_sum_pos'
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn_1 : n ≠ 0
h_1 : x = -1 ∧ Even n
h : x = -1
hn : Even n
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0

Tactic:
simp only [h, hn, neg_one_geom_sum, if_true]

Premises used: if_true, neg_one_geom_sum
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
n : ℕ
x : R
hn : n ≠ 0
refine : ∀ (h : Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0), x = -1 ∧ Even n
⊢ 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]⟩
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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
contrapose! : ∀ (h : ∀ (_ : x = -1), ¬Even n), Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0
⊢ x = -1 ∧ Even n

Tactic:
contrapose! h
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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
⊢ x = -1 ∨ x ≠ -1

Tactic:
have hx := eq_or_ne x (-1)
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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
inr : ∀ (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

Tactic:
rcases hx with hx | hx
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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
inl : Ne.{u_1 + 1} (α := R) (if Even n then 0 else 1) 0
⊢ Ne.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i) 0

Tactic:
rw [hx, neg_one_geom_sum]

Premises used: neg_one_geom_sum
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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) (if Even n then 0 else 1) 0

Tactic:
simp only [h hx, ite_false, ne_eq, one_ne_zero, not_false_eq_true]

Premises used: ite_false, ne_eq, one_ne_zero, not_false_eq_true
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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

Tactic:
geom_sum_ne_zero hx hn

Premises used: geom_sum_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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

Tactic:
exact geom_sum_ne_zero hx hn

Premises used: geom_sum_ne_zero
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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
rw₁₅ 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

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]

Premises used: not_iff_not, or_congr, geom_sum_pos_iff, add_eq_zero_iff_eq_neg, Nat.not_even_iff_odd, and_comm, eq_comm, imp_iff_not_or, geom_sum_eq_zero_iff_neg_one, le_iff_lt_or_eq, not_lt, or_comm, not_and, Decidable.and_or_imp
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
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)
rw₇ 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)
⊢ (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)

Tactic:
rw [Nat.sub_mul, mul_comm, sum_mul, one_mul, sum_range_succ', sum_range_succ, pow_zero,
        Nat.div_one]

Premises used: Nat.div_one, pow_zero, Nat.sub_mul, mul_comm, Finset.sum_range_succ', Finset.sum_range_succ, one_mul, Finset.sum_mul
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
a b n : ℕ
h : ∀ (i : ℕ) (hi : i ∈ range n), a / b ^ (i + 1) * b ≤ a / b ^ i
⊢ ∑ 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)

Tactic:
gcongr with i hi
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
a b n i : ℕ
hi : i ∈ range n
h : a / b ^ i / b * b ≤ a / b ^ i
⊢ a / b ^ (i + 1) * b ≤ a / b ^ i

Tactic:
rw [pow_succ, ← Nat.div_div_eq_div_mul]

Premises used: pow_succ, Nat.div_div_eq_div_mul
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
a b n i : ℕ
hi : i ∈ range n
⊢ a / b ^ i / b * b ≤ a / b ^ i

Tactic:
Nat.div_mul_le_self _ _

Premises used: Nat.div_mul_le_self
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
a b n i : ℕ
hi : i ∈ range n
⊢ a / b ^ i / b * b ≤ a / b ^ i

Tactic:
exact Nat.div_mul_le_self _ _

Premises used: Nat.div_mul_le_self
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i ∈ range n, a / b ^ i ≤ a * b / (b - 1)

Tactic:
(Nat.le_div_iff_mul_le <| tsub_pos_of_lt hb).2 ?_

Premises used: Iff.mpr, Nat.le_div_iff_mul_le, tsub_pos_of_lt
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
refine : (∑ i ∈ range n, a / b ^ i) * (b - 1) ≤ a * b
⊢ ∑ i ∈ range n, a / b ^ i ≤ a * b / (b - 1)

Tactic:
refine (Nat.le_div_iff_mul_le <| tsub_pos_of_lt hb).2 ?_

Premises used: Iff.mpr, Nat.le_div_iff_mul_le, tsub_pos_of_lt
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a : ℕ
zero : 0 ≤ a * b
⊢ (∑ i ∈ range 0, a / b ^ i) * (b - 1) ≤ a * b

Tactic:
rw [sum_range_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, Finset.sum_range_zero
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a * b

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a * b

Tactic:
exact Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
succ : (b - 1) * ∑ i ∈ range (n + 1), a / b ^ i ≤ a * b
⊢ (∑ i ∈ range (n + 1), a / b ^ i) * (b - 1) ≤ a * b

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (b - 1) * ∑ i ∈ range (n + 1), a / b ^ i ≤ a * b

Tactic:
(Nat.pred_mul_geom_sum_le a b n).trans tsub_le_self

Premises used: Nat.pred_mul_geom_sum_le, tsub_le_self, LE.le.trans
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ (b - 1) * ∑ i ∈ range (n + 1), a / b ^ i ≤ a * b

Tactic:
exact (Nat.pred_mul_geom_sum_le a b n).trans tsub_le_self

Premises used: Nat.pred_mul_geom_sum_le, tsub_le_self, LE.le.trans
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
zero : ∑ i ∈ Ico 1 0, a / b ^ i ≤ a / (b - 1)
succ : ∀ (n : ℕ), ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a / (b - 1)
⊢ ∑ i ∈ Ico 1 n, a / b ^ i ≤ a / (b - 1)

Tactic:
rcases n with - | n
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ LE.le (α := ℕ) 0 1

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a / (b - 1)

Tactic:
Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a : ℕ
⊢ 0 ≤ a / (b - 1)

Tactic:
exact Nat.zero_le _

Premises used: Nat.zero_le
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
succ : a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)
⊢ ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a / (b - 1)

Tactic:
rw [← add_le_add_iff_left a]

Premises used: add_le_add_iff_left
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
rw : a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / 1 + ∑ i ∈ Ico 1 n.succ, a / b ^ i
rw₁ rw₂ : a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a + ∑ i ∈ Ico 1 n.succ, a / b ^ i
⊢ a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i

Tactic:
rw [pow_zero, Nat.div_one]

Premises used: Nat.div_one, pow_zero
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
rw :
  a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i =
    a / HPow.hPow (β := ℕ) b 0 + ∑ x ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) n.succ, a / b ^ x
rw₁ : 0 ∉ Ico (HAdd.hAdd (α := ℕ) 0 1) n.succ
⊢ a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = ∑ i ∈ range n.succ, a / b ^ i

Tactic:
rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert]

Premises used: Finset.insert_Ico_add_one_left_eq_Ico, Nat.succ_pos, Finset.range_eq_Ico, Finset.sum_insert
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i =
    a / HPow.hPow (β := ℕ) b 0 + ∑ x ∈ Ico (HAdd.hAdd (α := ℕ) 0 1) n.succ, a / b ^ x

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ 0 ∉ Ico (HAdd.hAdd (α := ℕ) 0 1) n.succ

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ ∑ i ∈ range n.succ, a / b ^ i ≤ a * b / (b - 1)

Tactic:
Nat.geom_sum_le hb a _

Premises used: Nat.geom_sum_le
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
⊢ 1 ≤ b

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
rw : a * b / (b - 1) = a * (1 + (b - 1)) / (b - 1)
rw₁ rw₂ : a * b / (b - 1) = a * b / (b - 1)
⊢ a * b / (b - 1) = (a * 1 + a * (b - 1)) / (b - 1)

Tactic:
rw [← mul_add, add_tsub_cancel_of_le (by lia)]

Premises used: mul_add, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
rw : (a + a * (b - 1)) / (b - 1) = a + a / (b - 1)
rw₁ : a / (b - 1) + a = a + a / (b - 1)
rw₂ rw₃ : a + a / (b - 1) = a + a / (b - 1)
⊢ (a * 1 + a * (b - 1)) / (b - 1) = a + a / (b - 1)

Tactic:
rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]

Premises used: add_comm, Nat.add_mul_div_right, mul_one, tsub_pos_of_lt
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
b : ℕ
hb : 2 ≤ b
a n : ℕ
i : a + ∑ i ∈ Ico 1 n.succ, a / b ^ i = a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i
i₁ : a / HPow.hPow (β := ℕ) b 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i = ∑ i ∈ range n.succ, a / b ^ i
i₂ : a * b / (b - 1) = (a * 1 + a * (b - 1)) / (b - 1)
i₃ : (a * 1 + a * (b - 1)) / (b - 1) = a + a / (b - 1)
⊢ a + ∑ i ∈ Ico 1 (n + 1), a / b ^ i ≤ a + a / (b - 1)

Tactic:
calc
    (a + ∑ i ∈ Ico 1 n.succ, a / b ^ i) = a / b ^ 0 + ∑ i ∈ Ico 1 n.succ, a / b ^ i := by
      rw [pow_zero, Nat.div_one]
    _ = ∑ i ∈ range n.succ, a / b ^ i := by
      rw [range_eq_Ico, ← Finset.insert_Ico_add_one_left_eq_Ico (Nat.succ_pos _), sum_insert] <;>
        simp
    _ ≤ a * b / (b - 1) := Nat.geom_sum_le hb a _
    _ = (a * 1 + a * (b - 1)) / (b - 1) := by rw [← mul_add, add_tsub_cancel_of_le (by lia)]
    _ = a + a / (b - 1) := by rw [mul_one, Nat.add_mul_div_right _ _ (tsub_pos_of_lt hb), add_comm]

Premises used: HMul.hMul, HSub.hSub, Finset.Ico, HDiv.hDiv, Finset.range, HPow.hPow, HAdd.hAdd, Nat.geom_sum_le, OfNat.ofNat, Nat.succ, Finset.sum
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
m n : ℕ
s : Finset ℕ
hm : 2 ≤ m
hs : ∀ k ∈ s, k < n
⊢ 0 < m

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Ring.GeomSum
Goal:
m n : ℕ
s : Finset ℕ
hm : 2 ≤ m
hs : ∀ k ∈ s, k < n
⊢ LT.lt (α := ℕ) 0 1

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
rw : b = 1 * b
rw₁ rw₂ : b = b
⊢ b = (a + c) * b

Tactic:
rw [add_ac, one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
rw : a * b + c * b = c * (a + b)
rw₁ : c * a + c * b = c * (a + b)
rw₂ rw₃ : c * a + c * b = c * a + c * b
⊢ (a + c) * b = c * (a + b)

Tactic:
rw [add_mul, mul, mul_add]

Premises used: add_mul, mul_add
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : NonAssocSemiring R
a b c : R
mul : a * b = c * a
add_ab : a + b = 1
add_ac : a + c = 1
rw : c * 1 = c
rw₁ rw₂ : c = c
⊢ c * (a + b) = c

Tactic:
rw [add_ab, mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).1 = (↑b : R × R).1
⊢ a = b

Tactic:
Subtype.ext <| Prod.ext_iff.mpr ⟨eq, eq_of_mul_eq_add_eq_one a.1.1 ?_ a.2.2 ?_⟩

Premises used: Iff.mpr, Prod.ext_iff, Prod.fst, And.right, And.intro, Subtype.val, eq_of_mul_eq_add_eq_one, Subtype.property, Subtype.ext
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).1 = (↑b : R × R).1
refine_1 : (↑a : R × R).1 * (↑a : R × R).2 = (↑b : R × R).2 * (↑a : R × R).1
refine_2 : (↑a : R × R).1 + (↑b : R × R).2 = 1
⊢ a = b

Tactic:
refine Subtype.ext <| Prod.ext_iff.mpr ⟨eq, eq_of_mul_eq_add_eq_one a.1.1 ?_ a.2.2 ?_⟩

Premises used: Iff.mpr, Prod.ext_iff, Prod.fst, And.right, And.intro, Subtype.val, eq_of_mul_eq_add_eq_one, Subtype.property, Subtype.ext
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).1 = (↑b : R × R).1
refine_1 : 0 = (↑b : R × R).2 * (↑a : R × R).1
refine_1₁ : 0 = (↑a : R × R).1 * (↑b : R × R).2
refine_1₂ : 0 = (↑b : R × R).1 * (↑b : R × R).2
refine_1₃ refine_1₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (↑a : R × R).1 * (↑a : R × R).2 = (↑b : R × R).2 * (↑a : R × R).1

Tactic:
rw [a.2.1, mul_comm, eq, b.2.1]

Premises used: And.left, mul_comm, Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).1 = (↑b : R × R).1
refine_2 : (↑b : R × R).1 + (↑b : R × R).2 = 1
refine_2₁ refine_2₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ (↑a : R × R).1 + (↑b : R × R).2 = 1

Tactic:
rw [eq, b.2.2]

Premises used: And.right, Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
⊢ a = b

Tactic:
Subtype.ext <| Prod.ext_iff.mpr ⟨eq_of_mul_eq_add_eq_one a.1.2 ?_ ?_ ?_, eq⟩

Premises used: Iff.mpr, Prod.ext_iff, And.intro, Subtype.val, Prod.snd, eq_of_mul_eq_add_eq_one, Subtype.ext
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
refine_1 : (↑a : R × R).2 * (↑a : R × R).1 = (↑b : R × R).1 * (↑a : R × R).2
refine_2 : (↑a : R × R).2 + (↑a : R × R).1 = 1
refine_3 : (↑a : R × R).2 + (↑b : R × R).1 = 1
⊢ a = b

Tactic:
refine Subtype.ext <| Prod.ext_iff.mpr ⟨eq_of_mul_eq_add_eq_one a.1.2 ?_ ?_ ?_, eq⟩

Premises used: Iff.mpr, Prod.ext_iff, And.intro, Subtype.val, Prod.snd, eq_of_mul_eq_add_eq_one, Subtype.ext
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
refine_1 : (↑a : R × R).1 * (↑a : R × R).2 = (↑b : R × R).1 * (↑a : R × R).2
refine_1₁ : 0 = (↑b : R × R).1 * (↑a : R × R).2
refine_1₂ : 0 = (↑b : R × R).1 * (↑b : R × R).2
refine_1₃ refine_1₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (↑a : R × R).2 * (↑a : R × R).1 = (↑b : R × R).1 * (↑a : R × R).2

Tactic:
rw [mul_comm, a.2.1, eq, b.2.1]

Premises used: And.left, mul_comm, Subtype.property
-- Module: Mathlib.Algebra.Order.Ring.Idempotent
Goal:
R : Type u_1
inst : CommSemiring R
a b : { a : R × R // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a : R × R).2 = (↑b : R × R).2
refine_2 : (↑a : R × R).1 + (↑a : R × R).2 = 1
refine_2₁ refine_2₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ (↑a : R × R).2 + (↑a : R × R).1 = 1

Tactic:
rw [add_comm, a.2.2]

Premises used: add_comm, And.right, Subtype.property