symm
case h.e'_2
x : ℕ
hx : ¬x = 0
⊢ UniqueFactorizationMonoid.normalizedFactors x =
    Multiset.filter (fun a => 2 = a ∨ Odd a) (UniqueFactorizationMonoid.normalizedFactors x)
case h.e'_2
x : ℕ
hx : ¬x = 0
⊢ Multiset.filter (fun a => 2 = a ∨ Odd a) (UniqueFactorizationMonoid.normalizedFactors x) =
    UniqueFactorizationMonoid.normalizedFactors x