refine factorsOddPrimeOrFour.unique' hf ?_ ?_
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ factorsOddPrimeOrFour f.prod = f
case refine_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ 0 < f.prod

case refine_2
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ Even (evenFactorExp f.prod)