intro x hx
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ ∀ (x : ℤ), ¬x ∈ g
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ False