Theorem: factorsOddPrimeOrFour.pow (Flt/OddPrimeOrFour.lean)

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