diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean
index a3f2e5c82f..8a9bd0cd75 100644
--- a/src/Init/Lean/Elab/BuiltinNotation.lean
+++ b/src/Init/Lean/Elab/BuiltinNotation.lean
@@ -17,6 +17,16 @@ fun stx expectedType? => do
   let a := stx.getArg 2;
   elabTerm (mkAppStx f #[a]) expectedType?
 
+def mkProjStx (t : Syntax) (i : Syntax) : Syntax :=
+Syntax.node `Lean.Parser.Term.proj #[t, mkAtom("."), i]
+
+@[builtinTermElab dollarProj] def elabDollarProj : TermElab :=
+fun stx expectedType? => do
+  -- term `$.` field
+  let f := stx.getArg 0;
+  let i := stx.getArg 2;
+  elabTerm (mkProjStx f i) expectedType?
+
 def elabInfix (f : Syntax) : TermElab :=
 fun stx expectedType? => do
   -- term `op` term
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index bd0f021ebf..53ac7bcaec 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -154,3 +154,4 @@ f a
 #eval run "#check #[1, 2, 3].foldl (fun r a => r.push a) #[]"
 #eval run "#check #[1, 2, 3].foldl (fun r a => (r.push a).push a) #[]"
 #eval run "#check #[1, 2, 3].foldl (fun r a => ((r.push a).push a).push a) #[]"
+#eval run "#check #[].push one $.push two $.push zero $.size.succ"