convert(UniqueFactorizationMonoid.normalizedFactors_prod hx).symm
x : ℕ
hx : x ≠ 0
⊢ Associated x (2 ^ evenFactorExp x * (oddFactors x).prod)
case h.e'_4
x : ℕ
hx : x ≠ 0
⊢ 2 ^ evenFactorExp x * (oddFactors x).prod = (UniqueFactorizationMonoid.normalizedFactors x).prod