feat: add on_goals tactic

[digama0]

trafficstars

This generalizes the on_goal tactic to allow targeting multiple goals at once, and it focuses on each of them when calling the given tactic sequence, like all_goals but for a subset of goals. It retains its "in-place" behavior: the remaining goals retain the same relative positions to the new goals as the old ones.

It also adds another tactic on_goals, with the same syntax. on_goals will run its tactic block only once, on a tactic state consisting of all selected goals. It does not keep subgoal ordering: all the newly generated goals will be at the start of the list and all unselected goals will be at the end. (So on_goals 1 3 5 => skip is a useful operation: it will place 1,3,5 at the start of the list.)

[gebner]

IIRC we had a long discussion on whether this is the right API. https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/rotate/near/270911783 At least on_goal and on_goals should have distinct names so that they can't be confused.