no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : α
⊢ map Subtype.val (factors' a) = map Associates.mk (factors a)
simp [factors', Multiset.map_pmap, Multiset.pmap_eq_map]