Does `squeeze_dsimp` ever not return `dsimp only`?

Stream: general

[Kevin Buzzard]

A trick I learnt relatively recently was that if I wanted to know what dsimp was doing, then squeeze_dsimp was not the way to find out; in fact one should just do set_option trace.dsimplify true, search the output for ==> and then try and manually figure out the name of the lemmas which were being applied. Is there any way of making squeeze_dsimp not return Try this: dsimp only? Should this tactic simply be removed, if not?

[Mario Carneiro]

It works correctly in lean 4

[Mario Carneiro]

It is unlikely this will be fixed in lean 3, dsimp? has a better chance of working than squeeze_dsimp