feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat

[kmill]

Replaces @[eliminator] with two attributes @[induction_eliminator] and @[cases_eliminator] for defining custom eliminators for the induction and cases tactics, respectively.

Adds Nat.recAux and Nat.casesAuxOn, which are eliminators that are defeq to Nat.rec and Nat.casesOn, but these use 0 and n + 1 rather than Nat.zero and Nat.succ n.

For example, using induction to prove that the factorial function is positive now has the following goal states (thanks also to #3616 for the goal state after unfolding).

example : 0 < fact x := by
  induction x with
  | zero => decide
  | succ x ih =>
    /-
    x : Nat
    ih : 0 < fact x
    ⊢ 0 < fact (x + 1)
    -/
    unfold fact
    /-
    ...
    ⊢ 0 < (x + 1) * fact x
    -/
    simpa using ih

Thanks to @adamtopaz for initial work on splitting the @[eliminator] attribute.

[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 611b1746896bbadf459c00cc218fa31cf51b4e08 --onto ae492265fec103aa834d897bf9f68c94d10f0785. (2024-03-07 06:38:33)