rw [UniqueFactorizationMonoid.normalizedFactors_mul h₀ hz, Multiset.count_add, ← h₁,
  UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.count_nsmul,
  UniqueFactorizationMonoid.normalizedFactors_irreducible Int.prime_two.irreducible,
  Int.normalize_of_nonneg zero_le_two, Multiset.count_singleton_self, mul_one]
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)
no goals