refine' Multiset.Rel.mono _ p
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' f 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
⊢ Multiset.Rel (fun a b => Associated (Zsqrtd.norm a) (Zsqrtd.norm b)) f g