obtain ⟨r, hr⟩ : ∃ r, 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3 := by
  rcases hcube with (hcube | hcube | hcube) <;> [(use a); (use b); (use c)]
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
case intro
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3