awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
rw : x ^ m - 1 ∣ (x ^ m) ^ n - 1
⊢ x ^ m - 1 ∣ x ^ (m * n) - 1

Tactic:
rw [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
⊢ x ^ m - 1 ∣ (x ^ m) ^ n - 1

Tactic:
sub_one_dvd_pow_sub_one (x ^ m) n

Premises used: HPow.hPow, sub_one_dvd_pow_sub_one
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
m n : ℕ
⊢ x ^ m - 1 ∣ (x ^ m) ^ n - 1

Tactic:
exact sub_one_dvd_pow_sub_one (x ^ m) n

Premises used: HPow.hPow, sub_one_dvd_pow_sub_one
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
a b : ℕ
h : a ∣ b
obtain : ∀ (n : ℕ), r ^ a - 1 ∣ r ^ (a * n) - 1
⊢ r ^ a - 1 ∣ r ^ b - 1

Tactic:
obtain ⟨n, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
a n : ℕ
⊢ r ^ a - 1 ∣ r ^ (a * n) - 1

Tactic:
pow_one_sub_dvd_pow_mul_sub_one r a n

Premises used: pow_one_sub_dvd_pow_mul_sub_one
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
a n : ℕ
⊢ r ^ a - 1 ∣ r ^ (a * n) - 1

Tactic:
exact pow_one_sub_dvd_pow_mul_sub_one r a n

Premises used: pow_one_sub_dvd_pow_mul_sub_one
-- Module: Mathlib.Algebra.Ring.GeomSum
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
neg : ∀ (hp₀ : ¬p = 0), r ^ p ^ a - r ∣ r ^ p ^ b - r
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

Tactic:
by_cases hp₀ : p = 0
-- Module: Mathlib.Algebra.Ring.GeomSum
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
neg : ∀ (hb₀ : ¬b = 0), r ^ p ^ a - r ∣ r ^ p ^ b - r
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

Tactic:
by_cases hb₀ : b = 0
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : b = 0
pos : r ^ HPow.hPow (α := ℕ) 0 a - r ∣ 0
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

Tactic:
rw [hp₀, hb₀, pow_zero, pow_one, sub_self]

Premises used: sub_self, pow_zero, pow_one
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : b = 0
⊢ r ^ HPow.hPow (α := ℕ) 0 a - r ∣ 0

Tactic:
dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : b = 0
⊢ r ^ HPow.hPow (α := ℕ) 0 a - r ∣ 0

Tactic:
exact dvd_zero _

Premises used: dvd_zero
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
p b : ℕ
hp₀ : p = 0
hb₀ : ¬b = 0
h : 0 ∣ b
⊢ b = 0

Tactic:
rw [zero_dvd_iff] at h

Premises used: zero_dvd_iff
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
p b : ℕ
hp₀ : p = 0
hb₀ : ¬b = 0
h : b = 0
⊢ False

Tactic:
tauto
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
⊢ a ≠ 0

Tactic:
have ha₀ : a ≠ 0 := by rintro rfl; rw [zero_dvd_iff] at h; tauto
-- Module: Mathlib.Algebra.Ring.GeomSum
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
neg₂ neg₃ : HPow.hPow (β := ℕ) r 0 - r ∣ HPow.hPow (β := ℕ) r 0 - r
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

Tactic:
rw [hp₀, zero_pow ha₀, zero_pow hb₀]

Premises used: zero_pow
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
⊢ ∀ (c : ℕ), 1 ≤ p ^ c

Tactic:
have hp (c) : 1 ≤ p ^ c := Nat.pow_pos <| pos_of_ne_zero hp₀
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
hp : ∀ (c : ℕ), 1 ≤ p ^ c
neg : r * (r ^ (p ^ a - 1) - 1) ∣ r * (r ^ (p ^ b - 1) - 1)
⊢ r ^ p ^ a - r ∣ r ^ p ^ b - r

Tactic:
rw [← Nat.sub_add_cancel (hp a), ← Nat.sub_add_cancel (hp b), pow_succ', pow_succ',
    ← mul_sub_one, ← mul_sub_one]

Premises used: mul_sub_one, Nat.sub_add_cancel, pow_succ'
-- Module: Mathlib.Algebra.Ring.GeomSum
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)

Tactic:
mul_dvd_mul_left _ <| dvd_pow_sub_one_of_dvd <| Int.natCast_dvd_natCast.mp ?_

Premises used: mul_dvd_mul_left, dvd_pow_sub_one_of_dvd, Iff.mp, Int.natCast_dvd_natCast
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
hp : ∀ (c : ℕ), 1 ≤ p ^ c
neg : Dvd.dvd (α := ℤ) (↑(p ^ a - 1) : ℤ) (↑(p ^ b - 1) : ℤ)
⊢ r * (r ^ (p ^ a - 1) - 1) ∣ r * (r ^ (p ^ b - 1) - 1)

Tactic:
refine mul_dvd_mul_left _ <| dvd_pow_sub_one_of_dvd <| Int.natCast_dvd_natCast.mp ?_

