induction' s using Multiset.induction_on with a s ih hs
p : ℕ
hp : OddPrimeOrFour p
s : Multiset ℕ
hs : ∀ r ∈ s, OddPrimeOrFour r
hdvd : p ∣ s.prod
⊢ p ∈ s
case empty
p : ℕ
hp : OddPrimeOrFour p
hs : ∀ r ∈ 0, OddPrimeOrFour r
hdvd : p ∣ Multiset.prod 0
⊢ p ∈ 0

case cons
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ (a ::ₘ s).prod
⊢ p ∈ a ::ₘ s