awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ))
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)
⊢ 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]
-- 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 (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 suffices : emultiplicity (α := ℤ) 2 (↑2 : ℤ) = 1
Tactic: suffices emultiplicity (2 : ℤ) ↑(2 : ℕ) = 1 by 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
⊢ emultiplicity (α := ℤ) 2 (↑2 : ℤ) = 1
have norm_cast : emultiplicity (α := ℕ) 2 2 = 1
Tactic: norm_cast
-- 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 2 = 1
have rw : FiniteMultiplicity (α := ℕ) 2 2
Tactic: rw [FiniteMultiplicity.emultiplicity_self]
-- 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
⊢ FiniteMultiplicity (α := ℕ) 2 2
have rw : Ne (α := ℕ) 2 1 ∧ LT.lt (α := ℕ) 0 2
Tactic: rw [Nat.finiteMultiplicity_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
⊢ ¬2 ∣ HPow.hPow (β := ℕ) x 2
have rw : Odd (HPow.hPow (β := ℕ) x 2)
Tactic: rw [← even_iff_two_dvd, Int.not_even_iff_odd]
-- 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
⊢ Odd (HPow.hPow (β := ℕ) x 2)
have ha : Odd x
Tactic: apply Odd.pow
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
have inl : ∀ (hyx : y ≤ x),
  emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
Tactic: obtain hyx | hyx := le_total y x
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
inl :
  ∀ (hyx : y ≤ x),
    emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
have inr : ∀ (hyx : x ≤ y),
  emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
Tactic: obtain hyx | hyx := le_total y x
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
have inl : emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
  emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
Tactic: rw [← Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
have inl : emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
  emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x + y) : ℤ) + emultiplicity 2 (x - y) + emultiplicity 2 n
Tactic: rw [← Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
    emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x + y) : ℤ) + emultiplicity 2 (x - y) + emultiplicity 2 n
have inl : emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
  emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x + y) : ℤ) + emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x - y) : ℤ) + emultiplicity 2 n
Tactic: rw [← Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
have inl : emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
  emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x + y) : ℤ) + emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x - y) : ℤ) + emultiplicity 2 n
Tactic: iterate 3 rw [← Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x ^ n - y ^ n) : ℤ) + 1 =
    emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x + y) : ℤ) + emultiplicity (α := ℤ) (↑2 : ℤ) (↑(x - y) : ℤ) + emultiplicity 2 n
have inl : emultiplicity (↑2 : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) + 1 =
  emultiplicity (↑2 : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
      emultiplicity (↑2 : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
    emultiplicity 2 n
Tactic: simp only [Int.ofNat_sub hyx, Int.ofNat_sub (pow_le_pow_left' hyx _), Int.natCast_add,
      Int.natCast_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (↑2 : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) + 1 =
    emultiplicity (↑2 : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
        emultiplicity (↑2 : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
      emultiplicity 2 n
have inl : ∀ (hx : ¬Dvd.dvd (α := ℤ) (↑2 : ℤ) (↑x : ℤ)) {n : ℕ} (hn : Even n) (hyx : y ≤ x),
  emultiplicity (↑2 : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) + 1 =
    emultiplicity (↑2 : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
        emultiplicity (↑2 : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
      emultiplicity 2 n
Tactic: rw [← Int.natCast_dvd_natCast] at hx
Cleared hypotheses: hx, n, hn, hyx
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬Dvd.dvd (α := ℤ) (↑2 : ℤ) (↑x : ℤ)
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (↑2 : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) + 1 =
    emultiplicity (↑2 : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
        emultiplicity (↑2 : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
      emultiplicity 2 n
have inl : ∀ (hxy : (↑2 : ℤ) ∣ HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) (hx : ¬Dvd.dvd (α := ℤ) (↑2 : ℤ) (↑x : ℤ)) {n : ℕ}
  (hn : Even n) (hyx : y ≤ x),
  emultiplicity (↑2 : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) + 1 =
    emultiplicity (↑2 : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
        emultiplicity (↑2 : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
      emultiplicity 2 n
Tactic: rw [← Int.natCast_dvd_natCast, Int.ofNat_sub hyx] at hxy
Cleared hypotheses: hxy, hx, n, hn, hyx
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hxy : (↑2 : ℤ) ∣ HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
hx : ¬Dvd.dvd (α := ℤ) (↑2 : ℤ) (↑x : ℤ)
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity (↑2 : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) + 1 =
    emultiplicity (↑2 : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
        emultiplicity (↑2 : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) +
      emultiplicity 2 n
have h : emultiplicity 2 n = emultiplicity (α := ℤ) 2 (↑n : ℤ)
Tactic: convert! Int.two_pow_sub_pow hxy hx hn using 2
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hxy : (↑2 : ℤ) ∣ HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
hx : ¬Dvd.dvd (α := ℤ) (↑2 : ℤ) (↑x : ℤ)
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity 2 n = emultiplicity (α := ℤ) 2 (↑n : ℤ)
have h : emultiplicity (α := ℤ) (↑2 : ℤ) (↑n : ℤ) = emultiplicity (α := ℤ) 2 (↑n : ℤ)
Tactic: rw [← Int.natCast_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 (x ^ n - y ^ n) + 1 = padicValNat 2 (x + y) + padicValNat 2 (x - y) + padicValNat 2 n
have simp : HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x ^ n - y ^ n)) : ℕ∞) (↑1 : ℕ∞) =
  HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
Tactic: simp only [← Nat.cast_inj (R := ℕ∞), Nat.cast_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x ^ n - y ^ n)) : ℕ∞) (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
have rw : emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
  HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
rw :
  emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x ^ n - y ^ n)) : ℕ∞) (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
have rw₁ : x ^ n - y ^ n ≠ 0
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
have rw : emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
  emultiplicity 2 (x + y) + (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
rw :
  emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    emultiplicity 2 (x + y) + (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
⊢ emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
have rw₁ : x + y ≠ 0
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    emultiplicity 2 (x + y) + (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
have rw : emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
  emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + (↑(padicValNat 2 n) : ℕ∞)
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
rw :
  emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + (↑(padicValNat 2 n) : ℕ∞)
⊢ emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    emultiplicity 2 (x + y) + (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
have rw₁ : x - y ≠ 0
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + (↑(padicValNat 2 n) : ℕ∞)
have rw : emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x ^ n - y ^ n)) : ℕ∞) (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
have iterate : emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
Tactic: iterate 4 rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
iterate :
  emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
iterate₁ : n ≠ 0
⊢ HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x ^ n - y ^ n)) : ℕ∞) (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
have iterate₂ : x - y ≠ 0
Tactic: iterate 4 rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
iterate :
  emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
iterate₁ : n ≠ 0
iterate₂ : x - y ≠ 0
⊢ HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x ^ n - y ^ n)) : ℕ∞) (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
have iterate₃ : x + y ≠ 0
Tactic: iterate 4 rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
iterate :
  emultiplicity 2 (x ^ n - y ^ n) + (↑1 : ℕ∞) = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n
iterate₁ : n ≠ 0
iterate₂ : x - y ≠ 0
iterate₃ : x + y ≠ 0
⊢ HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x ^ n - y ^ n)) : ℕ∞) (↑1 : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat 2 (x + y)) : ℕ∞) (↑(padicValNat 2 (x - y)) : ℕ∞) + (↑(padicValNat 2 n) : ℕ∞)
have iterate₄ : x ^ n - y ^ n ≠ 0
Tactic: iterate 4 rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 ((x + 1) * (x - 1)) ≥ 3
have refine : HPow.hPow (α := ℕ) (β := ℕ) 2 3 ∣ (x + 1) * (x - 1)
Tactic: refine (padicValNat_dvd_iff_le (by grind [mul_ne_zero])).mp ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ HPow.hPow (α := ℕ) (β := ℕ) 2 3 ∣ (x + 1) * (x - 1)
have simp : 8 ∣ HPow.hPow (β := ℕ) x 2 - 1
Tactic: simp [← Nat.pow_two_sub_pow_two x 1]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 n + 2 ≤ padicValNat 2 (x ^ n - 1)
have this : padicValNat 2 ((x + 1) * (x - 1)) ≥ 3
Tactic: have : padicValNat 2 ((x + 1) * (x - 1)) ≥ 3 := by
    refine (padicValNat_dvd_iff_le (by grind [mul_ne_zero])).mp ?_
    simp [← Nat.pow_two_sub_pow_two x 1]
    grind [Nat.eight_dvd_sq_sub_one_of_odd]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (hypothesis)
Goal:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
this : padicValNat 2 ((x + 1) * (x - 1)) ≥ 3
⊢ padicValNat 2 n + 2 ≤ padicValNat 2 (x ^ n - 1)
have this₁ : padicValNat 2 (x ^ n - 1) + 1 = padicValNat 2 (x + 1) + padicValNat 2 (x - 1) + padicValNat 2 n
Tactic: have := pow_two_sub_one h1x hx hn hneven
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ padicValNat p (x ^ n - y ^ n) = padicValNat p (x - y) + padicValNat p n
have rw : (↑(padicValNat p (x ^ n - y ^ n)) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
Tactic: rw [← Nat.cast_inj (R := ℕ∞), Nat.cast_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ (↑(padicValNat p (x ^ n - y ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have rw : emultiplicity p (x ^ n - y ^ n) = HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
rw : emultiplicity p (x ^ n - y ^ n) = HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
⊢ (↑(padicValNat p (x ^ n - y ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have rw₁ : x ^ n - y ^ n ≠ 0
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ emultiplicity p (x ^ n - y ^ n) = HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have rw : emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + (↑(padicValNat p n) : ℕ∞)
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
rw : emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + (↑(padicValNat p n) : ℕ∞)
⊢ emultiplicity p (x ^ n - y ^ n) = HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have rw₁ : x - y ≠ 0
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + (↑(padicValNat p n) : ℕ∞)
have rw : emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ (↑(padicValNat p (x ^ n - y ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have iterate : emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
Tactic: iterate 3 rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
iterate : emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
iterate₁ : n ≠ 0
⊢ (↑(padicValNat p (x ^ n - y ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have iterate₂ : x - y ≠ 0
Tactic: iterate 3 rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
iterate : emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n
iterate₁ : n ≠ 0
iterate₂ : x - y ≠ 0
⊢ (↑(padicValNat p (x ^ n - y ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x - y)) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have iterate₃ : x ^ n - y ^ n ≠ 0
Tactic: iterate 3 rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ padicValNat p (x ^ n + y ^ n) = padicValNat p (x + y) + padicValNat p n
have zero : ∀ (hxy : p ∣ x + 0), padicValNat p (x ^ n + HPow.hPow (α := ℕ) 0 n) = padicValNat p (x + 0) + padicValNat p n
Tactic: rcases y with - | y
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
zero : ∀ (hxy : p ∣ x + 0), padicValNat p (x ^ n + HPow.hPow (α := ℕ) 0 n) = padicValNat p (x + 0) + padicValNat p n
⊢ padicValNat p (x ^ n + y ^ n) = padicValNat p (x + y) + padicValNat p n
have succ : ∀ (y : ℕ) (hxy : p ∣ x + (y + 1)), padicValNat p (x ^ n + (y + 1) ^ n) = padicValNat p (x + (y + 1)) + padicValNat p n
Tactic: rcases y with - | y
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ padicValNat p (x ^ n + (y + 1) ^ n) = padicValNat p (x + (y + 1)) + padicValNat p n
have succ : (↑(padicValNat p (x ^ n + (y + 1) ^ n)) : ℕ∞) =
  HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
Tactic: rw [← Nat.cast_inj (R := ℕ∞), Nat.cast_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ (↑(padicValNat p (x ^ n + (y + 1) ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have succ : emultiplicity p (x ^ n + (y + 1) ^ n) =
  HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
succ :
  emultiplicity p (x ^ n + (y + 1) ^ n) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
⊢ (↑(padicValNat p (x ^ n + (y + 1) ^ n)) : ℕ∞) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have succ₁ : x ^ n + (y + 1) ^ n ≠ 0
Tactic: rw [padicValNat_eq_emultiplicity]
-- Lean 4 proof step from Mathlib.NumberTheory.Multiplicity (goal)
Goal:
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ emultiplicity p (x ^ n + (y + 1) ^ n) =
    HAdd.hAdd (α := ℕ∞) (↑(padicValNat p (x + (y + 1))) : ℕ∞) (↑(padicValNat p n) : ℕ∞)
have succ : emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + (↑(padicValNat p n) : ℕ∞)
Tactic: rw [padicValNat_eq_emultiplicity]