rw [Multiset.filter_add_filter]
case neg
x : ℕ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x) +
      Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors x)
case neg
x : ℕ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (fun a => 2 = a ∨ Odd a) (UniqueFactorizationMonoid.normalizedFactors x) +
      Multiset.filter (fun a => 2 = a ∧ Odd a) (UniqueFactorizationMonoid.normalizedFactors x)