awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Multiplicity
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
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)
⊢ 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

Premises used: Nat.prime_iff_prime_int
-- Module: Mathlib.NumberTheory.Multiplicity
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)
succ₂ : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑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 [emultiplicity_pow_sub_pow_of_prime hp,
    emultiplicity_pow_prime_pow_sub_pow_prime_pow hp hp1 hxy hx, h.emultiplicity_eq_multiplicity]

Premises used: FiniteMultiplicity.emultiplicity_eq_multiplicity, emultiplicity_pow_sub_pow_of_prime, emultiplicity_pow_prime_pow_sub_pow_prime_pow
-- Module: Mathlib.NumberTheory.Multiplicity
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 : ℤ) ∣ (∑ i ∈ range (p ^ multiplicity p (n + 1)), x ^ i * y ^ (p ^ multiplicity p (n + 1) - 1 - i)) * (x - y)
⊢ (↑p : ℤ) ∣ x ^ p ^ multiplicity p (n + 1) - y ^ p ^ multiplicity p (n + 1)

Tactic:
rw [← geom_sum₂_mul]

Premises used: geom_sum₂_mul
-- Module: Mathlib.NumberTheory.Multiplicity
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 : ℤ) ∣ (∑ i ∈ range (p ^ multiplicity p (n + 1)), x ^ i * y ^ (p ^ multiplicity p (n + 1) - 1 - i)) * (x - y)

Tactic:
dvd_mul_of_dvd_right hxy

Premises used: Int.dvd_mul_of_dvd_right
-- Module: Mathlib.NumberTheory.Multiplicity
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 : ℤ) ∣ (∑ i ∈ range (p ^ multiplicity p (n + 1)), x ^ i * y ^ (p ^ multiplicity p (n + 1) - 1 - i)) * (x - y)

Tactic:
exact dvd_mul_of_dvd_right hxy

Premises used: Int.dvd_mul_of_dvd_right
-- Module: Mathlib.NumberTheory.Multiplicity
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)

Tactic:
fun h => hx (hp.dvd_of_dvd_pow h)

Premises used: Prime.dvd_of_dvd_pow, Not
-- Module: Mathlib.NumberTheory.Multiplicity
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)

Tactic:
exact fun h => hx (hp.dvd_of_dvd_pow h)

Premises used: Prime.dvd_of_dvd_pow
-- Module: Mathlib.NumberTheory.Multiplicity
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 ∣ k
⊢ ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑k : ℤ)

Tactic:
rw [Int.natCast_dvd_natCast]

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Multiplicity
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

Tactic:
hpn ⟨c, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.NumberTheory.Multiplicity
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)
succ : n + 1 = p ^ (multiplicity p (n + 1) + 1) * c
⊢ False

Tactic:
refine hpn ⟨c, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.NumberTheory.Multiplicity
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)
succ : n + 1 = p ^ multiplicity p (n + 1) * p * c
succ₁ succ₂ succ₃ succ₄ : n + 1 = p ^ multiplicity p (n + 1) * (p * c)
⊢ n + 1 = p ^ (multiplicity p (n + 1) + 1) * c

Tactic:
rwa [pow_succ, mul_assoc]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x + y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
hn : Odd n
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
⊢ emultiplicity (↑p : ℤ) (x ^ n + y ^ n) = emultiplicity (↑p : ℤ) (x + y) + emultiplicity p n

Tactic:
rw [← sub_neg_eq_add] at hxy

Premises used: sub_neg_eq_add
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : (↑p : ℤ) ∣ x - -y
hx : ¬(↑p : ℤ) ∣ x
n : ℕ
hn : Odd n
rw : 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

Tactic:
rw [← sub_neg_eq_add, ← sub_neg_eq_add, ← Odd.neg_pow hn]

Premises used: Odd.neg_pow, sub_neg_eq_add
-- Module: Mathlib.NumberTheory.Multiplicity
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

Tactic:
Int.emultiplicity_pow_sub_pow hp hp1 hxy hx n

Premises used: Int.emultiplicity_pow_sub_pow
-- Module: Mathlib.NumberTheory.Multiplicity
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

Tactic:
exact Int.emultiplicity_pow_sub_pow hp hp1 hxy hx n

Premises used: Int.emultiplicity_pow_sub_pow
-- Module: Mathlib.NumberTheory.Multiplicity
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
inr : ∀ (hyx : x ≤ y), 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

Tactic:
obtain hyx | hyx := le_total y x

Premises used: le_total
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
inl : 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

Tactic:
rw [← Int.natCast_emultiplicity]

Premises used: Int.natCast_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
inl :
  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

Tactic:
rw [← Int.natCast_emultiplicity]

Premises used: Int.natCast_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
inl :
  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

Tactic:
iterate 2 rw [← Int.natCast_emultiplicity]

