mathlib3

d36af184 - feat(tactic/induction): add induction'/cases'/eliminate_hyp/eliminate_expr tactics (#5027)

feat(tactic/induction): add induction'/cases'/eliminate_hyp/eliminate_expr tactics (#5027) This PR adds interactive tactics `induction'` and `cases'` as well as non-interactive variants `eliminate_hyp` and `eliminate_expr`. The tactics are similar to standard `induction` and `cases`, but they feature several improvements: - `induction'` performs 'dependent induction', which means it takes the indices of indexed inductive types fully into account. This is convenient, for example, for programming language or logic formalisations, which tend to rely heavily on indexed types. - `induction'` by default generalises everything that can be generalised. This is to support beginners, who often struggle to identify that a proof requires a generalised induction hypothesis. In cases where this feature hinders more than it helps, it can easily be turned off. - `induction'` and `cases'` generate much more human-friendly names than their standard counterparts. This is, again, mostly to support beginners. Experts should usually supply explicit names to make proof scripts more robust. - `cases'` works for some rare goals which `cases` does not support, but should otherwise be mostly a drop-in replacement (except for the generated names).