rw [Multiset.prod_zero] at h
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : Multiset.prod 0 = g.prod
⊢ 0 = g
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
⊢ 0 = g