diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 20302035b3..d6dfbc59d2 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -690,10 +690,12 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
     match lvalRes with
     | LValResolution.projIdx structName idx =>
       let f := mkProj structName idx f
+      addTermInfo lval.getRef f
       loop f lvals
     | LValResolution.projFn baseStructName structName fieldName =>
       let f ← mkBaseProjections baseStructName structName f
       let projFn ← mkConst (baseStructName ++ fieldName)
+      addTermInfo lval.getRef projFn
       if lvals.isEmpty then
         let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f }
         elabAppArgs projFn namedArgs args expectedType? explicit ellipsis
@@ -703,6 +705,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
     | LValResolution.const baseStructName structName constName =>
       let f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f
       let projFn ← mkConst constName
+      addTermInfo lval.getRef projFn
       if lvals.isEmpty then
         let projFnType ← inferType projFn
         let (args, namedArgs) ← addLValArg baseStructName constName f args namedArgs projFnType
@@ -711,6 +714,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
         let f ← elabAppArgs projFn #[] #[Arg.expr f] (expectedType? := none) (explicit := false) (ellipsis := false)
         loop f lvals
     | LValResolution.localRec baseName fullName fvar =>
+      addTermInfo lval.getRef fvar
       if lvals.isEmpty then
         let fvarType ← inferType fvar
         let (args, namedArgs) ← addLValArg baseName fullName f args namedArgs fvarType
@@ -720,6 +724,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
         loop f lvals
     | LValResolution.getOp fullName idx =>
       let getOpFn ← mkConst fullName
+      addTermInfo lval.getRef getOpFn
       if lvals.isEmpty then
         let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f }
         let namedArgs ← addNamedArg namedArgs { name := `idx,  val := Arg.stx idx }
@@ -770,6 +775,8 @@ private partial def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level)
     -- Set `errToSorry` to `false` if `funLVals` > 1. See comment above about the interaction between `errToSorry` and `observing`.
     withReader (fun ctx => { ctx with errToSorry := funLVals.length == 1 && ctx.errToSorry }) do
       funLVals.foldlM (init := acc) fun acc ⟨f, fields⟩ => do
+        unless lvals.isEmpty && args.isEmpty && namedArgs.isEmpty do
+          addTermInfo fIdent f
         let lvals' := fields.map (LVal.fieldName fIdent)
         let s ← observing do
           let e ← elabAppLVals f (lvals' ++ lvals) namedArgs args expectedType? explicit ellipsis
@@ -784,17 +791,17 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     withReader (fun ctx => { ctx with errToSorry := false }) do
       f.getArgs.foldlM (fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit ellipsis true acc) acc
   else match f with
-  | `($(e).$idx:fieldIdx) =>
-    let idx := idx.isFieldIdx?.get!
-    elabAppFn e (LVal.fieldIdx f idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
+  | `($(e).$idxStx:fieldIdx) =>
+    let idx := idxStx.isFieldIdx?.get!
+    elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
   | `($e |>. $field) => do
      let f ← `($(e).$field)
      elabAppFn f lvals namedArgs args expectedType? explicit ellipsis overloaded acc
   | `($(e).$field:ident) =>
-    let newLVals := field.getId.eraseMacroScopes.components.map (fun n => LVal.fieldName f (toString n))
+    let newLVals := field.getId.eraseMacroScopes.components.map (fun n => LVal.fieldName field (toString n))
     elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-  | `($e[$idx]) =>
-    elabAppFn e (LVal.getOp f idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
+  | `($e[%$bracket $idx]) =>
+    elabAppFn e (LVal.getOp bracket idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
   | `($id:ident@$t:term) =>
     throwError "unexpected occurrence of named pattern"
   | `($id:ident) => do
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 5784b2f26a..19557f8b34 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -287,7 +287,9 @@ def liftTermElabM {α} (declName? : Option Name) (x : TermElabM α) : CommandEla
   let (((ea, termS), metaS), coreS) ← liftEIO x
   let infoTrees        := termS.infoState.trees.map fun tree =>
     let tree := tree.substitute termS.infoState.assignment
-    InfoTree.context { env := coreS.env, mctx := metaS.mctx, currNamespace := scope.currNamespace, openDecls := scope.openDecls, options := scope.opts } tree
+    InfoTree.context {
+      env := coreS.env, fileMap := ctx.fileMap, mctx := metaS.mctx, currNamespace := scope.currNamespace, openDecls := scope.openDecls, options := scope.opts
+    } tree
   modify fun s => { s with
     env             := coreS.env
     messages        := addTraceAsMessages ctx (s.messages ++ termS.messages) coreS.traceState
diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index 573f91d26e..11a2ae9c9b 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -20,6 +20,7 @@ open Std (PersistentArray PersistentArray.empty PersistentHashMap)
    assignments are stored at `mctx`. -/
 structure ContextInfo where
   env           : Environment
+  fileMap       : FileMap
   mctx          : MetavarContext := {}
   options       : Options        := {}
   currNamespace : Name           := Name.anonymous
@@ -101,7 +102,9 @@ def ContextInfo.ppSyntax (info : ContextInfo) (lctx : LocalContext) (stx : Synta
 
 def TermInfo.format (cinfo : ContextInfo) (info : TermInfo) : IO Format := do
   cinfo.runMetaM info.lctx do
-    return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)}"
+    let pos    := info.stx.getPos.getD 0
+    let endPos := info.stx.getTailPos.getD pos
+    return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {cinfo.fileMap.toPosition pos}-{cinfo.fileMap.toPosition endPos}"
 
 def ContextInfo.ppGoals (cinfo : ContextInfo) (goals : List MVarId) : IO Format :=
   if goals.isEmpty then
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index e38e77b3de..bd0e737ac2 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -279,6 +279,11 @@ inductive LVal where
   | fieldName (ref : Syntax) (name : String)
   | getOp     (ref : Syntax) (idx : Syntax)
 
+def LVal.getRef : LVal → Syntax
+  | LVal.fieldIdx ref _  => ref
+  | LVal.fieldName ref _ => ref
+  | LVal.getOp ref _     => ref
+
 instance : ToString LVal where
   toString
     | LVal.fieldIdx _ i => toString i
@@ -987,6 +992,10 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
       | some expectedType => elabImplicitLambda stx catchExPostpone expectedType #[]
       | none              => elabUsingElabFns stx expectedType? catchExPostpone
 
+def addTermInfo (stx : Syntax) (e : Expr) : TermElabM Unit := do
+  if (← getInfoState).enabled then
+    pushInfoTree <| InfoTree.node (children := {}) <| Info.ofTermInfo { lctx := (← getLCtx), expr := e, stx := stx }
+
 def mkTermInfo (stx : Syntax) (e : Expr) : TermElabM (Sum Info MVarId) := do
   let isHole? : TermElabM (Option MVarId) := do
     match e with
diff --git a/tests/lean/run/infoTree.lean b/tests/lean/run/infoTree.lean
index 5c0092b9c1..2e62dff0d3 100644
--- a/tests/lean/run/infoTree.lean
+++ b/tests/lean/run/infoTree.lean
@@ -26,4 +26,7 @@ def f2 : (x y : Nat) → (b : Bool) → Nat :=
     let z1 := z + w
     z + z1
 
+def f3 (s : Nat × Array (Array Nat)) : Array Nat :=
+  s.2[1].push s.1
+
 showInfoTrees!