case inl
R : Type ?u.872951
n✝ x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 n

case inr
R : Type ?u.872951
n✝ x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : x ≤ y
⊢ multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 n
R : Type ?u.872951
n✝ x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
⊢ multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 n
obtain hyx | hyx := le_total y x
case inl
R : Type ?u.872951
n✝ x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity ↑2 ↑(x ^ n - y ^ n) + 1 = multiplicity ↑2 ↑(x + y) + multiplicity ↑2 ↑(x - y) + multiplicity 2 n
case inl
R : Type ?u.872951
n✝ x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 n
iterate 3 rw [← multiplicity.Int.coe_nat_multiplicity]
case inl
R : Type ?u.872951
n✝ x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 = multiplicity (↑2) (↑x + ↑y) + multiplicity (↑2) (↑x - ↑y) + multiplicity 2 n
case inl
R : Type ?u.872951
n✝ x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity ↑2 ↑(x ^ n - y ^ n) + 1 = multiplicity ↑2 ↑(x + y) + multiplicity ↑2 ↑(x - y) + multiplicity 2 n
simp only [Int.ofNat_sub hyx, Int.ofNat_sub (pow_le_pow_of_le_left' hyx _), Int.ofNat_add,
  Int.coe_nat_pow]
case inl
R : Type ?u.872951
n✝ x y : ℕ
hxy : 2 ∣ x - y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 = multiplicity (↑2) (↑x + ↑y) + multiplicity (↑2) (↑x - ↑y) + multiplicity 2 n
case inl
R : Type ?u.872951
n✝ x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 = multiplicity (↑2) (↑x + ↑y) + multiplicity (↑2) (↑x - ↑y) + multiplicity 2 n
rw [← Int.coe_nat_dvd] at hx
case inl
R : Type ?u.872951
n✝ x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 = multiplicity (↑2) (↑x + ↑y) + multiplicity (↑2) (↑x - ↑y) + multiplicity 2 n
case inl
R : Type ?u.872951
n✝ x y : ℕ
hxy : 2 ∣ x - y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 = multiplicity (↑2) (↑x + ↑y) + multiplicity (↑2) (↑x - ↑y) + multiplicity 2 n
rw [← Int.coe_nat_dvd, Int.ofNat_sub hyx] at hxy
case h.e'_3.h.e'_6
R : Type ?u.872951
n✝ x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity 2 n = multiplicity 2 ↑n
case inl
R : Type ?u.872951
n✝ x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity (↑2) (↑x ^ n - ↑y ^ n) + 1 = multiplicity (↑2) (↑x + ↑y) + multiplicity (↑2) (↑x - ↑y) + multiplicity 2 n
convert Int.two_pow_sub_pow hxy hx hn using 2
case h.e'_3.h.e'_6
R : Type ?u.872951
n✝ x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity ↑2 ↑n = multiplicity 2 ↑n
case h.e'_3.h.e'_6
R : Type ?u.872951
n✝ x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity 2 n = multiplicity 2 ↑n
rw [← multiplicity.Int.coe_nat_multiplicity]
no goals
case h.e'_3.h.e'_6
R : Type ?u.872951
n✝ x y : ℕ
hxy : ↑2 ∣ ↑x - ↑y
hx : ¬↑2 ∣ ↑x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity ↑2 ↑n = multiplicity 2 ↑n
rfl
case inl
R : Type ?u.872951
n✝ x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity ↑2 ↑(x ^ n - y ^ n) + 1 = multiplicity ↑2 ↑(x + y) + multiplicity ↑2 ↑(x - y) + multiplicity 2 n
case inl
R : Type ?u.872951
n✝ x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ multiplicity ↑2 ↑(x ^ n - y ^ n) + 1 = multiplicity ↑2 ↑(x + y) + multiplicity 2 (x - y) + multiplicity 2 n
rw [← multiplicity.Int.coe_nat_multiplicity]
no goals
case inr
R : Type ?u.872951
n✝ x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : x ≤ y
⊢ multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 n
simp only [Nat.sub_eq_zero_iff_le.mpr hyx,
  Nat.sub_eq_zero_iff_le.mpr (pow_le_pow_of_le_left' hyx n), multiplicity.zero,
  PartENat.top_add, PartENat.add_top]