The code contains some documentation how it works.
I added a number of tests, and used it to automate many existing lemmas in the gmultiset file.
Note that this required restructuring the file quite a bit, since I needed some basic lemmas (now in section basic_lemmas) to define the tactic, and wanted to use the tactic subsequently to prove many of the existing lemmas (now in section multiset_unfold). None of the lemma statements changed, only many proofs are replaced by a mere call to multiset_solver.
/cc @msammler