Theorem: even_and_oddFactors (Flt/OddPrimeOrFour.lean)

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

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

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