intro x hx
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
⊢ ∀ x ∈ factorsOddPrimeOrFour f.prod, OddPrimeOrFour x
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ factorsOddPrimeOrFour f.prod
⊢ OddPrimeOrFour x