automatic tracing of failures

Stream: mathlib4

[Jireh Loreaux]

It occurs to me that many users may not know how to debug various tactic failures, but for many tactics we have good tracing in place.

I think it would be great if we could do one of the following:

1. Display the relevant trace automatically when the tactic fails.
2. Tell the user in the infoview how to enable the various traces (as sometimes there are multiple possibilities) via set_option. Bonus points if this is clickable and automatically inserts it immediately prior to the declaration containing the tactic.

[Snir Broshi]

FWIW grind shows traces (or at least the final state) on failure but I have no idea how to read it; it would be great if there are some UX improvements to be had for grind failures as well.
(I wonder if I'm in the minority or the majority about this)