simp [evenFactorExp]
case h.e'_4
x : ℕ
hx : x ≠ 0
⊢ 2 ^ evenFactorExp x * (oddFactors x).prod = (UniqueFactorizationMonoid.normalizedFactors x).prod
case h.e'_4
x : ℕ
hx : x ≠ 0
⊢ 2 ^ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) * (oddFactors x).prod =
    (UniqueFactorizationMonoid.normalizedFactors x).prod