How to find out which instance was inferred?

Stream: new members

[Michael Rothgang]

Given a successful proof "by infer_instance", how can I find out where this instance is defined? (In my case, I tried reading the relevant files and searching the API docs, both not successfully.)

Case in point, I'd like to understand why this works

import Mathlib
lemma aux {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] :
    LocallyCompactSpace E := by infer_instance

and this does not

import Mathlib
lemma aux {E : Type*} (𝕜 : Type u) [NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜]
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
    -- error: failed to synthesize instance LocallyCompactSpace E
    LocallyCompactSpace E := by infer_instance

More specifically, where I'd start to add such an instance.

[Yaël Dillies]

Use #synth instead.

[Yaël Dillies]

import Mathlib

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]

#synth LocallyCompactSpace E  -- tells you what instance it finds

[Michael Rothgang]

Thank you, works like a charm :-)

[Utensil Song]

You might also want to read 7. Hierarchies in #mil which teaches a few other helpful tricks like set_option trace.Meta.synthInstance true, set_option synthInstance.checkSynthOrder false, check Something.mk, whatsnew in etc.

Particularly, set_option trace.Meta.synthInstance true is very helpful when you are working inside your lemma, there would be blue squiggles under where Lean synthesize instances so you don't have to figure out how to tell #synth what you are working with in a different way.