Premises used: Int.natCast_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
inl :
  emultiplicity (↑p : ℤ) (HSub.hSub (α := ℤ) (↑(x ^ n) : ℤ) (↑(y ^ n) : ℤ)) =
    emultiplicity (α := ℤ) (↑p : ℤ) (↑(x - y) : ℤ) + emultiplicity p n
⊢ emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n - y ^ n) : ℤ) =
    emultiplicity (α := ℤ) (↑p : ℤ) (↑(x - y) : ℤ) + emultiplicity p n

Tactic:
rw [Int.ofNat_sub (Nat.pow_le_pow_left hyx n)]

Premises used: Int.ofNat_sub, Nat.pow_le_pow_left
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
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
⊢ emultiplicity (↑p : ℤ) (HSub.hSub (α := ℤ) (↑(x ^ n) : ℤ) (↑(y ^ n) : ℤ)) =
    emultiplicity (α := ℤ) (↑p : ℤ) (↑(x - y) : ℤ) + emultiplicity p n

Tactic:
rw [← Int.natCast_dvd_natCast] at hxy hx

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Multiplicity
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
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
⊢ emultiplicity (↑p : ℤ) (HSub.hSub (α := ℤ) (↑(x ^ n) : ℤ) (↑(y ^ n) : ℤ)) =
    emultiplicity (α := ℤ) (↑p : ℤ) (↑(x - y) : ℤ) + emultiplicity p n

Tactic:
rw [Int.natCast_sub hyx] at *

Premises used: Int.natCast_sub
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : (↑p : ℤ) ∣ HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
hx : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x : ℤ)
n : ℕ
hyx : y ≤ x
⊢ emultiplicity (↑p : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) =
    emultiplicity (↑p : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) + emultiplicity p n

Tactic:
Int.emultiplicity_pow_sub_pow hp hp1 hxy hx n

Premises used: Int.emultiplicity_pow_sub_pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : (↑p : ℤ) ∣ HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)
hx : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x : ℤ)
n : ℕ
hyx : y ≤ x
⊢ emultiplicity (↑p : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n - HPow.hPow (α := ℤ) (↑y : ℤ) n) =
    emultiplicity (↑p : ℤ) (HSub.hSub (α := ℤ) (↑x : ℤ) (↑y : ℤ)) + emultiplicity p n

Tactic:
exact Int.emultiplicity_pow_sub_pow hp hp1 hxy hx n

Premises used: Int.emultiplicity_pow_sub_pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : x ≤ y
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n

Tactic:
simp only [Nat.sub_eq_zero_iff_le.mpr (Nat.pow_le_pow_left hyx n), emultiplicity_zero,
    Nat.sub_eq_zero_iff_le.mpr hyx, top_add]

Premises used: Iff.mpr, Nat.sub_eq_zero_iff_le, emultiplicity_zero, top_add, Nat.pow_le_pow_left
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
rw : 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

Tactic:
rw [← Int.natCast_emultiplicity]

Premises used: Int.natCast_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
rw :
  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

Tactic:
rw [← Int.natCast_emultiplicity]

Premises used: Int.natCast_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
iterate :
  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

Tactic:
iterate 2 rw [← Int.natCast_emultiplicity]

Premises used: Int.natCast_emultiplicity
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
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
⊢ emultiplicity (α := ℤ) (↑p : ℤ) (↑(x ^ n + y ^ n) : ℤ) =
    emultiplicity (α := ℤ) (↑p : ℤ) (↑(x + y) : ℤ) + emultiplicity p n

Tactic:
rw [← Int.natCast_dvd_natCast] at hxy hx

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.NumberTheory.Multiplicity
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
⊢ (↑p : ℤ) ∣ HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)

Tactic:
push_cast at *
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hx : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x : ℤ)
n : ℕ
hn : Odd n
hxy : (↑p : ℤ) ∣ HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)
⊢ emultiplicity (↑p : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n + HPow.hPow (α := ℤ) (↑y : ℤ) n) =
    emultiplicity (↑p : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) + emultiplicity p n

Tactic:
Int.emultiplicity_pow_add_pow hp hp1 hxy hx hn

Premises used: Int.emultiplicity_pow_add_pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hx : ¬Dvd.dvd (α := ℤ) (↑p : ℤ) (↑x : ℤ)
n : ℕ
hn : Odd n
hxy : (↑p : ℤ) ∣ HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)
⊢ emultiplicity (↑p : ℤ) (HPow.hPow (α := ℤ) (↑x : ℤ) n + HPow.hPow (α := ℤ) (↑y : ℤ) n) =
    emultiplicity (↑p : ℤ) (HAdd.hAdd (α := ℤ) (↑x : ℤ) (↑y : ℤ)) + emultiplicity p n

Tactic:
exact Int.emultiplicity_pow_add_pow hp hp1 hxy hx hn

