rw [Multiset.rel_zero_left]
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ Multiset.Rel Associated 0 g
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ g = 0