Make rcases use the induction/cases framework

[kmill]

Currently rcases uses Lean.MVarId.cases, but the cases tactic uses its own system of applying casesOn.

The rcases tactic should use the same system as cases.

Note that #3747 introduced a hack into Lean.MVarId.cases via the useNatCasesAuxOn argument for the "beautiful Nat induction" project. This should be removed, since this has a general solution via @[induction_eliminator] and @[cases_eliminator] in induction/cases. (The Lean.MVarId.cases is a low-level function that should not use user-defined eliminators.)

[nomeata]

The Lean.MVarId.cases is a low-level function that should not use user-defined eliminators.)

Maybe worth renaming. It's confusing if Lean.MVarId.foo and tactic foo are mostly unrelated.