## Stream: new members

### Topic: looking up instance definitions

#### Justus Springer (Mar 17 2021 at 09:31):

In this example:

import order.filter.basic

variables {α : Type*}

open filter

example (S T : set α) : principal S ≤ principal T ↔ S ⊆ T :=
begin
sorry,
end


I would like to look up the definition of ≤ for filters. However, when I Ctrl+Click on it in VScode, I get referred to the general definition in the class has_le at core.lean. Is there a quick way to look up instance specific definitions like this?

#### Johan Commelin (Mar 17 2021 at 09:36):

variables (α : Type*)
#check (by apply_instance : has_le (filter α)) -- apparently has_le comes from preorder
#check (by apply_instance : preorder (filter α)) -- see partial_order
#check (by apply_instance : partial_order (filter α)) -- found it: filter.partial_order
#check filter.partial_order -- Ctrl-click here


#### Johan Commelin (Mar 17 2021 at 09:36):

I agree that it would be cool if there were a tactic that took care of the intermediate step.

#### Justus Springer (Mar 17 2021 at 09:38):

thanks, that's a cool trick!

#### Kevin Buzzard (Mar 17 2021 at 10:11):

I always use the infoview for this now:
infoview.png

#### Johan Commelin (Mar 17 2021 at 10:11):

ooh, right, that makes a lot of sense (-;

#### Kevin Buzzard (Mar 17 2021 at 10:12):

You just trace back to where something is actually defined and then jump to definition for the last thing.

Last updated: May 13 2021 at 20:13 UTC