rw [← Multiset.rel_map, factors_unique_prod hf hg <| Zsqrtd.associated_norm_of_associated h,
  Multiset.rel_eq]
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
p : ∀ x ∈ f, ∀ y ∈ g, (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y → Associated' x y
⊢ Multiset.Rel (fun a b => (Int.natAbs ∘ Zsqrtd.norm) a = (Int.natAbs ∘ Zsqrtd.norm) b) f g
no goals