obtain ⟨q, hq⟩ : Even (c + b) := by simp [hb, hc, parity_simps]
case intro
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = p + p
⊢ ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3
case intro.intro
a b c : ℤ
hapos : a ≠ 0
h : a ^ 3 + b ^ 3 = c ^ 3
hbccoprime : IsCoprime b c
hb : ¬Even b
hc : ¬Even c
p : ℤ
hp : c - b = p + p
q : ℤ
hq : c + b = q + q
⊢ ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3