Theorem: even_and_odd_factors' (Flt/OddPrimeOrFour.lean)

State before:
x : ℤ
⊢ UniqueFactorizationMonoid.normalizedFactors x = Multiset.replicate (evenFactorExp x) 2 + oddFactors x
Tactic:
convert even_and_odd_factors'' x
State after:
case h.e'_3.h.e'_5
x : ℤ
⊢ Multiset.replicate (evenFactorExp x) 2 = Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x)

State before:
case h.e'_3.h.e'_5
x : ℤ
⊢ Multiset.replicate (evenFactorExp x) 2 = Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x)
Tactic:
simp [evenFactorExp, ← Multiset.filter_eq]
State after:
no goals