awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 rw : (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - (∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
  x ^ n - x ^ m * y ^ (n - m)
Tactic: rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add,
    add_tsub_cancel_of_le hmn, sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ 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
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)))
rw :
  (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - (∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
⊢ (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 rw₁ : (x - y) * ∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
  x ^ n - x ^ m * y ^ (n - m)
Tactic: rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add,
    add_tsub_cancel_of_le hmn, sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ 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
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)))
rw :
  (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - (∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
rw₁ :
  (x - y) * ∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) -
      (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
⊢ (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 rw₂ : x ^ n - y ^ n - (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) = x ^ n - x ^ m * y ^ (n - m)
Tactic: rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add,
    add_tsub_cancel_of_le hmn, sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ 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
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)))
rw :
  (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - (∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
rw₁ :
  (x - y) * ∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) -
      (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
rw₂ : x ^ n - y ^ n - (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) = x ^ n - x ^ m * y ^ (n - m)
⊢ (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 rw₃ : x ^ n - y ^ n - ((x - y) * ∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m) = x ^ n - x ^ m * y ^ (n - m)
Tactic: rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add,
    add_tsub_cancel_of_le hmn, sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ 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
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)))
rw :
  (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - (∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
rw₁ :
  (x - y) * ∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) -
      (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
rw₂ : x ^ n - y ^ n - (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) = x ^ n - x ^ m * y ^ (n - m)
rw₃ : x ^ n - y ^ n - ((x - y) * ∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m) = x ^ n - x ^ m * y ^ (n - m)
⊢ (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 rw₄ : x ^ n - y ^ n - (x ^ m - y ^ m) * y ^ (n - m) = x ^ n - x ^ m * y ^ (n - m)
Tactic: rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add,
    add_tsub_cancel_of_le hmn, sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ 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
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)))
rw :
  (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - (∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
rw₁ :
  (x - y) * ∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) -
      (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
rw₂ : x ^ n - y ^ n - (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) = x ^ n - x ^ m * y ^ (n - m)
rw₃ : x ^ n - y ^ n - ((x - y) * ∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m) = x ^ n - x ^ m * y ^ (n - m)
rw₄ : x ^ n - y ^ n - (x ^ m - y ^ m) * y ^ (n - m) = x ^ n - x ^ m * y ^ (n - m)
⊢ (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 rw₅ : x ^ n - y ^ n - (x ^ m * y ^ (n - m) - y ^ m * y ^ (n - m)) = x ^ n - x ^ m * y ^ (n - m)
Tactic: rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add,
    add_tsub_cancel_of_le hmn, sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ 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
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)))
rw :
  (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - (∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
rw₁ :
  (x - y) * ∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) -
      (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
rw₂ : x ^ n - y ^ n - (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) = x ^ n - x ^ m * y ^ (n - m)
rw₃ : x ^ n - y ^ n - ((x - y) * ∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m) = x ^ n - x ^ m * y ^ (n - m)
rw₄ : x ^ n - y ^ n - (x ^ m - y ^ m) * y ^ (n - m) = x ^ n - x ^ m * y ^ (n - m)
rw₅ : x ^ n - y ^ n - (x ^ m * y ^ (n - m) - y ^ m * y ^ (n - m)) = x ^ n - x ^ m * y ^ (n - m)
⊢ (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 rw₆ : x ^ n - y ^ n - (x ^ m * y ^ (n - m) - y ^ (m + (n - m))) = x ^ n - x ^ m * y ^ (n - m)
Tactic: rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add,
    add_tsub_cancel_of_le hmn, sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ 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
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)))
rw :
  (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - (∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
rw₁ :
  (x - y) * ∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) -
      (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
rw₂ : x ^ n - y ^ n - (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) = x ^ n - x ^ m * y ^ (n - m)
rw₃ : x ^ n - y ^ n - ((x - y) * ∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m) = x ^ n - x ^ m * y ^ (n - m)
rw₄ : x ^ n - y ^ n - (x ^ m - y ^ m) * y ^ (n - m) = x ^ n - x ^ m * y ^ (n - m)
rw₅ : x ^ n - y ^ n - (x ^ m * y ^ (n - m) - y ^ m * y ^ (n - m)) = x ^ n - x ^ m * y ^ (n - m)
rw₆ : x ^ n - y ^ n - (x ^ m * y ^ (n - m) - y ^ (m + (n - m))) = x ^ n - x ^ m * y ^ (n - m)
⊢ (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 rw₇ : x ^ n - y ^ n - (x ^ m * y ^ (n - m) - y ^ n) = x ^ n - x ^ m * y ^ (n - m)
Tactic: rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add,
    add_tsub_cancel_of_le hmn, sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ 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
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)))
rw :
  (x - y) * (∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) - (∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
rw₁ :
  (x - y) * ∑ k ∈ range n, x ^ k * y ^ (n - 1 - k) -
      (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) =
    x ^ n - x ^ m * y ^ (n - m)
rw₂ : x ^ n - y ^ n - (x - y) * ((∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m)) = x ^ n - x ^ m * y ^ (n - m)
rw₃ : x ^ n - y ^ n - ((x - y) * ∑ i ∈ range m, x ^ i * y ^ (m - 1 - i)) * y ^ (n - m) = x ^ n - x ^ m * y ^ (n - m)
rw₄ : x ^ n - y ^ n - (x ^ m - y ^ m) * y ^ (n - m) = x ^ n - x ^ m * y ^ (n - m)
rw₅ : x ^ n - y ^ n - (x ^ m * y ^ (n - m) - y ^ m * y ^ (n - m)) = x ^ n - x ^ m * y ^ (n - m)
rw₆ : x ^ n - y ^ n - (x ^ m * y ^ (n - m) - y ^ (m + (n - m))) = x ^ n - x ^ m * y ^ (n - m)
rw₇ : x ^ n - y ^ n - (x ^ m * y ^ (n - m) - y ^ n) = x ^ n - x ^ m * y ^ (n - m)
⊢ (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 rw₈ : x ^ n - x ^ m * y ^ (n - m) = x ^ n - x ^ m * y ^ (n - m)
Tactic: rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add,
    add_tsub_cancel_of_le hmn, sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ 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
n : ℕ
⊢ ∑ i ∈ range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)
have simp_rw : Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i * y ^ (n - i)) (∑ x_1 ∈ range n, x ^ x_1 * y ^ (n - 1 - x_1 + 1))
Tactic: simp_rw [mul_sum, sum_range_succ_comm, tsub_self, pow_zero, mul_one, add_right_inj, ← mul_assoc,
    (h.symm.pow_right _).eq, mul_assoc, ← pow_succ']
-- 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 : ℕ
⊢ Eq.{u_1 + 1} (α := R) (∑ i ∈ range n, x ^ i * y ^ (n - i)) (∑ x_1 ∈ range n, x ^ x_1 * y ^ (n - 1 - x_1 + 1))
have refine : ∀ (i : ℕ) (hi : i ∈ range n), x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)
Tactic: refine sum_congr rfl fun i hi => ?_
-- 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 i : ℕ
hi : i ∈ range n
this : n - 1 - i + 1 = n - i
⊢ x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)
have rw : x ^ i * y ^ (n - i) = x ^ i * y ^ (n - i)
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
n i : ℕ
hi : i ∈ range n
⊢ x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)
have suffices : n - 1 - i + 1 = n - i
Tactic: suffices n - 1 - i + 1 = n - i by rw [this]
-- 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 : ℕ
hi : i ∈ range n
⊢ n - 1 - i + 1 = n - i
have hi₁ : i < n
Tactic: rw [Finset.mem_range] at hi
Cleared hypotheses: hi
-- 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
⊢ (∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m
have a : MulOpposite.op ((∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y)) = MulOpposite.op (x ^ n - y ^ (n - m) * x ^ m)
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
m n : ℕ
hmn : m ≤ n
⊢ MulOpposite.op ((∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y)) = MulOpposite.op (x ^ n - y ^ (n - m) * x ^ m)
have a : (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 ∈ Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
  MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
Tactic: simp only [op_sub, op_mul, op_pow, op_sum]
-- 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 ∈ Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k)
    (∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k))
