convert even_and_odd_factors'' x
x : ℕ
⊢ UniqueFactorizationMonoid.normalizedFactors x = Multiset.replicate (evenFactorExp x) 2 + oddFactors x
case h.e'_3.h.e'_5
x : ℕ
⊢ Multiset.replicate (evenFactorExp x) 2 = Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x)