awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p : ℤ) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p : ℤ) (x - y) + emultiplicity p (n + 1)
have succ : ∀ (hp : Prime (M := ℤ) (↑p : ℤ)) (hp1 : Odd p) {x y : ℤ} (hxy : (↑p : ℤ) ∣ x - y) (hx : ¬(↑p : ℤ) ∣ x) (n : ℕ)
  (h : FiniteMultiplicity p (n + 1)) (hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1) (k : ℕ)
  (hk : n + 1 = p ^ multiplicity p (n + 1) * k),
  emultiplicity (↑p : ℤ) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p : ℤ) (x - y) + emultiplicity p (n + 1)
Tactic: rw [Nat.prime_iff_prime_int] at hp
Cleared hypotheses: hp, hp1, x, y, hxy, hx, n, h, hpn, k, hk
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime (M := ℤ) (↑p : ℤ)
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p : ℤ) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p : ℤ) (x - y) + emultiplicity p (n + 1)
have succ : (↑p : ℤ) ∣ x ^ p ^ multiplicity p (n + 1) - y ^ p ^ multiplicity p (n + 1)
Tactic: rw [emultiplicity_pow_sub_pow_of_prime hp,
    emultiplicity_pow_prime_pow_sub_pow_prime_pow hp hp1 hxy hx, h.emultiplicity_eq_multiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime (M := ℤ) (↑p : ℤ)
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
succ : (↑p : ℤ) ∣ x ^ p ^ multiplicity p (n + 1) - y ^ p ^ multiplicity p (n + 1)
⊢ emultiplicity (↑p : ℤ) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p : ℤ) (x - y) + emultiplicity p (n + 1)
have succ₁ : ¬(↑p : ℤ) ∣ x ^ p ^ multiplicity p (n + 1)
Tactic: rw [emultiplicity_pow_sub_pow_of_prime hp,
    emultiplicity_pow_prime_pow_sub_pow_prime_pow hp hp1 hxy hx, h.emultiplicity_eq_multiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime (M := ℤ) (↑p : ℤ)
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
succ : (↑p : ℤ) ∣ x ^ p ^ multiplicity p (n + 1) - y ^ p ^ multiplicity p (n + 1)
succ₁ : ¬(↑p : ℤ) ∣ x ^ p ^ multiplicity p (n + 1)
⊢ emultiplicity (↑p : ℤ) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p : ℤ) (x - y) + emultiplicity p (n + 1)
have succ₂ : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑k : ℤ)
Tactic: rw [emultiplicity_pow_sub_pow_of_prime hp,
    emultiplicity_pow_prime_pow_sub_pow_prime_pow hp hp1 hxy hx, h.emultiplicity_eq_multiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime (M := ℤ) (↑p : ℤ)
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ (↑p : ℤ) ∣ x ^ p ^ multiplicity p (n + 1) - y ^ p ^ multiplicity p (n + 1)
have succ : (↑p : ℤ) ∣ (∑ i ∈ range (p ^ multiplicity p (n + 1)), x ^ i * y ^ (p ^ multiplicity p (n + 1) - 1 - i)) * (x - y)
Tactic: rw [← geom_sum₂_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime (M := ℤ) (↑p : ℤ)
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑k : ℤ)
have succ : ¬p ∣ k
Tactic: rw [Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime (M := ℤ) (↑p : ℤ)
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
c : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * (p * c)
⊢ False
have succ : n + 1 = p ^ (multiplicity p (n + 1) + 1) * c
Tactic: refine hpn ⟨c, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime (M := ℤ) (↑p : ℤ)
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
c : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * (p * c)
⊢ n + 1 = p ^ (multiplicity p (n + 1) + 1) * c
have succ : n + 1 = p ^ multiplicity p (n + 1) * p * c
Tactic: rwa [pow_succ, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x + y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity (↑p : ℤ) (x ^ n + y ^ n) = emultiplicity (↑p : ℤ) (x + y) + emultiplicity p n
have rw : ∀ (hxy : (↑p : ℤ) ∣ x - -y) (hx : ¬(↑p : ℤ) ∣ x) {n : ℕ} (hn : Odd n),
  emultiplicity (↑p : ℤ) (x ^ n + y ^ n) = emultiplicity (↑p : ℤ) (x + y) + emultiplicity p n
Tactic: rw [← sub_neg_eq_add] at hxy
Cleared hypotheses: hxy, hx, n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - -y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity (↑p : ℤ) (x ^ n + y ^ n) = emultiplicity (↑p : ℤ) (x + y) + emultiplicity p n
have rw : emultiplicity (↑p : ℤ) (x ^ n - (-y) ^ n) = emultiplicity (↑p : ℤ) (x - -y) + emultiplicity p n
Tactic: rw [← sub_neg_eq_add, ← sub_neg_eq_add, ← Odd.neg_pow hn]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
have inl : ∀ (hyx : y ≤ x), emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
Tactic: obtain hyx | hyx := le_total y x
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
inl : ∀ (hyx : y ≤ x), emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
have inr : ∀ (hyx : x ≤ y), emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
Tactic: obtain hyx | hyx := le_total y x
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
have inl : emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n - y ^ n) : ℤ) = emultiplicity p (x - y) + emultiplicity p n
Tactic: rw [← Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n - y ^ n) : ℤ) = emultiplicity p (x - y) + emultiplicity p n
have inl : emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n - y ^ n) : ℤ) =
  emultiplicity (α := ℤ) (↑p : ℤ) (↑(x - y) : ℤ) + emultiplicity p n
