feat: upstream casesm and cases_type tactics

[semorrison]

No description provided.

[fgdorais]

This looks really good to me except for the naming convention. I think it *m suffix is not great, I understand such suffixes are somewhat common in Mathlib, but they are obscure for core Lean users and Std shouldn't delve into arcana. I would prefer the self-explanatory *_matching or perhaps *_match to save a few keystrokes.

[digama0]

I don't like the name cases_match either because cases already overlaps significantly with the match tactic, and it's not really clear that this means match in a completely different sense: not matching on the value itself as an inductive type, but rather finding patterns in the specified targets.

How do people feel about not using a word at all and instead just using a symbol or other keyword, like cases * as patt in h or similar? I think it would be more (grammatically) productive to use some modifier language like this to describe matching patterns rather than suffixed tactic names.