exact hf x hx
case h'
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated x.norm y.norm
⊢ OddPrimeOrFour x.norm.natAbs
no goals