Theorem: even_and_oddFactors (FltRegular/FltThree/OddPrimeOrFour.lean)

State before:
x : ℕ
hx : x ≠ 0
⊢ Associated x (2 ^ evenFactorExp x * (oddFactors x).prod)
Tactic:
convert(UniqueFactorizationMonoid.normalizedFactors_prod hx).symm
State after:
case h.e'_4
x : ℕ
hx : x ≠ 0
⊢ 2 ^ evenFactorExp x * (oddFactors x).prod = (UniqueFactorizationMonoid.normalizedFactors x).prod

State before:
case h.e'_4
x : ℕ
hx : x ≠ 0
⊢ 2 ^ evenFactorExp x * (oddFactors x).prod = (UniqueFactorizationMonoid.normalizedFactors x).prod
Tactic:
simp [evenFactorExp]
State after:
case h.e'_4
x : ℕ
hx : x ≠ 0
⊢ 2 ^ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) * (oddFactors x).prod =
    (UniqueFactorizationMonoid.normalizedFactors x).prod

State before:
case h.e'_4
x : ℕ
hx : x ≠ 0
⊢ 2 ^ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) * (oddFactors x).prod =
    (UniqueFactorizationMonoid.normalizedFactors x).prod
Tactic:
rw [Multiset.pow_count, ← Multiset.prod_add, ← even_and_odd_factors'' x]
State after:
no goals