have refine : ∀ k ∈ Ico m n,
  MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
Tactic: refine sum_congr rfl fun k _ => ?_
-- 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
k : ℕ
h_1 : k ∈ Ico m n
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)
have hp : Commute (MulOpposite.op y ^ (n - 1 - k)) (MulOpposite.op x ^ k)
Tactic: have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
-- 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
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 ∈ Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
have this : Eq.{u_1 + 1} (α := Rᵐᵒᵖ) (∑ k ∈ Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k)
  (∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k))
Tactic: have : (∑ k ∈ Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k) =
      ∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) := by
    refine sum_congr rfl fun k _ => ?_
    have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
    simpa [Commute, SemiconjBy] using hp
-- 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 ∈ Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k)
    (∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k))
⊢ (MulOpposite.op x - MulOpposite.op y) * ∑ x_1 ∈ Ico m n, MulOpposite.op y ^ (n - 1 - x_1) * MulOpposite.op x ^ x_1 =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
have a : (MulOpposite.op x - MulOpposite.op y) * ∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) =
  MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)
Tactic: simp only [this]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
hmn : m ≤ n
⊢ (∑ i ∈ Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m
have rw : HSub.hSub (α := R) (∑ k ∈ range n, x ^ k) (∑ k ∈ range m, x ^ k) * (x - 1) = x ^ n - x ^ m
Tactic: rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul, geom_sum_mul, sub_sub_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
hmn : m ≤ n
rw : HSub.hSub (α := R) (∑ k ∈ range n, x ^ k) (∑ k ∈ range m, x ^ k) * (x - 1) = x ^ n - x ^ m
⊢ (∑ i ∈ Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m
have rw₁ : (∑ k ∈ range n, x ^ k) * (x - 1) - (∑ k ∈ range m, x ^ k) * (x - 1) = x ^ n - x ^ m
Tactic: rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul, geom_sum_mul, sub_sub_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
hmn : m ≤ n
rw : HSub.hSub (α := R) (∑ k ∈ range n, x ^ k) (∑ k ∈ range m, x ^ k) * (x - 1) = x ^ n - x ^ m
rw₁ : (∑ k ∈ range n, x ^ k) * (x - 1) - (∑ k ∈ range m, x ^ k) * (x - 1) = x ^ n - x ^ m
⊢ (∑ i ∈ Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m
have rw₂ : x ^ n - 1 - (∑ k ∈ range m, x ^ k) * (x - 1) = x ^ n - x ^ m
Tactic: rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul, geom_sum_mul, sub_sub_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
hmn : m ≤ n
rw : HSub.hSub (α := R) (∑ k ∈ range n, x ^ k) (∑ k ∈ range m, x ^ k) * (x - 1) = x ^ n - x ^ m
rw₁ : (∑ k ∈ range n, x ^ k) * (x - 1) - (∑ k ∈ range m, x ^ k) * (x - 1) = x ^ n - x ^ m
rw₂ : x ^ n - 1 - (∑ k ∈ range m, x ^ k) * (x - 1) = x ^ n - x ^ m
⊢ (∑ i ∈ Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m
have rw₃ : x ^ n - 1 - (x ^ m - 1) = x ^ n - x ^ m
Tactic: rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul, geom_sum_mul, sub_sub_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
hmn : m ≤ n
rw : HSub.hSub (α := R) (∑ k ∈ range n, x ^ k) (∑ k ∈ range m, x ^ k) * (x - 1) = x ^ n - x ^ m
rw₁ : (∑ k ∈ range n, x ^ k) * (x - 1) - (∑ k ∈ range m, x ^ k) * (x - 1) = x ^ n - x ^ m
rw₂ : x ^ n - 1 - (∑ k ∈ range m, x ^ k) * (x - 1) = x ^ n - x ^ m
rw₃ : x ^ n - 1 - (x ^ m - 1) = x ^ n - x ^ m
⊢ (∑ i ∈ Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m
have rw₄ : x ^ n - x ^ m = x ^ n - x ^ m
Tactic: rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul, geom_sum_mul, sub_sub_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
hmn : m ≤ n
⊢ (∑ i ∈ Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n
have rw : HSub.hSub (α := R) (∑ k ∈ range n, x ^ k) (∑ k ∈ range m, x ^ k) * (1 - x) = x ^ m - x ^ n
Tactic: rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul_neg, geom_sum_mul_neg, sub_sub_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
hmn : m ≤ n
rw : HSub.hSub (α := R) (∑ k ∈ range n, x ^ k) (∑ k ∈ range m, x ^ k) * (1 - x) = x ^ m - x ^ n
⊢ (∑ i ∈ Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n
have rw₁ : (∑ k ∈ range n, x ^ k) * (1 - x) - (∑ k ∈ range m, x ^ k) * (1 - x) = x ^ m - x ^ n
Tactic: rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul_neg, geom_sum_mul_neg, sub_sub_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
hmn : m ≤ n
rw : HSub.hSub (α := R) (∑ k ∈ range n, x ^ k) (∑ k ∈ range m, x ^ k) * (1 - x) = x ^ m - x ^ n
rw₁ : (∑ k ∈ range n, x ^ k) * (1 - x) - (∑ k ∈ range m, x ^ k) * (1 - x) = x ^ m - x ^ n
⊢ (∑ i ∈ Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n
have rw₂ : 1 - x ^ n - (∑ k ∈ range m, x ^ k) * (1 - x) = x ^ m - x ^ n
Tactic: rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul_neg, geom_sum_mul_neg, sub_sub_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
hmn : m ≤ n
rw : HSub.hSub (α := R) (∑ k ∈ range n, x ^ k) (∑ k ∈ range m, x ^ k) * (1 - x) = x ^ m - x ^ n
rw₁ : (∑ k ∈ range n, x ^ k) * (1 - x) - (∑ k ∈ range m, x ^ k) * (1 - x) = x ^ m - x ^ n
rw₂ : 1 - x ^ n - (∑ k ∈ range m, x ^ k) * (1 - x) = x ^ m - x ^ n
⊢ (∑ i ∈ Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n
have rw₃ : 1 - x ^ n - (1 - x ^ m) = x ^ m - x ^ n
Tactic: rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul_neg, geom_sum_mul_neg, sub_sub_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
hmn : m ≤ n
rw : HSub.hSub (α := R) (∑ k ∈ range n, x ^ k) (∑ k ∈ range m, x ^ k) * (1 - x) = x ^ m - x ^ n
rw₁ : (∑ k ∈ range n, x ^ k) * (1 - x) - (∑ k ∈ range m, x ^ k) * (1 - x) = x ^ m - x ^ n
rw₂ : 1 - x ^ n - (∑ k ∈ range m, x ^ k) * (1 - x) = x ^ m - x ^ n
rw₃ : 1 - x ^ n - (1 - x ^ m) = x ^ m - x ^ n
⊢ (∑ i ∈ Ico m n, x ^ i) * (1 - x) = x ^ m - x ^ n
have rw₄ : x ^ m - x ^ n = x ^ m - x ^ n
Tactic: rw [sum_Ico_eq_sub _ hmn, sub_mul, geom_sum_mul_neg, geom_sum_mul_neg, sub_sub_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
x y : R
n : ℕ
h : Odd n
⊢ x + y ∣ x ^ n + y ^ n
have h₁ : (∑ i ∈ range n, x ^ i * (-y) ^ (n - 1 - i)) * (x - -y) = x ^ n - (-y) ^ n
Tactic: have h₁ := geom_sum₂_mul x (-y) n
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
x y : R
n : ℕ
h : Odd n
h₁ : (∑ i ∈ range n, x ^ i * (-y) ^ (n - 1 - i)) * (x - -y) = x ^ n - (-y) ^ n
⊢ x + y ∣ x ^ n + y ^ n
have h₂ : (∑ i ∈ range n, x ^ i * (-y) ^ (n - 1 - i)) * (x + y) = x ^ n + y ^ n
Tactic: rw [Odd.neg_pow h y, sub_neg_eq_add, sub_neg_eq_add] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
x y n : ℕ
⊢ x - y ∣ x ^ n - y ^ n
have inl : ∀ (h : y ≤ x), x - y ∣ x ^ n - y ^ n
Tactic: rcases le_or_gt y x with h | h
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
x y n : ℕ
inl : ∀ (h : y ≤ x), x - y ∣ x ^ n - y ^ n
⊢ x - y ∣ x ^ n - y ^ n
have inr : ∀ (h : x < y), x - y ∣ x ^ n - y ^ n
Tactic: rcases le_or_gt y x with h | h
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
x y n : ℕ
h : y ≤ x
⊢ x - y ∣ x ^ n - y ^ n
have this : y ^ n ≤ x ^ n
Tactic: have : y ^ n ≤ x ^ n := Nat.pow_le_pow_left h _
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (hypothesis)
Goal:
x y n : ℕ
h : x < y
⊢ x - y ∣ x ^ n - y ^ n
have this : x ^ n ≤ y ^ n
Tactic: have : x ^ n ≤ y ^ n := Nat.pow_le_pow_left h.le _
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
m k x y : ℕ
hmk : m ∣ k
⊢ x ^ m - y ^ m ∣ x ^ k - y ^ k
have obtain : ∀ (n : ℕ), x ^ m - y ^ m ∣ x ^ (m * n) - y ^ (m * n)
Tactic: obtain ⟨n, rfl⟩ := hmk
Cleared hypotheses: k, hmk
-- Lean 4 proof step from Mathlib.Algebra.Ring.GeomSum (goal)
Goal:
m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ ∑ k ∈ range n, m ^ k = (m ^ n - 1) / (m - 1)
have refine : m ^ n = (∑ k ∈ range n, m ^ k) * (m - 1) + 1
Tactic: refine (Nat.div_eq_of_eq_mul_left (tsub_pos_iff_lt.2 hm) <| tsub_eq_of_eq_add ?_).symm
-- Lean 4 proof step from Mathlib.Algebra.Ring.GrindInstances (goal)
Goal:
α : Type u_1
s : Semiring α
⊢ OfNat.ofNat (HAdd.hAdd (α := ℕ) 1 1) = HAdd.hAdd (α := α) (OfNat.ofNat 1) 1
have change : (↑2 : α) = HAdd.hAdd (α := α) 1 1
Tactic: change Nat.cast 2 = 1 + 1
-- Lean 4 proof step from Mathlib.Algebra.Ring.GrindInstances (goal)
Goal:
α : Type u_1
s : Semiring α
⊢ (↑2 : α) = HAdd.hAdd (α := α) 1 1
have rw : Eq.{u_1 + 1} (α := α) (↑2 : α) 2
Tactic: rw [one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Algebra.Ring.GrindInstances (goal)
Goal:
α : Type u_1
s : Semiring α
n : ℕ
⊢ OfNat.ofNat (n + 2 + 1) = HAdd.hAdd (α := α) (OfNat.ofNat (n + 2)) 1
have change : (↑(n + 2 + 1) : α) = HAdd.hAdd (α := α) (↑(n + 2) : α) 1
Tactic: change Nat.cast (n + 2 + 1) = Nat.cast (n + 2) + 1