## Stream: new members

### Topic: Doing #check inside a proof

#### Jakob Scholbach (Mar 17 2021 at 18:53):

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

#### Patrick Massot (Mar 17 2021 at 18:54):

use have or let

#### Johan Commelin (Mar 17 2021 at 18:54):

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

#### Johan Commelin (Mar 17 2021 at 18:54):

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

#### Jakob Scholbach (Mar 17 2021 at 19:04):

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!

Last updated: May 08 2021 at 10:12 UTC