diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 3980c6d9ca..23f9721b6a 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -919,6 +919,17 @@ private def getAppNumArgsAux : Expr → Nat → Nat
 def getAppNumArgs (e : Expr) : Nat :=
   getAppNumArgsAux e 0
 
+/--
+Like `Lean.Expr.getAppFn` but assumes the application has up to `maxArgs` arguments.
+If there are any more arguments than this, then they are returned by `getAppFn` as part of the function.
+
+In particular, if the given expression is a sequence of function applications `f a₁ .. aₙ`,
+returns `f a₁ .. aₖ` where `k` is minimal such that `n - k ≤ maxArgs`.
+-/
+def getBoundedAppFn : (maxArgs : Nat) → Expr → Expr
+  | maxArgs' + 1, .app f _ => getBoundedAppFn maxArgs' f
+  | _, e => e
+
 private def getAppArgsAux : Expr → Array Expr → Nat → Array Expr
   | app f a, as, i => getAppArgsAux f (as.set! i a) (i-1)
   | _,       as, _ => as
@@ -929,6 +940,21 @@ private def getAppArgsAux : Expr → Array Expr → Nat → Array Expr
   let nargs := e.getAppNumArgs
   getAppArgsAux e (mkArray nargs dummy) (nargs-1)
 
+private def getBoundedAppArgsAux : Expr → Array Expr → Nat → Array Expr
+  | app f a, as, i + 1 => getBoundedAppArgsAux f (as.set! i a) i
+  | _,       as, _     => as
+
+/--
+Like `Lean.Expr.getAppArgs` but returns up to `maxArgs` arguments.
+
+In particular, given `f a₁ a₂ ... aₙ`, returns `#[aₖ₊₁, ..., aₙ]`
+where `k` is minimal such that the size of this array is at most `maxArgs`.
+-/
+@[inline] def getBoundedAppArgs (maxArgs : Nat) (e : Expr) : Array Expr :=
+  let dummy := mkSort levelZero
+  let nargs := min maxArgs e.getAppNumArgs
+  getBoundedAppArgsAux e (mkArray nargs dummy) nargs
+
 private def getAppRevArgsAux : Expr → Array Expr → Array Expr
   | app f a, as => getAppRevArgsAux f (as.push a)
   | _,       as => as
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index ba547db886..45c675e6be 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -104,72 +104,94 @@ def delabAppFn : Delab := do
   else
     delab
 
+/--
+A structure that records details of a function parameter.
+-/
 structure ParamKind where
+  /-- Binder name for the parameter. -/
   name        : Name
+  /-- Binder info for the parameter. -/
   bInfo       : BinderInfo
+  /-- The default value for the parameter, if the parameter has a default value. -/
   defVal      : Option Expr := none
+  /-- Whether the parameter is an autoparam (i.e., whether it uses a tactic for the default value). -/
   isAutoParam : Bool := false
 
+/--
+Returns true if the parameter is an explicit parameter that has neither a default value nor a tactic.
+-/
 def ParamKind.isRegularExplicit (param : ParamKind) : Bool :=
   param.bInfo.isExplicit && !param.isAutoParam && param.defVal.isNone
 
-/-- Return array with n-th element set to kind of n-th parameter of `e`. -/
-partial def getParamKinds : DelabM (Array ParamKind) := do
-  let e ← getExpr
+/--
+Given a function `f` supplied with arguments `args`, returns an array whose n-th element
+is set to the kind of the n-th argument's associated parameter.
+We do not assume the expression `mkAppN f args` is sensical,
+and this function captures errors (except for panics) and returns the empty array.
+
+The returned array might be longer than the number of arguments.
+It gives parameter kinds for the fully-applied function.
+Note: the `defVal` expressions are only guaranteed to be valid for parameters associated to the supplied arguments;
+after this, they might refer to temporary fvars.
+
+This function properly handles "overapplied" functions.
+For example, while `id` takes one explicit argument, it can take more than one explicit
+argument when its arguments are specialized to function types, like in `id id 2`.
+-/
+def getParamKinds (f : Expr) (args : Array Expr) : MetaM (Array ParamKind) := do
   try
     withTransparency TransparencyMode.all do
