cases' h1 with h1 h1 <;> rw [h1]
case intro
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
⊢ Multiset.prod f ∣ a
case intro.inr
a b : ℤ√(-3)
h : IsCoprime a.re a.im
f : Multiset (ℤ√(-3)) := factorization' h
hmem : b ∈ f
h1 : a = -Multiset.prod f
⊢ Multiset.prod f ∣ -Multiset.prod f