apply factors_unique_prod hf hg
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hf' : ∀ (x : ℤ√(-3)), x ∈ f → IsCoprime x.re x.im
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hg' : ∀ (x : ℤ√(-3)), x ∈ g → IsCoprime x.re x.im
h : Associated (Multiset.prod f) (Multiset.prod g)
p : ∀ (x : ℤ√(-3)), x ∈ f → ∀ (y : ℤ√(-3)), y ∈ g → Associated (Zsqrtd.norm x) (Zsqrtd.norm y) → Associated' x y
⊢ Multiset.Rel Associated (Multiset.map (fun a => Zsqrtd.norm a) f) (Multiset.map (fun b => Zsqrtd.norm b) g)
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hf' : ∀ (x : ℤ√(-3)), x ∈ f → IsCoprime x.re x.im
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hg' : ∀ (x : ℤ√(-3)), x ∈ g → IsCoprime x.re x.im
h : Associated (Multiset.prod f) (Multiset.prod g)
p : ∀ (x : ℤ√(-3)), x ∈ f → ∀ (y : ℤ√(-3)), y ∈ g → Associated (Zsqrtd.norm x) (Zsqrtd.norm y) → Associated' x y
⊢ Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))