-      forallTelescopeArgs e.getAppFn e.getAppArgs fun params _ => do
-        params.mapM fun param => do
-          let l ← param.fvarId!.getDecl
-          pure { name := l.userName, bInfo := l.binderInfo, defVal := l.type.getOptParamDefault?, isAutoParam := l.type.isAutoParam }
+      let mut result : Array ParamKind := Array.mkEmpty args.size
+      let mut fnType ← inferType f
+      let mut j := 0
+      for i in [0:args.size] do
+        unless fnType.isForall do
+          fnType ← whnf (fnType.instantiateRevRange j i args)
+          j := i
+        let .forallE n t b bi := fnType | failure
+        let defVal := t.getOptParamDefault? |>.map (·.instantiateRevRange j i args)
+        result := result.push { name := n, bInfo := bi, defVal, isAutoParam := t.isAutoParam }
+        fnType := b
+      fnType := fnType.instantiateRevRange j args.size args
+      -- We still want to consider parameters past the ones for the supplied arguments.
+      forallTelescopeReducing fnType fun xs _ => do
+        xs.foldlM (init := result) fun result x => do
+          let l ← x.fvarId!.getDecl
+          -- Warning: the defVal might refer to fvars that are only valid in this context
+          pure <| result.push { name := l.userName, bInfo := l.binderInfo, defVal := l.type.getOptParamDefault?, isAutoParam := l.type.isAutoParam }
   catch _ => pure #[] -- recall that expr may be nonsensical
