improve introspection for variables in lemmas

I was asked to migrate this issue from the VS Code repository (https://github.com/leanprover/vscode-lean/issues/168).

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

I'm working on the very first Lean tutorial (00_first_proofs.lean).

An example of my issue is lemma inf_lt. The given proof uses the .2 syntax for accessing part of the x is_an_inf_of A assumption. I found the tutorial text difficult to follow because I did not remember which part of the is_an_inf_of assumption was which. As you can see below, mousing over the .2 syntax gives information on the exact tactic instead of explaining the second part of the assumption as expected:

Right-clicking .2 and choosing Go To Definition also takes me to the definition of the exact tactic. I also tried mousing over the hx in the goals area, but no information is given there. Inspecting hx doesn't do what I would expect, either; the expected behavior is to show or jump to the declared assumption, but instead it brings the goal window into focus.

This makes it quite a bit more difficult to work through the tutorial. In the case of the .2, to find the definition the user must locate the declaration of hx (not difficult but still an extra step), then follow the trail via is_an_inf_of -> is_a_max_of.

Reproduces how often: 100%

Versions

Lean (version 3.16.1, commit d8a3085bf62e, Release)
Mac OS 10.15.5

Start with the migrated VS Code issue and the example in 00_first_proofs.lean, especially lemma inf_lt, the .2 expression, and the hx assumption. Trace how hover, Go To Definition, and inspection currently behave there; done means these interactions explain or navigate to the relevant assumption rather than showing the exact tactic or focusing the goal window.