induction eliminator

[Seasawher]

Added @[induction_eliminator] and @[cases_eliminator] attributes to be able to define custom eliminators for the induction and cases tactics, replacing the @[eliminator] attribute. Gives custom eliminators for Nat so that induction and cases put goal states into terms of 0 and n + 1 rather than Nat.zero and Nat.succ n. Added option tactic.customEliminators to control whether to use custom eliminators. Added a hack for rcases/rintro/obtain to use the custom eliminator for Nat. #3629, #3655, and #3747.

https://github.com/leanprover/lean4/blob/master/RELEASES.md#v480

[Seasawher]

Lean v4.8.0 からの新機能だが，詳細不明