Linter idea: `h1 h2` hypotheses in induction

Stream: mathlib4

[Yury G. Kudryashov]

I suggest that we rename hypotheses in all lemmas like docs#Finset.cons_induction_on from h/h<num>/h_<num> to meaningful names like empty/cons/etc

[Mario Carneiro]

Does this need a linter? It sounds like just a refactor

[Yury G. Kudryashov]

git grep for elab_as_eliminator?

[Notification Bot]

9 messages were moved from this topic to #mathlib4 > removing unprimed closure induction principles by Eric Wieser.