awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 grind
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
⊢ Odd x
have rwa : ¬Even x
Tactic: rwa [← Int.not_even_iff_odd, even_iff_two_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
⊢ emultiplicity 2 (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i) = (↑1 : ℕ∞)
have hx_odd : Odd x
Tactic: have hx_odd : Odd x := by rwa [← Int.not_even_iff_odd, even_iff_two_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
⊢ emultiplicity 2 (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i) = (↑1 : ℕ∞)
have hxy_even : Even (x - y)
Tactic: have hxy_even : Even (x - y) := even_iff_two_dvd.mpr (dvd_trans (by decide) hxy)
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ emultiplicity 2 (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i) = (↑1 : ℕ∞)
have hy_odd : Odd y
Tactic: have hy_odd : Odd y := by simpa using hx_odd.sub_even hxy_even
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ emultiplicity 2 (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i) = (↑1 : ℕ∞)
have refine_1 : HPow.hPow (α := ℤ) (β := ℕ) 2 1 ∣ x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i
Tactic: refine emultiplicity_eq_coe.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
refine_1 : HPow.hPow (α := ℤ) (β := ℕ) 2 1 ∣ x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i
⊢ emultiplicity 2 (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i) = (↑1 : ℕ∞)
have refine_2 : ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣ x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i
Tactic: refine emultiplicity_eq_coe.mpr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ HPow.hPow (α := ℤ) (β := ℕ) 2 1 ∣ x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i
have refine_1 : Even (x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i)
Tactic: rw [pow_one, ← even_iff_two_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣ x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i
have refine_2 : ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣
    x ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0 + y ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0
Tactic: rcases i with - | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
refine_2 :
  ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣
      x ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0 + y ^ HPow.hPow (α := ℕ) (β := ℕ) 2 0
⊢ ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣ x ^ HPow.hPow (α := ℕ) 2 i + y ^ HPow.hPow (α := ℕ) 2 i
have refine_2₁ : ∀ (i : ℕ),
  ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣ x ^ HPow.hPow (α := ℕ) 2 (i + 1) + y ^ HPow.hPow (α := ℕ) 2 (i + 1)
Tactic: rcases i with - | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ HPow.hPow (α := ℕ) 2 (i + 1) % 4 = 1
⊢ ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣ x ^ HPow.hPow (α := ℕ) 2 (i + 1) + y ^ HPow.hPow (α := ℕ) 2 (i + 1)
have rw : ¬HAdd.hAdd (α := ℤ) 1 1 % 4 = 0
Tactic: rw [show (2 ^ (1 + 1) : ℤ) = 4 by simp, Int.dvd_iff_emod_eq_zero, Int.add_emod,
      this _ hx_odd, this _ hy_odd]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
⊢ ¬HPow.hPow (α := ℤ) 2 (HAdd.hAdd (α := ℕ) 1 1) ∣ x ^ HPow.hPow (α := ℕ) 2 (i + 1) + y ^ HPow.hPow (α := ℕ) 2 (i + 1)
have refine_2 : ∀ (x : ℤ), Odd x → x ^ HPow.hPow (α := ℕ) 2 (i + 1) % 4 = 1
Tactic: suffices ∀ x : ℤ, Odd x → x ^ 2 ^ (i + 1) % 4 = 1 by
    rw [show (2 ^ (1 + 1) : ℤ) = 4 by simp, Int.dvd_iff_emod_eq_zero, Int.add_emod,
      this _ hx_odd, this _ hy_odd]
    decide
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x_1 y : ℤ
hx_1 : ¬2 ∣ x_1
hxy : 4 ∣ x_1 - y
hx_odd : Odd x_1
hxy_even : Even (x_1 - y)
hy_odd : Odd y
i : ℕ
x : ℤ
hx : Odd x
⊢ x ^ HPow.hPow (α := ℕ) 2 (i + 1) % 4 = 1
have refine_2 : x ^ (2 * HPow.hPow (α := ℕ) 2 i) % 4 = 1
Tactic: rw [pow_succ', mul_comm, pow_mul, Int.sq_mod_four_eq_one_of_odd hx.pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x_1 y : ℤ
hx_1 : ¬2 ∣ x_1
hxy : 4 ∣ x_1 - y
hx_odd : Odd x_1
hxy_even : Even (x_1 - y)
hy_odd : Odd y
i : ℕ
x : ℤ
hx : Odd x
refine_2 : x ^ (2 * HPow.hPow (α := ℕ) 2 i) % 4 = 1
⊢ x ^ HPow.hPow (α := ℕ) 2 (i + 1) % 4 = 1
have refine_2₁ : x ^ (HPow.hPow (α := ℕ) 2 i * 2) % 4 = 1
Tactic: rw [pow_succ', mul_comm, pow_mul, Int.sq_mod_four_eq_one_of_odd hx.pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x_1 y : ℤ
hx_1 : ¬2 ∣ x_1
hxy : 4 ∣ x_1 - y
hx_odd : Odd x_1
hxy_even : Even (x_1 - y)
hy_odd : Odd y
i : ℕ
x : ℤ
hx : Odd x
refine_2 : x ^ (2 * HPow.hPow (α := ℕ) 2 i) % 4 = 1
refine_2₁ : x ^ (HPow.hPow (α := ℕ) 2 i * 2) % 4 = 1
⊢ x ^ HPow.hPow (α := ℕ) 2 (i + 1) % 4 = 1
have refine_2₂ : HPow.hPow (β := ℕ) (x ^ HPow.hPow (α := ℕ) 2 i) 2 % 4 = 1
Tactic: rw [pow_succ', mul_comm, pow_mul, Int.sq_mod_four_eq_one_of_odd hx.pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x_1 y : ℤ
hx_1 : ¬2 ∣ x_1
hxy : 4 ∣ x_1 - y
hx_odd : Odd x_1
hxy_even : Even (x_1 - y)
hy_odd : Odd y
i : ℕ
x : ℤ
hx : Odd x
refine_2 : x ^ (2 * HPow.hPow (α := ℕ) 2 i) % 4 = 1
refine_2₁ : x ^ (HPow.hPow (α := ℕ) 2 i * 2) % 4 = 1
refine_2₂ : HPow.hPow (β := ℕ) (x ^ HPow.hPow (α := ℕ) 2 i) 2 % 4 = 1
⊢ x ^ HPow.hPow (α := ℕ) 2 (i + 1) % 4 = 1
have refine_2₃ : Eq (α := ℤ) 1 1
Tactic: rw [pow_succ', mul_comm, pow_mul, Int.sq_mod_four_eq_one_of_odd hx.pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
⊢ Odd x
have rwa : ¬Even x
Tactic: rwa [← Int.not_even_iff_odd, even_iff_two_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
⊢ emultiplicity 2 (x ^ n - y ^ n) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑n : ℤ)
have hx_odd : Odd x
Tactic: have hx_odd : Odd x := by rwa [← Int.not_even_iff_odd, even_iff_two_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
⊢ emultiplicity 2 (x ^ n - y ^ n) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑n : ℤ)
have hxy_even : Even (x - y)
Tactic: have hxy_even : Even (x - y) := even_iff_two_dvd.mpr (dvd_trans (by decide) hxy)
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ emultiplicity 2 (x ^ n - y ^ n) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑n : ℤ)
have hy_odd : Odd y
Tactic: have hy_odd : Odd y := by simpa using hx_odd.sub_even hxy_even
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ emultiplicity 2 (x ^ n - y ^ n) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑n : ℤ)
have zero : emultiplicity 2 (HPow.hPow (β := ℕ) x 0 - HPow.hPow (β := ℕ) y 0) =
  emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑0 : ℤ)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
zero :
  emultiplicity 2 (HPow.hPow (β := ℕ) x 0 - HPow.hPow (β := ℕ) y 0) =
    emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑0 : ℤ)
⊢ emultiplicity 2 (x ^ n - y ^ n) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑n : ℤ)
have succ : ∀ (n : ℕ),
  emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
have h : FiniteMultiplicity 2 n.succ
Tactic: have h : FiniteMultiplicity 2 n.succ := Nat.finiteMultiplicity_iff.mpr ⟨by simp, n.succ_pos⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
have succ : ∀ (hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1) (k : ℕ)
  (hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k),
  emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
Tactic: rcases emultiplicity_eq_coe.mp h.emultiplicity_eq_multiplicity with ⟨⟨k, hk⟩, hpn⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
have succ : emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) =
  emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
Tactic: rw [hk, pow_mul, pow_mul, emultiplicity_pow_sub_pow_of_prime,
    Int.two_pow_two_pow_sub_pow_two_pow _ hxy hx, ← hk]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
succ :
  emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) =
    emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
