obtain ⟨q, hq₁, hq₂⟩ := ih (fun r hr => hs _ (Multiset.mem_cons_of_mem hr)) h
case h₂.inr
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
case h₂.inr.intro.intro
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ Multiset.prod s
q : ℤ
hq₁ : q ∈ s
hq₂ : Associated p q
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q