obtain ⟨m, hm⟩ := even_iff_two_dvd.mp heven
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a))
case intro
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a))