trace_simp / simp +trace / ...?

Stream: lean4

[Vasiliy Yorkin]

Hi!
I want to understand which lemmas the simp tactic used when simplifying a given (sub)goal. Is there a way to find this out?

example : ¬(p → q) → p ∧ ¬q := by
    intro h_npq
    simp at h_npq
    assumption

[Max Nowak 🐉]

You can use simp? and look at the infoview

[Max Nowak 🐉]

And a bit more advanced, but you can use show_term MY_TACTIC to show the proof term generated by the tactic

[Vasiliy Yorkin]

thank you!

[Aaron Liu]

You can set_option trace.Meta.Tactic.simp true