have succ₁ : Prime (M := ℤ) 2
Tactic: rw [hk, pow_mul, pow_mul, emultiplicity_pow_sub_pow_of_prime,
    Int.two_pow_two_pow_sub_pow_two_pow _ hxy hx, ← hk]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
succ :
  emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) =
    emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
succ₁ : Prime (M := ℤ) 2
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
have succ₂ : 2 ∣ x ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) - y ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1))
Tactic: rw [hk, pow_mul, pow_mul, emultiplicity_pow_sub_pow_of_prime,
    Int.two_pow_two_pow_sub_pow_two_pow _ hxy hx, ← hk]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
succ :
  emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) =
    emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
succ₁ : Prime (M := ℤ) 2
succ₂ : 2 ∣ x ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) - y ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1))
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
have succ₃ : ¬2 ∣ x ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1))
Tactic: rw [hk, pow_mul, pow_mul, emultiplicity_pow_sub_pow_of_prime,
    Int.two_pow_two_pow_sub_pow_two_pow _ hxy hx, ← hk]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
succ :
  emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) =
    emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
succ₁ : Prime (M := ℤ) 2
succ₂ : 2 ∣ x ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) - y ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1))
succ₃ : ¬2 ∣ x ^ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1))
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
have succ₄ : ¬Dvd.dvd (α := ℤ) 2 (↑k : ℤ)
Tactic: rw [hk, pow_mul, pow_mul, emultiplicity_pow_sub_pow_of_prime,
    Int.two_pow_two_pow_sub_pow_two_pow _ hxy hx, ← hk]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
