apply (Multiset.dvd_prod hmem).trans
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = f.prod ∨ a = -f.prod
⊢ b ∣ a
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = f.prod ∨ a = -f.prod
⊢ f.prod ∣ a