English
If two multisets of irreducibles have the same product up to association, then the multisets are associated as multisets.
Русский
Если две мультимножества ирредуцируемых имеют одинаковый произведение до ассоциации, то сами множества ассоциированы.
LaTeX
$$$\forall p,q:\; \text{Multiset}(\mathrm{Associates}(\alpha))\; (\forall a\in p, \mathrm{Irreducible}(a)) \rightarrow (\forall a\in q, \mathrm{Irreducible}(a)) \rightarrow p.prod = q.prod \Rightarrow p = q.$$$
Lean4
theorem unique' {p q : Multiset (Associates α)} :
(∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → p.prod = q.prod → p = q :=
by
apply Multiset.induction_on_multiset_quot p
apply Multiset.induction_on_multiset_quot q
intro s t hs ht eq
refine Multiset.map_mk_eq_map_mk_of_rel (UniqueFactorizationMonoid.factors_unique ?_ ?_ ?_)
· exact fun a ha => irreducible_mk.1 <| hs _ <| Multiset.mem_map_of_mem _ ha
· exact fun a ha => irreducible_mk.1 <| ht _ <| Multiset.mem_map_of_mem _ ha
have eq' : (Quot.mk Setoid.r : α → Associates α) = Associates.mk := funext quot_mk_eq_mk
rwa [eq', prod_mk, prod_mk, mk_eq_mk_iff_associated] at eq
