apply Associated.trans _ this
case h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) a
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))