⊢ emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) =
    emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(n + 1) : ℤ)
have succ : emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) = emultiplicity 2 (x - y) + emultiplicity 2 (n + 1)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
⊢ emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) = emultiplicity 2 (x - y) + emultiplicity 2 (n + 1)
have succ : emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞) = emultiplicity 2 (x - y) + (↑(multiplicity 2 (n + 1)) : ℕ∞)
Tactic: rw [h.emultiplicity_eq_multiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
⊢ ¬Dvd.dvd (α := ℤ) 2 (↑k : ℤ)
have succ : ¬2 ∣ k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
⊢ ¬2 ∣ k
have succ : ∀ (hpn : 2 ∣ k), HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1) + 1) ∣ n + 1
Tactic: contrapose hpn
Cleared hypotheses: hpn
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
hpn : 2 ∣ k
| n + 1
have rw : HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
Tactic: rw [hk]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
k : ℕ
hk : n + 1 = HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
hpn : 2 ∣ k
⊢ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * 2 ∣ n + 1
have succ : HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * 2 ∣ HPow.hPow (α := ℕ) 2 (multiplicity 2 (n + 1)) * k
Tactic: conv_rhs => rw [hk]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hn : Even n
⊢ Odd y
have hx₁ : Odd x
Tactic: rw [← even_iff_two_dvd, Int.not_even_iff_odd] at hx
Cleared hypotheses: hx, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : Odd x
hn : Even n
⊢ Odd y
have hxy₁ : Even (-(x - y))
Tactic: replace hxy := (@even_neg _ _ (x - y)).mpr (even_iff_two_dvd.mpr hxy)
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
n : ℕ
hx : Odd x
hn : Even n
hxy : Even (-(x - y))
⊢ Odd y
have h : y = -(x - y) + x
Tactic: convert! Even.add_odd hxy hx
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hn : Even n
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑n : ℤ)
have hy : Odd y
Tactic: have hy : Odd y := by
    rw [← even_iff_two_dvd, Int.not_even_iff_odd] at hx
    replace hxy := (@even_neg _ _ (x - y)).mpr (even_iff_two_dvd.mpr hxy)
    convert! Even.add_odd hxy hx
    abel
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hn : Even n
hy : Odd y
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑n : ℤ)
have obtain : ∀ (d : ℕ),
  emultiplicity 2 (x ^ (d + d) - y ^ (d + d)) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(d + d) : ℤ)
