awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
n : ℕ
h : Commute x y
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) (∑ i ∈ range n, y ^ i * x ^ (n - 1 - i))
have zero : Eq.{u_1 + 1} (α := R) (∑ i ∈ range 0, x ^ i * y ^ (HSub.hSub (α := ℕ) 0 1 - i))
  (∑ i ∈ range 0, y ^ i * x ^ (HSub.hSub (α := ℕ) 0 1 - i))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
n : ℕ
h : Commute x y
zero :
  Eq.{u_1 + 1} (α := R) (∑ i ∈ range 0, x ^ i * y ^ (HSub.hSub (α := ℕ) 0 1 - i))
    (∑ i ∈ range 0, y ^ i * x ^ (HSub.hSub (α := ℕ) 0 1 - i))
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) (∑ i ∈ range n, y ^ i * x ^ (n - 1 - i))
have succ : ∀ (n : ℕ),
  Eq.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1), x ^ i * y ^ (n + 1 - 1 - i))
    (∑ i ∈ range (n + 1), y ^ i * x ^ (n + 1 - 1 - i))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range (n + 1), x ^ i * y ^ (n + 1 - 1 - i))
    (∑ i ∈ range (n + 1), y ^ i * x ^ (n + 1 - 1 - i))
have succ : Eq.{u_1 + 1} (α := R) (∑ x_1 ∈ range (n + 1), x ^ x_1 * y ^ (n - x_1)) (∑ x_1 ∈ range (n + 1), y ^ x_1 * x ^ (n - x_1))
Tactic: simp only [Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ x_1 ∈ range (n + 1), x ^ x_1 * y ^ (n - x_1))
    (∑ x_1 ∈ range (n + 1), y ^ x_1 * x ^ (n - x_1))
have succ : Eq.{u_1 + 1} (α := R) (∑ r ∈ range (n + 1), x ^ (n - r) * y ^ (n - (n - r)))
  (∑ x_1 ∈ range (n + 1), y ^ x_1 * x ^ (n - x_1))
Tactic: rw [← Finset.sum_flip]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ r ∈ range (n + 1), x ^ (n - r) * y ^ (n - (n - r)))
    (∑ x_1 ∈ range (n + 1), y ^ x_1 * x ^ (n - x_1))
