rw [Multiset.filter_eq_nil]
case h.e'_3.h.e'_6
x : ℕ
hx : ¬x = 0
⊢ Multiset.filter (fun a => 2 = a ∧ Odd a) (UniqueFactorizationMonoid.normalizedFactors x) = 0
case h.e'_3.h.e'_6
x : ℕ
hx : ¬x = 0
⊢ ∀ a ∈ UniqueFactorizationMonoid.normalizedFactors x, ¬(2 = a ∧ Odd a)