feat(tactic/rcases): type ascriptions in rcases (#3730)
This is a general rewrite of the `rcases` tactic, with the primary intent of adding support for type ascriptions in `rcases` patterns but it also includes a bunch more documentation, as well as making the grammar simpler, avoiding the strict tuple/alts alternations required by the previous `many` constructor (and the need for `rcases_patt_inverted` for whether the constructor means `tuple` of `alts` or `alts` of `tuple`).
From a user perspective, it should not be noticeably different, except:
* You can now use parentheses freely in patterns, so things like `a | (b | c)` work
* You can use type ascriptions
The new `rcases` is backward compatible with the old one, except that `rcases e with a` (where `a` is a name) no longer does any cases and is basically just another way to write `have a := e`; to get the same effect as `cases e with a` you have to write `rcases e with ⟨a⟩` instead.
