rw [Multiset.pow_count, ← Multiset.prod_add, ← even_and_odd_factors'' x]
case h.e'_4
x : ℤ
hx : x ≠ 0
⊢ 2 ^ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) * Multiset.prod (oddFactors x) =
    Multiset.prod (UniqueFactorizationMonoid.normalizedFactors x)
no goals