exact And.imp_left (UniqueFactorizationMonoid.prime_of_normalized_factor _)
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 ∈ UniqueFactorizationMonoid.normalizedFactors a ∧ Odd x → Prime x ∧ Odd x
no goals