How to find definition of notation for an specific instance?

Stream: new members

[Fernando Chu]

For example, what's the best way to figure out what ⊆ means in this context?

import Mathlib

example (X : Type) (A B C : Set X) : A ⊆ B → B ⊆ C → A ⊆ C := by
  sorry

My current approach would be going to the definition of ⊆, then going to definition of Subset, then loogling the HasSubset instance of Set X, which points me to the LE instance on Set X which finally points me to Set.Subset.

Is there a better way? (In this particular example I can make a good guess of what is the definition name, but I'm wondering for the general case)

[Niels Voss]

This isn't a great solution but you can do

#synth HasSubset (Set _)

to skip the loogle step

[Kenny Lau]

@Fernando Chu

import Mathlib

example (X : Type) (A B C : Set X) : A ⊆ B → B ⊆ C → A ⊆ C := by
  unfold_projs

(which you should not include in any code that you actually care about)

[Fernando Chu]

Precisely what I wanted, thank you!

[Snir Broshi]

Using vscode's "go to definition" on notation works, though it usually finds multiple definitions with the most specific instance being the last one, so just ctrl/cmd click on the notation and go down to the last option