How to investigate slow dsimp

Stream: mathlib4

[Joël Riou]

Currently, docs#CategoryTheory.Functor.commShiftIso is defined as the iso field of the typeclass Functor.CommShift, but the relatively new syntax about making explicit certain variables of typeclasses would allow to remove the need for the extra definition Functor.commShiftIso, which is what I am trying to do in #31504.
I do not know exactly how, but this leads to a very significant slowdown in the file CategoryTheory.Triangulated.Opposite.Functor.
I could get mapTriangleOpCompTriangleOpEquivalenceFunctorApp to compile in a reasonable time by squeezing dsimp (which is not a very good solution as simp should take care of this):
https://github.com/joelriou/mathlib4/blob/f797c24145813ce2a10367a2602c3cc0be5ca210/Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean#L172-L196
The generation of the simps-lemmas attached to this definition is also extremely long. How could I investigate further what is creating this slow-down?
I have tried

set_option profiler true in
attribute [simps! hom_hom₁ hom_hom₂ hom_hom₃]
  mapTriangleOpCompTriangleOpEquivalenceFunctorApp

but it only tells me "dsimp took 2.25s".

[Yaël Dillies]

Is it possible that extra reductions are happening? Eg simp knows how to reduce Prod.fst (a, b) to a, but not necessarily Prod.myOwnFst (a, b) where Prod.myOwnFirst is a wrapper around Prod.fst

[Jovan Gerbscheid]

You should use set_option trace.profiler true in. This lets you see which parts are slow.

[Joël Riou]

Thanks very much! Indeed, this gives more details. It seems it was trying to apply the irrelevant simp lemmas attached to docs#CategoryTheory.Adjunction.rightAdjointCommShift. The slow down seems mostly fixed by not making these simp lemmas.