refine factors_unique_prod' ?_ hf (factorsOddPrimeOrFour.prod' ha heven)
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
⊢ factorsOddPrimeOrFour f.prod = f
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
ha : 0 < f.prod
heven : Even (evenFactorExp f.prod)
⊢ ∀ x ∈ factorsOddPrimeOrFour f.prod, OddPrimeOrFour x