Kinds of induction' to be removed

Stream: mathlib4

[Jeremy Tan]

@Peter Nelson on #23324:

I am not sure that 5 is a large enough number for this to be a no-brainer. I would personally rather see opinions on scope of induction' removal actively solicited on Zulip (perhaps in the form of a poll) and/or a clear statement from maintainers on what their plan is for induction' before I am happy with this kind of PR being merged.

What kinds of induction' would you like to have removed?

[Eric Wieser]

Choose a number n such that the number of lines to review is less than 20?

[Eric Wieser]

Though I feel like there are probably more useful maintenance tasks than cleaning up induction'.

[Kevin Buzzard]

e.g. cleaning up erw

[Eric Wieser]

Or if you're set on doing things around induction, replacing ugly refine some_induct (motive := ..) with induction ... with

[Jeremy Tan]

Kevin Buzzard said:

e.g. cleaning up erw

I actually have #23389 cleaning up a few erw

[Jeremy Tan]

Nevertheless my choice of 5 was inspired by @Jireh Loreaux's comment on my prior PR about induction' with many variables being hard to figure out. I did not choose 4 because one of the targets I included in my automated removal PR (#23211) had 4 variables

[Jeremy Tan]

As you can see in #23324, some uses of induction' also named more variables than necessary. The extra variables are ignored and only cause more confusion

[Jeremy Tan]

Ignored silently, I must emphasise

[Eric Wieser]

That's indeed bad, but if only _some_ of them are ignored, it would be easier to review a PR consisting of just those

[Eric Wieser]

Or really, a smaller PR of any form; 68 files is a lot to touch, especially when some are much more justifiable changes than others

[Jeremy Tan]

@Eric Wieser #23419

[Jeremy Tan]

After the removal of 5+ variable induction' (#23324, #23419, #23650) the next class I want to remove is those generating only one subgoal, starting with #23676

[Jeremy Tan]

Please get #23324 merged by the way

[Eric Wieser]

Thanks for splitting things. I think this most recent split is precisely the one where the gain is most marginal