-where
-  forallTelescopeArgs f args k := do
-    forallBoundedTelescope (← inferType f) args.size fun xs b =>
-      if xs.isEmpty || xs.size == args.size then
-        -- we still want to consider optParams
-        forallTelescopeReducing b fun ys b => k (xs ++ ys) b
-      else
-        forallTelescopeArgs (mkAppN f $ args.shrink xs.size) (args.extract xs.size args.size) fun ys b =>
-          k (xs ++ ys) b
-
-@[builtin_delab app]
-def delabAppExplicit : Delab := do
-  let paramKinds ← getParamKinds
-  let tagAppFn ← getPPOption getPPTagAppFns
-  let (fnStx, _, argStxs) ← withAppFnArgs
-    (do
-      let stx ← withOptionAtCurrPos `pp.tagAppFns tagAppFn delabAppFn
-      let needsExplicit := stx.raw.getKind != ``Lean.Parser.Term.explicit
-      let stx ← if needsExplicit then `(@$stx) else pure stx
-      pure (stx, paramKinds.toList, #[]))
-    (fun ⟨fnStx, paramKinds, argStxs⟩ => do
-      let isInstImplicit := match paramKinds with
-                            | [] => false
-                            | param :: _ => param.bInfo == BinderInfo.instImplicit
-      let argStx ← if ← getPPOption getPPAnalysisHole then `(_)
-                   else if isInstImplicit == true then
-                     let stx ← if ← getPPOption getPPInstances then delab else `(_)
-                     if ← getPPOption getPPInstanceTypes then
-                       let typeStx ← withType delab
-                       `(($stx : $typeStx))
-                     else pure stx
-                   else delab
-      pure (fnStx, paramKinds.tailD [], argStxs.push argStx))
-  return Syntax.mkApp fnStx argStxs
 
 def shouldShowMotive (motive : Expr) (opts : Options) : MetaM Bool := do
   pure (getPPMotivesAll opts)
   <||> (pure (getPPMotivesPi opts) <&&> returnsPi motive)
   <||> (pure (getPPMotivesNonConst opts) <&&> isNonConstFun motive)
 
-def isRegularApp : DelabM Bool := do
+/--
+Returns true if an application should use explicit mode when delaborating.
+-/
+def useAppExplicit (paramKinds : Array ParamKind) : DelabM Bool := do
+  if ← getPPOption getPPExplicit then
+    if paramKinds.any (fun param => !param.isRegularExplicit) then return true
+
+  -- If the expression has an implicit function type, fall back to delabAppExplicit.
+  -- This is e.g. necessary for `@Eq`.
+  let isImplicitApp ← try
+      let ty ← whnf (← inferType (← getExpr))
+      pure <| ty.isForall && (ty.binderInfo matches .implicit | .instImplicit)
+    catch _ => pure false
+  if isImplicitApp then return true
+
+  return false
+
+/--
+Returns true if the application is a candidate for unexpanders.
+-/
+def isRegularApp (maxArgs : Nat) : DelabM Bool := do
   let e ← getExpr
-  if not (unfoldMDatas e.getAppFn).isConst then return false
-  if ← withNaryFn (withMDatasOptions (getPPOption getPPUniverses <||> getPPOption getPPAnalysisBlockImplicit)) then return false
-  for i in [:e.getAppNumArgs] do
-    if ← withNaryArg i (getPPOption getPPAnalysisNamedArg) then return false
-  return true
+  if not (unfoldMDatas (e.getBoundedAppFn maxArgs)).isConst then return false
+  withBoundedAppFnArgs maxArgs
+    (not <$> withMDatasOptions (getPPOption getPPUniverses <||> getPPOption getPPAnalysisBlockImplicit))
+    (fun b => pure b <&&> not <$> getPPOption getPPAnalysisNamedArg)
 
 def unexpandRegularApp (stx : Syntax) : Delab := do
   let Expr.const c .. := (unfoldMDatas (← getExpr).getAppFn) | unreachable!
@@ -204,25 +226,42 @@ def unexpandStructureInstance (stx : Syntax) : Delab := whenPPOption getPPStruct
     if (← getPPOption getPPStructureInstanceType) then delab >>= pure ∘ some else pure none
   `({ $fields,* $[: $tyStx]? })
 
-@[builtin_delab app]
-def delabAppImplicit : Delab := do
+/--
+Delaborates a function application in explicit mode, and ensures the resulting
+head syntax is wrapped with `@`.
+-/
+def delabAppExplicitCore (maxArgs : Nat) (delabHead : Delab) (paramKinds : Array ParamKind) (tagAppFn : Bool) : Delab := do
+  let (fnStx, _, argStxs) ← withBoundedAppFnArgs maxArgs
+    (do
+      let stx ← withOptionAtCurrPos `pp.tagAppFns tagAppFn delabHead
+      let needsExplicit := stx.raw.getKind != ``Lean.Parser.Term.explicit
+      let stx ← if needsExplicit then `(@$stx) else pure stx
+      pure (stx, paramKinds.toList, #[]))
+    (fun ⟨fnStx, paramKinds, argStxs⟩ => do
+      let isInstImplicit := match paramKinds with
+                            | [] => false
+                            | param :: _ => param.bInfo == BinderInfo.instImplicit
+      let argStx ← if ← getPPOption getPPAnalysisHole then `(_)
+                   else if isInstImplicit == true then
+                     let stx ← if ← getPPOption getPPInstances then delab else `(_)
+                     if ← getPPOption getPPInstanceTypes then
+                       let typeStx ← withType delab
+                       `(($stx : $typeStx))
+                     else pure stx
+                   else delab
+      pure (fnStx, paramKinds.tailD [], argStxs.push argStx))
+  return Syntax.mkApp fnStx argStxs
+
+/--
+Delaborates a function application in the standard mode, where implicit arguments are generally not
+included.
+-/
+def delabAppImplicitCore (maxArgs : Nat) (delabHead : Delab) (paramKinds : Array ParamKind) (tagAppFn : Bool) : Delab := do
   -- TODO: always call the unexpanders, make them guard on the right # args?
-  let paramKinds ← getParamKinds
-  if ← getPPOption getPPExplicit then
-    if paramKinds.any (fun param => !param.isRegularExplicit) then failure
-
-  -- If the application has an implicit function type, fall back to delabAppExplicit.
-  -- This is e.g. necessary for `@Eq`.
-  let isImplicitApp ← try
-      let ty ← whnf (← inferType (← getExpr))
-      pure <| ty.isForall && (ty.binderInfo == BinderInfo.implicit || ty.binderInfo == BinderInfo.instImplicit)
-    catch _ => pure false
-  if isImplicitApp then failure
-
-  let tagAppFn ← getPPOption getPPTagAppFns
-  let (fnStx, _, argStxs) ← withAppFnArgs
-    (withOptionAtCurrPos `pp.tagAppFns tagAppFn <|
-      return (← delabAppFn, paramKinds.toList, #[]))
+  let (fnStx, _, argStxs) ← withBoundedAppFnArgs maxArgs
+    (do
+      let stx ← withOptionAtCurrPos `pp.tagAppFns tagAppFn delabHead
+      return (stx, paramKinds.toList, #[]))
     (fun (fnStx, paramKinds, argStxs) => do
       let arg ← getExpr
       let opts ← getOptions
@@ -247,12 +286,60 @@ def delabAppImplicit : Delab := do
       pure (fnStx, paramKinds.tailD [], argStxs))
   let stx := Syntax.mkApp fnStx argStxs
 
-  if ← isRegularApp then
+  if ← isRegularApp maxArgs then
     (guard (← getPPOption getPPNotation) *> unexpandRegularApp stx)
     <|> (guard (← getPPOption getPPStructureInstances) *> unexpandStructureInstance stx)
     <|> pure stx
   else pure stx
 
+/--
+Delaborates applications. Removes up to `maxArgs` arguments to form
+the "head" of the application and delaborates the head using `delabHead`.
+The remaining arguments are processed depending on whether heuristics indicate that the application
+should be delaborated using `@`.
+-/
+def delabAppCore (maxArgs : Nat) (delabHead : Delab) : Delab := do
+  let tagAppFn ← getPPOption getPPTagAppFns
+  let e ← getExpr
+  let paramKinds ← getParamKinds (e.getBoundedAppFn maxArgs) (e.getBoundedAppArgs maxArgs)
+
+  let useExplicit ← useAppExplicit paramKinds
+
+  if useExplicit then
+    delabAppExplicitCore maxArgs delabHead paramKinds tagAppFn
+  else
+    delabAppImplicitCore maxArgs delabHead paramKinds tagAppFn
+
+/--
+Default delaborator for applications.
+-/
+@[builtin_delab app]
+def delabApp : Delab := do
+  delabAppCore (← getExpr).getAppNumArgs delabAppFn
+
+/--
+The `withOverApp` combinator allows delaborators to handle "over-application" by using the core
+application delaborator to handle additional arguments.
+
+For example, suppose `f : {A : Type} → Foo A → A` and we want to implement a delaborator for
+applications `f x` to pretty print as `F[x]`. Because `A` is a type variable we might encounter
+a term of the form `@f (A → B) x y`, which has an additional argument `y`.
+With this combinator one can use an arity-2 delaborator to pretty print this as `F[x] y`.
+
+* `arity`: the expected number of arguments to `f`.
+  The combinator will fail if fewer than this number of arguments are passed,
+  and if more than this number of arguments are passed the arguments are handled using
+  the standard application delaborator.
+* `x`: constructs data corresponding to the main application (`f x` in the example)
+-/
+def withOverApp (arity : Nat) (x : Delab) : Delab := do
+  let n := (← getExpr).getAppNumArgs
+  guard <| n ≥ arity
+  if n == arity then
+    x
+  else
+    delabAppCore (n - arity) x
+
 /-- State for `delabAppMatch` and helpers. -/
 structure AppMatchState where
   info        : MatcherInfo
@@ -394,25 +481,12 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
         `(match $[$st.discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*)
     return Syntax.mkApp stx st.moreArgs
 
-/--
-Annotation key to use in hack for overapplied `let_fun` notation.
--/
-def delabLetFunKey : Name := `_delabLetFun
-
 /--
 Delaborates applications of the form `letFun v (fun x => b)` as `let_fun x := v; b`.
 -/
 @[builtin_delab app.letFun]
-def delabLetFun : Delab := whenPPOption getPPNotation do
+def delabLetFun : Delab := whenPPOption getPPNotation <| withOverApp 4 do
   let e ← getExpr
-  let nargs := e.getAppNumArgs
-  if 4 < nargs then
-    -- It's overapplied. Hack: insert metadata around the first four arguments and delaborate again.
-    -- This will cause the app delaborator to delaborate `(letFun v f) x1 ... xn` with `letFun v f` as the function.
-    let args := e.getAppArgs
-    let f := mkAppN e.getAppFn (args.extract 0 4)
-    let e' := mkAppN (mkAnnotation delabLetFunKey f) (args.extract 4 args.size)
-    return (← withTheReader SubExpr ({· with expr := e'}) delab)
   guard <| e.getAppNumArgs == 4
   let Expr.lam n _ b _ := e.appArg! | failure
   let n ← getUnusedName n b
@@ -611,13 +685,13 @@ def delabLit : Delab := do
 
 -- `@OfNat.ofNat _ n _` ~> `n`
 @[builtin_delab app.OfNat.ofNat]
-def delabOfNat : Delab := whenPPOption getPPCoercions do
+def delabOfNat : Delab := whenPPOption getPPCoercions <| withOverApp 3 do
   let .app (.app _ (.lit (.natVal n))) _ ← getExpr | failure
   return quote n
 
 -- `@OfDecimal.ofDecimal _ _ m s e` ~> `m*10^(sign * e)` where `sign == 1` if `s = false` and `sign = -1` if `s = true`
 @[builtin_delab app.OfScientific.ofScientific]
-def delabOfScientific : Delab := whenPPOption getPPCoercions do
+def delabOfScientific : Delab := whenPPOption getPPCoercions <| withOverApp 5 do
   let expr ← getExpr
   guard <| expr.getAppNumArgs == 5
   let .lit (.natVal m) ← pure (expr.getArg! 2) | failure
@@ -654,24 +728,23 @@ def delabProj : Delab := do
 /-- Delaborate a call to a projection function such as `Prod.fst`. -/
 @[builtin_delab app]
 def delabProjectionApp : Delab := whenPPOption getPPStructureProjections $ do
-  let e@(Expr.app fn _) ← getExpr | failure
+  let Expr.app fn _ ← getExpr | failure
   let .const c@(.str _ f) _ ← pure fn.getAppFn | failure
   let env ← getEnv
   let some info ← pure $ env.getProjectionFnInfo? c | failure
   -- can't use with classes since the instance parameter is implicit
   guard $ !info.fromClass
-  -- projection function should be fully applied (#struct params + 1 instance parameter)
-  -- TODO: support over-application
-  guard $ e.getAppNumArgs == info.numParams + 1
   -- If pp.explicit is true, and the structure has parameters, we should not
   -- use field notation because we will not be able to see the parameters.
   let expl ← getPPOption getPPExplicit
   guard $ !expl || info.numParams == 0
-  let appStx ← withAppArg delab
-  `($(appStx).$(mkIdent f):ident)
+  -- projection function should be fully applied (#struct params + 1 instance parameter)
+  withOverApp (info.numParams + 1) do
+    let appStx ← withAppArg delab
+    `($(appStx).$(mkIdent f):ident)
 
 @[builtin_delab app.dite]
-def delabDIte : Delab := whenPPOption getPPNotation do
+def delabDIte : Delab := whenPPOption getPPNotation <| withOverApp 5 do
   -- Note: we keep this as a delaborator for now because it actually accesses the expression.
   guard $ (← getExpr).getAppNumArgs == 5
   let c ← withAppFn $ withAppFn $ withAppFn $ withAppArg delab
@@ -688,7 +761,7 @@ where
         return (← delab, h.getId)
 
 @[builtin_delab app.cond]
-def delabCond : Delab := whenPPOption getPPNotation do
+def delabCond : Delab := whenPPOption getPPNotation <| withOverApp 4 do
   guard $ (← getExpr).getAppNumArgs == 4
   let c ← withAppFn $ withAppFn $ withAppArg delab
   let t ← withAppFn $ withAppArg delab
diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
index e09bddb5a6..3a044c6df0 100644
--- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
@@ -42,12 +42,28 @@ def withAppArg  (x : m α) : m α := do descend (← getExpr).appArg! 1 x
 def withType (x : m α) : m α := do
   descend (← Meta.inferType (← getExpr)) Pos.typeCoord x -- phantom positions for types
 
+/--
+Uses `xa` to compute the fold across the arguments of an application,
+where `xf` provides the initial value and is evaluated in the context of the head of the application.
+-/
 partial def withAppFnArgs (xf : m α) (xa : α → m α) : m α := do
   if (← getExpr).isApp then
     let acc ← withAppFn (withAppFnArgs xf xa)
     withAppArg (xa acc)
   else xf
 
+/--
+Uses `xa` to compute the fold across up to `maxArgs` outermost arguments of an application,
+where `xf` provides the initial value and is evaluated in the context of the application minus
+the arguments being folded across.
+-/
+def withBoundedAppFnArgs (maxArgs : Nat) (xf : m α) (xa : α → m α) : m α := do
+  match maxArgs, (← getExpr) with
+  | maxArgs' + 1, .app .. =>
+    let acc ← withAppFn (withBoundedAppFnArgs maxArgs' xf xa)
+    withAppArg (xa acc)
+  | _, _ => xf
+
 def withBindingDomain (x : m α) : m α := do descend (← getExpr).bindingDomain! 0 x
 
 def withBindingBody (n : Name) (x : m α) : m α := do
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index 280ea1e53b..6b353b2120 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -80,7 +80,7 @@ def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos :=
     if explicit then
       withOptionAtCurrPos pp.tagAppFns.name true do
       withOptionAtCurrPos pp.explicit.name true do
-        delabAppImplicit <|> delabAppExplicit
+        delabApp
     else
       delab
   let ⟨fmt, infos⟩ ← PrettyPrinter.ppExprWithInfos e (delab := delab)
diff --git a/tests/lean/283.lean.expected.out b/tests/lean/283.lean.expected.out
index 7a45c17bbd..92b3751dbe 100644
--- a/tests/lean/283.lean.expected.out
+++ b/tests/lean/283.lean.expected.out
@@ -1,7 +1,7 @@
 283.lean:1:24-1:25: error: application type mismatch
-  f (f ?m)
+  f f
 argument
-  f ?m
+  f
 has type
   ?m : Sort ?u
 but is expected to have type
diff --git a/tests/lean/439.lean.expected.out b/tests/lean/439.lean.expected.out
index 3a5aeae62c..5d7dae74a8 100644
--- a/tests/lean/439.lean.expected.out
+++ b/tests/lean/439.lean.expected.out
@@ -1,20 +1,20 @@
 fn.imp : {p : P} → Bar.fn p
 439.lean:18:7-18:12: error: function expected at
-  Fn.imp fn
+  fn.imp
 term has type
   Bar.fn ?m
 439.lean:29:7-29:11: error: function expected at
-  Fn.imp fn
+  fn.imp
 term has type
   Bar.fn ?m
-Fn.imp fn : Bar.fn p
-Fn.imp fn' Bp : Bar.fn p
+fn.imp : Bar.fn p
+fn'.imp Bp : Bar.fn p
 439.lean:39:11-39:12: error: application type mismatch
-  Fn.imp fn' p
+  fn'.imp p
 argument
   p
 has type
   P : Sort u
 but is expected to have type
   Bar.fn ?m : Sort ?u
-Fn.imp fn' (sorryAx (Bar.fn ?m) true) : Bar.fn ?m
+fn'.imp (sorryAx (Bar.fn ?m) true) : Bar.fn ?m
diff --git a/tests/lean/delabApp.lean b/tests/lean/delabApp.lean
new file mode 100644
index 0000000000..70835df07b
--- /dev/null
+++ b/tests/lean/delabApp.lean
@@ -0,0 +1,39 @@
+/-!
+# Testing features of the app delaborator, including overapplication
+-/
+
+/-!
+Check that the optional value equality check is specialized to the supplied arguments
+(rather than, formerly, the locally-defined fvars from a telescope).
+-/
+def foo (α : Type) [Inhabited α] (x : α := default) : α := x
+
+#check foo Nat
+#check foo Nat 1
+
+/-!
+Check that overapplied projections pretty print using projection notation.
+-/
+
+structure Foo where
+  f : Nat → Nat
+
+#check ∀ (x : Foo), x.f 1 = 0
+
+/-!
+Overapplied `letFun`
+-/
+#check (have f := id; f) 1
+
+/-!
+Overapplied `OfNat.ofNat`
+-/
+instance : OfNat (Nat → Nat) 1 where
+  ofNat := id
+
+#check (1 : Nat → Nat) 2
+
+/-!
+Overapplied `dite`
+-/
+#check (if h : True then id else id) 1
diff --git a/tests/lean/delabApp.lean.expected.out b/tests/lean/delabApp.lean.expected.out
new file mode 100644
index 0000000000..4831d315f8
--- /dev/null
+++ b/tests/lean/delabApp.lean.expected.out
@@ -0,0 +1,8 @@
+foo Nat : Nat
+foo Nat 1 : Nat
+∀ (x : Foo), x.f 1 = 0 : Prop
+(let_fun f := id;
+  f)
+  1 : Nat
+1 2 : Nat
+(if h : True then id else id) 1 : Nat
diff --git a/tests/lean/eagerCoeExpansion.lean.expected.out b/tests/lean/eagerCoeExpansion.lean.expected.out
index cd504e4e44..efdd015cf1 100644
--- a/tests/lean/eagerCoeExpansion.lean.expected.out
+++ b/tests/lean/eagerCoeExpansion.lean.expected.out
@@ -9,4 +9,4 @@ fun (a : Nat) =>
     (@Eq.{1} Bool (@bne.{0} Nat instBEqNat a (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))) Bool.true)
     (@Eq.{1} Bool (@bne.{0} Nat instBEqNat a (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) Bool.true)
 def s : Option Nat :=
-HOrElse.hOrElse (ConstantFunction.f myFun 3) fun x => ConstantFunction.f myFun 4
+HOrElse.hOrElse (myFun.f 3) fun x => myFun.f 4
diff --git a/tests/lean/ppMotives.lean.expected.out b/tests/lean/ppMotives.lean.expected.out
index f99a4985ae..e345ca95d2 100644
--- a/tests/lean/ppMotives.lean.expected.out
+++ b/tests/lean/ppMotives.lean.expected.out
@@ -4,7 +4,7 @@ fun x x_1 =>
     (fun x f x_2 =>
       (match x_2, x with
         | a, Nat.zero => fun x => a
-        | a, Nat.succ b => fun x => Nat.succ (PProd.fst x.fst a))
+        | a, Nat.succ b => fun x => Nat.succ (x.fst.fst a))
         f)
     x
 protected def Nat.add : Nat → Nat → Nat :=
@@ -13,7 +13,7 @@ fun x x_1 =>
     (fun x f x_2 =>
       (match (motive := Nat → (x : Nat) → Nat.below (motive := fun x => Nat → Nat) x → Nat) x_2, x with
         | a, Nat.zero => fun x => a
-        | a, Nat.succ b => fun x => Nat.succ (PProd.fst x.fst a))
+        | a, Nat.succ b => fun x => Nat.succ (x.fst.fst a))
         f)
     x
 theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), HEq (cast h a) a :=
diff --git a/tests/lean/sorryAtError.lean.expected.out b/tests/lean/sorryAtError.lean.expected.out
index b71549c1c6..bae3916f4f 100644
--- a/tests/lean/sorryAtError.lean.expected.out
+++ b/tests/lean/sorryAtError.lean.expected.out
@@ -1,5 +1,5 @@
 sorryAtError.lean:13:46-13:47: error: application type mismatch
-  Ty.ty ty Γ
+  ty.ty Γ
 argument
   Γ
 has type