simp [evenFactorExp]
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors (4 * z)) =
    2 + Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors z)