simp [evenFactorExp, oddFactors]
case neg
x : ℕ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) + oddFactors x
case neg
x : ℕ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) +
      Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors x)