feat: make rcases use the custom Nat eliminator

[kmill]

As a special case, makes the rcases machinery use Nat.casesAuxOn so that goal states see 0 and n + 1 rather than Nat.zero and Nat.succ n. This is a followup to enabling custom eliminators for cases and induction.

This doesn't use custom eliminators in general since rcases uses Lean.MVarId.cases, which is completely different from what cases and induction use.

[digama0]

This seems a bit specialized. I think it would be better to just use the default custom eliminator for the type in MVarId.cases (why is it "completely different from what cases does" in the first place?)

[kmill]

@digama0 Good, you saw this, I was going to ping you to take a look.

This is part of the "nat induction beautification" project. Leo was OK with custom induction principles for Nat in particular, and for induction/cases, the more general solution went through because it was easy.

There are two issues with Lean.MVarId.cases:

1. It is not able to analyze a custom induction principle, like what's done in Lean.Meta.getElimExprInfo, so there's more work that would need to be done if it's not just special casing Nat.casesOn (as Nat.casesAuxOn is defeq, so there's no harm in swapping it out).
2. It turns out enabling this custom induction principle breaks the equation lemma generator, which is why it's behind a flag. It really seems to be meant for doing cases to get pristine constructors.

Probably what would be better is to modify rcases to use the induction/cases framework than to use Lean.MVarId.cases, but that's not packaged up in a useable form. In the short term, having a special case for Nat would finish nat induction beautification.

I'm not sure about the right implementation for rcases, but I created this PR with one possibility to start that conversation.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0c6c5d226883980cfe986886681e68e9924f2bd --onto 80d2455b6401acf6b0d107388b814c175e64c0d3. (2024-03-25 20:07:11)

[digama0]

Probably what would be better is to modify rcases to use the induction/cases framework than to use Lean.MVarId.cases, but that's not packaged up in a useable form. In the short term, having a special case for Nat would finish nat induction beautification.

I think that MVarId.cases should "use the induction/cases framework" to the extent possible. But as a short term measure I agree with the changes in this PR (we should have some issue or TODO to avoid losing track of this though).