Add `by` parameter to `multiset_solver`
The tactics naive_solver
and set_solver
have a by
parameter to specify the tactic that is used on the leafs. This MR adds such a parameter to multiset_solver
too, and similar to naive_solver
/set_solver
lets it default to eauto
.
I cannot easily come up with useful test cases where we need the full power of eauto
. Either just fast_done
is sufficient (e.g., if the goal is an equality, see test_goal_{1,2}
and gmultiset_singleton_subseteq
) or you need eauto
with some hints (see test_goal_3
). Nonetheless, I think it makes sense to be consistent with naive_solver
/set_solver
to avoid issues such as !420 (merged).