obtain rfl : p + q = c := by
  apply Int.eq_of_mul_eq_mul_left two_ne_zero
  rw [mul_add, ← hp, ← hq]
  ring
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 = 2 * p
q : ℤ
hq : c + b = 2 * q
⊢ ∃ 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 : ℤ
hapos : a ≠ 0
hb : ¬Even b
p q : ℤ
h : a ^ 3 + b ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime b (p + q)
hc : ¬Even (p + q)
hp : p + q - b = 2 * p
hq : p + q + b = 2 * q
⊢ ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3