conv_rhs => rw [←this]
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
⊢ (factorsOddPrimeOrFour a).prod = a
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
⊢ (factorsOddPrimeOrFour a).prod = (UniqueFactorizationMonoid.normalizedFactors a).prod