Suggestion -- Tell me what simp/dsimp does

Stream: general

[Mason McBride]

It would be great to know what theorems simp just used to close my goal. I think this shuold be standard it would help the learning curve of lean greatly because sifting through the library is very inefficient if simp can find it for me and just tell me what's relevant.

[Sébastien Gouëzel]

simp? does that.

[Mason McBride]

Thank you, lean is amazing

[Tomas Skrivan]

You can also add

set_option trace.Meta.Tactic.simp.rewrite true

To see the list of all the rewrites. Very useful when you want to understand what simp just did.