no goals
R : Type ?u.857609
n✝ : ℕ
x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
⊢ multiplicity 2 (x ^ 2 ^ n - y ^ 2 ^ n) = multiplicity 2 (x - y) + ↑n
simp only [pow_two_pow_sub_pow_two_pow n, multiplicity.mul Int.prime_two,
  multiplicity.Finset.prod Int.prime_two, add_comm, Nat.cast_one, Finset.sum_const,
  Finset.card_range, nsmul_one, Int.two_pow_two_pow_add_two_pow_two_pow hx hxy]