Tactic: obtain ⟨d, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ emultiplicity 2 (x ^ (d + d) - y ^ (d + d)) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(d + d) : ℤ)
have simp : emultiplicity 2 (HPow.hPow (β := ℕ) x 2 ^ d - HPow.hPow (β := ℕ) y 2 ^ d) + 1 =
  emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(2 * d) : ℤ)
Tactic: simp only [← two_mul, pow_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
have rw : HSub.hSub (α := ℤ) 1 1 % 4 = 0
Tactic: rw [Int.dvd_iff_emod_eq_zero, Int.sub_emod, Int.sq_mod_four_eq_one_of_odd _,
      Int.sq_mod_four_eq_one_of_odd hy]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
rw : HSub.hSub (α := ℤ) 1 1 % 4 = 0
⊢ 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
have rw₁ : Odd x
Tactic: rw [Int.dvd_iff_emod_eq_zero, Int.sub_emod, Int.sq_mod_four_eq_one_of_odd _,
      Int.sq_mod_four_eq_one_of_odd hy]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ emultiplicity 2 (HPow.hPow (β := ℕ) x 2 ^ d - HPow.hPow (β := ℕ) y 2 ^ d) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(2 * d) : ℤ)
have hxy4 : 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
Tactic: have hxy4 : 4 ∣ x ^ 2 - y ^ 2 := by
    rw [Int.dvd_iff_emod_eq_zero, Int.sub_emod, Int.sq_mod_four_eq_one_of_odd _,
      Int.sq_mod_four_eq_one_of_odd hy]
    · simp
    · simp only [← Int.not_even_iff_odd, even_iff_two_dvd, hx, not_false_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
⊢ emultiplicity 2 (HPow.hPow (β := ℕ) x 2 ^ d - HPow.hPow (β := ℕ) y 2 ^ d) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(2 * d) : ℤ)
have rw : emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1 =
  emultiplicity 2 (x + y) + emultiplicity 2 (x - y) +
    (emultiplicity (α := ℤ) 2 (↑2 : ℤ) + emultiplicity (α := ℤ) 2 (↑d : ℤ))
Tactic: rw [Int.two_pow_sub_pow' d hxy4 _, sq_sub_sq, ← Int.ofNat_mul_ofNat,
    emultiplicity_mul Int.prime_two, emultiplicity_mul Int.prime_two]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
rw :
  emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) +
      (emultiplicity (α := ℤ) 2 (↑2 : ℤ) + emultiplicity (α := ℤ) 2 (↑d : ℤ))
⊢ emultiplicity 2 (HPow.hPow (β := ℕ) x 2 ^ d - HPow.hPow (β := ℕ) y 2 ^ d) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑(2 * d) : ℤ)
have rw₁ : ¬2 ∣ HPow.hPow (β := ℕ) x 2
Tactic: rw [Int.two_pow_sub_pow' d hxy4 _, sq_sub_sq, ← Int.ofNat_mul_ofNat,
    emultiplicity_mul Int.prime_two, emultiplicity_mul Int.prime_two]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
this : emultiplicity (α := ℤ) 2 (↑2 : ℤ) = 1
⊢ emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) +
      (emultiplicity (α := ℤ) 2 (↑2 : ℤ) + emultiplicity (α := ℤ) 2 (↑d : ℤ))
have rw : emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1 =
  emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + (1 + emultiplicity (α := ℤ) 2 (↑d : ℤ))
Tactic: rw [this, add_comm 1, ← add_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ HPow.hPow (β := ℕ) x 2 - HPow.hPow (β := ℕ) y 2
this : emultiplicity (α := ℤ) 2 (↑2 : ℤ) = 1
rw :
  emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + (1 + emultiplicity (α := ℤ) 2 (↑d : ℤ))
⊢ emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) +
      (emultiplicity (α := ℤ) 2 (↑2 : ℤ) + emultiplicity (α := ℤ) 2 (↑d : ℤ))
have rw₁ : emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1 =
  emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + (emultiplicity (α := ℤ) 2 (↑d : ℤ) + 1)
Tactic: rw [this, add_comm 1, ← add_assoc]