feat(group_theory/submonoid/membership): `exists_multiset_of_mem_clos…

…ure` (#10256)

Version of `exists_list_of_mem_closure` for `comm_monoid`.

src/group_theory/submonoid/membership.lean

@@ -196,6 +196,14 @@ begin
   exact ⟨list.map coe l, λ y hy, let ⟨z, hz, hy⟩ := list.mem_map.1 hy in hy ▸ z.2, hx⟩
 end
 
+@[to_additive]
+lemma exists_multiset_of_mem_closure {M : Type*} [comm_monoid M] {s : set M}
+  {x : M} (hx : x ∈ closure s) : ∃ (l : multiset M) (hl : ∀ y ∈ l, y ∈ s), l.prod = x :=
+begin
+  obtain ⟨l, h1, h2⟩ := exists_list_of_mem_closure hx,
+  exact ⟨l, h1, (multiset.coe_prod l).trans h2⟩,
+end
+
 /-- The submonoid generated by an element. -/
 def powers (n : M) : submonoid M :=
 submonoid.copy (powers_hom M n).mrange (set.range ((^) n : ℕ → M)) $