simp only [oddFactors, Multiset.mem_filter]
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ Multiset.replicate (evenFactorExp f.prod / 2) 4 ∨ x ∈ oddFactors f.prod
⊢ x ∈ oddFactors f.prod → x.Prime ∧ Odd x
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
x : ℕ
hx : x ∈ Multiset.replicate (evenFactorExp f.prod / 2) 4 ∨ x ∈ oddFactors f.prod
⊢ x ∈ UniqueFactorizationMonoid.normalizedFactors f.prod ∧ Odd x → x.Prime ∧ Odd x