intro f g hf hg hassoc
⊢ ∀ {f g : Multiset (ℤ√(-3))},
    (∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)) →
      (∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)) →
        Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g)) →
          Multiset.Rel Associated (Multiset.map Zsqrtd.norm f) (Multiset.map Zsqrtd.norm g)
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
⊢ Multiset.Rel Associated (Multiset.map Zsqrtd.norm f) (Multiset.map Zsqrtd.norm g)