apply Or.imp _ _ 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 : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ OddPrimeOrFour x
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 ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ Multiset.replicate (evenFactorExp a / 2) 4 → x = 4

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 ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ oddFactors a → Prime x ∧ Odd x