Two questions about instance synthesis

Stream: mathlib4

[Sina Hazratpour 𓃵]

1. If I have a theorem whose proof is by infer_instance is there a way to get the list of instances used in the inference displayed in the Lean's infoview? a command ideally?
2. Is there a way to know the places in mathlib's category theory where infer_instance has the longest list of instances in its inference?

[Ruben Van de Velde]

Maybe #synth is of interest to you

[Sina Hazratpour 𓃵]

#synth can be made to work for the first question. I was wondering if we have something similar to show_term but for instances.

[Yakov Pechersky]

Some pretty printer option, likely more surgical could help, but a big hammer would be pp.all which iiuc would show the instance?