intro x hx
case refine_2
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
⊢ ∀ x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g, OddPrimeOrFour x
case refine_2
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
x : ℕ
hx : x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g
⊢ OddPrimeOrFour x