VS Code help

Stream: new members

[Ben Toner]

When looking at this lemma in VS Code, is there a way to jump to the definition of (re_clm : 𝕜 →L[ℝ] ℝ).times_cont_diff? When I hover or use the "Go to Definition" command, it takes me to the definition of exact.

lemma times_cont_diff_norm_sq : times_cont_diff ℝ n (λ x : E, ∥x∥ ^ 2) :=
begin
  simp only [sq, ← inner_self_eq_norm_sq],
  exact (re_clm : 𝕜 →L[ℝ] ℝ).times_cont_diff.comp (times_cont_diff_id.inner times_cont_diff_id)
end

[Eric Wieser]

You can sometimes get around this by putting the expression in a have := ... first

[Eric Wieser]

Failing that, #check always behaves

[Ben Toner]

@Eric Wieser Thanks, #check works.