diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 44d67707ec..59a16ad02a 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -40,7 +40,7 @@ instance : ToString NamedArg where
   toString s := "(" ++ toString s.name ++ " := " ++ toString s.val ++ ")"
 
 def throwInvalidNamedArg {α} (namedArg : NamedArg) (fn? : Option Name) : TermElabM α :=
-  withRef namedArg.ref $ match fn? with
+  withRef namedArg.ref <| match fn? with
     | some fn => throwError "invalid argument name '{namedArg.name}' for function '{fn}'"
     | none    => throwError "invalid argument name '{namedArg.name}' for function"
 
@@ -50,7 +50,7 @@ def throwInvalidNamedArg {α} (namedArg : NamedArg) (fn? : Option Name) : TermEl
 def addNamedArg (namedArgs : Array NamedArg) (namedArg : NamedArg) : TermElabM (Array NamedArg) := do
   if namedArgs.any (namedArg.name == ·.name) then
     throwError "argument '{namedArg.name}' was already set"
-  pure $ namedArgs.push namedArg
+  return namedArgs.push namedArg
 
 private def ensureArgType (f : Expr) (arg : Expr) (expectedType : Expr) : TermElabM Expr := do
   let argType ← inferType arg
@@ -185,7 +185,7 @@ private def hasOptAutoParams (type : Expr) : M Bool := do
   forallTelescopeReducing type fun xs type =>
     xs.anyM fun x => do
       let xType ← inferType x
-      pure $ xType.getOptParamDefault?.isSome || xType.getAutoParamTactic?.isSome
+      return xType.getOptParamDefault?.isSome || xType.getAutoParamTactic?.isSome
 
 /- Return true if `fType` contains `OptParam` or `AutoParams` -/
 private def fTypeHasOptAutoParams : M Bool := do
@@ -539,11 +539,11 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     let fieldNames := getStructureFields env structName
     if h : idx - 1 < fieldNames.size then
       if isStructure env structName then
-        pure $ LValResolution.projFn structName structName (fieldNames.get ⟨idx - 1, h⟩)
+        return LValResolution.projFn structName structName (fieldNames.get ⟨idx - 1, h⟩)
       else
         /- `structName` was declared using `inductive` command.
            So, we don't projection functions for it. Thus, we use `Expr.proj` -/
-        pure $ LValResolution.projIdx structName (idx - 1)
+        return LValResolution.projIdx structName (idx - 1)
     else
       throwLValError e eType m!"invalid projection, structure has only {fieldNames.size} field(s)"
   | some structName, LVal.fieldName _ fieldName =>
@@ -776,7 +776,7 @@ private partial def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level)
       let s ← observing do
         let e ← elabAppLVals f (lvals' ++ lvals) namedArgs args expectedType? explicit ellipsis
         if overloaded then ensureHasType expectedType? e else pure e
-      pure $ acc.push s
+      return acc.push s
 
 
 private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Array NamedArg) (args : Array Arg)
@@ -819,16 +819,16 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
          arbitrary terms. If they are not being used as a function, we should elaborate using the expectedType. -/
       let s ←
         if overloaded then
-          observing $ elabTermEnsuringType f expectedType? catchPostpone
+          observing <| elabTermEnsuringType f expectedType? catchPostpone
         else
-          observing $ elabTerm f expectedType?
-      pure $ acc.push s
+          observing <| elabTerm f expectedType?
+      return acc.push s
     else
       let s ← observing do
         let f ← elabTerm f none catchPostpone
         let e ← elabAppLVals f lvals namedArgs args expectedType? explicit ellipsis
         if overloaded then ensureHasType expectedType? e else pure e
-      pure $ acc.push s
+      return acc.push s
 
 private def isSuccess (candidate : TermElabResult Expr) : Bool :=
   match candidate with
@@ -841,13 +841,13 @@ private def getSuccess (candidates : Array (TermElabResult Expr)) : Array (TermE
 private def toMessageData (ex : Exception) : TermElabM MessageData := do
   let pos ← getRefPos
   match ex.getRef.getPos? with
-  | none       => pure ex.toMessageData
+  | none       => return ex.toMessageData
   | some exPos =>
     if pos == exPos then
-      pure ex.toMessageData
+      return ex.toMessageData
     else
       let exPosition := (← getFileMap).toPosition exPos
-      pure m!"{exPosition.line}:{exPosition.column} {ex.toMessageData}"
+      return m!"{exPosition.line}:{exPosition.column} {ex.toMessageData}"
 
 private def toMessageList (msgs : Array MessageData) : MessageData :=
   indentD (MessageData.joinSep msgs.toList m!"\n\n")
@@ -866,8 +866,7 @@ private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array A
   else
     let successes := getSuccess candidates
     if successes.size == 1 then
-      let e ← applyResult successes[0]
-      pure e
+      applyResult successes[0]
     else if successes.size > 1 then
       let lctx ← getLCtx
       let opts ← getOptions
@@ -876,7 +875,7 @@ private def elabAppAux (f : Syntax) (namedArgs : Array NamedArg) (args : Array A
         | _                     => unreachable!
       throwErrorAt f "ambiguous, possible interpretations {toMessageList msgs}"
     else
-      withRef f $ mergeFailures candidates
+      withRef f <| mergeFailures candidates
 
 partial def expandApp (stx : Syntax) (pattern := false) : TermElabM (Syntax × Array NamedArg × Array Arg × Bool) := do
   let f    := stx[0]
@@ -894,12 +893,12 @@ partial def expandApp (stx : Syntax) (pattern := false) : TermElabM (Syntax × A
       let name := stx[1].getId.eraseMacroScopes
       let val  := stx[3]
       let namedArgs ← addNamedArg namedArgs { ref := stx, name := name, val := Arg.stx val }
-      pure (namedArgs, args)
+      return (namedArgs, args)
     else if stx.getKind == `Lean.Parser.Term.ellipsis then
       throwErrorAt stx "unexpected '..'"
     else
-      pure (namedArgs, args.push $ Arg.stx stx)
-  pure (f, namedArgs, args, ellipsis)
+      return (namedArgs, args.push $ Arg.stx stx)
+  return (f, namedArgs, args, ellipsis)
 
 @[builtinTermElab app] def elabApp : TermElab := fun stx expectedType? =>
   withoutPostponingUniverseConstraints do