have hpnezero : p ≠ 0 := by
  rintro rfl
  rw [sub_zero, zero_add, add_left_eq_self] at h
  exact hapos (pow_eq_zero h)
case intro.intro
a : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 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 : ℤ
hapos : a ≠ 0
p q : ℤ
hc : ¬Even (p + q)
hb : ¬Even (q - p)
h : a ^ 3 + (q - p) ^ 3 = (p + q) ^ 3
hbccoprime : IsCoprime (q - p) (p + q)
hp : p + q - (q - p) = 2 * p
hq : p + q + (q - p) = 2 * q
hpnezero : p ≠ 0
⊢ ∃ p q, p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3