Verbose failing simpa?

Stream: mathlib4

[Yaël Dillies]

Could we make simpa? output the list of lemmas it used, even if it failed to close the goal? It's really annoying having to take apart the simpa invokation when debugging.