-- Mathlib/NumberTheory/Multiplicity.lean
theorem Nat.two_pow_sub_pow {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

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

Tactic:
rw [← Int.natCast_emultiplicity]

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

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

Tactic:
iterate 3 rw [← Int.natCast_emultiplicity]

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

Proof state:
case inr
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : x ≤ y
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

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

Result:
no goals

Proof state:
case h.e'_3.h.e'_6
x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity 2 n = emultiplicity 2 ↑n

Tactic:
rw [← Int.natCast_emultiplicity]

Result:
case h.e'_3.h.e'_6
x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity ↑2 ↑n = emultiplicity 2 ↑n

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

Tactic:
convert Int.two_pow_sub_pow hxy hx hn using 2

Result:
case h.e'_3.h.e'_6
x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity 2 n = emultiplicity 2 ↑n

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

Tactic:
obtain hyx | hyx := le_total y x

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

case inr
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : x ≤ y
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

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

Tactic:
rw [← Int.natCast_dvd_natCast, Int.ofNat_sub hyx] at hxy

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

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

Tactic:
simp only [Int.ofNat_sub hyx, Int.ofNat_sub (pow_le_pow_left' hyx _), Int.ofNat_add,
  Int.natCast_pow]

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

Proof state:
case h.e'_3.h.e'_6
x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity ↑2 ↑n = emultiplicity 2 ↑n

Tactic:
rfl

Result:
no goals

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

Tactic:
rw [← Int.natCast_dvd_natCast] at hx

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