have := hs a (Multiset.mem_cons_self _ _)
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
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
this : OddPrimeOrFour a
⊢ p ∈ a ::ₘ s