rw [h1, hf, Multiset.prod_nsmul, Odd.neg_pow]
case intro.intro.inr
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = -Multiset.prod (factorization' hcoprime)
⊢ a = (-Multiset.prod f) ^ 3
case intro.intro.inr.a
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = -Multiset.prod (factorization' hcoprime)
⊢ Odd 3