How to find the proof that simp found?

Stream: new members

[TessaCoil]

When I use simp, there isn't an easy way to see what proof it found.
I can use simp? and that sometimes gives me a hint, but sometimes it's clearly using other things than just what it suggests.
Is there an easy debugging way to output the thing simp found? (without having to dump the whole trace?)

[Scott Morrison]

simp? is usually pretty great (i.e. you could usually convert the output to a simp_rw or rw by reordering what it gives you).

Maybe you could post a #mwe?

sometimes show_term can be helpful, but usually not.

[Johan Commelin]

@TessaCoil in Lean 3 you can also use squeeze_simp. In Lean 4, simp? should be reliable. If simp? doesn't give the correct output in Lean 4, then that's a bug that we would like to know about.