rw [isUnit_iff_dvd_one]
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ IsUnit x
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ x ∣ 1