Premises used: Int.emultiplicity_pow_add_pow
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
R : Type u_1
inst : CommRing R
x y : R
⊢ 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:
simp only [pow_zero, pow_one, range_zero, prod_empty, one_mul]

Premises used: Finset.prod_empty, pow_zero, pow_one, one_mul, Finset.range_zero
-- Module: Mathlib.NumberTheory.Multiplicity
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)
rw₄ 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)
⊢ 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:
rw [this, hd, Finset.prod_range_succ, ← mul_assoc, mul_comm (x ^ 2 ^ d + y ^ 2 ^ d)]

Premises used: mul_assoc, HPow.hPow, HAdd.hAdd, mul_comm, Finset.prod_range_succ, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Multiplicity
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)
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)
⊢ 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:
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)]
-- Module: Mathlib.NumberTheory.Multiplicity
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)
succ :
  x ^ HPow.hPow (α := ℕ) 2 (d + 1) - y ^ HPow.hPow (α := ℕ) 2 (d + 1) =
    (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.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:
rw [Nat.succ_eq_add_one]

Premises used: Nat.succ_eq_add_one
-- Module: Mathlib.NumberTheory.Multiplicity
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) =
    (x ^ HPow.hPow (α := ℕ) 2 d + y ^ HPow.hPow (α := ℕ) 2 d) *
      (x ^ HPow.hPow (α := ℕ) 2 d - y ^ HPow.hPow (α := ℕ) 2 d)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Multiplicity
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)
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)
⊢ 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)

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

Premises used: Finset.prod_empty, Nat.succ_eq_add_one, pow_zero, pow_one, one_mul, Finset.range_zero
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
x : ℤ
hx : ∃ (k : ℤ), x = 2 * k + 1
rcases : ∀ (w : ℤ), HPow.hPow (β := ℕ) (2 * w + 1) 2 % 4 = 1
⊢ HPow.hPow (β := ℕ) x 2 % 4 = 1

Tactic:
rcases hx with ⟨_, rfl⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
w : ℤ
ring_nf : (1 + w * 4 + HPow.hPow (β := ℕ) w 2 * 4) % 4 = 1
⊢ HPow.hPow (β := ℕ) (2 * w + 1) 2 % 4 = 1

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
w : ℤ
rw : HMod.hMod (α := ℤ) 1 4 = 1
⊢ (1 + w * 4 + HPow.hPow (β := ℕ) w 2 * 4) % 4 = 1

Tactic:
rw [add_assoc, ← add_mul, Int.add_mul_emod_self_right]

Premises used: add_mul, add_assoc, Int.add_mul_emod_self_right
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
w : ℤ
⊢ HMod.hMod (α := ℤ) 1 4 = 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
k : ℤ
hk : Odd k
rcases : ∀ (m : ℤ), 8 ∣ HPow.hPow (β := ℕ) (2 * m + 1) 2 - 1
⊢ 8 ∣ HPow.hPow (β := ℕ) k 2 - 1

Tactic:
rcases hk with ⟨m, rfl⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
m : ℤ
⊢ HPow.hPow (β := ℕ) (2 * m + 1) 2 - 1 = 4 * (m * (m + 1))

Tactic:
ring
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
m : ℤ
⊢ 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
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
m : ℤ
eq : HPow.hPow (β := ℕ) (2 * m + 1) 2 - 1 = 4 * (m * (m + 1))
⊢ 8 ∣ HPow.hPow (β := ℕ) (2 * m + 1) 2 - 1

Tactic:
simpa [eq] using (mul_dvd_mul_iff_left four_ne_zero).mpr (two_dvd_mul_add_one m)

Premises used: Iff.mpr, four_ne_zero, Int.two_dvd_mul_add_one, mul_dvd_mul_iff_left
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
k : ℕ
hk : Odd k
rcases : ∀ (m : ℕ), 8 ∣ HPow.hPow (β := ℕ) (2 * m + 1) 2 - 1
⊢ 8 ∣ HPow.hPow (β := ℕ) k 2 - 1

Tactic:
rcases hk with ⟨m, rfl⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
m : ℕ
⊢ HPow.hPow (β := ℕ) (2 * m + 1) 2 - 1 = 4 * (m * (m + 1))

Tactic:
grind
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
m : ℕ
⊢ 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
-- Module: Mathlib.NumberTheory.Multiplicity
Goal:
m : ℕ
eq : HPow.hPow (β := ℕ) (2 * m + 1) 2 - 1 = 4 * (m * (m + 1))
⊢ 8 ∣ HPow.hPow (β := ℕ) (2 * m + 1) 2 - 1

Tactic:
simpa [eq] using (mul_dvd_mul_iff_left four_ne_zero).mpr (two_dvd_mul_add_one m)

Premises used: Iff.mpr, four_ne_zero, mul_dvd_mul_iff_left, Nat.two_dvd_mul_add_one