Tactic: rw [← Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
have inl : emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n - y ^ n) : ℤ) =
  emultiplicity (α := ℤ) (↑p : ℤ) (↑(x - y) : ℤ) + emultiplicity p n
Tactic: iterate 2 rw [← Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n - y ^ n) : ℤ) =
    emultiplicity (α := ℤ) (↑p : ℤ) (↑(x - y) : ℤ) + emultiplicity p n
have inl : emultiplicity (↑p : ℤ) (HSub.hSub (α := ℤ) (↑(x ^ n) : ℤ) (↑(y ^ n) : ℤ)) =
  emultiplicity (α := ℤ) (↑p : ℤ) (↑(x - y) : ℤ) + emultiplicity p n
Tactic: rw [Int.ofNat_sub (Nat.pow_le_pow_left hyx n)]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ emultiplicity (↑p : ℤ) (HSub.hSub (α := ℤ) (↑(x ^ n) : ℤ) (↑(y ^ n) : ℤ)) =
    emultiplicity (α := ℤ) (↑p : ℤ) (↑(x - y) : ℤ) + emultiplicity p n
have inl : ∀ (hxy : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(x - y) : ℤ)) (hx : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x : ℤ)) (n : ℕ) (hyx : y ≤ x),
  emultiplicity (↑p : ℤ) (HSub.hSub (α := ℤ) (↑(x ^ n) : ℤ) (↑(y ^ n) : ℤ)) =
    emultiplicity (α := ℤ) (↑p : ℤ) (↑(x - y) : ℤ) + emultiplicity p n
Tactic: rw [← Int.natCast_dvd_natCast] at hxy hx
Cleared hypotheses: hxy, hx, n, hyx
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(x - y) : ℤ)
hx : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x : ℤ)
n : ℕ
hyx : y ≤ x
⊢ emultiplicity (↑p : ℤ) (HSub.hSub (α := ℤ) (↑(x ^ n) : ℤ) (↑(y ^ n) : ℤ)) =
    emultiplicity (α := ℤ) (↑p : ℤ) (↑(x - y) : ℤ) + emultiplicity p n
have inl : ∀ (hxy : (↑p : ℤ) ∣ HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) (hx : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x : ℤ)) (n : ℕ)
  (hyx : y ≤ x),
  emultiplicity (↑p : ℤ) (HSub.hSub (α := ℤ) (↑(x ^ n) : ℤ) (↑(y ^ n) : ℤ)) =
    emultiplicity (↑p : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) + emultiplicity p n
Tactic: rw [Int.natCast_sub hyx] at *
Cleared hypotheses: hxy, hx, n, hyx
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity p (x ^ n + y ^ n) = emultiplicity p (x + y) + emultiplicity p n
have rw : emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n + y ^ n) : ℤ) = emultiplicity p (x + y) + emultiplicity p n
Tactic: rw [← Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n + y ^ n) : ℤ) = emultiplicity p (x + y) + emultiplicity p n
have rw : emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n + y ^ n) : ℤ) =
  emultiplicity (α := ℤ) (↑p : ℤ) (↑(x + y) : ℤ) + emultiplicity p n
