obtain ⟨u, hu⟩ := hcube
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
hcube : ∃ r, p ^ 2 + 3 * q ^ 2 = r ^ 3
⊢ ∃ a b, p = a * (a - 3 * b) * (a + 3 * b) ∧ q = 3 * b * (a - b) * (a + b) ∧ IsCoprime a b ∧ (Even a ↔ ¬Even b)
case intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
⊢ ∃ a b, p = a * (a - 3 * b) * (a + 3 * b) ∧ q = 3 * b * (a - b) * (a + b) ∧ IsCoprime a b ∧ (Even a ↔ ¬Even b)