looking up instance definitions

Stream: new members

[Justus Springer]

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]

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]

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

[Justus Springer]

thanks, that's a cool trick!

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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