simp only [factorsOddPrimeOrFour, nsmul_add, Multiset.nsmul_replicate, evenFactorExp.pow,
  Nat.mul_div_assoc _ (even_iff_two_dvd.mp hz), oddFactors.pow]
z : ℤ
n : ℕ
hz : Even (evenFactorExp z)
⊢ factorsOddPrimeOrFour (z ^ n) = n • factorsOddPrimeOrFour z
no goals