Doing #check inside a proof

Stream: new members

[Jakob Scholbach]

Is there a way to use #check inside a proof? Or some other way to "debug" what a certain expression is?

[Patrick Massot]

use have or let

[Johan Commelin]

@Jakob Scholbach If you are using VScode, you can also click on expressions in the goal window to get more info.

[Johan Commelin]

But this only works if you don't have an error.

[Jakob Scholbach]

Yes, @Johan Commelin I was aware of clicking at things, but my problem was / is that I often need to figure out why I can't invoke some theorem in some specific way. But @Patrick Massot s advice is helpful, merci bien!