no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a b : Associates α
x✝¹ x✝ : α
⊢ Associates.out (Quotient.mk (Associated.setoid α) x✝¹ * Quotient.mk (Associated.setoid α) x✝) =
    Associates.out (Quotient.mk (Associated.setoid α) x✝¹) * Associates.out (Quotient.mk (Associated.setoid α) x✝)
simp only [Associates.quotient_mk_eq_mk, out_mk, mk_mul_mk, normalize.map_mul]