rw [even_and_odd_factors' _, Multiset.prod_add, factorsOddPrimeOrFour, Multiset.prod_add, hm,
  Nat.mul_div_right _ zero_lt_two, Multiset.prod_replicate, Multiset.prod_replicate, pow_mul, h₁]
case intro
a : ℕ
ha : 0 < a
heven : Even (evenFactorExp a)
h₁ : 2 ^ 2 = 4
this : (UniqueFactorizationMonoid.normalizedFactors a).prod = a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ (factorsOddPrimeOrFour a).prod = (UniqueFactorizationMonoid.normalizedFactors a).prod
no goals