Changing the heuristic for case names in induction

Stream: lean4

[Eric Wieser]

I have quite a few induction principles where the statement is something like

@[elab_as_elim]
theorem my_ind {motive} (hfoo : ∀ x, motive (foo x)) (hbar : ∀ y, motive (bar y)) (z) : motive y := sorry

When used with induction, this gives

induction z using my_ind with
| hfoo x => sorry
| hbar x => sorry

These hs are annoying, since they don't appear when using primitive recursors.

Of course, you can fix the lemma statement to use nicer names for the hypotheses, but now the induction principle itself is hard to read (and prove) due to name shadowing:

@[elab_as_elim]
theorem my_ind {motive}
    -- two `foo`s and two `bar`s
    (foo : ∀ x, motive (foo x)) (bar : ∀ y, motive (bar y)) (z) : motive y :=
  sorry

Should induction strip h prefices when naming goals?

[Eric Wieser]

A real example of this happening is src#Finset.cons_induction

[Damiano Testa]

I'm in favour of removing the h.

I also think that giving more thought to the names chosen for the hypotheses is more important in Lean4, given the new feature of being able to single out implicit arguments by calling them by their tag.