intro x hx
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ ∀ (x : ℤ), x ∈ factorsOddPrimeOrFour a → OddPrimeOrFour x
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ factorsOddPrimeOrFour a
⊢ OddPrimeOrFour x