simp [hp.not_unit, ← isUnit_iff_dvd_one] at hdvd
case h₁
p : ℤ
hp : OddPrimeOrFour p
s : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s
hs : ∀ (r : ℤ), r ∈ 0 → OddPrimeOrFour r
hdvd : p ∣ Multiset.prod 0
⊢ ∃ q, q ∈ 0 ∧ Associated p q
no goals