Finset.induction implicit arguments

Stream: mathlib4

[Patrick Massot]

In docs#Finset.induction the insert argument has implicit arguments that create a lot of | @insert a s ha IH => as in https://github.com/leanprover-community/mathlib4/blob/3dc1d31710850d3262c788dde83ba5da96f1727a/Mathlib/RingTheory/Ideal/IsPrimary.lean#L69 for instance. Should we change this?

[Eric Wieser]

More generally, do we ever want such arguments in elab_as_elim induction principles?

[Eric Wieser]

Alternatively, would a core change to enable writing | insert {a s} ha IH => make this less annoying? After all, we already have that syntax for fun

[Ruben Van de Velde]

Eric Wieser said:

Alternatively, would a core change to enable writing | insert {a s} ha IH => make this less annoying? After all, we already have that syntax for fun

Yes, definitely. And otherwise we should make all arguments explicit

[Eric Wieser]

Patrick Massot said:

as in https://github.com/leanprover-community/mathlib4/blob/3dc1d31710850d3262c788dde83ba5da96f1727a/Mathlib/RingTheory/Ideal/IsPrimary.lean#L69 for instance.

In this example I don't think a and s are actually used, and | insert ha IH would have worked

[Eric Wieser]

But certainly I've written | @insert a s ha IH in the past just because the tombstones in the goal are very distracting

[Eric Wieser]

So maybe there's another feature request here: stop showing tombstones when using widgets, and instead:

• Keep showing the x : Nat lines as faded out
• Make using x in the proof return an error like "x is not accessible" rather than "no variable x"

[Eric Wieser]

(in plain text mode keeping around the tombstones is probably sensible)

[Patrick Massot]

I often write | insert {a s} ha IH => before remembering it doesn’t work.