Improved verbosity of simp_all

Stream: new members

[Plamen Dimitrov]

Hi all, sometimes using simp_all works like magic in proving goals that I want to reach. The problem with this is that I don't like magic and would love if there is a way to make simp_all expand on the simplifications that were applied. Does anyone know of a way to turn some of the automation in place here into a more detailed feedback on how the goal was proven? In particular what I am after is a way to have simp_all not simply reach a goal but explain the steps in reaching it, even if it means "unfolding" its work into more verbose set of Lean 4 statements.

[Johan Commelin]

I think simp_all? works, right?

[Plamen Dimitrov]

Interesting! I hope there could be more "?" syntax usage in other places to obtain more self-explanatory behavior of the various proof search automation. Thanks for the pointer!