Tactic: rw [← Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity p (x ^ n + y ^ n) = emultiplicity p (x + y) + emultiplicity p n
have iterate : emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n + y ^ n) : ℤ) =
  emultiplicity (α := ℤ) (↑p : ℤ) (↑(x + y) : ℤ) + emultiplicity p n
Tactic: iterate 2 rw [← Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n + y ^ n) : ℤ) =
    emultiplicity (α := ℤ) (↑p : ℤ) (↑(x + y) : ℤ) + emultiplicity p n
have rw : ∀ (hxy : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(x + y) : ℤ)) (hx : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x : ℤ)) {n : ℕ} (hn : Odd n),
  emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n + y ^ n) : ℤ) =
    emultiplicity (α := ℤ) (↑p : ℤ) (↑(x + y) : ℤ) + emultiplicity p n
Tactic: rw [← Int.natCast_dvd_natCast] at hxy hx
Cleared hypotheses: hxy, hx, n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : Dvd.dvd (α := ℤ) (↑p : ℤ) (↑(x + y) : ℤ)
hx : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x : ℤ)
n : ℕ
hn : Odd n
⊢ emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n + y ^ n) : ℤ) =
    emultiplicity (α := ℤ) (↑p : ℤ) (↑(x + y) : ℤ) + emultiplicity p n