have succ : ∀ (i : ℕ) (hi : i ∈ range (n + 1)), x ^ (n - i) * y ^ (n - (n - i)) = y ^ i * x ^ (n - i)
Tactic: refine Finset.sum_congr rfl fun i hi => ?_
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : y ≤ x
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
have h : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
Tactic: apply eq_tsub_of_add_eq
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : x ≤ y
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n
have rw : (∑ j ∈ range n, x ^ (n - 1 - j) * y ^ (n - 1 - (n - 1 - j))) * (y - x) = y ^ n - x ^ n
Tactic: rw [← Finset.sum_range_reflect]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : x ≤ y
n : ℕ
⊢ (∑ j ∈ range n, x ^ (n - 1 - j) * y ^ (n - 1 - (n - 1 - j))) * (y - x) = y ^ n - x ^ n
have h : ∀ x_1 ∈ range n, x ^ (n - 1 - x_1) * y ^ (n - 1 - (n - 1 - x_1)) = y ^ x_1 * x ^ (n - 1 - x_1)
Tactic: convert! geom_sum₂_mul_of_ge hxy n using 3
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : x ≤ y
n x_1 : ℕ
h : x_1 ∈ range n
⊢ x ^ (n - 1 - x_1) * y ^ (n - 1 - (n - 1 - x_1)) = y ^ x_1 * x ^ (n - 1 - x_1)
have a : x_1 < n
Tactic: simp_all only [Finset.mem_range]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : x ≤ y
n x_1 : ℕ
h : x_1 < n
⊢ x ^ (n - 1 - x_1) * y ^ (n - 1 - (n - 1 - x_1)) = y ^ x_1 * x ^ (n - 1 - x_1)
have h : y ^ (n - 1 - (n - 1 - x_1)) * x ^ (n - 1 - x_1) = y ^ x_1 * x ^ (n - 1 - x_1)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : AddLeftReflectLE R
inst_3 : AddLeftMono R
inst_4 : ExistsAddOfLE R
inst_5 : Sub R
inst_6 : OrderedSub R
x y : R
hxy : x ≤ y
n x_1 : ℕ
h : x_1 < n
⊢ y ^ (n - 1 - (n - 1 - x_1)) * x ^ (n - 1 - x_1) = y ^ x_1 * x ^ (n - 1 - x_1)
have h : n - 1 - (n - 1 - x_1) = x_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
k : ℕ
hk : Eq.{u_1 + 1} (α := R) (∑ i ∈ range k, HPow.hPow (α := R) (-1) i) (if Even k then 0 else 1)
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range (k + 1), HPow.hPow (α := R) (-1) i) (if Even (k + 1) then 0 else 1)
have succ : (HPow.hPow (α := R) (-1) k + if Even k then 0 else 1) = if ¬Even k then 0 else 1
Tactic: simp only [geom_sum_succ', Nat.even_add_one, hk]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
k : ℕ
hk : Eq.{u_1 + 1} (α := R) (∑ i ∈ range k, HPow.hPow (α := R) (-1) i) (if Even k then 0 else 1)
⊢ (HPow.hPow (α := R) (-1) k + if Even k then 0 else 1) = if ¬Even k then 0 else 1
have pos : ∀ (h : Even k), HPow.hPow (α := R) (-1) k + 0 = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
k : ℕ
hk : Eq.{u_1 + 1} (α := R) (∑ i ∈ range k, HPow.hPow (α := R) (-1) i) (if Even k then 0 else 1)
pos : ∀ (h : Even k), HPow.hPow (α := R) (-1) k + 0 = 1
⊢ (HPow.hPow (α := R) (-1) k + if Even k then 0 else 1) = if ¬Even k then 0 else 1
have neg : ∀ (h : ¬Even k), HPow.hPow (α := R) (-1) k + 1 = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
k : ℕ
hk : Eq.{u_1 + 1} (α := R) (∑ i ∈ range k, HPow.hPow (α := R) (-1) i) (if Even k then 0 else 1)
h : Even k
⊢ HPow.hPow (α := R) (-1) k + 0 = 1
have pos : HAdd.hAdd (α := R) 1 0 = 1
Tactic: rw [h.neg_one_pow, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
k : ℕ
hk : Eq.{u_1 + 1} (α := R) (∑ i ∈ range k, HPow.hPow (α := R) (-1) i) (if Even k then 0 else 1)
h : Even k
pos : HAdd.hAdd (α := R) 1 0 = 1
⊢ HPow.hPow (α := R) (-1) k + 0 = 1
have pos₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [h.neg_one_pow, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
k : ℕ
hk : Eq.{u_1 + 1} (α := R) (∑ i ∈ range k, HPow.hPow (α := R) (-1) i) (if Even k then 0 else 1)
h : ¬Even k
⊢ HPow.hPow (α := R) (-1) k + 1 = 0
have neg : HAdd.hAdd (α := R) (-1) 1 = 0
Tactic: rw [(Nat.not_even_iff_odd.1 h).neg_one_pow, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
k : ℕ
hk : Eq.{u_1 + 1} (α := R) (∑ i ∈ range k, HPow.hPow (α := R) (-1) i) (if Even k then 0 else 1)
h : ¬Even k
neg : HAdd.hAdd (α := R) (-1) 1 = 0
⊢ HPow.hPow (α := R) (-1) k + 1 = 0
have neg₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [(Nat.not_even_iff_odd.1 h).neg_one_pow, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, HPow.hPow (α := R) (-1) i) (if Even n then 0 else 1)
have zero : Eq.{u_1 + 1} (α := R) (∑ i ∈ range 0, HPow.hPow (α := R) (-1) i) (if Even (α := ℕ) 0 then 0 else 1)
Tactic: induction n with
  | zero => simp
  | succ k hk =>
    simp only [geom_sum_succ', Nat.even_add_one, hk]
    split_ifs with h
    · rw [h.neg_one_pow, add_zero]
    · rw [(Nat.not_even_iff_odd.1 h).neg_one_pow, neg_add_cancel]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
zero : Eq.{u_1 + 1} (α := R) (∑ i ∈ range 0, HPow.hPow (α := R) (-1) i) (if Even (α := ℕ) 0 then 0 else 1)
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, HPow.hPow (α := R) (-1) i) (if Even n then 0 else 1)
have succ : ∀ (k : ℕ) (hk : Eq.{u_1 + 1} (α := R) (∑ i ∈ range k, HPow.hPow (α := R) (-1) i) (if Even k then 0 else 1)),
  Eq.{u_1 + 1} (α := R) (∑ i ∈ range (k + 1), HPow.hPow (α := R) (-1) i) (if Even (k + 1) then 0 else 1)
Tactic: induction n with
  | zero => simp
  | succ k hk =>
    simp only [geom_sum_succ', Nat.even_add_one, hk]
    split_ifs with h
    · rw [h.neg_one_pow, add_zero]
    · rw [(Nat.not_even_iff_odd.1 h).neg_one_pow, neg_add_cancel]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
have this : (∑ i ∈ range n, (x - y + y) ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = (x - y + y) ^ n
Tactic: have := (h.sub_left (Commute.refl y)).geom_sum₂_mul_add n
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
this : (∑ i ∈ range n, (x - y + y) ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = (x - y + y) ^ n
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
have this₁ : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
Tactic: rw [sub_add_cancel] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
this : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
have rw : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n - y ^ n
Tactic: rw [← this, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
this : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
rw :
  (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) =
    (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n - y ^ n
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
have rw₁ : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y)
Tactic: rw [← this, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ (y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n
have a : MulOpposite.op ((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = MulOpposite.op (y ^ n - x ^ n)
Tactic: apply op_injective
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ MulOpposite.op ((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) = MulOpposite.op (y ^ n - x ^ n)
have a : MulOpposite.op (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (MulOpposite.op y - MulOpposite.op x) =
  MulOpposite.op y ^ n - MulOpposite.op x ^ n
Tactic: simp only [op_mul, op_sub, op_pow]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
⊢ (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n
have rw : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = -(y ^ n - x ^ n)
Tactic: rw [← neg_sub (y ^ n), ← h.mul_neg_geom_sum₂, ← neg_mul, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
rw : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = -(y ^ n - x ^ n)
⊢ (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n
have rw₁ : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = -((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i))
Tactic: rw [← neg_sub (y ^ n), ← h.mul_neg_geom_sum₂, ← neg_mul, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
rw : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = -(y ^ n - x ^ n)
rw₁ : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = -((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i))
⊢ (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n
have rw₂ : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = -(y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)
Tactic: rw [← neg_sub (y ^ n), ← h.mul_neg_geom_sum₂, ← neg_mul, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
rw : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = -(y ^ n - x ^ n)
rw₁ : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = -((y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i))
rw₂ : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = -(y - x) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)
⊢ (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = x ^ n - y ^ n
have rw₃ : (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) = (x - y) * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)
Tactic: rw [← neg_sub (y ^ n), ← h.mul_neg_geom_sum₂, ← neg_mul, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
| 1 - x ^ n
have rw : HPow.hPow (α := R) 1 n - x ^ n
Tactic: rw [← one_pow n]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
⊢ 1 - x ∣ 1 - x ^ n
have conv_rhs : 1 - x ∣ HPow.hPow (α := R) 1 n - x ^ n
Tactic: conv_rhs => rw [← one_pow n]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
| x ^ n - 1
have rw : x ^ n - HPow.hPow (α := R) 1 n
Tactic: rw [← one_pow n]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
⊢ x - 1 ∣ x ^ n - 1
have conv_rhs : x - 1 ∣ x ^ n - HPow.hPow (α := R) 1 n
Tactic: conv_rhs => rw [← one_pow n]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
⊢ x ^ m - 1 ∣ x ^ (m * n) - 1
have rw : x ^ m - 1 ∣ (x ^ m) ^ n - 1
Tactic: rw [pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
a b : ℕ
h : a ∣ b
⊢ r ^ a - 1 ∣ r ^ b - 1
have obtain : ∀ (n : ℕ), r ^ a - 1 ∣ r ^ (a * n) - 1
Tactic: obtain ⟨n, rfl⟩ := h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
have pos : ∀ (hp₀ : p = 0), r ^ p ^ a - r ∣ r ^ p ^ b - r
Tactic: by_cases hp₀ : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
pos : ∀ (hp₀ : p = 0), r ^ p ^ a - r ∣ r ^ p ^ b - r
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
have neg : ∀ (hp₀ : ¬p = 0), r ^ p ^ a - r ∣ r ^ p ^ b - r
Tactic: by_cases hp₀ : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
have pos : ∀ (hb₀ : b = 0), r ^ p ^ a - r ∣ r ^ p ^ b - r
Tactic: by_cases hb₀ : b = 0
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
pos : ∀ (hb₀ : b = 0), r ^ p ^ a - r ∣ r ^ p ^ b - r
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
have neg : ∀ (hb₀ : ¬b = 0), r ^ p ^ a - r ∣ r ^ p ^ b - r
Tactic: by_cases hb₀ : b = 0
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : b = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
have pos : r ^ HPow.hPow (α := ℕ) 0 a - r ∣ 0
Tactic: rw [hp₀, hb₀, pow_zero, pow_one, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
r : R
p b : ℕ
hp₀ : p = 0
hb₀ : ¬b = 0
h : 0 ∣ b
⊢ False
have h₁ : b = 0
Tactic: rw [zero_dvd_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
have ha₀ : a ≠ 0
Tactic: have ha₀ : a ≠ 0 := by rintro rfl; rw [zero_dvd_iff] at h; tauto
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
ha₀ : a ≠ 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
have neg : r ^ HPow.hPow (α := ℕ) 0 a - r ∣ r ^ HPow.hPow (α := ℕ) 0 b - r
Tactic: rw [hp₀, zero_pow ha₀, zero_pow hb₀]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
ha₀ : a ≠ 0
neg : r ^ HPow.hPow (α := ℕ) 0 a - r ∣ r ^ HPow.hPow (α := ℕ) 0 b - r
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
have neg₁ : HPow.hPow (β := ℕ) r 0 - r ∣ r ^ HPow.hPow (α := ℕ) 0 b - r
Tactic: rw [hp₀, zero_pow ha₀, zero_pow hb₀]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
ha₀ : a ≠ 0
neg : r ^ HPow.hPow (α := ℕ) 0 a - r ∣ r ^ HPow.hPow (α := ℕ) 0 b - r
neg₁ : HPow.hPow (β := ℕ) r 0 - r ∣ r ^ HPow.hPow (α := ℕ) 0 b - r
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
have neg₂ : HPow.hPow (β := ℕ) r 0 - r ∣ HPow.hPow (β := ℕ) r 0 - r
Tactic: rw [hp₀, zero_pow ha₀, zero_pow hb₀]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
have hp : ∀ (c : ℕ), 1 ≤ p ^ c
Tactic: have hp (c) : 1 ≤ p ^ c := Nat.pow_pos <| pos_of_ne_zero hp₀
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
hp : ∀ (c : ℕ), 1 ≤ p ^ c
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r
have neg : r * (r ^ (p ^ a - 1) - 1) ∣ r * (r ^ (p ^ b - 1) - 1)
Tactic: rw [← Nat.sub_add_cancel (hp a), ← Nat.sub_add_cancel (hp b), pow_succ', pow_succ',
    ← mul_sub_one, ← mul_sub_one]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
hp : ∀ (c : ℕ), 1 ≤ p ^ c
⊢ r * (r ^ (p ^ a - 1) - 1) ∣ r * (r ^ (p ^ b - 1) - 1)
have neg : Dvd.dvd (α := ℤ) (↑(p ^ a - 1) : ℤ) (↑(p ^ b - 1) : ℤ)
Tactic: refine mul_dvd_mul_left _ <| dvd_pow_sub_one_of_dvd <| Int.natCast_dvd_natCast.mp ?_
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
hp : ∀ (c : ℕ), 1 ≤ p ^ c
⊢ Dvd.dvd (α := ℤ) (↑(p ^ a - 1) : ℤ) (↑(p ^ b - 1) : ℤ)
have neg : HPow.hPow (α := ℤ) (↑p : ℤ) a - 1 ∣ HPow.hPow (α := ℤ) (↑p : ℤ) b - 1
Tactic: push_cast [hp a, hp b]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1
have this : (∑ i ∈ range n, x ^ i * HPow.hPow (α := R) 1 (n - 1 - i)) * (x - 1) = x ^ n - HPow.hPow (α := R) 1 n
Tactic: have := (Commute.one_right x).geom_sum₂_mul n
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n
have this : -((∑ i ∈ range n, x ^ i) * (x - 1)) = -(x ^ n - 1)
Tactic: have := congr_arg Neg.neg (geom_sum_mul x n)
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)
have rw : (x - y) * HSub.hSub (α := R) (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k)) (∑ k ∈ range m, x ^ k * y ^ (n - 1 - k)) =
  x ^ n - x ^ m * y ^ (n - m)
Tactic: rw [sum_Ico_eq_sub _ hmn]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ Eq.{u_1 + 1} (α := R) (∑ k ∈ range m, x ^ k * y ^ (n - 1 - k))
    (∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)))
have refine : ∀ (j : ℕ) (j_in : j ∈ range m), x ^ j * y ^ (n - 1 - j) = x ^ j * (y ^ (n - m) * y ^ (m - 1 - j))
Tactic: refine sum_congr rfl fun j j_in => ?_
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * (y ^ (n - m) * y ^ (m - 1 - j))
have rw : x ^ j * y ^ (n - 1 - j) = x ^ j * y ^ (n - m + (m - 1 - j))
Tactic: rw [← pow_add]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * y ^ (n - m + (m - 1 - j))
have e_a : n - 1 - j = n - m + (m - 1 - j)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ n - 1 - j = n - m + (m - 1 - j)
have j_in₁ : j < m
Tactic: rw [mem_range] at j_in
Cleared hypotheses: j_in
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
⊢ (x - y) * HSub.hSub (α := R) (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k)) (∑ k ∈ range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)
have this : Eq.{u_1 + 1} (α := R) (∑ k ∈ range m, x ^ k * y ^ (n - 1 - k)) (∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)))
Tactic: have :
    ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) =
      ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)) := by
    refine sum_congr rfl fun j j_in => ?_
    rw [← pow_add]
    congr
    rw [mem_range] at j_in
    lia
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
this :
  Eq.{u_1 + 1} (α := R) (∑ k ∈ range m, x ^ k * y ^ (n - 1 - k))
    (∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)))
⊢ (x - y) * HSub.hSub (α := R) (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k)) (∑ k ∈ range m, x ^ k * y ^ (n - 1 - k)) =
    x ^ n - x ^ m * y ^ (n - m)
have rw : (x - y) *
    HSub.hSub (α := R) (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k))
      (∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))) =
  x ^ n - x ^ m * y ^ (n - m)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
this :
  Eq.{u_1 + 1} (α := R) (∑ k ∈ range m, x ^ k * y ^ (n - 1 - k))
    (∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)))
⊢ (x - y) *
      HSub.hSub (α := R) (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k))
        (∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k))) =
    x ^ n - x ^ m * y ^ (n - m)
have simp_rw : (x - y) *
    HSub.hSub (α := R) (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k))
      (∑ x_1 ∈ range m, x ^ x_1 * (y ^ (m - 1 - x_1) * y ^ (n - m))) =
  x ^ n - x ^ m * y ^ (n - m)
Tactic: simp_rw [pow_mul_comm y (n - m) _]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
this :
  Eq.{u_1 + 1} (α := R) (∑ k ∈ range m, x ^ k * y ^ (n - 1 - k))
    (∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)))
⊢ (x - y) *
      HSub.hSub (α := R) (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k))
        (∑ x_1 ∈ range m, x ^ x_1 * (y ^ (m - 1 - x_1) * y ^ (n - m))) =
    x ^ n - x ^ m * y ^ (n - m)
have simp_rw : (x - y) *
    HSub.hSub (α := R) (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k))
      (∑ x_1 ∈ range m, x ^ x_1 * y ^ (m - 1 - x_1) * y ^ (n - m)) =
  x ^ n - x ^ m * y ^ (n - m)
Tactic: simp_rw [← mul_assoc]