fix: goto-definition for binrel% operators (≥, ≤, etc.)

This PR fixes goto-definition for binary relation operators.

**Problem:** Goto-def on `≥` went to the macro rule instead of `GE.ge`.

**Root cause:** In `elabBinRelCore`, the "uncomparable types" path (line 536)
called `elabAppArgs` directly without wrapping in `withTermInfoContext'`,
unlike `binop%` which goes through `toExprCore` that creates nested TermInfo.

**Fix:** Wrap the `elabAppArgs` call with `withTermInfoContext'` to match
`binop%` behavior.

**Note:** Initially tried adding `withInfo := true` to `resolveId? stx[1]`,
but that creates TermInfo with the unapplied type `{α : Type} → [LE α] → ...`
rather than the concrete instantiated type like `Nat → Nat → Prop`.

Author: alok

src/Lean/Elab/Extra.lean

@@ -541,7 +541,10 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
       let rhs ← withRef rhsStx <| toBoolIfNecessary rhs
       let lhsType ← inferType lhs
       let rhs ← withRef rhsStx <| ensureHasType lhsType rhs
-      elabAppArgs f #[] #[Arg.expr lhs, Arg.expr rhs] expectedType? (explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
+      -- Wrap in TermInfo to match binop% behavior for goto-definition
+      withRef stx <|
+        withTermInfoContext' .anonymous stx do
+          elabAppArgs f #[] #[Arg.expr lhs, Arg.expr rhs] expectedType? (explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
     else
       let mut maxType := r.max?.get!
       /- If `noProp == true` and `maxType` is `Prop`, then set `maxType := Bool`. `See toBoolIfNecessary` -/