Debug logging for dsimp autoUnfold

Stream: lean4

[Siddharth Bhat]

I'm debugging a simp-set, where

  dsimp (config := { autoUnfold := true }) only [ConcreteOrMVar.instantiate_concrete_eq]

succeeds, while the same without autoUnfold := true fails. dsimp made no progress. I was wondering how I could find out what definitions dsimp chose to unfold with autoUnfold enabled. Is there a pp` option to trace this?

If not, what's the easiest way to find out what changed between the two invocations of dsimp (with and without autoUnfold enabled).