Premises used: mul_dvd_mul_left, dvd_pow_sub_one_of_dvd, Iff.mp, Int.natCast_dvd_natCast
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
hp : ∀ (c : ℕ), 1 ≤ p ^ c
neg : HPow.hPow (α := ℤ) (↑p : ℤ) a - 1 ∣ HPow.hPow (α := ℤ) (↑p : ℤ) b - 1
⊢ Dvd.dvd (α := ℤ) (↑(p ^ a - 1) : ℤ) (↑(p ^ b - 1) : ℤ)

Tactic:
push_cast [hp a, hp b]
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
hp : ∀ (c : ℕ), 1 ≤ p ^ c
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) a - 1 ∣ HPow.hPow (α := ℤ) (↑p : ℤ) b - 1

Tactic:
dvd_pow_sub_one_of_dvd h

Premises used: dvd_pow_sub_one_of_dvd
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : ¬p = 0
hp : ∀ (c : ℕ), 1 ≤ p ^ c
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) a - 1 ∣ HPow.hPow (α := ℤ) (↑p : ℤ) b - 1

Tactic:
exact dvd_pow_sub_one_of_dvd h

Premises used: dvd_pow_sub_one_of_dvd
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
⊢ (∑ 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
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
this : (∑ i ∈ range n, x ^ i * HPow.hPow (α := R) 1 (n - 1 - i)) * (x - 1) = x ^ n - HPow.hPow (α := R) 1 n
⊢ (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

Tactic:
rw [one_pow, geom_sum₂_with_one] at this

Premises used: one_pow, geom_sum₂_with_one
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
this : (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1
⊢ (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

Tactic:
this
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
this : (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1
⊢ (∑ i ∈ range n, x ^ i) * (x - 1) = x ^ n - 1

Tactic:
exact this
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
⊢ op ((x - 1) * ∑ i ∈ range n, x ^ i) = op (x ^ n - 1)

Tactic:
simpa using geom_sum_mul (op x) n

Premises used: geom_sum_mul, MulOpposite.op
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
⊢ -((∑ i ∈ range n, x ^ i) * (x - 1)) = -(x ^ n - 1)

Tactic:
have := congr_arg Neg.neg (geom_sum_mul x n)
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
this : -((∑ i ∈ range n, x ^ i) * (x - 1)) = -(x ^ n - 1)
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
rw [neg_sub, ← mul_neg, neg_sub] at this

Premises used: neg_sub, mul_neg
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
this : (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
this
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
this : (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n
⊢ (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n

Tactic:
exact this
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x : R
n : ℕ
⊢ op ((1 - x) * ∑ i ∈ range n, x ^ i) = op (1 - x ^ n)

Tactic:
simpa using geom_sum_mul_neg (op x) n

Premises used: geom_sum_mul_neg, MulOpposite.op
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
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)
⊢ (x - y) * ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = x ^ n - x ^ m * y ^ (n - m)

Tactic:
rw [sum_Ico_eq_sub _ hmn]

Premises used: Finset.sum_Ico_eq_sub
-- Module: Mathlib.Algebra.Ring.GeomSum
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)))

Tactic:
sum_congr rfl fun j j_in => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
refine : ∀ (j : ℕ) (j_in : j ∈ range m), x ^ j * y ^ (n - 1 - j) = x ^ j * (y ^ (n - m) * y ^ (m - 1 - j))
⊢ 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:
refine sum_congr rfl fun j j_in => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
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
rw : x ^ j * y ^ (n - 1 - j) = x ^ j * y ^ (n - m + (m - 1 - j))
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * (y ^ (n - m) * y ^ (m - 1 - j))

Tactic:
rw [← pow_add]

Premises used: pow_add
-- Module: Mathlib.Algebra.Ring.GeomSum
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
e_a : n - 1 - j = n - m + (m - 1 - j)
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * y ^ (n - m + (m - 1 - j))

Tactic:
congr
-- Module: Mathlib.Algebra.Ring.GeomSum
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
⊢ j < m

Tactic:
rw [mem_range] at j_in

Premises used: Finset.mem_range
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j < m
⊢ n - 1 - j = n - m + (m - 1 - j)

Tactic:
lia
-- Module: Mathlib.Algebra.Ring.GeomSum
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)))

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
-- Module: Mathlib.Algebra.Ring.GeomSum
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) *
      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)
⊢ (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 [this]
-- Module: Mathlib.Algebra.Ring.GeomSum
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)))
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)
⊢ (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:
simp_rw [pow_mul_comm y (n - m) _]

Premises used: HSub.hSub, pow_mul_comm
-- Module: Mathlib.Algebra.Ring.GeomSum
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)))
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)
⊢ (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]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Ring.GeomSum
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)
rw₈ rw₉ : x ^ n - x ^ 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)

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)]

Premises used: sub_sub_sub_cancel_right, HMul.hMul, mul_sub, mul_assoc, HSub.hSub, pow_add, Commute.mul_geom_sum₂, sub_mul, HPow.hPow, add_tsub_cancel_of_le, Finset.sum_mul
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
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))
⊢ ∑ i ∈ range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)

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']

