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

Proof state:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - 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)

Tactic:
rw [this, add_comm 1, ← add_assoc]

Result:
no goals

Proof state:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ ¬2 ∣ x ^ 2

Tactic:
rw [← even_iff_two_dvd, Int.not_even_iff_odd]

Result:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ Odd (x ^ 2)

Proof state:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : Odd x
hn : Even n
⊢ Odd y

Tactic:
replace hxy := (@even_neg _ _ (x - y)).mpr (even_iff_two_dvd.mpr hxy)

Result:
x y : ℤ
n : ℕ
hx : Odd x
hn : Even n
hxy : Even (-(x - y))
⊢ Odd y

Proof state:
case h.e'_3
x y : ℤ
n : ℕ
hx : Odd x
hn : Even n
hxy : Even (-(x - y))
⊢ y = -(x - y) + x

Tactic:
abel

Result:
no goals

Proof state:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hn : Even n
⊢ Odd y

Tactic:
rw [← even_iff_two_dvd, Int.not_even_iff_odd] at hx

Result:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : Odd x
hn : Even n
⊢ Odd y

Proof state:
x y : ℤ
n : ℕ
hx : Odd x
hn : Even n
hxy : Even (-(x - y))
⊢ Odd y

Tactic:
convert Even.add_odd hxy hx

Result:
case h.e'_3
x y : ℤ
n : ℕ
hx : Odd x
hn : Even n
hxy : Even (-(x - y))
⊢ y = -(x - y) + x

Proof state:
case ha
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ Odd x

Tactic:
simp only [← Int.not_even_iff_odd, even_iff_two_dvd, hx, not_false_iff]

Result:
no goals

Proof state:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ (1 - 1) % 4 = 0

Tactic:
norm_num

Result:
no goals

Proof state:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ Odd x

Tactic:
simp only [← Int.not_even_iff_odd, even_iff_two_dvd, hx, not_false_iff]

Result:
no goals

Proof state:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ 4 ∣ x ^ 2 - y ^ 2

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]

Result:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ (1 - 1) % 4 = 0

x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ Odd x

Proof state:
case intro
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - 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)

Tactic:
suffices emultiplicity (2 : ℤ) ↑(2 : ℕ) = 1 by rw [this, add_comm 1, ← add_assoc]

Result:
case intro
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ emultiplicity 2 ↑2 = 1

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

Tactic:
obtain ⟨d, hd⟩ := hn

Result:
case intro
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hd : n = d + d
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 ↑n

Proof state:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ Odd (x ^ 2)

Tactic:
apply Odd.pow

Result:
case ha
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ Odd x

Proof state:
case intro
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hd : n = d + d
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 ↑n

Tactic:
subst hd

Result:
case intro
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)

Proof state:
case intro
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ 2 ≠ 1 ∧ 0 < 2

Tactic:
decide

Result:
no goals

Proof state:
case intro
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ emultiplicity 2 ((x ^ 2) ^ d - (y ^ 2) ^ d) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 ↑(2 * d)

Tactic:
rw [Int.two_pow_sub_pow' d hxy4 _, sq_sub_sq, ← Int.ofNat_mul_out,
  emultiplicity_mul Int.prime_two, emultiplicity_mul Int.prime_two]

Result:
case intro
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - 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)

x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ ¬2 ∣ x ^ 2

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

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

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

Proof state:
case intro
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ FiniteMultiplicity 2 2

Tactic:
rw [Nat.finiteMultiplicity_iff]

Result:
case intro
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ 2 ≠ 1 ∧ 0 < 2

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

Tactic:
simp only [← two_mul, pow_mul]

Result:
case intro
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ emultiplicity 2 ((x ^ 2) ^ d - (y ^ 2) ^ d) + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 ↑(2 * d)

Proof state:
case intro
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ emultiplicity 2 ↑2 = 1

Tactic:
norm_cast

Result:
case intro
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ emultiplicity 2 2 = 1

Proof state:
case intro
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ emultiplicity 2 2 = 1

Tactic:
rw [FiniteMultiplicity.emultiplicity_self]

Result:
case intro
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
⊢ FiniteMultiplicity 2 2