-- Mathlib/NumberTheory/Multiplicity.lean
theorem Nat.emultiplicity_pow_sub_pow {x y : ℕ} (hxy : p ∣ x - y) (hx : ¬p ∣ x) (n : ℕ) :
    emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n

Proof state:
case inl
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

Tactic:
rw [Int.natCast_sub hyx] at *

Result:
case inl
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

Proof state:
case inl
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

Tactic:
push_cast at *

Result:
case inl
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

Proof state:
case inl
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

Tactic:
iterate 2 rw [← Int.natCast_emultiplicity]

Result:
case inl
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

Proof state:
case inr
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]

Result:
no goals

Proof state:
case inl
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

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

Result:
case inl
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

Proof state:
case inl
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

Tactic:
exact Int.emultiplicity_pow_sub_pow hp hp1 hxy hx n

Result:
no goals

Proof state:
case inl
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

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

Result:
case inl
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

Proof state:
case inl
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

Tactic:
rw [← Int.natCast_emultiplicity]

Result:
case inl
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

Proof state:
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

Tactic:
obtain hyx | hyx := le_total y x

Result:
case inl
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

case inr
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