no goals
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
n : α
⊢ (factorization n).support = Multiset.toFinset (normalizedFactors n)
simp [factorization, Multiset.toFinsupp_support]