obtain ⟨h1, h2⟩ := factorization'_prop hcoprime
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
⊢ ∃ g, factorization' hcoprime = 3 • g
case intro
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
h1 : a = Multiset.prod (factorization' hcoprime) ∨ a = -Multiset.prod (factorization' hcoprime)
h2 : ∀ (pq : ℤ√(-3)), pq ∈ factorization' hcoprime → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
⊢ ∃ g, factorization' hcoprime = 3 • g