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

State before:
z : ℤ
n : ℕ
⊢ evenFactorExp (z ^ n) = n * evenFactorExp z
Tactic:
simp only [evenFactorExp]
State after:
z : ℤ
n : ℕ
⊢ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors (z ^ n)) =
    n * Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors z)

State before:
z : ℤ
n : ℕ
⊢ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors (z ^ n)) =
    n * Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors z)
Tactic:
rw [UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.count_nsmul]
State after:
no goals