have hxy₁ : (↑p : ℤ) ∣ HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)
Tactic: push_cast at *
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
d : ℕ
hd :
  x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d =
    (∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
this :
  x ^ HPow.hPow (α := ℕ) 2 d.succ - y ^ HPow.hPow (α := ℕ) 2 d.succ =
    (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      (x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d)
⊢ x ^ HPow.hPow (α := ℕ) 2 (d + 1) - y ^ HPow.hPow (α := ℕ) 2 (d + 1) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
have rw : (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) * (x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d) =
  (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
Tactic: rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
d : ℕ
hd :
  x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d =
    (∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
this :
  x ^ HPow.hPow (α := ℕ) 2 d.succ - y ^ HPow.hPow (α := ℕ) 2 d.succ =
    (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      (x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d)
rw :
  (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      (x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
⊢ x ^ HPow.hPow (α := ℕ) 2 (d + 1) - y ^ HPow.hPow (α := ℕ) 2 (d + 1) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
have rw₁ : (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
    ((∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)) =
  (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
Tactic: rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
d : ℕ
hd :
  x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d =
    (∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
this :
  x ^ HPow.hPow (α := ℕ) 2 d.succ - y ^ HPow.hPow (α := ℕ) 2 d.succ =
    (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      (x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d)
rw :
  (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      (x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
rw₁ :
  (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      ((∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
⊢ x ^ HPow.hPow (α := ℕ) 2 (d + 1) - y ^ HPow.hPow (α := ℕ) 2 (d + 1) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
have rw₂ : (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
    ((∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)) =
  (∏ x_1 ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 x_1 + y ^ HPow.hPow (α := ℕ) 2 x_1)) *
      (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
    (x - y)
Tactic: rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
d : ℕ
hd :
  x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d =
    (∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
this :
  x ^ HPow.hPow (α := ℕ) 2 d.succ - y ^ HPow.hPow (α := ℕ) 2 d.succ =
    (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      (x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d)
rw :
  (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      (x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
rw₁ :
  (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      ((∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
rw₂ :
  (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      ((∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)) =
    (∏ x_1 ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 x_1 + y ^ HPow.hPow (α := ℕ) 2 x_1)) *
        (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      (x - y)
⊢ x ^ HPow.hPow (α := ℕ) 2 (d + 1) - y ^ HPow.hPow (α := ℕ) 2 (d + 1) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
have rw₃ : ((x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      ∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) *
    (x - y) =
  (∏ x_1 ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 x_1 + y ^ HPow.hPow (α := ℕ) 2 x_1)) *
      (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
    (x - y)
Tactic: rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
d : ℕ
hd :
  x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d =
    (∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
this :
  x ^ HPow.hPow (α := ℕ) 2 d.succ - y ^ HPow.hPow (α := ℕ) 2 d.succ =
    (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      (x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d)
rw :
  (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      (x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
rw₁ :
  (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      ((∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
rw₂ :
  (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      ((∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)) =
    (∏ x_1 ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 x_1 + y ^ HPow.hPow (α := ℕ) 2 x_1)) *
        (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      (x - y)
rw₃ :
  ((x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
        ∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) *
      (x - y) =
    (∏ x_1 ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 x_1 + y ^ HPow.hPow (α := ℕ) 2 x_1)) *
        (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      (x - y)
⊢ x ^ HPow.hPow (α := ℕ) 2 (d + 1) - y ^ HPow.hPow (α := ℕ) 2 (d + 1) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
have rw₄ : (∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) *
      (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
    (x - y) =
  (∏ x_1 ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 x_1 + y ^ HPow.hPow (α := ℕ) 2 x_1)) *
      (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
    (x - y)
Tactic: rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
d : ℕ
hd :
  x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d =
    (∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
⊢ x ^ HPow.hPow (α := ℕ) 2 (d + 1) - y ^ HPow.hPow (α := ℕ) 2 (d + 1) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
have succ : x ^ HPow.hPow (α := ℕ) 2 d.succ - y ^ HPow.hPow (α := ℕ) 2 d.succ =
  (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) * (x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d)
Tactic: suffices x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d) by
      rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
n : ℕ
⊢ x ^ HPow.hPow (α := ℕ) 2 n - y ^ HPow.hPow (α := ℕ) 2 n =
    (∏ i ∈ range n, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
have zero : x ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0 - y ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0 =
  (∏ i ∈ range 0, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
Tactic: induction n with
  | zero => simp only [pow_zero, pow_one, range_zero, prod_empty, one_mul]
  | succ d hd =>
    suffices x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d) by
      rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]
    rw [Nat.succ_eq_add_one]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R
n : ℕ
zero :
  x ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0 - y ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0 =
    (∏ i ∈ range 0, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
⊢ x ^ HPow.hPow (α := ℕ) 2 n - y ^ HPow.hPow (α := ℕ) 2 n =
    (∏ i ∈ range n, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
have succ : ∀ (d : ℕ)
  (hd :
    x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d =
      (∏ i ∈ range d, (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)),
  x ^ HPow.hPow (α := ℕ) 2 (d + 1) - y ^ HPow.hPow (α := ℕ) 2 (d + 1) =
    (∏ i ∈ range (d + 1), (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)) * (x - y)
Tactic: induction n with
  | zero => simp only [pow_zero, pow_one, range_zero, prod_empty, one_mul]
  | succ d hd =>
    suffices x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d) by
      rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]
    rw [Nat.succ_eq_add_one]
    ring
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x : ℤ
hx : ∃ (k : ℤ), x = 2 * k + 1
⊢ HPow.hPow (β := ℕ) x 2 % 4 = 1
have rcases : ∀ (w : ℤ), HPow.hPow (β := ℕ) (2 * w + 1) 2 % 4 = 1
Tactic: rcases hx with ⟨_, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
w : ℤ
⊢ HPow.hPow (β := ℕ) (2 * w + 1) 2 % 4 = 1
have ring_nf : (1 + w * 4 + HPow.hPow (β := ℕ) w 2 * 4) % 4 = 1
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
w : ℤ
⊢ (1 + w * 4 + HPow.hPow (β := ℕ) w 2 * 4) % 4 = 1
have rw : HMod.hMod (α := ℤ) 1 4 = 1
Tactic: rw [add_assoc, ← add_mul, Int.add_mul_emod_self_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
k : ℤ
hk : Odd k
⊢ 8 ∣ HPow.hPow (β := ℕ) k 2 - 1
have rcases : ∀ (m : ℤ), 8 ∣ HPow.hPow (β := ℕ) (2 * m + 1) 2 - 1
Tactic: rcases hk with ⟨m, rfl⟩
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
m : ℤ
⊢ 8 ∣ HPow.hPow (β := ℕ) (2 * m + 1) 2 - 1
have eq : HPow.hPow (β := ℕ) (2 * m + 1) 2 - 1 = 4 * (m * (m + 1))
Tactic: have eq : (2 * m + 1) ^ 2 - 1 = 4 * (m * (m + 1)) := by ring