feat(tactic/rcases): rcases_many (#4569)
This allows you to pattern match many variables at once, using the
syntax `obtain ⟨a|b, c|d⟩ := ⟨x, y⟩`. This doesn't require any change
to the front end documentation, as it is in some sense the obvious thing,
but this doesn't break any existing uses because this could never work
before (since the expected type of the tuple expression is not known).
