simp_rw [← Multiset.map_map, prod_map_natAbs, prod_map_norm, ← Int.associated_iff_natAbs]
case refine_3
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f).prod = (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g).prod
case refine_3
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ Associated f.prod.norm g.prod.norm