Premises used: Finset.mul_sum, Commute.pow_right, mul_assoc, tsub_self, Finset.sum_range_succ_comm, pow_zero, Commute.symm, mul_one, Commute.eq, add_right_inj, pow_succ'
-- Module: Mathlib.Algebra.Ring.GeomSum
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))

Tactic:
sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n : ℕ
refine : ∀ (i : ℕ) (hi : i ∈ range n), x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)
⊢ 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:
refine sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
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
rw rw₁ : x ^ i * y ^ (n - i) = x ^ i * y ^ (n - i)
⊢ x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n i : ℕ
hi : i ∈ range n
suffices : n - 1 - i + 1 = n - i
⊢ x ^ i * y ^ (n - i) = x ^ i * y ^ (n - 1 - i + 1)

Tactic:
suffices n - 1 - i + 1 = n - i by rw [this]
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n i : ℕ
hi : i ∈ range n
⊢ i < n

Tactic:
rw [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
n i : ℕ
hi : i < n
⊢ n - 1 - i + 1 = n - i

Tactic:
lia
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
a : MulOpposite.op ((∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y)) = MulOpposite.op (x ^ n - y ^ (n - m) * x ^ m)
⊢ (∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m

Tactic:
apply op_injective

Premises used: MulOpposite.op_injective
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
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)
⊢ MulOpposite.op ((∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y)) = MulOpposite.op (x ^ n - y ^ (n - m) * x ^ m)

Tactic:
simp only [op_sub, op_mul, op_pow, op_sum]

Premises used: MulOpposite.op_pow, MulOpposite.op_mul, Finset.op_sum, MulOpposite.op_sub
-- Module: Mathlib.Algebra.Ring.GeomSum
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))

Tactic:
sum_congr rfl fun k _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
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)
⊢ 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:
refine sum_congr rfl fun k _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Ring.GeomSum
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
⊢ 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
-- Module: Mathlib.Algebra.Ring.GeomSum
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
hp : Commute (MulOpposite.op y ^ (n - 1 - k)) (MulOpposite.op x ^ k)
⊢ MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k = MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k)

Tactic:
simpa [Commute, SemiconjBy] using hp

Premises used: SemiconjBy, Commute
-- Module: Mathlib.Algebra.Ring.GeomSum
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))

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
-- Module: Mathlib.Algebra.Ring.GeomSum
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))
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)
⊢ (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 [this]
-- Module: Mathlib.Algebra.Ring.GeomSum
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) * ∑ i ∈ Ico m n, MulOpposite.op x ^ i * MulOpposite.op y ^ (n - 1 - i) =
    MulOpposite.op x ^ n - MulOpposite.op x ^ m * MulOpposite.op y ^ (n - m)

Tactic:
(Commute.op h).mul_geom_sum₂_Ico hmn

Premises used: Commute.mul_geom_sum₂_Ico, Commute.op
-- Module: Mathlib.Algebra.Ring.GeomSum
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) * ∑ 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:
convert! (Commute.op h).mul_geom_sum₂_Ico hmn

Premises used: Commute.mul_geom_sum₂_Ico, Commute.op
-- Module: Mathlib.Algebra.Ring.GeomSum
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
rw₄ rw₅ : x ^ n - x ^ m = x ^ n - x ^ m
⊢ (∑ i ∈ Ico m n, x ^ i) * (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]

Premises used: sub_sub_sub_cancel_right, Finset.sum_Ico_eq_sub, geom_sum_mul, sub_mul
-- Module: Mathlib.Algebra.Ring.GeomSum
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
rw₄ rw₅ : x ^ m - x ^ n = x ^ m - x ^ n
⊢ (∑ i ∈ Ico m n, x ^ i) * (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]

Premises used: Finset.sum_Ico_eq_sub, sub_mul, geom_sum_mul_neg, sub_sub_sub_cancel_left
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommRing R
x : R
m n : ℕ
⊢ (x ^ m - 1) * ∑ k ∈ range n, x ^ k = (x ^ n - 1) * ∑ k ∈ range m, x ^ k

Tactic:
grind [geom_sum_mul]

Premises used: geom_sum_mul
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommRing R
x y : R
n : ℕ
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Tactic:
(Commute.all x y).geom_sum₂_mul n

Premises used: Commute.geom_sum₂_mul, Commute.all
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommRing R
x y : R
n : ℕ
⊢ x - y ∣ x ^ n - y ^ n

Tactic:
(Commute.all x y).sub_dvd_pow_sub_pow n

Premises used: Commute.sub_dvd_pow_sub_pow, Commute.all
-- Module: Mathlib.Algebra.Ring.GeomSum
Goal:
R : Type u_1
inst : CommRing R
x y : R
n : ℕ
h : Odd n
⊢ (∑ i ∈ range n, x ^ i * (-y) ^ (n - 1 - i)) * (x - -y) = x ^ n - (-y) ^ n

Tactic:
have h₁ := geom_sum₂_mul x (-y) n
-- Module: Mathlib.Algebra.Ring.GeomSum
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
⊢ (∑ 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₁

Premises used: Odd.neg_pow, sub_neg_eq_add