have := UniqueFactorizationMonoid.normalizedFactors_prod ha.ne'
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
⊢ (factorsOddPrimeOrFour a).prod = a
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : Associated (UniqueFactorizationMonoid.normalizedFactors a).prod a
⊢ (factorsOddPrimeOrFour a).prod = a