feat: custom eliminators for `induction` and `cases` tactics, and beautiful eliminators for `Nat` (#3629)

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).
```lean
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.