Go to definition on `congr(...)` goes to the def of `id`

Stream: mathlib4

[Kyle Miller]

What do we need to do to fix the elaborator for congr(...) so that "go to definition" works and doesn't just go to docs#id ?

import Mathlib.Tactic.TermCongr

example (x y : Nat) (h : x = y) : x + 1 = y + 1 := congr($h + 1)

Even "go to definition" on the + goes to id

I'm guessing it's id because the last step of the elaborator is mkExpectedTypeHint. Was I supposed to add some TermInfo to the info trees?