Code action for induction ... using ...

[PatrickMassot]

The current induction code action is really nice, but it doesn't work when using a non-default induction rule.

[nomeata]

Is there a possibility to replace it with a generic code action that works for any tactic that produces multiple named goals (induction, cases, refine with ?foo, probably more)? That would likely automatically pick up the right case name with induction … using, and be more generally useful.