rw [← Multiset.rel_eq]
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ f = factorsOddPrimeOrFour a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ Multiset.Rel (fun x x_1 => x = x_1) f (factorsOddPrimeOrFour a)