From 12e2a791702934f17106410530fd5929137d20e0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 3 Feb 2022 18:08:14 -0800
Subject: [PATCH] chore: fix codebase after removing auto pure

---
 src/Init/Data/Array/Basic.lean                |   2 +-
 src/Init/Meta.lean                            |   2 +-
 src/Init/Notation.lean                        |   6 +-
 src/Init/Prelude.lean                         |   6 +-
 src/Init/System/IO.lean                       |  16 +-
 src/Lean/Attributes.lean                      |   2 +-
 src/Lean/Data/Json/Basic.lean                 |  18 +-
 src/Lean/Data/Json/FromToJson.lean            |   8 +-
 src/Lean/Data/Json/Parser.lean                |  70 +++----
 src/Lean/Data/JsonRpc.lean                    |  26 +--
 src/Lean/Data/Lsp/Diagnostics.lean            |  16 +-
 src/Lean/Data/Lsp/Extra.lean                  |   6 +-
 src/Lean/Data/Lsp/InitShutdown.lean           |   8 +-
 src/Lean/Data/Lsp/Internal.lean               |  12 +-
 src/Lean/Data/Lsp/Ipc.lean                    |   8 +-
 src/Lean/Data/Lsp/TextSync.lean               |   6 +-
 src/Lean/Data/Lsp/Workspace.lean              |   6 +-
 src/Lean/Data/Parsec.lean                     |  10 +-
 src/Lean/Data/Xml/Parser.lean                 | 194 +++++++++---------
 src/Lean/DocString.lean                       |   4 +-
 src/Lean/Elab/Binders.lean                    |   4 +-
 src/Lean/Elab/BuiltinCommand.lean             |   2 +-
 src/Lean/Elab/BuiltinNotation.lean            |   2 +-
 src/Lean/Elab/BuiltinTerm.lean                |   4 +-
 src/Lean/Elab/Command.lean                    |   2 +-
 src/Lean/Elab/Declaration.lean                |  22 +-
 src/Lean/Elab/Deriving/BEq.lean               |   6 +-
 src/Lean/Elab/Deriving/DecEq.lean             |   6 +-
 src/Lean/Elab/Deriving/FromToJson.lean        |  10 +-
 src/Lean/Elab/Deriving/Hashable.lean          |   6 +-
 src/Lean/Elab/Deriving/Inhabited.lean         |   2 +-
 src/Lean/Elab/Deriving/Ord.lean               |  10 +-
 src/Lean/Elab/Deriving/Repr.lean              |  10 +-
 src/Lean/Elab/Deriving/Util.lean              |   2 +-
 src/Lean/Elab/Do.lean                         |  59 +++---
 src/Lean/Elab/ElabRules.lean                  |   4 +-
 src/Lean/Elab/Extra.lean                      |   2 +-
 src/Lean/Elab/InfoTree.lean                   |   2 +-
 src/Lean/Elab/MacroArgUtil.lean               |  22 +-
 src/Lean/Elab/Match.lean                      |   8 +-
 src/Lean/Elab/MutualDef.lean                  |   2 +-
 src/Lean/Elab/Notation.lean                   |   6 +-
 src/Lean/Elab/PreDefinition/Basic.lean        |   2 +-
 src/Lean/Elab/PreDefinition/Eqns.lean         |  18 +-
 src/Lean/Elab/PreDefinition/Main.lean         |   2 +-
 .../PreDefinition/Structural/IndPred.lean     |   4 +-
 .../Structural/SmartUnfolding.lean            |   2 +-
 src/Lean/Elab/PreDefinition/WF/Eqns.lean      |   4 +-
 src/Lean/Elab/PreDefinition/WF/Fix.lean       |   8 +-
 src/Lean/Elab/PreDefinition/WF/Main.lean      |   2 +-
 src/Lean/Elab/Quotation.lean                  |  30 +--
 src/Lean/Elab/Quotation/Precheck.lean         |   4 +-
 src/Lean/Elab/Quotation/Util.lean             |   6 +-
 src/Lean/Elab/StructInst.lean                 |   2 +-
 src/Lean/Elab/Structure.lean                  |  14 +-
 src/Lean/Elab/Syntax.lean                     |   8 +-
 src/Lean/Elab/Tactic/Conv/Pattern.lean        |   2 +-
 src/Lean/Elab/Tactic/Induction.lean           |   6 +-
 src/Lean/Elab/Tactic/Simp.lean                |   2 +-
 src/Lean/Elab/Term.lean                       |   2 +-
 src/Lean/Elab/Util.lean                       |   6 +-
 src/Lean/Environment.lean                     |   4 +-
 src/Lean/Hygiene.lean                         |   4 +-
 src/Lean/KeyedDeclsAttribute.lean             |   2 +-
 src/Lean/LocalContext.lean                    |   2 +-
 src/Lean/Meta/ACLt.lean                       |  16 +-
 src/Lean/Meta/AbstractMVars.lean              |   2 +-
 src/Lean/Meta/Check.lean                      |   4 +-
 src/Lean/Meta/DiscrTree.lean                  |   6 +-
 src/Lean/Meta/ExprDefEq.lean                  |   6 +-
 src/Lean/Meta/IndPredBelow.lean               |  80 ++++----
 src/Lean/Meta/Injective.lean                  |   2 +-
 src/Lean/Meta/Instances.lean                  |   4 +-
 src/Lean/Meta/LevelDefEq.lean                 |   2 +-
 src/Lean/Meta/Match/Match.lean                |   9 +-
 src/Lean/Meta/Match/MatchEqs.lean             |   4 +-
 src/Lean/Meta/Offset.lean                     |   4 +-
 src/Lean/Meta/Reduce.lean                     |   4 +-
 src/Lean/Meta/SizeOf.lean                     |   2 +-
 src/Lean/Meta/SynthInstance.lean              |   8 +-
 src/Lean/Meta/Tactic/AuxLemma.lean            |   4 +-
 src/Lean/Meta/Tactic/Delta.lean               |   4 +-
 src/Lean/Meta/Tactic/Simp/Main.lean           |   6 +-
 src/Lean/Meta/Tactic/Simp/Rewrite.lean        |   4 +-
 src/Lean/Meta/Tactic/Simp/SimpAll.lean        |   2 +-
 src/Lean/Meta/Tactic/Simp/SimpLemmas.lean     |  12 +-
 src/Lean/Meta/WHNF.lean                       |  12 +-
 src/Lean/MonadEnv.lean                        |   2 +-
 src/Lean/Parser/Extension.lean                |   6 +-
 src/Lean/ParserCompiler.lean                  |   4 +-
 src/Lean/PrettyPrinter/Delaborator/Basic.lean |  27 +--
 .../PrettyPrinter/Delaborator/Builtins.lean   |  62 +++---
 .../PrettyPrinter/Delaborator/SubExpr.lean    |   6 +-
 .../Delaborator/TopDownAnalyze.lean           |  54 ++---
 src/Lean/PrettyPrinter/Formatter.lean         |   4 +-
 src/Lean/ReducibilityAttrs.lean               |   8 +-
 src/Lean/Server/AsyncList.lean                |   8 +-
 src/Lean/Server/Completion.lean               |  16 +-
 src/Lean/Server/FileWorker.lean               |  20 +-
 .../Server/FileWorker/RequestHandling.lean    |  10 +-
 .../Server/FileWorker/WidgetRequests.lean     |  12 +-
 src/Lean/Server/InfoUtils.lean                |   4 +-
 src/Lean/Server/References.lean               |   2 +-
 src/Lean/Server/Requests.lean                 |  12 +-
 src/Lean/Server/Rpc/Basic.lean                |   6 +-
 src/Lean/Server/Rpc/Deriving.lean             |   4 +-
 src/Lean/Server/Rpc/RequestHandling.lean      |   6 +-
 src/Lean/Server/Snapshots.lean                |   8 +-
 src/Lean/Server/Watchdog.lean                 |  22 +-
 src/Lean/Syntax.lean                          |   2 +-
 src/Lean/Util/Path.lean                       |  16 +-
 src/Lean/Widget/InteractiveCode.lean          |   8 +-
 src/Lean/Widget/InteractiveDiagnostic.lean    |  20 +-
 src/Lean/Widget/InteractiveGoal.lean          |   2 +-
 src/Lean/Widget/TaggedText.lean               |  10 +-
 src/Leanc.lean                                |   6 +-
 src/Leanpkg.lean                              |   2 +-
 src/Leanpkg/Build.lean                        |   2 +-
 src/Leanpkg/Git.lean                          |   6 +-
 src/Leanpkg/Manifest.lean                     |  10 +-
 src/Leanpkg/Resolve.lean                      |  10 +-
 src/Leanpkg/Toml.lean                         |   2 +-
 122 files changed, 674 insertions(+), 677 deletions(-)

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 779f194e7e..6b56e5ff22 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -540,7 +540,7 @@ def filter (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Ar
 @[inline]
 def filterM [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
   as.foldlM (init := #[]) (start := start) (stop := stop) fun r a => do
-    if (← p a) then r.push a else r
+    if (← p a) then return r.push a else return r
 
 @[specialize]
 def filterMapM [Monad m] (f : α → m (Option β)) (as : Array α) (start := 0) (stop := as.size) : m (Array β) :=
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 634302daf7..0c5259dbf4 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -779,7 +779,7 @@ instance : Quote Substring := ⟨fun s => Syntax.mkCApp `String.toSubstring #[qu
 
 -- in contrast to `Name.toString`, we can, and want to be, precise here
 private def getEscapedNameParts? (acc : List String) : Name → OptionM (List String)
-  | Name.anonymous => acc
+  | Name.anonymous => return acc
   | Name.str n s _ => do
     let s ← Name.escapePart s
     getEscapedNameParts? (s::acc) n
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index fd101e139d..13a8f71265 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -23,7 +23,7 @@ end Lean.Parser.Syntax
 macro "max"  : prec => `(1024) -- maximum precedence used in term parsers, in particular for terms in function position (`ident`, `paren`, ...)
 macro "arg"  : prec => `(1023) -- precedence used for application arguments (`do`, `by`, ...)
 macro "lead" : prec => `(1022) -- precedence used for terms not supposed to be used as arguments (`let`, `have`, ...)
-macro "(" p:prec ")" : prec => p
+macro "(" p:prec ")" : prec => return p
 macro "min"  : prec => `(10)   -- minimum precedence used in term parsers
 macro "min1" : prec => `(11)   -- `(min+1) we can only `min+1` after `Meta.lean`
 /-
@@ -35,7 +35,7 @@ macro "default" : prio => `(1000)
 macro "low"     : prio => `(100)
 macro "mid"     : prio => `(1000)
 macro "high"    : prio => `(10000)
-macro "(" p:prio ")" : prio => p
+macro "(" p:prio ")" : prio => return p
 
 -- Basic notation for defining parsers
 -- NOTE: precedence must be at least `arg` to be used in `macro` without parentheses
@@ -208,7 +208,7 @@ notation:50 e:51 " matches " p:51 => ((match e with | p => true | _ => false) :
 -- Declare `this` as a keyword that unhygienically binds to a scope-less `this` assumption (or other binding).
 -- The keyword prevents declaring a `this` binding except through metapgrogramming, as is done by `have`/`show`.
 /-- Special identifier introduced by "anonymous" `have : ...`, `suffices p ...` etc. -/
-macro tk:"this" : term => Syntax.ident tk.getHeadInfo "this".toSubstring `this []
+macro tk:"this" : term => return Syntax.ident tk.getHeadInfo "this".toSubstring `this []
 
 namespace Parser.Tactic
 /--
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index a84a27ca96..24595e9b8e 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1308,7 +1308,7 @@ def Array.sequenceMap {α : Type u} {β : Type v} {m : Type v → Type w} [Monad
         match i with
         | 0           => pure bs
         | Nat.succ i' => Bind.bind (f (as.get ⟨j, hlt⟩)) fun b => loop i' (hAdd j 1) (bs.push b))
-      (fun _ => bs)
+      (fun _ => pure bs)
   loop as.size 0 Array.empty
 
 /-- A Function for lifting a computation from an inner Monad to an outer Monad.
@@ -2032,8 +2032,8 @@ class MonadQuotation (m : Type → Type) extends MonadRef m where
 
 export MonadQuotation (getCurrMacroScope getMainModule withFreshMacroScope)
 
-def MonadRef.mkInfoFromRefPos [Monad m] [MonadRef m] : m SourceInfo := do
-  SourceInfo.fromRef (← getRef)
+def MonadRef.mkInfoFromRefPos [Monad m] [MonadRef m] : m SourceInfo :=
+  return SourceInfo.fromRef (← getRef)
 
 instance {m n : Type → Type} [MonadFunctor m n] [MonadLift m n] [MonadQuotation m] : MonadQuotation n where
   getCurrMacroScope   := liftM (m := m) getCurrMacroScope
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index 8651685a0e..582ec001c7 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -144,7 +144,7 @@ namespace EIO
 
 /-- `EIO` specialization of `BaseIO.bindTask`. -/
 @[inline] def bindTask (t : Task α) (f : α → EIO ε (Task (Except ε β))) (prio := Task.Priority.default) : BaseIO (Task (Except ε β)) :=
-  BaseIO.bindTask t (fun a => f a |>.catchExceptions fun e => Task.pure <| Except.error e) prio
+  BaseIO.bindTask t (fun a => f a |>.catchExceptions fun e => return Task.pure <| Except.error e) prio
 
 /-- `EIO` specialization of `BaseIO.mapTasks`. -/
 @[inline] def mapTasks (f : List α → EIO ε β) (tasks : List (Task α)) (prio := Task.Priority.default) : BaseIO (Task (Except ε β)) :=
@@ -200,7 +200,7 @@ def sleep (ms : UInt32) : IO Unit :=
 
 /-- Wait for the task to finish, then return its result. -/
 @[extern "lean_io_wait"] constant wait (t : Task α) : BaseIO α :=
-  t.get
+  return t.get
 
 /-- Wait until any of the tasks in the given list has finished, then return its result. -/
 @[extern "lean_io_wait_any"] constant waitAny : @& List (Task α) → IO α
@@ -395,16 +395,16 @@ constant metadata : @& FilePath → IO IO.FS.Metadata
 
 def isDir (p : FilePath) : BaseIO Bool := do
   match (← p.metadata.toBaseIO) with
-  | Except.ok m => m.type == IO.FS.FileType.dir
-  | Except.error _ => false
+  | Except.ok m => return m.type == IO.FS.FileType.dir
+  | Except.error _ => return false
 
-def pathExists (p : FilePath) : BaseIO Bool := do
-  (← p.metadata.toBaseIO).toBool
+def pathExists (p : FilePath) : BaseIO Bool :=
+  return (← p.metadata.toBaseIO).toBool
 
 /--
   Return all filesystem entries of a preorder traversal of all directories satisfying `enter`, starting at `p`.
   Symbolic links are visited as well by default. -/
-partial def walkDir (p : FilePath) (enter : FilePath → IO Bool := fun _ => true) : IO (Array FilePath) :=
+partial def walkDir (p : FilePath) (enter : FilePath → IO Bool := fun _ => pure true) : IO (Array FilePath) :=
   Prod.snd <$> StateT.run (go p) #[]
 where
   go p := do
@@ -421,7 +421,7 @@ where
           if (← enter p) then
             go p'
       | FS.FileType.dir => go d.path
-      | _ => ()
+      | _ => return ()
 
 end System.FilePath
 
diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index d44c2f0cd2..3d88eb4e1a 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -418,7 +418,7 @@ def Attribute.erase (declName : Name) (attrName : Name) : AttrM Unit := do
 @[export lean_update_env_attributes]
 def updateEnvAttributesImpl (env : Environment) : IO Environment := do
   let map ← attributeMapRef.get
-  let s ← attributeExtension.getState env
+  let s := attributeExtension.getState env
   let s := map.foldl (init := s) fun s attrName attrImpl =>
     if s.map.contains attrName then
       s
diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean
index 203258ce2b..ee0ed8d924 100644
--- a/src/Lean/Data/Json/Basic.lean
+++ b/src/Lean/Data/Json/Basic.lean
@@ -183,44 +183,44 @@ def isNull : Json -> Bool
   | _    => false
 
 def getObj? : Json → Except String (RBNode String (fun _ => Json))
-  | obj kvs => kvs
+  | obj kvs => return kvs
   | _       => throw "object expected"
 
 def getArr? : Json → Except String (Array Json)
-  | arr a => a
+  | arr a => return a
   | _     => throw "array expected"
 
 def getStr? : Json → Except String String
-  | str s => s
+  | str s => return s
   | _     => throw "String expected"
 
 def getNat? : Json → Except String Nat
-  | (n : Nat) => n
+  | (n : Nat) => return n
   | _         => throw "Natural number expected"
 
 def getInt? : Json → Except String Int
-  | (i : Int) => i
+  | (i : Int) => return i
   | _         => throw "Integer expected"
 
 def getBool? : Json → Except String Bool
-  | (b : Bool) => b
+  | (b : Bool) => return b
   | _          => throw "Bool expected"
 
 def getNum? : Json → Except String JsonNumber
-  | num n => n
+  | num n => return n
   | _     => throw "number expected"
 
 def getObjVal? : Json → String → Except String Json
   | obj kvs, k =>
     match kvs.find compare k with
-    | some v => v
+    | some v => return v
     | none => throw s!"property not found: {k}"
   | _      , _ => throw "object expected"
 
 def getArrVal? : Json → Nat → Except String Json
   | arr a, i =>
     match a.get? i with
-    | some v => v
+    | some v => return v
     | none => throw s!"index out of bounds: {i}"
   | _    , _ => throw "array expected"
 
diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean
index 58dd8811dc..accf79ebfa 100644
--- a/src/Lean/Data/Json/FromToJson.lean
+++ b/src/Lean/Data/Json/FromToJson.lean
@@ -81,7 +81,7 @@ instance : FromJson Name where
     if s == "[anonymous]" then
       return Name.anonymous
     else
-      let some n ← Syntax.decodeNameLit ("`" ++ s)
+      let some n := Syntax.decodeNameLit ("`" ++ s)
         | throw s!"expected a `Name`, got '{j}'"
       return n
 
@@ -92,7 +92,7 @@ instance : ToJson Name where
 cannot represent 64-bit numbers. -/
 def bignumFromJson? (j : Json) : Except String Nat := do
   let s ← j.getStr?
-  let some v ← Syntax.decodeNatLitVal? s -- TODO maybe this should be in Std
+  let some v := Syntax.decodeNatLitVal? s -- TODO maybe this should be in Std
     | throw s!"expected a string-encoded number, got '{j}'"
   return v
 
@@ -122,8 +122,8 @@ instance : ToJson UInt64 where
 namespace Json
 
 instance : FromJson Structured := ⟨fun
-  | arr a => Structured.arr a
-  | obj o => Structured.obj o
+  | arr a => return Structured.arr a
+  | obj o => return Structured.obj o
   | j     => throw s!"expected structured object, got '{j}'"⟩
 
 instance : ToJson Structured := ⟨fun
diff --git a/src/Lean/Data/Json/Parser.lean b/src/Lean/Data/Json/Parser.lean
index 1255653ae6..c68944c2f3 100644
--- a/src/Lean/Data/Json/Parser.lean
+++ b/src/Lean/Data/Json/Parser.lean
@@ -30,24 +30,24 @@ def hexChar : Parsec Nat := do
 def escapedChar : Parsec Char := do
   let c ← anyChar
   match c with
-  | '\\' => '\\'
-  | '"'  => '"'
-  | '/'  => '/'
-  | 'b'  => '\x08'
-  | 'f'  => '\x0c'
-  | 'n'  => '\n'
-  | 'r'  => '\x0d'
-  | 't'  => '\t'
+  | '\\' => return '\\'
+  | '"'  => return '"'
+  | '/'  => return '/'
+  | 'b'  => return '\x08'
+  | 'f'  => return '\x0c'
+  | 'n'  => return '\n'
+  | 'r'  => return '\x0d'
+  | 't'  => return '\t'
   | 'u'  =>
     let u1 ← hexChar; let u2 ← hexChar; let u3 ← hexChar; let u4 ← hexChar
-    Char.ofNat $ 4096*u1 + 256*u2 + 16*u3 + u4
+    return Char.ofNat $ 4096*u1 + 256*u2 + 16*u3 + u4
   | _ => fail "illegal \\u escape"
 
 partial def strCore (acc : String) : Parsec String := do
   let c ← peek!
   if c = '"' then -- "
     skip
-    acc
+    return acc
   else
     let c ← anyChar
     let ec ←
@@ -57,7 +57,7 @@ partial def strCore (acc : String) : Parsec String := do
       -- the JSON standard is not definite: both directly printing the character
       -- and encoding it with multiple \u is allowed. we choose the former.
       else if 0x0020 ≤ c.val ∧ c.val ≤ 0x10ffff then
-        c
+        pure c
       else
         fail "unexpected character in string"
     strCore (acc.push ec)
@@ -65,27 +65,27 @@ partial def strCore (acc : String) : Parsec String := do
 def str : Parsec String := strCore ""
 
 partial def natCore (acc digits : Nat) : Parsec (Nat × Nat) := do
-  let some c ← peek? | (acc, digits)
+  let some c ← peek? | return (acc, digits)
   if '0' ≤ c ∧ c ≤ '9' then
     skip
     let acc' := 10*acc + (c.val.toNat - '0'.val.toNat)
     natCore acc' (digits+1)
   else
-    (acc, digits)
+    return (acc, digits)
 
 @[inline]
 def lookahead (p : Char → Prop) (desc : String) [DecidablePred p] : Parsec Unit := do
   let c ← peek!
   if p c then
-    ()
+    return ()
   else
-    fail $ "expected " ++ desc
+    fail <| "expected " ++ desc
 
 @[inline]
 def natNonZero : Parsec Nat := do
   lookahead (fun c => '1' ≤ c ∧ c ≤ '9') "1-9"
   let (n, _) ← natCore 0 0
-  n
+  return n
 
 @[inline]
 def natNumDigits : Parsec (Nat × Nat) := do
@@ -95,7 +95,7 @@ def natNumDigits : Parsec (Nat × Nat) := do
 @[inline]
 def natMaybeZero : Parsec Nat := do
   let (n, _) ← natNumDigits
-  n
+  return n
 
 def num : Parsec JsonNumber := do
   let c ← peek!
@@ -120,9 +120,9 @@ def num : Parsec JsonNumber := do
       if d > USize.size then fail "too many decimals"
       let mantissa' := sign * (res * (10^d : Nat) + n)
       let exponent' := d
-      JsonNumber.mk mantissa' exponent'
+      pure <| JsonNumber.mk mantissa' exponent'
     else
-      JsonNumber.fromInt (sign * res)
+      pure <| JsonNumber.fromInt (sign * res)
   let c? ← peek?
   if c? = some 'e' ∨ c? = some 'E' then
     skip
@@ -130,14 +130,14 @@ def num : Parsec JsonNumber := do
     if c = '-' then
       skip
       let n ← natMaybeZero
-      res.shiftr n
+      return res.shiftr n
     else
       if c = '+' then skip
       let n ← natMaybeZero
       if n > USize.size then fail "exp too large"
-      res.shiftl n
+      return res.shiftl n
   else
-    res
+    return res
 
 partial def arrayCore (anyCore : Unit → Parsec Json) (acc : Array Json) : Parsec (Array Json) := do
   let hd ← anyCore ()
@@ -145,7 +145,7 @@ partial def arrayCore (anyCore : Unit → Parsec Json) (acc : Array Json) : Pars
   let c ← anyChar
   if c = ']' then
     ws
-    acc'
+    return acc'
   else if c = ',' then
     ws
     arrayCore anyCore acc'
@@ -160,11 +160,11 @@ partial def objectCore (anyCore : Unit → Parsec Json) : Parsec (RBNode String
   let c ← anyChar
   if c = '}' then
     ws
-    RBNode.singleton k v
+    return RBNode.singleton k v
   else if c = ',' then
     ws
     let kvs ← objectCore anyCore
-    kvs.insert compare k v
+    return kvs.insert compare k v
   else
     fail "unexpected character in object"
 
@@ -177,37 +177,37 @@ partial def anyCore (u : Unit) : Parsec Json := do
     let c ← peek!
     if c = ']' then
       skip; ws
-      Json.arr (Array.mkEmpty 0)
+      return Json.arr (Array.mkEmpty 0)
     else
       let a ← arrayCore anyCore (Array.mkEmpty 4)
-      Json.arr a
+      return Json.arr a
   else if c = '{' then
     skip; ws
     let c ← peek!
     if c = '}' then
       skip; ws
-      Json.obj (RBNode.leaf)
+      return Json.obj (RBNode.leaf)
     else
       let kvs ← objectCore anyCore
-      Json.obj kvs
+      return Json.obj kvs
   else if c = '\"' then
     skip
     let s ← strCore ""
     ws
-    Json.str s
+    return Json.str s
   else if c = 'f' then
     skipString "false"; ws
-    Json.bool false
+    return Json.bool false
   else if c = 't' then
     skipString "true"; ws
-    Json.bool true
+    return Json.bool true
   else if c = 'n' then
     skipString "null"; ws
-    Json.null
+    return Json.null
   else if c = '-' ∨ ('0' ≤ c ∧ c ≤ '9') then
     let n ← num
     ws
-    Json.num n
+    return Json.num n
   else
     fail "unexpected input"
 
@@ -216,7 +216,7 @@ def any : Parsec Json := do
   ws
   let res ← anyCore ()
   eof
-  res
+  return res
 
 end Json.Parser
 
diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean
index fc0c476275..3c26188457 100644
--- a/src/Lean/Data/JsonRpc.lean
+++ b/src/Lean/Data/JsonRpc.lean
@@ -48,16 +48,16 @@ inductive ErrorCode where
   deriving Inhabited, BEq
 
 instance : FromJson ErrorCode := ⟨fun
-  | num (-32700 : Int) => ErrorCode.parseError
-  | num (-32600 : Int) => ErrorCode.invalidRequest
-  | num (-32601 : Int) => ErrorCode.methodNotFound
-  | num (-32602 : Int) => ErrorCode.invalidParams
-  | num (-32603 : Int) => ErrorCode.internalError
-  | num (-32002 : Int) => ErrorCode.serverNotInitialized
-  | num (-32001 : Int) => ErrorCode.unknownErrorCode
-  | num (-32801 : Int) => ErrorCode.contentModified
-  | num (-32800 : Int) => ErrorCode.requestCancelled
-  | num (-32900 : Int) => ErrorCode.rpcNeedsReconnect
+  | num (-32700 : Int) => return ErrorCode.parseError
+  | num (-32600 : Int) => return ErrorCode.invalidRequest
+  | num (-32601 : Int) => return ErrorCode.methodNotFound
+  | num (-32602 : Int) => return ErrorCode.invalidParams
+  | num (-32603 : Int) => return ErrorCode.internalError
+  | num (-32002 : Int) => return ErrorCode.serverNotInitialized
+  | num (-32001 : Int) => return ErrorCode.unknownErrorCode
+  | num (-32801 : Int) => return ErrorCode.contentModified
+  | num (-32800 : Int) => return ErrorCode.requestCancelled
+  | num (-32900 : Int) => return ErrorCode.rpcNeedsReconnect
   | _  => throw "expected error code"⟩
 
 instance : ToJson ErrorCode := ⟨fun
@@ -141,8 +141,8 @@ instance (a b : RequestID) : Decidable (a < b) :=
 
 instance : FromJson RequestID := ⟨fun j =>
   match j with
-  | str s => RequestID.str s
-  | num n => RequestID.num n
+  | str s => return RequestID.str s
+  | num n => return RequestID.num n
   | _     => throw "a request id needs to be a number or a string"⟩
 
 instance : ToJson RequestID := ⟨fun rid =>
@@ -196,7 +196,7 @@ instance [FromJson α] : FromJson (Notification α) where
   fromJson? j := do
     let msg : Message ← fromJson? j
     if let Message.notification method params? := msg then
-      let params ← params?
+      let params := params?
       let param : α ← fromJson? (toJson params)
       pure $ ⟨method, param⟩
     else throw "not a notfication"
diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean
index 2f84efe0f1..5752e96b75 100644
--- a/src/Lean/Data/Lsp/Diagnostics.lean
+++ b/src/Lean/Data/Lsp/Diagnostics.lean
@@ -24,10 +24,10 @@ inductive DiagnosticSeverity where
 
 instance : FromJson DiagnosticSeverity := ⟨fun j =>
   match j.getNat? with
-  | Except.ok 1 => DiagnosticSeverity.error
-  | Except.ok 2 => DiagnosticSeverity.warning
-  | Except.ok 3 => DiagnosticSeverity.information
-  | Except.ok 4 => DiagnosticSeverity.hint
+  | Except.ok 1 => return DiagnosticSeverity.error
+  | Except.ok 2 => return DiagnosticSeverity.warning
+  | Except.ok 3 => return DiagnosticSeverity.information
+  | Except.ok 4 => return DiagnosticSeverity.hint
   | _           => throw s!"unknown DiagnosticSeverity '{j}'"⟩
 
 instance : ToJson DiagnosticSeverity := ⟨fun
@@ -42,8 +42,8 @@ inductive DiagnosticCode where
   deriving Inhabited, BEq
 
 instance : FromJson DiagnosticCode := ⟨fun
-  | num (i : Int) => DiagnosticCode.int i
-  | str s         => DiagnosticCode.string s
+  | num (i : Int) => return DiagnosticCode.int i
+  | str s         => return DiagnosticCode.string s
   | j             => throw s!"expected string or integer diagnostic code, got '{j}'"⟩
 
 instance : ToJson DiagnosticCode := ⟨fun
@@ -57,8 +57,8 @@ inductive DiagnosticTag where
 
 instance : FromJson DiagnosticTag := ⟨fun j =>
   match j.getNat? with
-  | Except.ok 1 => DiagnosticTag.unnecessary
-  | Except.ok 2 => DiagnosticTag.deprecated
+  | Except.ok 1 => return DiagnosticTag.unnecessary
+  | Except.ok 2 => return DiagnosticTag.deprecated
   | _      => throw "unknown DiagnosticTag"⟩
 
 instance : ToJson DiagnosticTag := ⟨fun
diff --git a/src/Lean/Data/Lsp/Extra.lean b/src/Lean/Data/Lsp/Extra.lean
index 9d496c5ba7..9684dc52fc 100644
--- a/src/Lean/Data/Lsp/Extra.lean
+++ b/src/Lean/Data/Lsp/Extra.lean
@@ -30,7 +30,7 @@ structure WaitForDiagnosticsParams where
 structure WaitForDiagnostics
 
 instance : FromJson WaitForDiagnostics :=
-  ⟨fun j => WaitForDiagnostics.mk⟩
+  ⟨fun j => pure WaitForDiagnostics.mk⟩
 
 instance : ToJson WaitForDiagnostics :=
   ⟨fun o => mkObj []⟩
@@ -41,8 +41,8 @@ inductive LeanFileProgressKind
 
 instance : FromJson LeanFileProgressKind := ⟨fun j =>
   match j.getNat? with
-  | Except.ok 1 => LeanFileProgressKind.processing
-  | Except.ok 2 => LeanFileProgressKind.fatalError
+  | Except.ok 1 => return LeanFileProgressKind.processing
+  | Except.ok 2 => return LeanFileProgressKind.fatalError
   | _           => throw s!"unknown LeanFileProgressKind '{j}'"⟩
 
 instance : ToJson LeanFileProgressKind := ⟨fun
diff --git a/src/Lean/Data/Lsp/InitShutdown.lean b/src/Lean/Data/Lsp/InitShutdown.lean
index 04dd474c6e..eff005e2a3 100644
--- a/src/Lean/Data/Lsp/InitShutdown.lean
+++ b/src/Lean/Data/Lsp/InitShutdown.lean
@@ -28,9 +28,9 @@ inductive Trace where
 
 instance : FromJson Trace := ⟨fun j =>
   match j.getStr? with
-  | Except.ok "off"      => Trace.off
-  | Except.ok "messages" => Trace.messages
-  | Except.ok "verbose"  => Trace.verbose
+  | Except.ok "off"      => return Trace.off
+  | Except.ok "messages" => return Trace.messages
+  | Except.ok "verbose"  => return Trace.verbose
   | _               => throw "uknown trace"⟩
 
 instance Trace.hasToJson : ToJson Trace :=
@@ -92,7 +92,7 @@ inductive InitializedParams where
   | mk
 
 instance : FromJson InitializedParams :=
-  ⟨fun _ => InitializedParams.mk⟩
+  ⟨fun _ => pure InitializedParams.mk⟩
 
 instance : ToJson InitializedParams :=
   ⟨fun _ => Json.null⟩
diff --git a/src/Lean/Data/Lsp/Internal.lean b/src/Lean/Data/Lsp/Internal.lean
index 8e9bc8a481..a69a2cc686 100644
--- a/src/Lean/Data/Lsp/Internal.lean
+++ b/src/Lean/Data/Lsp/Internal.lean
@@ -34,13 +34,13 @@ def fromString (s : String) : Except String RefIdent := do
   let sName := s.drop 2
   -- See `FromJson Name`
   let name ← match sName with
-    | "[anonymous]" => Name.anonymous
+    | "[anonymous]" => pure Name.anonymous
     | _ => match Syntax.decodeNameLit ("`" ++ sName) with
-      | some n => n
+      | some n => pure n
       | none => throw s!"expected a Name, got {sName}"
   match sPrefix with
-    | "c:" => RefIdent.const name
-    | "f:" => RefIdent.fvar <| FVarId.mk name
+    | "c:" => return RefIdent.const name
+    | "f:" => return RefIdent.fvar <| FVarId.mk name
     | _ => throw "string must start with 'c:' or 'f:'"
 
 end RefIdent
@@ -80,8 +80,8 @@ instance : ToJson ModuleRefs where
 instance : FromJson ModuleRefs where
   fromJson? j := do
     let node ← j.getObj?
-    node.foldM (init := HashMap.empty) fun m k v => do
-      m.insert (← RefIdent.fromString k) (← fromJson? v)
+    node.foldM (init := HashMap.empty) fun m k v =>
+      return m.insert (← RefIdent.fromString k) (← fromJson? v)
 
 /-- `$/lean/ileanInfoUpdate` and `$/lean/ileanInfoFinal` watchdog<-worker notifications.
 
diff --git a/src/Lean/Data/Lsp/Ipc.lean b/src/Lean/Data/Lsp/Ipc.lean
index 21c880591f..334e451bca 100644
--- a/src/Lean/Data/Lsp/Ipc.lean
+++ b/src/Lean/Data/Lsp/Ipc.lean
@@ -28,10 +28,10 @@ abbrev IpcM := ReaderT (Process.Child ipcStdioConfig) IO
 variable [ToJson α]
 
 def stdin : IpcM FS.Stream := do
-  FS.Stream.ofHandle (←read).stdin
+  return FS.Stream.ofHandle (←read).stdin
 
 def stdout : IpcM FS.Stream := do
-  FS.Stream.ofHandle (←read).stdout
+  return FS.Stream.ofHandle (←read).stdout
 
 def writeRequest (r : Request α) : IpcM Unit := do
   (←stdin).writeLspRequest r
@@ -59,7 +59,7 @@ partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target :
   let rec loop : IpcM (List (Notification PublishDiagnosticsParams)) := do
     match (←readMessage) with
     | Message.response id _ =>
-      if id == waitForDiagnosticsId then []
+      if id == waitForDiagnosticsId then return []
       else loop
     | Message.responseError id code msg _ =>
       if id == waitForDiagnosticsId then
@@ -67,7 +67,7 @@ partial def collectDiagnostics (waitForDiagnosticsId : RequestID := 0) (target :
       else loop
     | Message.notification "textDocument/publishDiagnostics" (some param) =>
       match fromJson? (toJson param) with
-      | Except.ok diagnosticParam => ⟨"textDocument/publishDiagnostics", diagnosticParam⟩ :: (←loop)
+      | Except.ok diagnosticParam => return ⟨"textDocument/publishDiagnostics", diagnosticParam⟩ :: (←loop)
       | Except.error inner => throw $ userError s!"Cannot decode publishDiagnostics parameters\n{inner}"
     | _ => loop
   loop
diff --git a/src/Lean/Data/Lsp/TextSync.lean b/src/Lean/Data/Lsp/TextSync.lean
index eec6d0da90..99d61ead33 100644
--- a/src/Lean/Data/Lsp/TextSync.lean
+++ b/src/Lean/Data/Lsp/TextSync.lean
@@ -21,9 +21,9 @@ inductive TextDocumentSyncKind where
 
 instance : FromJson TextDocumentSyncKind := ⟨fun j =>
   match j.getNat? with
-  | Except.ok 0 => TextDocumentSyncKind.none
-  | Except.ok 1 => TextDocumentSyncKind.full
-  | Except.ok 2 => TextDocumentSyncKind.incremental
+  | Except.ok 0 => return TextDocumentSyncKind.none
+  | Except.ok 1 => return TextDocumentSyncKind.full
+  | Except.ok 2 => return TextDocumentSyncKind.incremental
   | _      => throw "unknown TextDocumentSyncKind"⟩
 
 instance : ToJson TextDocumentSyncKind := ⟨fun
diff --git a/src/Lean/Data/Lsp/Workspace.lean b/src/Lean/Data/Lsp/Workspace.lean
index 237c26602a..3ec4f3f1ed 100644
--- a/src/Lean/Data/Lsp/Workspace.lean
+++ b/src/Lean/Data/Lsp/Workspace.lean
@@ -48,9 +48,9 @@ inductive FileChangeType
 instance : FromJson FileChangeType where
   fromJson? j := do
     match (← fromJson? j : Nat) with
-      | 1 => FileChangeType.Created
-      | 2 => FileChangeType.Changed
-      | 3 => FileChangeType.Deleted
+      | 1 => return FileChangeType.Created
+      | 2 => return FileChangeType.Changed
+      | 3 => return FileChangeType.Deleted
       | _ => throw s!"expected 1, 2, or 3, got {j}"
 
 instance : ToJson FileChangeType where
diff --git a/src/Lean/Data/Parsec.lean b/src/Lean/Data/Parsec.lean
index 8a05482f97..2cfa540abd 100644
--- a/src/Lean/Data/Parsec.lean
+++ b/src/Lean/Data/Parsec.lean
@@ -112,24 +112,24 @@ def skipChar (c : Char) : Parsec Unit := pchar c *> pure ()
 @[inline]
 def digit : Parsec Char := attempt do
   let c ← anyChar
-  if '0' ≤ c ∧ c ≤ '9' then c else fail s!"digit expected"
+  if '0' ≤ c ∧ c ≤ '9' then return c else fail s!"digit expected"
 
 @[inline]
 def hexDigit : Parsec Char := attempt do
   let c ← anyChar
   if ('0' ≤ c ∧ c ≤ '9')
    ∨ ('a' ≤ c ∧ c ≤ 'a')
-   ∨ ('A' ≤ c ∧ c ≤ 'A') then c else fail s!"hex digit expected"
+   ∨ ('A' ≤ c ∧ c ≤ 'A') then return c else fail s!"hex digit expected"
 
 @[inline]
 def asciiLetter : Parsec Char := attempt do
   let c ← anyChar
-  if ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') then c else fail s!"ASCII letter expected"
+  if ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') then return c else fail s!"ASCII letter expected"
 
 @[inline]
 def satisfy (p : Char → Bool) : Parsec Char := attempt do
   let c ← anyChar
-  if p c then c else fail "condition not satisfied"
+  if p c then return c else fail "condition not satisfied"
 
 @[inline]
 def notFollowedBy (p : Parsec α) : Parsec Unit := λ it =>
@@ -157,7 +157,7 @@ def peek? : Parsec (Option Char) := fun it =>
 @[inline]
 def peek! : Parsec Char := do
   let some c ← peek? | fail unexpectedEndOfInput
-  c
+  return c
 
 @[inline]
 def skip : Parsec Unit := fun it =>
diff --git a/src/Lean/Data/Xml/Parser.lean b/src/Lean/Data/Xml/Parser.lean
index 25138df817..c213360861 100644
--- a/src/Lean/Data/Xml/Parser.lean
+++ b/src/Lean/Data/Xml/Parser.lean
@@ -23,28 +23,28 @@ abbrev LeanChar := Char
   https://www.w3.org/TR/xml/#sec-line-ends -/
 def endl : Parsec LeanChar := (skipString "\r\n" <|> skipChar '\r' <|> skipChar '\n') *> pure '\n'
 
-def quote (p : Parsec α) : Parsec α := 
+def quote (p : Parsec α) : Parsec α :=
   skipChar '\'' *> p <* skipChar '\''
   <|> skipChar '"' *> p <* skipChar '"'
 
 /-- https://www.w3.org/TR/xml/#NT-Char -/
-def Char : Parsec LeanChar := 
+def Char : Parsec LeanChar :=
   (attempt do
   let c ← anyChar
-  let cNat ← c.toNat
-  if (0x20 ≤ cNat ∧ cNat ≤ 0xD7FF) 
-   ∨ (0xE000 ≤ cNat ∧ cNat ≤ 0xFFFD) 
-   ∨ (0x10000 ≤ cNat ∧ cNat ≤ 0x10FFFF) then c else fail "expected xml char")
+  let cNat := c.toNat
+  if (0x20 ≤ cNat ∧ cNat ≤ 0xD7FF)
+   ∨ (0xE000 ≤ cNat ∧ cNat ≤ 0xFFFD)
+   ∨ (0x10000 ≤ cNat ∧ cNat ≤ 0x10FFFF) then pure c else fail "expected xml char")
   <|> pchar '\t' <|> endl
 
 /-- https://www.w3.org/TR/xml/#NT-S -/
-def S : Parsec String := 
+def S : Parsec String :=
   many1Chars (pchar ' ' <|> endl <|> pchar '\t')
-  
+
 /-- https://www.w3.org/TR/xml/#NT-Eq -/
 def Eq : Parsec Unit :=
   optional S *> skipChar '=' <* optional S
-  
+
 private def nameStartCharRanges : Array (Nat × Nat) :=
   #[(0xC0, 0xD6),
     (0xD8, 0xF6),
@@ -62,32 +62,32 @@ private def nameStartCharRanges : Array (Nat × Nat) :=
 /-- https://www.w3.org/TR/xml/#NT-NameStartChar -/
 def NameStartChar : Parsec LeanChar := attempt do
   let c ← anyChar
-  if ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') then c
-  else if c = ':' ∨ c = '_' then c
+  if ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') then pure c
+  else if c = ':' ∨ c = '_' then pure c
   else
     let cNum := c.toNat
-    if nameStartCharRanges.any (fun (lo, hi) => lo ≤ cNum ∧ cNum ≤ hi) then c
+    if nameStartCharRanges.any (fun (lo, hi) => lo ≤ cNum ∧ cNum ≤ hi) then pure c
     else fail "expected a name character"
-    
+
 /-- https://www.w3.org/TR/xml/#NT-NameChar -/
 def NameChar : Parsec LeanChar :=
-  NameStartChar <|> digit <|> pchar '-' <|> pchar '.' <|> pchar '\xB7' 
+  NameStartChar <|> digit <|> pchar '-' <|> pchar '.' <|> pchar '\xB7'
   <|> satisfy (λ c => ('\u0300' ≤ c ∧ c ≤ '\u036F') ∨ ('\u203F' ≤ c ∧ c ≤ '\u2040'))
-    
+
 /-- https://www.w3.org/TR/xml/#NT-Name -/
 def Name : Parsec String := do
   let x ← NameStartChar
   manyCharsCore NameChar x.toString
-  
+
 /-- https://www.w3.org/TR/xml/#NT-VersionNum -/
-def VersionNum : Parsec Unit := 
+def VersionNum : Parsec Unit :=
   skipString "1." <* (many1 digit)
 
 /-- https://www.w3.org/TR/xml/#NT-VersionInfo -/
 def VersionInfo : Parsec Unit := do
-  S *> 
-  skipString "version" 
-  Eq 
+  S *>
+  skipString "version"
+  Eq
   quote VersionNum
 
 /-- https://www.w3.org/TR/xml/#NT-EncName -/
@@ -116,56 +116,56 @@ def XMLdecl : Parsec Unit := do
   skipString "?>"
 
 /-- https://www.w3.org/TR/xml/#NT-Comment -/
-def Comment : Parsec String := 
+def Comment : Parsec String :=
   let notDash := Char.toString <$> satisfy (λ c => c ≠ '-')
   skipString "<!--" *>
-  Array.foldl String.append "" <$> many (notDash <|> (do 
-    let d ← pchar '-' 
+  Array.foldl String.append "" <$> many (notDash <|> (do
+    let d ← pchar '-'
     let c ← notDash
-    pure $ d.toString ++ c)) 
+    pure $ d.toString ++ c))
   <* skipString "-->"
 
 /-- https://www.w3.org/TR/xml/#NT-PITarget -/
-def PITarget : Parsec String := 
+def PITarget : Parsec String :=
   Name <* (skipChar 'X' <|> skipChar 'x') <* (skipChar 'M' <|> skipChar 'm') <* (skipChar 'L' <|> skipChar 'l')
 
 /-- https://www.w3.org/TR/xml/#NT-PI -/
-def PI : Parsec Unit := do 
+def PI : Parsec Unit := do
   skipString "<?"
   <* PITarget <*
   optional (S *> manyChars (notFollowedBy (skipString "?>") *> Char))
   skipString "?>"
 
 /-- https://www.w3.org/TR/xml/#NT-Misc -/
-def Misc : Parsec Unit := 
+def Misc : Parsec Unit :=
   Comment *> pure () <|> PI <|> S *> pure ()
-  
+
 /-- https://www.w3.org/TR/xml/#NT-SystemLiteral -/
 def SystemLiteral : Parsec String :=
   pchar '"' *> manyChars (satisfy λ c => c ≠ '"') <* pchar '"'
-  <|> pchar '\'' *> manyChars (satisfy λ c => c ≠ '\'') <* '\''
-  
+  <|> pchar '\'' *> manyChars (satisfy λ c => c ≠ '\'') <* pure '\''
+
 /-- https://www.w3.org/TR/xml/#NT-PubidChar -/
 def PubidChar : Parsec LeanChar :=
   asciiLetter <|> digit <|> endl <|> attempt do
   let c ← anyChar
-  if "-'()+,./:=?;!*#@$_%".contains c then c else fail "PublidChar expected"
+  if "-'()+,./:=?;!*#@$_%".contains c then pure c else fail "PublidChar expected"
 
 /-- https://www.w3.org/TR/xml/#NT-PubidLiteral -/
 def PubidLiteral : Parsec String :=
   pchar '"' *> manyChars PubidChar <* pchar '"'
-  <|> pchar '\'' *> manyChars (attempt do 
+  <|> pchar '\'' *> manyChars (attempt do
     let c ← PubidChar
-    if c = '\'' then fail "'\\'' not expected" else c) <* pchar '\''
+    if c = '\'' then fail "'\\'' not expected" else pure c) <* pchar '\''
 
 /-- https://www.w3.org/TR/xml/#NT-ExternalID -/
-def ExternalID : Parsec Unit := 
+def ExternalID : Parsec Unit :=
   skipString "SYSTEM" *> S *> SystemLiteral *> pure ()
   <|> skipString "PUBLIC" *> S *> PubidLiteral *> S *> SystemLiteral *> pure ()
 
 /-- https://www.w3.org/TR/xml/#NT-Mixed -/
-def Mixed : Parsec Unit := 
-  (do 
+def Mixed : Parsec Unit :=
+  (do
     skipChar '('
     optional S *>
     skipString "#PCDATA" *>
@@ -173,17 +173,17 @@ def Mixed : Parsec Unit :=
     optional S *>
     skipString ")*")
   <|> skipChar '(' *> (optional S) *> skipString "#PCDATA" <* (optional S) <* skipChar ')'
-  
+
 mutual
   /-- https://www.w3.org/TR/xml/#NT-cp -/
-  partial def cp : Parsec Unit := 
+  partial def cp : Parsec Unit :=
     (Name *> pure () <|> choice <|> seq) <* optional (skipChar '?' <|> skipChar '*' <|> skipChar '+')
-    
+
   /-- https://www.w3.org/TR/xml/#NT-choice -/
   partial def choice : Parsec Unit := do
     skipChar '('
     optional S *>
-    cp 
+    cp
     many1 (optional S *> skipChar '|' *> optional S *> cp) *>
     optional S *>
     skipChar ')'
@@ -192,7 +192,7 @@ mutual
   partial def seq : Parsec Unit := do
     skipChar '('
     optional S *>
-    cp 
+    cp
     many (optional S *> skipChar ',' *> optional S *> cp) *>
     optional S *>
     skipChar ')'
@@ -205,7 +205,7 @@ def children : Parsec Unit :=
 /-- https://www.w3.org/TR/xml/#NT-contentspec -/
 def contentspec : Parsec Unit := do
   skipString "EMPTY" <|> skipString "ANY" <|> Mixed <|> children
-  
+
 /-- https://www.w3.org/TR/xml/#NT-elementdecl -/
 def elementDecl : Parsec Unit := do
   skipString "<!ELEMENT"
@@ -216,48 +216,48 @@ def elementDecl : Parsec Unit := do
   skipChar '>'
 
 /-- https://www.w3.org/TR/xml/#NT-StringType -/
-def StringType : Parsec Unit := 
+def StringType : Parsec Unit :=
   skipString "CDATA"
-  
+
 /-- https://www.w3.org/TR/xml/#NT-TokenizedType -/
 def TokenizedType : Parsec Unit :=
-  skipString "ID" 
+  skipString "ID"
   <|> skipString "IDREF"
   <|> skipString "IDREFS"
   <|> skipString "ENTITY"
   <|> skipString "ENTITIES"
   <|> skipString "NMTOKEN"
   <|> skipString "NMTOKENS"
-  
+
 /-- https://www.w3.org/TR/xml/#NT-NotationType -/
 def NotationType : Parsec Unit := do
   skipString "NOTATION"
-  S *> 
+  S *>
   skipChar '(' <*
   optional S
   Name *> many (optional S *> skipChar '|' *> optional S *> Name) *>
   optional S *>
   skipChar ')'
-  
+
 /-- https://www.w3.org/TR/xml/#NT-Nmtoken -/
 def Nmtoken : Parsec String := do
   many1Chars NameChar
-  
+
 /-- https://www.w3.org/TR/xml/#NT-Enumeration -/
 def Enumeration : Parsec Unit := do
-  skipChar '(' 
+  skipChar '('
   optional S *>
   Nmtoken *> many (optional S *> skipChar '|' *> optional S *> Nmtoken) *>
   optional S *>
   skipChar ')'
-  
+
 /-- https://www.w3.org/TR/xml/#NT-EnumeratedType -/
 def EnumeratedType : Parsec Unit :=
   NotationType <|> Enumeration
-  
+
 /-- https://www.w3.org/TR/xml/#NT-AttType -/
 def AttType : Parsec Unit :=
-  StringType <|> TokenizedType <|> EnumeratedType 
+  StringType <|> TokenizedType <|> EnumeratedType
 
 def predefinedEntityToChar : String → Option LeanChar
 | "lt" => some '<'
@@ -268,7 +268,7 @@ def predefinedEntityToChar : String → Option LeanChar
 | _ => none
 
 /-- https://www.w3.org/TR/xml/#NT-EntityRef -/
-def EntityRef : Parsec $ Option LeanChar := attempt $ 
+def EntityRef : Parsec $ Option LeanChar := attempt $
   skipChar '&' *> predefinedEntityToChar <$> Name <* skipChar ';'
 
 @[inline]
@@ -276,23 +276,23 @@ def hexDigitToNat (c : LeanChar) : Nat :=
   if '0' ≤ c ∧ c ≤ '9' then c.toNat - '0'.toNat
   else if 'a' ≤ c ∧ c ≤ 'f' then c.toNat - 'a'.toNat + 10
   else c.toNat - 'A'.toNat + 10
-    
+
 def digitsToNat (base : Nat) (digits : Array Nat) : Nat :=
   digits.foldl (λ r d => r * base + d) 0
 
 /-- https://www.w3.org/TR/xml/#NT-CharRef -/
 def CharRef : Parsec LeanChar := do
   skipString "&#"
-  let charCode ← 
+  let charCode ←
     digitsToNat 10 <$> many1 (hexDigitToNat <$> digit)
     <|> skipChar 'x' *> digitsToNat 16 <$> many1 (hexDigitToNat <$> hexDigit)
   skipChar ';'
-  Char.ofNat charCode
+  return Char.ofNat charCode
 
 /-- https://www.w3.org/TR/xml/#NT-Reference -/
-def Reference : Parsec $ Option LeanChar := 
+def Reference : Parsec $ Option LeanChar :=
   EntityRef <|> some <$> CharRef
-  
+
 /-- https://www.w3.org/TR/xml/#NT-AttValue -/
 def AttValue : Parsec String := do
   let chars ←
@@ -300,56 +300,56 @@ def AttValue : Parsec String := do
     skipChar '"'
     many (some <$> satisfy (λ c => c ≠ '<' ∧ c ≠ '&' ∧ c ≠ '"') <|> Reference) <*
     skipChar '"')
-  <|> (do 
+  <|> (do
     skipChar '\''
-    many (some <$> satisfy (λ c => c ≠ '<' ∧ c ≠ '&' ∧ c ≠ '\'') <|> Reference) <* 
+    many (some <$> satisfy (λ c => c ≠ '<' ∧ c ≠ '&' ∧ c ≠ '\'') <|> Reference) <*
     skipChar '\'')
   return chars.foldl (λ s c => if let some c := c then s.push c else s) ""
-  
+
 /-- https://www.w3.org/TR/xml/#NT-DefaultDecl -/
-def DefaultDecl : Parsec Unit := 
-  skipString "#REQUIRED" 
+def DefaultDecl : Parsec Unit :=
+  skipString "#REQUIRED"
   <|> skipString "#IMPLIED"
   <|> optional (skipString "#FIXED" <* S) *> AttValue *> pure ()
 
 /-- https://www.w3.org/TR/xml/#NT-AttDef -/
 def AttDef : Parsec Unit :=
   S *> Name *> S *> AttType *> S *> DefaultDecl
-  
+
 /-- https://www.w3.org/TR/xml/#NT-AttlistDecl -/
 def AttlistDecl : Parsec Unit :=
   skipString "<!ATTLIST" *> S *> Name *> many AttDef *> optional S *> skipChar '>'
 
 /-- https://www.w3.org/TR/xml/#NT-PEReference -/
-def PEReference : Parsec Unit := 
+def PEReference : Parsec Unit :=
   skipChar '%' *> Name *> skipChar ';'
-  
+
 /-- https://www.w3.org/TR/xml/#NT-EntityValue -/
 def EntityValue : Parsec String := do
   let chars ←
-  (do 
-    skipChar '"' 
+  (do
+    skipChar '"'
     many (some <$> satisfy (λ c => c ≠ '%' ∧ c ≠ '&' ∧ c ≠ '"') <|> PEReference *> pure none <|> Reference) <*
     skipChar '"')
-  <|> (do 
-    skipChar '\'' 
+  <|> (do
+    skipChar '\''
     many (some <$> satisfy (λ c => c ≠ '%' ∧ c ≠ '&' ∧ c ≠ '\'') <|> PEReference *> pure none <|> Reference) <*
     skipChar '\'')
   return chars.foldl (λ s c => if let some c := c then s.push c else s) ""
-  
+
 
 /-- https://www.w3.org/TR/xml/#NT-NDataDecl -/
 def NDataDecl : Parsec Unit :=
   S *> skipString "NDATA" <* S <* Name
 
 /-- https://www.w3.org/TR/xml/#NT-EntityDef -/
-def EntityDef : Parsec Unit := 
+def EntityDef : Parsec Unit :=
   EntityValue *> pure () <|> (ExternalID <* optional NDataDecl)
 
 /-- https://www.w3.org/TR/xml/#NT-GEDecl -/
-def GEDecl : Parsec Unit := 
+def GEDecl : Parsec Unit :=
   skipString "<!ENTITY" *> S *> Name *> S *> EntityDef *> optional S *> skipChar '>'
-  
+
 /-- https://www.w3.org/TR/xml/#NT-PEDef -/
 def PEDef : Parsec Unit :=
   EntityValue *> pure () <|> ExternalID
@@ -361,7 +361,7 @@ def PEDecl : Parsec Unit :=
 /-- https://www.w3.org/TR/xml/#NT-EntityDecl -/
 def EntityDecl : Parsec Unit :=
   GEDecl <|> PEDecl
-  
+
 /-- https://www.w3.org/TR/xml/#NT-PublicID -/
 def PublicID : Parsec Unit :=
   skipString "PUBLIC" <* S <* PubidLiteral
@@ -371,7 +371,7 @@ def NotationDecl : Parsec Unit :=
   skipString "<!NOTATION" *> S *> Name *> (ExternalID <|> PublicID) *> optional S *> skipChar '>'
 
 /-- https://www.w3.org/TR/xml/#NT-markupdecl -/
-def markupDecl : Parsec Unit := 
+def markupDecl : Parsec Unit :=
   elementDecl <|> AttlistDecl <|> EntityDecl <|> NotationDecl <|> PI <|> (Comment *> pure ())
 
 /-- https://www.w3.org/TR/xml/#NT-DeclSep -/
@@ -393,33 +393,33 @@ def doctypedecl : Parsec Unit := do
   skipChar '>'
 
 /-- https://www.w3.org/TR/xml/#NT-prolog -/
-def prolog : Parsec Unit := 
+def prolog : Parsec Unit :=
   optional XMLdecl *>
   many Misc *>
   optional (doctypedecl <* many Misc) *> pure ()
-  
+
 /-- https://www.w3.org/TR/xml/#NT-Attribute -/
 def Attribute : Parsec (String × String) := do
   let name ← Name
   Eq
   let value ← AttValue
-  (name, value)
-  
+  return (name, value)
+
 protected def elementPrefix : Parsec (Array Content → Element) := do
-  skipChar '<' 
+  skipChar '<'
   let name ← Name
-  let attributes ← many (S *> Attribute) 
+  let attributes ← many (S *> Attribute)
   optional S *> pure ()
-  Element.Element name (Std.RBMap.fromList attributes.toList compare)
+  return Element.Element name (Std.RBMap.fromList attributes.toList compare)
 
 /-- https://www.w3.org/TR/xml/#NT-EmptyElemTag -/
 def EmptyElemTag (elem : Array Content → Element) : Parsec Element := do
   skipString "/>" *> pure (elem #[])
-  
+
 /-- https://www.w3.org/TR/xml/#NT-STag -/
 def STag (elem : Array Content → Element) : Parsec (Array Content → Element) := do
   skipChar '>' *> pure elem
-  
+
 /-- https://www.w3.org/TR/xml/#NT-ETag -/
 def ETag : Parsec Unit :=
   skipString "</" *> Name *> optional S *> skipChar '>'
@@ -439,35 +439,35 @@ def CData : Parsec String :=
 /-- https://www.w3.org/TR/xml/#NT-CDSect -/
 def CDSect : Parsec String :=
   CDStart *> CData <* CDEnd
-  
+
 /-- https://www.w3.org/TR/xml/#NT-CharData -/
 def CharData : Parsec String :=
   notFollowedBy (skipString "]]>") *> manyChars (satisfy λ c => c ≠ '<' ∧ c ≠ '&')
 
-mutual 
+mutual
   /-- https://www.w3.org/TR/xml/#NT-content -/
   partial def content : Parsec (Array Content) := do
     let x ← optional (Content.Character <$> CharData)
     let xs ← many do
-      let y ← 
+      let y ←
         attempt (some <$> Content.Element <$> element)
-        <|> (do let c ← Reference; c.map (Content.Character ∘ Char.toString))
+        <|> (do let c ← Reference; pure <| c.map (Content.Character ∘ Char.toString))
         <|> some <$> Content.Character <$> CDSect
-        <|> PI *> none
+        <|> PI *> pure none
         <|> some <$> Content.Comment <$> Comment
 
       let z ← optional (Content.Character <$> CharData)
-      #[y, z]
+      pure #[y, z]
     let xs := #[x] ++ xs.concatMap id |>.filterMap id
     let mut res := #[]
     for x in xs do
       if res.size > 0 then
         match res.back, x with
-        | Content.Character x, Content.Character y => res ← res.set! (res.size - 1) (Content.Character $ x ++ y)
-        | _, x => res ← res.push x
-      else res ← res.push x
-    res
-    
+        | Content.Character x, Content.Character y => res := res.set! (res.size - 1) (Content.Character $ x ++ y)
+        | _, x => res := res.push x
+      else res := res.push x
+    return res
+
   /-- https://www.w3.org/TR/xml/#NT-element -/
   partial def element : Parsec Element := do
     let elem ← Parser.elementPrefix
diff --git a/src/Lean/DocString.lean b/src/Lean/DocString.lean
index 33493caa32..9c50a22128 100644
--- a/src/Lean/DocString.lean
+++ b/src/Lean/DocString.lean
@@ -21,8 +21,8 @@ def addDocString' [Monad m] [MonadEnv m] (declName : Name) (docString? : Option
   | some docString => addDocString declName docString
   | none => return ()
 
-def findDocString? (env : Environment) (declName : Name) : IO (Option String) := do
-  (← builtinDocStrings.get).find? declName |>.orElse fun _ => docStringExt.find? env declName
+def findDocString? (env : Environment) (declName : Name) : IO (Option String) :=
+  return (← builtinDocStrings.get).find? declName |>.orElse fun _ => docStringExt.find? env declName
 
 private builtin_initialize moduleDocExt : SimplePersistentEnvExtension String (Std.PersistentArray String) ← registerSimplePersistentEnvExtension {
   name          := `moduleDocExt
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 1c6494f68b..435583588c 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -212,7 +212,7 @@ def elabBinder {α} (binder : Syntax) (x : Expr → TermElabM α) : TermElabM α
     -- elaborate independently from each other
     let dom ← elabType dom
     let rng ← elabType rng
-    mkForall (← MonadQuotation.addMacroScope `a) BinderInfo.default dom rng
+    return mkForall (← MonadQuotation.addMacroScope `a) BinderInfo.default dom rng
   | _                    => throwUnsupportedSyntax
 
 /--
@@ -391,7 +391,7 @@ def expandWhereDecls (whereDecls : Syntax) (body : Syntax) : MacroM Syntax :=
 
 def expandWhereDeclsOpt (whereDeclsOpt : Syntax) (body : Syntax) : MacroM Syntax :=
   if whereDeclsOpt.isNone then
-    body
+    return body
   else
     expandWhereDecls whereDeclsOpt[0] body
 
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index df81b565e0..33f7642d57 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -283,7 +283,7 @@ private def mkRunMetaEval (e : Expr) : MetaM Expr :=
     let α ← inferType e
     let u ← getDecLevel α
     let instVal ← mkEvalInstCore ``Lean.MetaEval e
-    let e ← mkAppN (mkConst ``Lean.runMetaEval [u]) #[α, instVal, env, opts, e]
+    let e := mkAppN (mkConst ``Lean.runMetaEval [u]) #[α, instVal, env, opts, e]
     instantiateMVars (← mkLambdaFVars #[env, opts] e)
 
 private def mkRunEval (e : Expr) : MetaM Expr := do
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 7279de6ed9..03b792083a 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -264,7 +264,7 @@ where
   | `(($e))         => return (← expandCDot? e).getD e
   | `(($e, $es,*))  => do
     let pairs ← mkPairs (#[e] ++ es)
-    (← expandCDot? pairs).getD pairs
+    return (← expandCDot? pairs).getD pairs
   | stx =>
     if !stx[1][0].isMissing && stx[1][1].isMissing then
       -- parsed `(` and `term`, assume it's a basic parenthesis to get any elaboration output at all
diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index 49b1c420e7..d951aaf146 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -215,8 +215,8 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
 /--
 A resolved name literal. Evaluates to the full name of the given constant if
 existent in the current context, or else fails. -/
-@[builtinTermElab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ => do
-  toExpr (← resolveGlobalConstNoOverloadWithInfo stx[2])
+@[builtinTermElab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ =>
+  return toExpr (← resolveGlobalConstNoOverloadWithInfo stx[2])
 
 @[builtinTermElab typeOf] def elabTypeOf : TermElab := fun stx _ => do
   inferType (← elabTerm stx[1] none)
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index f8fb067efe..022c5c6a38 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -298,7 +298,7 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do
 
   -- note the order: first process current messages & info trees, then add back old messages & trees,
   -- then convert new traces to messages
-  let mut msgs ← (← get).messages
+  let mut msgs := (← get).messages
   -- `stx.hasMissing` should imply `initMsgs.hasErrors`, but the latter should be cheaper to check in general
   if !showPartialSyntaxErrors.get (← getOptions) && initMsgs.hasErrors && stx.hasMissing then
     -- discard elaboration errors, except for a few important and unlikely misleading ones, on parse error
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index bd6d4ab4c9..6bc030b738 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -28,7 +28,7 @@ private def expandDeclIdNamespace? (declId : Syntax) : MacroM (Option (Name × S
   let (id, optUnivDeclStx) := expandDeclIdCore declId
   let scpView := extractMacroScopes id
   match scpView.name with
-  | Name.str Name.anonymous s _ => none
+  | Name.str Name.anonymous s _ => return none
   | Name.str pre s _            =>
     ensureValidNamespace pre
     let nameNew := { scpView with name := Name.mkSimple s }.review
@@ -36,15 +36,15 @@ private def expandDeclIdNamespace? (declId : Syntax) : MacroM (Option (Name × S
     -- name access the info tree node of the declaration name
     let id := mkIdent nameNew |>.setInfo declId.getHeadInfo
     if declId.isIdent then
-      some (pre, id)
+      return some (pre, id)
     else
-      some (pre, declId.setArg 0 id)
-  | _ => none
+      return some (pre, declId.setArg 0 id)
+  | _ => return none
 
 /- given declarations such as `@[...] def Foo.Bla.f ...` return `some (Foo.Bla, @[...] def f ...)` -/
 private def expandDeclNamespace? (stx : Syntax) : MacroM (Option (Name × Syntax)) := do
   if !stx.isOfKind `Lean.Parser.Command.declaration then
-    none
+    return none
   else
     let decl := stx[1]
     let k := decl.getKind
@@ -57,16 +57,16 @@ private def expandDeclNamespace? (stx : Syntax) : MacroM (Option (Name × Syntax
        k == ``Lean.Parser.Command.classInductive ||
        k == ``Lean.Parser.Command.structure then
       match (← expandDeclIdNamespace? decl[1]) with
-      | some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 1 declId))
-      | none              => none
+      | some (ns, declId) => return some (ns, stx.setArg 1 (decl.setArg 1 declId))
+      | none              => return none
     else if k == ``Lean.Parser.Command.instance then
       let optDeclId := decl[3]
-      if optDeclId.isNone then none
+      if optDeclId.isNone then return none
       else match (← expandDeclIdNamespace? optDeclId[0]) with
-        | some (ns, declId) => some (ns, stx.setArg 1 (decl.setArg 3 (optDeclId.setArg 0 declId)))
-        | none              => none
+        | some (ns, declId) => return some (ns, stx.setArg 1 (decl.setArg 3 (optDeclId.setArg 0 declId)))
+        | none              => return none
     else
-      none
+      return none
 
 def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
   -- leading_parser "axiom " >> declId >> declSig
diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean
index ac3caf9193..8b1da7aeef 100644
--- a/src/Lean/Elab/Deriving/BEq.lean
+++ b/src/Lean/Elab/Deriving/BEq.lean
@@ -69,8 +69,8 @@ where
     return alts
 
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
-  let auxFunName ← ctx.auxFunNames[i]
-  let indVal     ← ctx.typeInfos[i]
+  let auxFunName := ctx.auxFunNames[i]
+  let indVal     := ctx.typeInfos[i]
   let header     ← mkBEqHeader ctx indVal
   let mut body   ← mkMatch ctx header indVal auxFunName
   if ctx.usePartial then
@@ -98,7 +98,7 @@ private def mkBEqInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax
   return cmds
 
 private def mkBEqEnumFun (ctx : Context) (name : Name) : TermElabM Syntax := do
-  let auxFunName ← ctx.auxFunNames[0]
+  let auxFunName := ctx.auxFunNames[0]
   `(private def $(mkIdent auxFunName):ident  (x y : $(mkIdent name)) : Bool := x.toCtorIdx == y.toCtorIdx)
 
 private def mkBEqEnumCmd (name : Name): TermElabM (Array Syntax) := do
diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean
index 3814261f9a..d00c7f6bec 100644
--- a/src/Lean/Elab/Deriving/DecEq.lean
+++ b/src/Lean/Elab/Deriving/DecEq.lean
@@ -75,12 +75,12 @@ where
         else if (← compatibleCtors ctorName₁ ctorName₂) then
           patterns := patterns ++ #[(← `($(mkIdent ctorName₁) ..)), (← `($(mkIdent ctorName₂) ..))]
           let rhs ← `(isFalse (by intro h; injection h))
-          alts ← alts.push (← `(matchAltExpr| | $[$patterns:term],* => $rhs:term))
+          alts := alts.push (← `(matchAltExpr| | $[$patterns:term],* => $rhs:term))
     return alts
 
 def mkAuxFunction (ctx : Context) : TermElabM Syntax := do
-  let auxFunName ← ctx.auxFunNames[0]
-  let indVal     ← ctx.typeInfos[0]
+  let auxFunName := ctx.auxFunNames[0]
+  let indVal     :=ctx.typeInfos[0]
   let header     ← mkDecEqHeader ctx indVal
   let mut body   ← mkMatch ctx header indVal auxFunName header.argNames
   let binders    := header.binders
diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean
index 08905d93f1..59a14181ef 100644
--- a/src/Lean/Elab/Deriving/FromToJson.lean
+++ b/src/Lean/Elab/Deriving/FromToJson.lean
@@ -21,13 +21,13 @@ def mkJsonField (n : Name) : Bool × Syntax :=
 
 def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
   if declNames.size == 1 then
-    if (← isStructure (← getEnv) declNames[0]) then
+    if isStructure (← getEnv) declNames[0] then
       let cmds ← liftTermElabM none <| do
         let ctx ← mkContext "toJson" declNames[0]
         let header ← mkHeader ctx ``ToJson 1 ctx.typeInfos[0]
         let fields := getStructureFieldsFlattened (← getEnv) declNames[0] (includeSubobjectFields := false)
         let fields : Array Syntax ← fields.mapM fun field => do
-          let (isOptField, nm) ← mkJsonField field
+          let (isOptField, nm) := mkJsonField field
           if isOptField then `(opt $nm $(mkIdent <| header.targetNames[0] ++ field))
           else `([($nm, toJson $(mkIdent <| header.targetNames[0] ++ field))])
         let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]):ident $header.binders:explicitBinder* :=
@@ -102,7 +102,7 @@ where
 
 def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
   if declNames.size == 1 then
-    if (← isStructure (← getEnv) declNames[0]) then
+    if isStructure (← getEnv) declNames[0] then
       let cmds ← liftTermElabM none <| do
         let ctx ← mkContext "fromJson" declNames[0]
         let header ← mkHeader ctx ``FromJson 0 ctx.typeInfos[0]
@@ -178,10 +178,10 @@ where
             (fun jsons => do
               $[let $identNames:ident ← $fromJsons]*
               return $(mkIdent ctor):ident $identNames*))
-        (stx, ctorInfo.numFields)
+        pure (stx, ctorInfo.numFields)
   -- the smaller cases, especially the ones without fields are likely faster
   let alts := alts.qsort (fun (_, x) (_, y) => x < y)
-  alts.map Prod.fst
+  return alts.map Prod.fst
 
 builtin_initialize
   registerBuiltinDerivingHandler ``ToJson mkToJsonInstanceHandler
diff --git a/src/Lean/Elab/Deriving/Hashable.lean b/src/Lean/Elab/Deriving/Hashable.lean
index 449130feee..e341e949e0 100644
--- a/src/Lean/Elab/Deriving/Hashable.lean
+++ b/src/Lean/Elab/Deriving/Hashable.lean
@@ -54,8 +54,8 @@ where
     return alts
 
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
-  let auxFunName ← ctx.auxFunNames[i]
-  let indVal     ← ctx.typeInfos[i]
+  let auxFunName := ctx.auxFunNames[i]
+  let indVal     := ctx.typeInfos[i]
   let header     ← mkHashableHeader ctx indVal
   let body       ← mkMatch ctx header indVal i
   let binders    := header.binders
@@ -87,4 +87,4 @@ def mkHashableHandler (declNames : Array Name) : CommandElabM Bool := do
 
 builtin_initialize
   registerBuiltinDerivingHandler ``Hashable mkHashableHandler
-  registerTraceClass `Elab.Deriving.hashable
\ No newline at end of file
+  registerTraceClass `Elab.Deriving.hashable
diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean
index 335672dbd8..75ed7dd73e 100644
--- a/src/Lean/Elab/Deriving/Inhabited.lean
+++ b/src/Lean/Elab/Deriving/Inhabited.lean
@@ -92,7 +92,7 @@ where
           trace[Elab.Deriving.inhabited] "checking {instType} for '{ctorName}'"
           match (← trySynthInstance instType) with
           | LOption.some e =>
-            usedInstIdxs ← collectUsedLocalsInsts usedInstIdxs localInst2Index e
+            usedInstIdxs := collectUsedLocalsInsts usedInstIdxs localInst2Index e
           | _ =>
             trace[Elab.Deriving.inhabited] "failed to generate instance using '{ctorName}' {if addHypotheses then "(assuming parameters are inhabited)" else ""} because of field with type{indentExpr (← inferType x)}"
             ok := false
diff --git a/src/Lean/Elab/Deriving/Ord.lean b/src/Lean/Elab/Deriving/Ord.lean
index fab9d72f8c..02637c6cab 100644
--- a/src/Lean/Elab/Deriving/Ord.lean
+++ b/src/Lean/Elab/Deriving/Ord.lean
@@ -58,15 +58,15 @@ where
         let ltPatterns := indPatterns ++ #[lPat, ←`(_)]
         let gtPatterns := indPatterns ++ #[←`(_), rPat]
         let rhs ← rhsCont (← `(Ordering.eq))
-        #[←`(matchAltExpr| | $[$(patterns):term],* => $rhs:term),
-          ←`(matchAltExpr| | $[$(ltPatterns):term],* => Ordering.lt),
-          ←`(matchAltExpr| | $[$(gtPatterns):term],* => Ordering.gt)]
+        pure #[←`(matchAltExpr| | $[$(patterns):term],* => $rhs:term),
+               ←`(matchAltExpr| | $[$(ltPatterns):term],* => Ordering.lt),
+               ←`(matchAltExpr| | $[$(gtPatterns):term],* => Ordering.gt)]
       alts := alts ++ alt
     return alts.pop.pop
 
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
-  let auxFunName ← ctx.auxFunNames[i]
-  let indVal     ← ctx.typeInfos[i]
+  let auxFunName := ctx.auxFunNames[i]
+  let indVal     := ctx.typeInfos[i]
   let header     ← mkOrdHeader ctx indVal
   let mut body   ← mkMatch ctx header indVal auxFunName
   if ctx.usePartial || indVal.isRec then
diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean
index 3e15d5e996..338ab60752 100644
--- a/src/Lean/Elab/Deriving/Repr.lean
+++ b/src/Lean/Elab/Deriving/Repr.lean
@@ -22,9 +22,9 @@ def mkReprHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := d
 
 def mkBodyForStruct (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM Syntax := do
   let ctorVal ← getConstInfoCtor indVal.ctors.head!
-  let fieldNames ← getStructureFields (← getEnv) indVal.name
-  let numParams := indVal.numParams
-  let target    := mkIdent header.targetNames[0]
+  let fieldNames := getStructureFields (← getEnv) indVal.name
+  let numParams  := indVal.numParams
+  let target     := mkIdent header.targetNames[0]
   forallTelescopeReducing ctorVal.type fun xs _ => do
     let mut fields : Syntax ← `(Format.nil)
     let mut first := true
@@ -84,8 +84,8 @@ def mkBody (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName
     mkBodyForInduct ctx header indVal auxFunName
 
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
-  let auxFunName ← ctx.auxFunNames[i]
-  let indVal     ← ctx.typeInfos[i]
+  let auxFunName := ctx.auxFunNames[i]
+  let indVal     := ctx.typeInfos[i]
   let header     ← mkReprHeader ctx indVal
   let mut body   ← mkBody ctx header indVal auxFunName
   if ctx.usePartial then
diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean
index a184641147..783b9b408d 100644
--- a/src/Lean/Elab/Deriving/Util.lean
+++ b/src/Lean/Elab/Deriving/Util.lean
@@ -55,7 +55,7 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
   let indVal ← getConstInfoInduct typeName
   let mut typeInfos := #[]
   for typeName in indVal.all do
-    typeInfos ← typeInfos.push (← getConstInfoInduct typeName)
+    typeInfos := typeInfos.push (← getConstInfoInduct typeName)
   let mut auxFunNames := #[]
   for typeName in indVal.all do
     match typeName.eraseMacroScopes with
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 3d55c57703..f6357ef8b7 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -274,19 +274,19 @@ def mkAuxDeclFor {m} [Monad m] [MonadQuotation m] (e : Syntax) (mkCont : Syntax
 /- Convert `action _ e` instructions in `c` into `let y ← e; jmp _ jp (xs y)`. -/
 partial def convertTerminalActionIntoJmp (code : Code) (jp : Name) (xs : Array Name) : MacroM Code :=
   let rec loop : Code → MacroM Code
-    | Code.decl xs stx k           => do Code.decl xs stx (← loop k)
-    | Code.reassign xs stx k       => do Code.reassign xs stx (← loop k)
-    | Code.joinpoint n ps b k      => do Code.joinpoint n ps (← loop b) (← loop k)
-    | Code.seq e k                 => do Code.seq e (← loop k)
-    | Code.ite ref x? h c t e      => do Code.ite ref x? h c (← loop t) (← loop e)
-    | Code.«match» ref g ds t alts => do Code.«match» ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) })
+    | Code.decl xs stx k           => return Code.decl xs stx (← loop k)
+    | Code.reassign xs stx k       => return Code.reassign xs stx (← loop k)
+    | Code.joinpoint n ps b k      => return Code.joinpoint n ps (← loop b) (← loop k)
+    | Code.seq e k                 => return Code.seq e (← loop k)
+    | Code.ite ref x? h c t e      => return Code.ite ref x? h c (← loop t) (← loop e)
+    | Code.«match» ref g ds t alts => return Code.«match» ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← loop alt.rhs) })
     | Code.action e                => mkAuxDeclFor e fun y =>
       let ref := e
       -- We jump to `jp` with xs **and** y
       let jmpArgs := xs.map $ mkIdentFrom ref
       let jmpArgs := jmpArgs.push y
-      pure $ Code.jmp ref jp jmpArgs
-    | c                            => pure c
+      return Code.jmp ref jp jmpArgs
+    | c                            => return c
   loop code
 
 structure JPDecl where
@@ -358,14 +358,13 @@ def mkJmp (ref : Syntax) (rs : NameSet) (val : Syntax) (mkJPBody : Syntax → Ma
 
 /- `pullExitPointsAux rs c` auxiliary method for `pullExitPoints`, `rs` is the set of update variable in the current path.  -/
 partial def pullExitPointsAux : NameSet → Code → StateRefT (Array JPDecl) TermElabM Code
-  | rs, Code.decl xs stx k           => do Code.decl xs stx (← pullExitPointsAux (eraseVars rs xs) k)
-  | rs, Code.reassign xs stx k       => do Code.reassign xs stx (← pullExitPointsAux (insertVars rs xs) k)
-  | rs, Code.joinpoint j ps b k      => do Code.joinpoint j ps (← pullExitPointsAux rs b) (← pullExitPointsAux rs k)
-  | rs, Code.seq e k                 => do Code.seq e (← pullExitPointsAux rs k)
-  | rs, Code.ite ref x? o c t e      => do Code.ite ref x? o c (← pullExitPointsAux (eraseOptVar rs x?) t) (← pullExitPointsAux (eraseOptVar rs x?) e)
-  | rs, Code.«match» ref g ds t alts => do
-    Code.«match» ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) })
-  | rs, c@(Code.jmp _ _ _)           => pure c
+  | rs, Code.decl xs stx k           => return Code.decl xs stx (← pullExitPointsAux (eraseVars rs xs) k)
+  | rs, Code.reassign xs stx k       => return Code.reassign xs stx (← pullExitPointsAux (insertVars rs xs) k)
+  | rs, Code.joinpoint j ps b k      => return Code.joinpoint j ps (← pullExitPointsAux rs b) (← pullExitPointsAux rs k)
+  | rs, Code.seq e k                 => return Code.seq e (← pullExitPointsAux rs k)
+  | rs, Code.ite ref x? o c t e      => return Code.ite ref x? o c (← pullExitPointsAux (eraseOptVar rs x?) t) (← pullExitPointsAux (eraseOptVar rs x?) e)
+  | rs, Code.«match» ref g ds t alts => return Code.«match» ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← pullExitPointsAux (eraseVars rs alt.vars) alt.rhs) })
+  | rs, c@(Code.jmp _ _ _)           => return  c
   | rs, Code.«break» ref             => mkSimpleJmp ref rs (Code.«break» ref)
   | rs, Code.«continue» ref          => mkSimpleJmp ref rs (Code.«continue» ref)
   | rs, Code.«return» ref val        => mkJmp ref rs val (fun y => pure $ Code.«return» ref y)
@@ -433,29 +432,29 @@ def pullExitPoints (c : Code) : TermElabM Code := do
 
 partial def extendUpdatedVarsAux (c : Code) (ws : NameSet) : TermElabM Code :=
   let rec update : Code → TermElabM Code
-    | Code.joinpoint j ps b k          => do Code.joinpoint j ps (← update b) (← update k)
-    | Code.seq e k                     => do Code.seq e (← update k)
+    | Code.joinpoint j ps b k          => return Code.joinpoint j ps (← update b) (← update k)
+    | Code.seq e k                     => return Code.seq e (← update k)
     | c@(Code.«match» ref g ds t alts) => do
       if alts.any fun alt => alt.vars.any fun x => ws.contains x then
         -- If a pattern variable is shadowing a variable in ws, we `pullExitPoints`
         pullExitPoints c
       else
-        Code.«match» ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) })
-    | Code.ite ref none o c t e => do Code.ite ref none o c (← update t) (← update e)
+        return Code.«match» ref g ds t (← alts.mapM fun alt => do pure { alt with rhs := (← update alt.rhs) })
+    | Code.ite ref none o c t e => return Code.ite ref none o c (← update t) (← update e)
     | c@(Code.ite ref (some h) o cond t e) => do
       if ws.contains h then
         -- if the `h` at `if h:c then t else e` shadows a variable in `ws`, we `pullExitPoints`
         pullExitPoints c
       else
-        Code.ite ref (some h) o cond (← update t) (← update e)
-    | Code.reassign xs stx k => do Code.reassign xs stx (← update k)
+        return Code.ite ref (some h) o cond (← update t) (← update e)
+    | Code.reassign xs stx k => return Code.reassign xs stx (← update k)
     | c@(Code.decl xs stx k) => do
       if xs.any fun x => ws.contains x then
         -- One the declared variables is shadowing a variable in `ws`
         pullExitPoints c
       else
-        Code.decl xs stx (← update k)
-    | c => pure c
+        return Code.decl xs stx (← update k)
+    | c => return  c
   update c
 
 /-
@@ -540,7 +539,7 @@ private def mkPureUnit : MacroM Syntax :=
   ``(pure PUnit.unit)
 
 def mkPureUnitAction : MacroM CodeBlock := do
-  mkTerminalAction (← mkPureUnit)
+  return mkTerminalAction (← mkPureUnit)
 
 def mkUnless (cond : Syntax) (c : CodeBlock) : MacroM CodeBlock := do
   let thenBranch ← mkPureUnitAction
@@ -677,7 +676,7 @@ private def expandDoIf? (stx : Syntax) : MacroM (Option Syntax) := match stx wit
     let mut e      := e?.getD (← `(doSeq|pure PUnit.unit))
     let mut eIsSeq := true
     for (i, cond, t) in Array.zip (is.reverse.push i) (Array.zip (conds.reverse.push cond) (ts.reverse.push t)) do
-      e ← if eIsSeq then e else `(doSeq|$e:doElem)
+      e ← if eIsSeq then pure e else `(doSeq|$e:doElem)
       e ← withRef cond <| match cond with
         | `(doIfCond|let $pat := $d) => `(doElem| match%$i $d:term with | $pat:term => $t | _ => $e)
         | `(doIfCond|let $pat ← $d)  => `(doElem| match%$i ← $d    with | $pat:term => $t | _ => $e)
@@ -1084,14 +1083,14 @@ def matchNestedTermResult (term : Syntax) (uvars : Array Name) (a r bc : Bool) :
   match a, r, bc with
   | true, false, false =>
     if uvars.isEmpty then
-      toDoElems (← `(do $term:term))
+      return toDoElems (← `(do $term:term))
     else
-      toDoElems (← `(do let r ← $term:term; $u:term := r.2; pure r.1))
+      return toDoElems (← `(do let r ← $term:term; $u:term := r.2; pure r.1))
   | false, true, false =>
     if uvars.isEmpty then
-      toDoElems (← `(do let r ← $term:term; return r))
+      return toDoElems (← `(do let r ← $term:term; return r))
     else
-      toDoElems (← `(do let r ← $term:term; $u:term := r.2; return r.1))
+      return toDoElems (← `(do let r ← $term:term; $u:term := r.2; return r.1))
   | false, false, true => toDoElems <$>
     `(do let r ← $term:term;
          match r with
diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean
index 4eb04b4870..9612673b60 100644
--- a/src/Lean/Elab/ElabRules.lean
+++ b/src/Lean/Elab/ElabRules.lean
@@ -37,8 +37,8 @@ def elabElabRulesAux (doc? : Option Syntax) (attrKind : Syntax) (k : SyntaxNodeK
         throwErrorAt alt "invalid elab_rules alternative, unexpected syntax node kind '{k'}'"
     | _ => throwUnsupportedSyntax
   let catName ← match cat?, expty? with
-    | some cat, _ => cat.getId
-    | _, some _   => `term
+    | some cat, _ => pure cat.getId
+    | _, some _   => pure `term
     -- TODO: infer category from quotation kind, possibly even kind of quoted syntax?
     | _, _        => throwError "invalid elab_rules command, specify category using `elab_rules : <cat> ...`"
   if let some expId := expty? then
diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index 691472a750..275bc4516a 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/src/Lean/Elab/Extra.lean
@@ -156,7 +156,7 @@ where
     match s with
     | `(binop% $f $lhs $rhs) => processOp (lazy := false) f lhs rhs
     | `(binop_lazy% $f $lhs $rhs) => processOp (lazy := true) f lhs rhs
-    | `(($e)) => (← go e)
+    | `(($e)) => go e
     | _ =>
        return Tree.term s (← elabTerm s none)
 
diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index 9f9b57cff2..ae92c64e98 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -327,7 +327,7 @@ def withSaveInfoContext [MonadFinally m] [MonadEnv m] [MonadOptions m] [MonadMCt
       let st    ← getInfoState
       let trees ← st.trees.mapM fun tree => do
         let tree := tree.substitute st.assignment
-        InfoTree.context {
+        pure <| InfoTree.context {
           env := (← getEnv), fileMap := (← getFileMap), mctx := (← getMCtx), currNamespace := (← getCurrNamespace), openDecls := (← getOpenDecls), options := (← getOptions)
         } tree
       modifyInfoTrees fun _ => treesSaved ++ trees
diff --git a/src/Lean/Elab/MacroArgUtil.lean b/src/Lean/Elab/MacroArgUtil.lean
index 0b33eb8b24..5ff8f721bb 100644
--- a/src/Lean/Elab/MacroArgUtil.lean
+++ b/src/Lean/Elab/MacroArgUtil.lean
@@ -13,25 +13,25 @@ open Lean.Parser.Command
 /- Convert `macro` arg into a `syntax` command item and a pattern element -/
 def expandMacroArg (stx : Syntax) : MacroM (Syntax × Syntax) := do
   let (id?, id, stx) ← match (← expandMacros stx) with
-    | `(macroArg| $id:ident:$stx) => (some id, id, stx)
-    | `(macroArg| $stx:stx)       => (none, (← `(x)), stx)
+    | `(macroArg| $id:ident:$stx) => pure (some id, id, stx)
+    | `(macroArg| $stx:stx)       => pure (none, (← `(x)), stx)
     | _                           => Macro.throwUnsupported
   let pat ← match stx with
-    | `(stx| $s:strLit)      => mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
-    | `(stx| &$s:strLit)     => mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
-    | `(stx| optional($stx)) => mkSplicePat `optional id "?"
-    | `(stx| many($stx))     => mkSplicePat `many id "*"
-    | `(stx| many1($stx))    => mkSplicePat `many id "*"
+    | `(stx| $s:strLit)      => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
+    | `(stx| &$s:strLit)     => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
+    | `(stx| optional($stx)) => pure <| mkSplicePat `optional id "?"
+    | `(stx| many($stx))     => pure <| mkSplicePat `many id "*"
+    | `(stx| many1($stx))    => pure <| mkSplicePat `many id "*"
     | `(stx| sepBy($stx, $sep:strLit $[, $stxsep]? $[, allowTrailingSep]?)) =>
-      mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
+      pure <| mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
     | `(stx| sepBy1($stx, $sep:strLit $[, $stxsep]? $[, allowTrailingSep]?)) =>
-      mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
+      pure <| mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
     | _ => match id? with
       -- if there is a binding, we assume the user knows what they are doing
-      | some id => mkAntiquotNode id
+      | some id => pure <| mkAntiquotNode id
       -- otherwise `group` the syntax to enforce arity 1, e.g. for `noWs`
       | none    => return (← `(stx| group($stx)), mkAntiquotNode id)
-  (stx, pat)
+  pure (stx, pat)
 where mkSplicePat kind id suffix :=
   mkNullNode #[mkAntiquotSuffixSpliceNode kind (mkAntiquotNode id) suffix]
 
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 6740ae136c..a08514a807 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -103,7 +103,7 @@ private partial def elabMatchTypeAndDiscrs (discrStxs : Array Syntax) (matchOptT
           trace[Elab.match] "discr #{i} {discr} : {d}"
           if b.hasLooseBVars then
             isDep := true
-          matchType ← b.instantiate1 discr
+          matchType := b.instantiate1 discr
           discrs := discrs.push discr
         | _ =>
           throwError "invalid type provided to match-expression, function type with arity #{discrStxs.size} expected"
@@ -956,14 +956,14 @@ private def elabMatchCore (stx : Syntax) (expectedType? : Option Expr) : TermEla
 
 private def isPatternVar (stx : Syntax) : TermElabM Bool := do
   match (← resolveId? stx "pattern") with
-  | none   => isAtomicIdent stx
+  | none   => return isAtomicIdent stx
   | some f => match f with
     | Expr.const fName _ _ =>
       match (← getEnv).find? fName with
       | some (ConstantInfo.ctorInfo _) => return false
       | some _                         => return !hasMatchPatternAttribute (← getEnv) fName
-      | _                              => isAtomicIdent stx
-    | _ => isAtomicIdent stx
+      | _                              => return isAtomicIdent stx
+    | _ => return isAtomicIdent stx
 where
   isAtomicIdent (stx : Syntax) : Bool :=
     stx.isIdent && stx.getId.eraseMacroScopes.isAtomic
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 9da37787e6..da5a9cdcb8 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -169,7 +169,7 @@ private def expandWhereStructInst : Macro
         let mut val := val
         if let some ty := ty? then
           val ← `(($val : $ty))
-        val ← if binders.size > 0 then `(fun $[$binders]* => $val:term) else val
+        val ← if binders.size > 0 then `(fun $[$binders]* => $val:term) else pure val
         `(structInstField|$id:ident := $val)
       | _ => Macro.throwUnsupported
     `({ $[$structInstFields,]* })
diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean
index 0fdfa85856..e63dc22b1e 100644
--- a/src/Lean/Elab/Notation.lean
+++ b/src/Lean/Elab/Notation.lean
@@ -37,7 +37,7 @@ def expandNotationItemIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
 def expandNotationItemIntoPattern (stx : Syntax) : MacroM Syntax :=
   let k := stx.getKind
   if k == `Lean.Parser.Command.identPrec then
-    mkAntiquotNode stx[0]
+    return mkAntiquotNode stx[0]
   else if k == strLitKind then
     strLitToPattern stx
   else
@@ -96,8 +96,8 @@ private def expandNotationAux (ref : Syntax)
     -- Make sure the quotation pre-checker takes section variables into account for local notation.
     macroDecl ← `(section set_option quotPrecheck.allowSectionVars true $macroDecl end)
   match (← mkSimpleDelab attrKind vars pat qrhs |>.run) with
-  | some delabDecl => mkNullNode #[stxDecl, macroDecl, delabDecl]
-  | none           => mkNullNode #[stxDecl, macroDecl]
+  | some delabDecl => return mkNullNode #[stxDecl, macroDecl, delabDecl]
+  | none           => return mkNullNode #[stxDecl, macroDecl]
 
 @[builtinMacro Lean.Parser.Command.notation] def expandNotation : Macro
   | stx@`($attrKind:attrKind notation $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $items* => $rhs) => do
diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean
index 12320d7db5..fae04a1ec6 100644
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@@ -130,7 +130,7 @@ def addNonRec (preDef : PreDefinition) (applyAttrAfterCompilation := true) : Ter
   Eliminate recursive application annotations containing syntax. These annotations are used by the well-founded recursion module
   to produce better error messages. -/
 def eraseRecAppSyntaxExpr (e : Expr) : CoreM Expr :=
-  Core.transform e (post := fun e => TransformStep.done <| if (getRecAppSyntax? e).isSome then e.mdataExpr! else e)
+  Core.transform e (post := fun e => pure <| TransformStep.done <| if (getRecAppSyntax? e).isSome then e.mdataExpr! else e)
 
 def eraseRecAppSyntax (preDef : PreDefinition) : CoreM PreDefinition :=
   return { preDef with value := (← eraseRecAppSyntaxExpr preDef.value) }
diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index b6f14476d5..526b1119f8 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -25,13 +25,13 @@ partial def expand : Expr → Expr
 
 def expandRHS? (mvarId : MVarId) : MetaM (Option MVarId) := do
   let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) ← target.eq? | return none
+  let some (_, lhs, rhs) := target.eq? | return none
   unless rhs.isLet || rhs.isMData do return none
   return some (← replaceTargetDefEq mvarId (← mkEq lhs (expand rhs)))
 
 def funext? (mvarId : MVarId) : MetaM (Option MVarId) := do
   let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) ← target.eq? | return none
+  let some (_, lhs, rhs) := target.eq? | return none
   unless rhs.isLambda do return none
   commitWhenSome? do
     let [mvarId] ← apply mvarId (← mkConstWithFreshMVarLevels ``funext) | return none
@@ -66,7 +66,7 @@ structure Context where
 -/
 private def keepGoing (mvarId : MVarId) : ReaderT Context (StateRefT (Array Expr) MetaM) Bool := do
   let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) ← target.eq? | return false
+  let some (_, lhs, rhs) := target.eq? | return false
   let ctx ← read
   return Option.isSome <| rhs.find? fun e => ctx.declNames.any e.isAppOf && e.hasLooseBVars
 
@@ -122,9 +122,9 @@ private def saveEqn (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := wit
   let fvarState := collectFVars {} target
   let fvarState ← (← getLCtx).foldrM (init := fvarState) fun decl fvarState => do
     if fvarState.fvarSet.contains decl.fvarId then
-      collectFVars fvarState (← instantiateMVars decl.type)
+      return collectFVars fvarState (← instantiateMVars decl.type)
     else
-      fvarState
+      return fvarState
   let mut fvarIds ← sortFVarIds <| fvarState.fvarSet.toArray
   -- Include propositions that are not in fvarState.fvarSet, and only contains variables in
   for decl in (← getLCtx) do
@@ -176,13 +176,13 @@ def tryURefl (mvarId : MVarId) : MetaM Bool :=
 /-- Delta reduce the equation left-hand-side -/
 def deltaLHS (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
   let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) ← target.eq? | throwTacticEx `deltaLHS mvarId "equality expected"
+  let some (_, lhs, rhs) := target.eq? | throwTacticEx `deltaLHS mvarId "equality expected"
   let some lhs ← delta? lhs | throwTacticEx `deltaLHS mvarId "failed to delta reduce lhs"
   replaceTargetDefEq mvarId (← mkEq lhs rhs)
 
 def deltaRHS? (mvarId : MVarId) (declName : Name) : MetaM (Option MVarId) := withMVarContext mvarId do
   let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) ← target.eq? | throwTacticEx `deltaRHS mvarId "equality expected"
+  let some (_, lhs, rhs) := target.eq? | throwTacticEx `deltaRHS mvarId "equality expected"
   let some rhs ← delta? rhs.consumeMData (. == declName) | return none
   replaceTargetDefEq mvarId (← mkEq lhs rhs)
 
@@ -190,13 +190,13 @@ private partial def whnfAux (e : Expr) : MetaM Expr := do
   let e ← whnfI e -- Must reduce instances too, otherwise it will not be able to reduce `(Nat.rec ... ... (OfNat.ofNat 0))`
   let f := e.getAppFn
   match f with
-  | Expr.proj _ _ s _ => mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs
+  | Expr.proj _ _ s _ => return mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs
   | _ => return e
 
 /-- Apply `whnfR` to lhs, return `none` if `lhs` was not modified -/
 def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := withMVarContext mvarId do
   let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) ← target.eq? | throwTacticEx `whnfReducibleLHS mvarId "equality expected"
+  let some (_, lhs, rhs) := target.eq? | throwTacticEx `whnfReducibleLHS mvarId "equality expected"
   let lhs' ← whnfAux lhs
   if lhs' != lhs then
     return some (← replaceTargetDefEq mvarId (← mkEq lhs' rhs))
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index ffc39e0f6c..0cdcb5a44f 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -67,7 +67,7 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
   for preDef in preDefs do
     trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"
   let preDefs ← preDefs.mapM ensureNoUnassignedMVarsAtPreDef
-  let cliques ← partitionPreDefs preDefs
+  let cliques := partitionPreDefs preDefs
   let mut terminationBy ← liftMacroM <| WF.expandTerminationBy hints.terminationBy? (cliques.map fun ds => ds.map (·.declName))
   let mut decreasingBy  ← liftMacroM <| WF.expandTerminationHint hints.decreasingBy? (cliques.map fun ds => ds.map (·.declName))
   for preDefs in cliques do
diff --git a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
index 784a316ff8..9f83cd62c9 100644
--- a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean
@@ -32,7 +32,7 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr
             let ty ← inferType e
             let main ← mkFreshExprSyntheticOpaqueMVar ty
             if (← IndPredBelow.backwardsChaining main.mvarId! maxDepth) then
-              main
+              pure main
             else
               throwError "could not solve using backwards chaining {MessageData.ofGoal main.mvarId!}"
           else
@@ -49,7 +49,7 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr
               modify fun s => { s with addMatchers := s.addMatchers.push addMatcher }
               let some newApp ← matchMatcherApp? newApp | throwError "not a matcherApp: {newApp}"
               addBelow newApp
-            else matcherApp.toExpr
+            else pure matcherApp.toExpr
 
           let newApp ← addBelow matcherApp
           if newApp == matcherApp.toExpr then
diff --git a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean
index ed15a4d5a8..32d7c098e1 100644
--- a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean
@@ -52,7 +52,7 @@ where
               let containsSUnfoldMatch := Option.isSome <| altBody.find? fun e => smartUnfoldingMatch? e |>.isSome
               if !containsSUnfoldMatch then
                 let altBody ← mkLambdaFVars xs[numParams:xs.size] altBody
-                let altBody ← markSmartUnfoldigMatchAlt altBody
+                let altBody := markSmartUnfoldigMatchAlt altBody
                 mkLambdaFVars xs[0:numParams] altBody
               else
                 mkLambdaFVars xs altBody
diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
index e9e3b1fcd6..c3af74a627 100644
--- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean
@@ -18,7 +18,7 @@ structure EqnInfo extends EqnInfoCore where
 
 private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
   let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) ← target.eq? | throwTacticEx `deltaLHSUntilFix mvarId "equality expected"
+  let some (_, lhs, rhs) := target.eq? | throwTacticEx `deltaLHSUntilFix mvarId "equality expected"
   if lhs.isAppOf ``WellFounded.fix then
     return mvarId
   else
@@ -26,7 +26,7 @@ private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := withMVa
 
 private def rwFixEq (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
   let target ← getMVarType' mvarId
-  let some (_, lhs, rhs) ← target.eq? | unreachable!
+  let some (_, lhs, rhs) := target.eq? | unreachable!
   let h := mkAppN (mkConst ``WellFounded.fix_eq lhs.getAppFn.constLevels!) lhs.getAppArgs
   let r ← rewrite mvarId target h
   replaceTargetEq mvarId r.eNew r.eqProof
diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index 66eaf7c5ac..c0cd20558e 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -85,7 +85,7 @@ private partial def processSumCasesOn (x F val : Expr) (k : (x : Expr) → (F :
       return (← mkLambdaFVars xs type, ← getLevel type)
     let mkMinorNew (ctorName : Name) (minor : Expr) : TermElabM Expr :=
       lambdaTelescope minor fun xs body => do
-        let xNew ← xs[0]
+        let xNew := xs[0]
         let valNew ← mkLambdaFVars xs[1:] body
         let FTypeNew := FDecl.type.replaceFVar x (← mkAppOptM ctorName #[α, β, xNew])
         withLocalDeclD FDecl.userName FTypeNew fun FNew => do
@@ -101,7 +101,7 @@ private partial def processSumCasesOn (x F val : Expr) (k : (x : Expr) → (F :
 private partial def processPSigmaCasesOn (x F val : Expr) (k : (F : Expr) → (val : Expr) → TermElabM Expr) : TermElabM Expr := do
   if x.isFVar && val.isAppOfArity ``PSigma.casesOn 5 && val.getArg! 3 == x && (val.getArg! 4).isLambda && (val.getArg! 4).bindingBody!.isLambda then
     let args := val.getAppArgs
-    let [_, u, v] ← val.getAppFn.constLevels! | unreachable!
+    let [_, u, v] := val.getAppFn.constLevels! | unreachable!
     let α := args[0]
     let β := args[1]
     let FDecl ← getLocalDecl F.fvarId!
@@ -109,8 +109,8 @@ private partial def processPSigmaCasesOn (x F val : Expr) (k : (F : Expr) → (v
       let type ← mkArrow (FDecl.type.replaceFVar x xs[0]) type
       return (← mkLambdaFVars xs type, ← getLevel type)
     let minor ← lambdaTelescope args[4] fun xs body => do
-        let a ← xs[0]
-        let xNew ← xs[1]
+        let a := xs[0]
+        let xNew := xs[1]
         let valNew ← mkLambdaFVars xs[2:] body
         let FTypeNew := FDecl.type.replaceFVar x (← mkAppOptM `PSigma.mk #[α, β, a, xNew])
         withLocalDeclD FDecl.userName FTypeNew fun FNew => do
diff --git a/src/Lean/Elab/PreDefinition/WF/Main.lean b/src/Lean/Elab/PreDefinition/WF/Main.lean
index e8690b30e5..dadd2ecd46 100644
--- a/src/Lean/Elab/PreDefinition/WF/Main.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Main.lean
@@ -24,7 +24,7 @@ private def isOnlyOneUnaryDef (preDefs : Array PreDefinition) : MetaM Bool := do
 private partial def addNonRecPreDefs (preDefs : Array PreDefinition) (preDefNonRec : PreDefinition) : TermElabM Unit := do
   if (← isOnlyOneUnaryDef preDefs) then
     return ()
-  let Expr.forallE _ domain _ _ ← preDefNonRec.type | unreachable!
+  let Expr.forallE _ domain _ _ := preDefNonRec.type | unreachable!
   let us := preDefNonRec.levelParams.map mkLevelParam
   for fidx in [:preDefs.size] do
     let preDef := preDefs[fidx]
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 57f0caba46..0a742be120 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -26,8 +26,8 @@ private partial def floatOutAntiquotTerms : Syntax → StateT (Syntax → TermEl
         return ← withFreshMacroScope do
           let a ← `(a)
           modify (fun cont stx => (`(let $a:ident := $e; $stx) : TermElabM _))
-          stx.setArg 2 a
-    Syntax.node i k (← args.mapM floatOutAntiquotTerms)
+          pure <| stx.setArg 2 a
+    return Syntax.node i k (← args.mapM floatOutAntiquotTerms)
   | stx => pure stx
 
 private def getSepFromSplice (splice : Syntax) : Syntax :=
@@ -38,7 +38,7 @@ private def getSepFromSplice (splice : Syntax) : Syntax :=
 
 partial def mkTuple : Array Syntax → TermElabM Syntax
   | #[]  => `(Unit.unit)
-  | #[e] => e
+  | #[e] => return e
   | es   => do
     let stx ← mkTuple (es.eraseIdx 0)
     `(Prod.mk $(es[0]) $stx)
@@ -95,7 +95,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
   -- if antiquotation, insert contents as-is, else recurse
   | stx@(Syntax.node _ k _) => do
     if isAntiquot stx && !isEscapedAntiquot stx then
-      getAntiquotTerm stx
+      return getAntiquotTerm stx
     else if isTokenAntiquot stx && !isEscapedAntiquot stx then
       match stx[0] with
       | Syntax.atom _ val => `(Syntax.atom (Option.getD (getHeadInfo? $(getAntiquotTerm stx)) info) $(quote val))
@@ -118,7 +118,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
             | `optional => `(match $(getAntiquotTerm antiquot):term with
               | some x => Array.empty.push x
               | none   => Array.empty)
-            | `many     => getAntiquotTerm antiquot
+            | `many     => return getAntiquotTerm antiquot
             | `sepBy    => `(@SepArray.elemsAndSeps $(getSepFromSplice arg) $(getAntiquotTerm antiquot))
             | k         => throwErrorAt arg "invalid antiquotation suffix splice kind '{k}'"
         else if k == nullKind && isAntiquotSplice arg then
@@ -138,7 +138,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
           let arr ←
             if k == `sepBy then
               `(mkSepArray $arr (mkAtom $(getSepFromSplice arg)))
-            else arr
+            else pure arr
           let arr ← bindLets arr
           args := args.append arr
         else do
@@ -253,7 +253,7 @@ private def noOpMatchAdaptPats : HeadCheck → Alt → Alt
   | _,                 alt         => alt
 
 private def adaptRhs (fn : Syntax → TermElabM Syntax) : Alt → TermElabM Alt
-  | (pats, rhs) => do (pats, ← fn rhs)
+  | (pats, rhs) => return (pats, ← fn rhs)
 
 private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
   let pat := alt.fst.head!
@@ -334,7 +334,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
           let tuple ← mkTuple ids
           let mut yes := yes
           let resId ← match ids with
-            | #[id] => id
+            | #[id] => pure id
             | _     =>
               for id in ids do
                 yes ← `(let $id := tuples.map (fun $tuple => $id); $yes)
@@ -368,7 +368,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
               let argPats := quoted.getArgs.mapIdx fun i arg =>
                 let arg := if (i : Nat) == idx then mkNullNode #[arg] else arg
                 Unhygienic.run `(`($(arg)))
-              covered (fun (pats, rhs) => (argPats.toList ++ pats, rhs)) (exhaustive := true)
+              covered (fun (pats, rhs) => pure (argPats.toList ++ pats, rhs)) (exhaustive := true)
             else uncovered
           | _ => uncovered
         doMatch := fun yes no => do
@@ -405,7 +405,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
               uncovered
           | shape k' sz =>
             if k' == kind && sz == argPats.size then
-              covered (fun (pats, rhs) => (argPats.toList ++ pats, rhs)) (exhaustive := true)
+              covered (fun (pats, rhs) => pure (argPats.toList ++ pats, rhs)) (exhaustive := true)
             else
               uncovered
           | _ => uncovered,
@@ -428,7 +428,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
     | `($id:ident)      => unconditionally (`(let $id := discr; $(·)))
     | `($id:ident@$pat) => do
       let info ← getHeadInfo (pat::alt.1.tail!, alt.2)
-      { info with onMatch := fun taken => match info.onMatch taken with
+      return { info with onMatch := fun taken => match info.onMatch taken with
           | covered f exh => covered (fun alt => f alt >>= adaptRhs (`(let $id := discr; $(·)))) exh
           | r             => r }
     | _               => throwErrorAt pat "match (syntax) : unexpected pattern kind {pat}"
@@ -445,10 +445,10 @@ private def deduplicate (floatedLetDecls : Array Syntax) : Alt → TermElabM (Ar
       | #[] =>
         -- no antiquotations => introduce Unit parameter to preserve evaluation order
         let rhs' ← `(rhs Unit.unit)
-        (floatedLetDecls.push (← `(letDecl|rhs _ := $rhs)), (pats, rhs'))
+        pure (floatedLetDecls.push (← `(letDecl|rhs _ := $rhs)), (pats, rhs'))
       | vars =>
         let rhs' ← `(rhs $vars*)
-        (floatedLetDecls.push (← `(letDecl|rhs $vars:ident* := $rhs)), (pats, rhs'))
+        pure (floatedLetDecls.push (← `(letDecl|rhs $vars:ident* := $rhs)), (pats, rhs'))
 
 private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : TermElabM Syntax := do
   trace[Elab.match_syntax] "match {discrs} with {alts}"
@@ -460,7 +460,7 @@ private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : T
   | discr::discrs, alt::alts    => do
     let info ← getHeadInfo alt
     let pat  := alt.1.head!
-    let alts ← (alt::alts).mapM fun alt => do ((← getHeadInfo alt).onMatch info.check, alt)
+    let alts ← (alt::alts).mapM fun alt => return ((← getHeadInfo alt).onMatch info.check, alt)
     let mut yesAlts           := #[]
     let mut undecidedAlts     := #[]
     let mut nonExhaustiveAlts := #[]
@@ -512,7 +512,7 @@ def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
       throwUnsupportedSyntax
     let stx ← compileStxMatch discrs.toList (patss.map (·.toList) |>.zip rhss).toList
     trace[Elab.match_syntax.result] "{stx}"
-    stx
+    return stx
   | _ => throwUnsupportedSyntax
 
 /--
diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean
index 24f59ebc6a..75428b578e 100644
--- a/src/Lean/Elab/Quotation/Precheck.lean
+++ b/src/Lean/Elab/Quotation/Precheck.lean
@@ -52,7 +52,7 @@ Macros without registered precheck hook are unfolded, and identifier-less syntax
 
 partial def precheck : Precheck := fun stx => do
   if let p::_ := precheckAttribute.getValues (← getEnv) stx.getKind then
-    if ← catchInternalId unsupportedSyntaxExceptionId (do withRef stx <| p stx; true) (fun _ => false) then
+    if ← catchInternalId unsupportedSyntaxExceptionId (do withRef stx <| p stx; pure true) (fun _ => pure false) then
       return
   if stx.isAnyAntiquot then
     return
@@ -131,6 +131,6 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do
 @[builtinTermElab precheckedQuot] def elabPrecheckedQuot : TermElab := fun stx expectedType? => do
   let singleQuot := stx[1]
   runPrecheck singleQuot.getQuotContent
-  adaptExpander (fun _ => singleQuot) stx expectedType?
+  adaptExpander (fun _ => pure singleQuot) stx expectedType?
 
 end Lean.Elab.Term.Quotation
diff --git a/src/Lean/Elab/Quotation/Util.lean b/src/Lean/Elab/Quotation/Util.lean
index 684a6004e1..74e5e50946 100644
--- a/src/Lean/Elab/Quotation/Util.lean
+++ b/src/Lean/Elab/Quotation/Util.lean
@@ -27,9 +27,9 @@ partial def getPatternVars (stx : Syntax) : TermElabM (Array Syntax) :=
   if stx.isQuot then
     getAntiquotationIds stx
   else match stx with
-    | `(_)            => #[]
-    | `($id:ident)    => #[id]
-    | `($id:ident@$e) => do (← getPatternVars e).push id
+    | `(_)            => return #[]
+    | `($id:ident)    => return #[id]
+    | `($id:ident@$e) => return (← getPatternVars e).push id
     | _               => throwErrorAt stx "unsupported pattern in syntax match{indentD stx}"
 
 partial def getPatternsVars (pats : Array Syntax) : TermElabM (Array Syntax) :=
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 8630cad04b..7a964b88c3 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -450,7 +450,7 @@ private def getFieldIdx (structName : Name) (fieldNames : Array Name) (fieldName
   | none     => throwError "field '{fieldName}' is not a valid field of '{structName}'"
 
 def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (Option Syntax) := do
-  if (← findField? (← getEnv) structName fieldName).isNone then
+  if (findField? (← getEnv) structName fieldName).isNone then
     return none
   return some $ mkNode ``Lean.Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]
 
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 3526378e5c..3227436d6e 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -291,18 +291,18 @@ private def getFieldType (infos : Array StructFieldInfo) (parentStructName : Nam
     let visit (e : Expr) : MetaM TransformStep := do
       if let Expr.const subProjName .. := e.getAppFn then
         if let some { ctorName, numParams, .. } ← getProjectionFnInfo? subProjName then
-          let Name.str subStructName subFieldName .. ← subProjName
+          let Name.str subStructName subFieldName .. := subProjName
             | throwError "invalid projection name {subProjName}"
           let args := e.getAppArgs
           if args.get? numParams == parent then
-            let some existingFieldInfo ← findFieldInfo? infos subFieldName
+            let some existingFieldInfo := findFieldInfo? infos subFieldName
               | throwError "unexpected field access to {fieldName} in{indentExpr e}"
             return TransformStep.done <| mkAppN existingFieldInfo.fvar args[numParams+1:args.size]
       return TransformStep.done e
     let projType ← Meta.transform projType (post := visit)
     if projType.containsFVar parent.fvarId! then
       throwError "unsupported dependent field in {fieldName} : {projType}"
-    projType
+    return projType
 
 private def toVisibility (fieldInfo : StructureFieldInfo) : CoreM Visibility := do
   if isProtected (← getEnv) fieldInfo.projFn then
@@ -394,7 +394,7 @@ where
       if h : i < fieldNames.size then
         let fieldName := fieldNames.get ⟨i, h⟩
         let fieldType ← getFieldType infos parentStructName parentType fieldName
-        match (← findFieldInfo? infos fieldName) with
+        match findFieldInfo? infos fieldName with
         | some existingFieldInfo =>
           let existingFieldType ← inferType existingFieldInfo.fvar
           unless (← isDefEq fieldType existingFieldType) do
@@ -402,7 +402,7 @@ where
           /- Remark: if structure has a default value for this field, it will be set at the `processOveriddenDefaultValues` below. -/
           copy (i+1) infos (fieldMap.insert fieldName existingFieldInfo.fvar) expandedStructNames
         | none =>
-          let some fieldInfo ← getFieldInfo? (← getEnv) parentStructName fieldName | unreachable!
+          let some fieldInfo := getFieldInfo? (← getEnv) parentStructName fieldName | unreachable!
           let addNewField : TermElabM α := do
             let value? ← copyDefaultValue? fieldMap expandedStructNames parentStructName fieldName
             withLocalDecl fieldName fieldInfo.binderInfo fieldType fun fieldFVar => do
@@ -727,7 +727,7 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
   let env ← getEnv
   let structName := view.declName
   let sourceFieldNames := getStructureFieldsFlattened env structName
-  let structType ← mkAppN (Lean.mkConst structName (levelParams.map mkLevelParam)) params
+  let structType := mkAppN (Lean.mkConst structName (levelParams.map mkLevelParam)) params
   let Expr.const parentStructName us _ ← pure parentType.getAppFn | unreachable!
   let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
   withLocalDecl `self binfo structType fun source => do
@@ -743,7 +743,7 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
           result := mkApp result fieldVal
         else
           -- fieldInfo must be a field of `parentStructName`
-          let some fieldInfo ← getFieldInfo? env parentStructName fieldName | unreachable!
+          let some fieldInfo := getFieldInfo? env parentStructName fieldName | unreachable!
           if fieldInfo.subobject?.isNone then throwError "failed to build coercion to parent structure"
           let resultType ← whnfD (← inferType result)
           unless resultType.isForall do throwError "failed to build coercion to parent structure, unexpect type{indentExpr resultType}"
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 16d69fb357..7618b21829 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -115,7 +115,7 @@ where
       /- Convert `candidates` in a list of pairs `(c, isDescr)`, where `c` is the parser name,
          and `isDescr` is true iff `c` has type `Lean.ParserDescr` or `Lean.TrailingParser` -/
       let env ← getEnv
-      candidates.filterMap fun c =>
+      return candidates.filterMap fun c =>
          match env.find? c with
          | none      => none
          | some info =>
@@ -312,7 +312,7 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
   let precDefault  := if isAtomLikeSyntax syntaxParser then Parser.maxPrec else Parser.leadPrec
   let prec ← match prec? with
     | some prec => liftMacroM <| evalPrec prec
-    | none      => precDefault
+    | none      => pure precDefault
   let name ← match name? with
     | some name => pure name.getId
     | none => liftMacroM <| mkNameFromParserSyntax cat syntaxParser
@@ -366,11 +366,11 @@ def expandNoKindMacroRulesAux (alts : Array Syntax) (cmdName : String) (mkCmd :
     if altsNotK.isEmpty then
       mkCmd k altsK
     else
-      mkNullNode #[← mkCmd k altsK, ← mkCmd none altsNotK]
+      return mkNullNode #[← mkCmd k altsK, ← mkCmd none altsNotK]
 
 def strLitToPattern (stx: Syntax) : MacroM Syntax :=
   match stx.isStrLit? with
-  | some str => pure $ mkAtomFrom stx str
+  | some str => return mkAtomFrom stx str
   | none     => Macro.throwUnsupported
 
 builtin_initialize
diff --git a/src/Lean/Elab/Tactic/Conv/Pattern.lean b/src/Lean/Elab/Tactic/Conv/Pattern.lean
index b4cd78427b..bee3586bde 100644
--- a/src/Lean/Elab/Tactic/Conv/Pattern.lean
+++ b/src/Lean/Elab/Tactic/Conv/Pattern.lean
@@ -28,7 +28,7 @@ partial def matchPattern? (pattern : AbstractMVarsResult) (e : Expr) : MetaM (Op
       else if (← isDefEqGuarded pattern e) then
         return some (e, #[])
       else if e.isApp then
-        (← go? e.appFn!).map fun (f, extra) => (f, extra.push e.appArg!)
+        return (← go? e.appFn!).map fun (f, extra) => (f, extra.push e.appArg!)
       else
         return none
     withReducible <| go? e
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index ea9a0b897c..a3a32370f4 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -194,7 +194,7 @@ def evalAlts (elimInfo : ElimInfo) (alts : Array (Name × MVarId)) (optPreTac :
   let hasAlts := altsSyntax.size > 0
   if hasAlts then
     -- default to initial state outside of alts
-    withInfoContext go initialInfo
+    withInfoContext go (pure initialInfo)
   else go
 where
   go := do
@@ -243,7 +243,7 @@ where
             else
               throwError "alternative '{altName}' is not needed"
           let altVarNames := getAltVarNames altStx
-          let numFieldsToName ← if altHasExplicitModifier altStx then numFields else getNumExplicitFields altMVarId numFields
+          let numFieldsToName ← if altHasExplicitModifier altStx then pure numFields else getNumExplicitFields altMVarId numFields
           trace[Meta.debug] "numFields: {numFields}, numFieldsToName: {numFieldsToName}, altNames: {altVarNames.size}"
           if altVarNames.size > numFieldsToName then
             logError m!"too many variable names provided at alternative '{altName}', #{altVarNames.size} provided, but #{numFieldsToName} expected"
@@ -408,7 +408,7 @@ def elabCasesTargets (targets : Array Syntax) : TacticM (Array Expr) :=
       return args.map (·.expr)
     else
       liftMetaTacticAux fun mvarId => do
-        let argsToGeneralize ← args.filter fun arg => !(arg.expr.isFVar && arg.hName?.isNone)
+        let argsToGeneralize := args.filter fun arg => !(arg.expr.isFVar && arg.hName?.isNone)
         let (fvarIdsNew, mvarId) ← generalize mvarId argsToGeneralize
         let mut result := #[]
         let mut j := 0
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 0b9cd2d980..ca15f6cd15 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -132,7 +132,7 @@ private def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool)
         if arg.getKind == ``Lean.Parser.Tactic.simpErase then
           if eraseLocal && (← Term.isLocalIdent? arg[1]).isSome then
             -- We use `eraseCore` because the simp lemma for the hypothesis was not added yet
-            lemmas ← lemmas.eraseCore arg[1].getId
+            lemmas := lemmas.eraseCore arg[1].getId
           else
             let declName ← resolveGlobalConstNoOverloadWithInfo arg[1]
             lemmas ← lemmas.erase declName
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 827535fff0..aa1ab4af62 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -831,7 +831,7 @@ private def tryLiftAndCoe (errorMsgHeader? : Option String) (expectedType : Expr
         let v ← getLevel β
         let coeTInstType := Lean.mkForall `a BinderInfo.default α $ mkAppN (mkConst ``CoeT [u, v]) #[α, mkBVar 0, β]
         let coeTInstVal ← synthesizeInst coeTInstType
-        let eNew ← expandCoe (← mkAppN (Lean.mkConst ``Lean.Internal.liftCoeM [u_1, u_2, u_3]) #[m, n, α, β, monadLiftVal, coeTInstVal, monadInst, e])
+        let eNew ← expandCoe (mkAppN (Lean.mkConst ``Lean.Internal.liftCoeM [u_1, u_2, u_3]) #[m, n, α, β, monadLiftVal, coeTInstVal, monadInst, e])
         let eNewType ← inferType eNew
         unless (← isDefEq expectedType eNewType) do throwMismatch
         return eNew -- approach 3 worked
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index b4db28b40f..01de1dad2c 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -153,8 +153,8 @@ def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEn
     -- TODO: record recursive expansions in info tree?
     expandMacro?     := fun stx => do
       match (← expandMacroImpl? env stx) with
-      | some (_, Except.ok stx) => some stx
-      | _                       => none
+      | some (_, Except.ok stx) => return some stx
+      | _                       => return none
     hasDecl          := fun declName => return env.contains declName
     getCurrNamespace := return currNamespace
     resolveNamespace? := fun n => return ResolveName.resolveNamespace? env currNamespace openDecls n
@@ -190,7 +190,7 @@ partial def mkUnusedBaseName (baseName : Name) : MacroM Name := do
        if ← Macro.hasDecl (currNamespace ++ name) then
          loop (idx+1)
        else
-         name
+         return name
     loop 1
   else
     return baseName
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index d6fe85ef52..0c5f40faa6 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -564,7 +564,7 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st
   for mod in mods do
     for extDescr in pExtDescrs[startingAt:] do
       let entries := getEntriesFor mod extDescr.name 0
-      env ← extDescr.toEnvExtension.modifyState env fun s => { s with importedEntries := s.importedEntries.push entries }
+      env := extDescr.toEnvExtension.modifyState env fun s => { s with importedEntries := s.importedEntries.push entries }
   return env
 
 /--
@@ -592,7 +592,7 @@ where
       let prevSize := (← persistentEnvExtensionsRef.get).size
       let prevAttrSize ← getNumBuiltiAttributes
       let newState ← extDescr.addImportedFn s.importedEntries { env := env, opts := opts }
-      let mut env ← extDescr.toEnvExtension.setState env { s with state := newState }
+      let mut env := extDescr.toEnvExtension.setState env { s with state := newState }
       env ← ensureExtensionsArraySize env
       if (← persistentEnvExtensionsRef.get).size > prevSize || (← getNumBuiltiAttributes) > prevAttrSize then
         -- This branch is executed when `pExtDescrs[i]` is the extension associated with the `init` attribute, and
diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean
index db41efb8d2..4c3611e7b2 100644
--- a/src/Lean/Hygiene.lean
+++ b/src/Lean/Hygiene.lean
@@ -30,9 +30,9 @@ structure Unhygienic.Context where
 abbrev Unhygienic := ReaderT Lean.Unhygienic.Context <| StateM MacroScope
 namespace Unhygienic
 instance : MonadQuotation Unhygienic where
-  getRef              := do (← read).ref
+  getRef              := return (← read).ref
   withRef             := fun ref => withReader ({ · with ref := ref })
-  getCurrMacroScope   := do (← read).scope
+  getCurrMacroScope   := return (← read).scope
   getMainModule       := pure `UnhygienicMain
   withFreshMacroScope := fun x => do
     let fresh ← modifyGet fun n => (n, n + 1)
diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean
index 0d9779546f..4c41fefb3e 100644
--- a/src/Lean/KeyedDeclsAttribute.lean
+++ b/src/Lean/KeyedDeclsAttribute.lean
@@ -135,7 +135,7 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDe
     name            := df.name
     descr           := df.descr
     erase           := fun declName => do
-      let s ← ext.getState (← getEnv)
+      let s := ext.getState (← getEnv)
       let s ← s.erase df.name declName
       modifyEnv fun env => ext.modifyState env fun _ => s
     add             := fun declName stx attrKind => do
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index db26a8c6e5..4300f597b8 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -284,7 +284,7 @@ def getAt? (lctx : LocalContext) (i : Nat) : Option LocalDecl :=
 
 instance : ForIn m LocalContext LocalDecl where
   forIn lctx init f := lctx.decls.forIn init fun d? b => match d? with
-    | none   => ForInStep.yield b
+    | none   => return ForInStep.yield b
     | some d => f d b
 
 @[inline] def foldl (lctx : LocalContext) (f : β → LocalDecl → β) (init : β) (start : Nat := 0) : β :=
diff --git a/src/Lean/Meta/ACLt.lean b/src/Lean/Meta/ACLt.lean
index bcd9c7a4d3..bdef55613e 100644
--- a/src/Lean/Meta/ACLt.lean
+++ b/src/Lean/Meta/ACLt.lean
@@ -45,7 +45,7 @@ mutual
 -/
 unsafe def lt (a b : Expr) : MetaM Bool :=
   if ptrAddrUnsafe a == ptrAddrUnsafe b then
-    false
+    return false
   -- We ignore metadata
   else if a.isMData then
     lt a.mdataExpr! b
@@ -95,14 +95,14 @@ where
   lexSameCtor (a b : Expr) : MetaM Bool :=
     match a with
     -- Atomic
-    | Expr.bvar i ..    => i < b.bvarIdx!
-    | Expr.fvar id ..   => Name.lt id.name b.fvarId!.name
-    | Expr.mvar id ..   => Name.lt id.name b.mvarId!.name
-    | Expr.sort u ..    => Level.normLt u b.sortLevel!
-    | Expr.const n ..   => Name.lt n b.constName! -- We igore the levels
-    | Expr.lit v ..     => Literal.lt v b.litValue!
+    | Expr.bvar i ..    => return i < b.bvarIdx!
+    | Expr.fvar id ..   => return Name.lt id.name b.fvarId!.name
+    | Expr.mvar id ..   => return Name.lt id.name b.mvarId!.name
+    | Expr.sort u ..    => return Level.normLt u b.sortLevel!
+    | Expr.const n ..   => return Name.lt n b.constName! -- We igore the levels
+    | Expr.lit v ..     => return Literal.lt v b.litValue!
     -- Composite
-    | Expr.proj _ i e ..    => if i != b.projIdx! then i < b.projIdx! else lt e b.projExpr!
+    | Expr.proj _ i e ..    => if i != b.projIdx! then return i < b.projIdx! else lt e b.projExpr!
     | Expr.app ..           => ltApp a b
     | Expr.lam _ d e ..     => ltPair d e b.bindingDomain! b.bindingBody!
     | Expr.forallE _ d e .. => ltPair d e b.bindingDomain! b.bindingBody!
diff --git a/src/Lean/Meta/AbstractMVars.lean b/src/Lean/Meta/AbstractMVars.lean
index 6813105b78..34ac3d0bfa 100644
--- a/src/Lean/Meta/AbstractMVars.lean
+++ b/src/Lean/Meta/AbstractMVars.lean
@@ -84,7 +84,7 @@ partial def abstractExprMVars (e : Expr) : M Expr := do
       if decl.depth != s.mctx.depth then
         return e
       else
-        let (eNew, mctxNew) ← s.mctx.instantiateMVars e
+        let (eNew, mctxNew) := s.mctx.instantiateMVars e
         if e != eNew then
           modify fun s => { s with mctx := mctxNew }
           abstractExprMVars eNew
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index 4cf14d1d0a..e70f5d00e0 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -120,10 +120,10 @@ def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr) : MetaM MessageDat
     let expectedTypeType ← inferType expectedType
     let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
     let (givenTypeType, expectedTypeType) ← addPPExplicitToExposeDiff givenTypeType expectedTypeType
-    m!"has type{indentD m!"{givenType} : {givenTypeType}"}\nbut is expected to have type{indentD m!"{expectedType} : {expectedTypeType}"}"
+    return m!"has type{indentD m!"{givenType} : {givenTypeType}"}\nbut is expected to have type{indentD m!"{expectedType} : {expectedTypeType}"}"
   catch _ =>
     let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
-    m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}"
+    return m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}"
 
 def throwAppTypeMismatch {α} (f a : Expr) (extraMsg : MessageData := Format.nil) : MetaM α := do
   let (expectedType, binfo) ← getFunctionDomain f
diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index 87f89752e4..ca4cb158a0 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -446,11 +446,11 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
           return result
       let visitNonStar (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
         match findKey cs k with
-        | none   => result
+        | none   => return result
         | some c => getMatchLoop (todo ++ args) c.2 result
       let result ← visitStar result
       match k with
-      | Key.star  => result
+      | Key.star  => return result
       /-
         Recall that dependent arrows are `(Key.other, #[])`, and non-dependent arrows are `(Key.arrow, #[a, b])`.
         A non-dependent arrow may be an instance of a dependent arrow (stored at `DiscrTree`). Thus, we also visit the `Key.other` child.
@@ -534,7 +534,7 @@ where
             return result
         let visitNonStar (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
           match findKey cs k with
-          | none   => result
+          | none   => return result
           | some c => process 0 (todo ++ args) c.2 result
         match k with
         | Key.star  => cs.foldlM (init := result) fun result ⟨k, c⟩ => process k.arity todo c result
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index c8d32f357b..19550af0eb 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -341,9 +341,9 @@ where
         | _ => pure ()
       return false
     if xs.size <= 1 then
-      pure false
+      return false
     else
-      check (← getLCtx)
+      return check (← getLCtx)
 
   /- Traverse `e` and stores in the state `NameHashSet` any let-declaration with index greater than `(← read)`.
      The context `Nat` is the position of `xs[0]` in the local context. -/
@@ -1511,7 +1511,7 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
   whenUndefDo (isDefEqDelta t s) do
   if t.isConst && s.isConst then
     if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else return false
-  else if (← t.isApp <&&> s.isApp <&&> isDefEqApp t s) then
+  else if (← pure t.isApp <&&> pure s.isApp <&&> isDefEqApp t s) then
     return true
   else
     whenUndefDo (isDefEqStringLit t s) do
diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean
index e0c5c19122..853cd4617e 100644
--- a/src/Lean/Meta/IndPredBelow.lean
+++ b/src/Lean/Meta/IndPredBelow.lean
@@ -55,15 +55,15 @@ def mkContext (declName : Name) : MetaM Context := do
   let indVal ← getConstInfoInduct declName
   let typeInfos ← indVal.all.toArray.mapM getConstInfoInduct
   let motiveTypes ← typeInfos.mapM motiveType
-  let motives ← motiveTypes.mapIdxM fun j motive => do
-    (← motiveName motiveTypes j.val, motive)
+  let motives ← motiveTypes.mapIdxM fun j motive =>
+    return (← motiveName motiveTypes j.val, motive)
   let headers ← typeInfos.mapM $ mkHeader motives indVal.numParams
   return {
     motives := motives
     typeInfos := typeInfos
     numParams := indVal.numParams
     headers := headers
-    belowNames := (← indVal.all.toArray.map (· ++ `below))
+    belowNames := indVal.all.toArray.map (· ++ `below)
   }
 where
   motiveName (motiveTypes : Array Expr) (i : Nat) : MetaM Name :=
@@ -108,14 +108,14 @@ partial def mkCtorType
 where
   addHeaderVars (vars : Variables) := do
     let headersWithNames ← ctx.headers.mapIdxM fun idx header =>
-      (ctx.belowNames[idx], fun _ : Array Expr => pure header)
+      return (ctx.belowNames[idx], fun _ : Array Expr => pure header)
 
     withLocalDeclsD headersWithNames fun xs =>
       addMotives { vars with indVal := xs }
 
   addMotives (vars : Variables) := do
     let motiveBuilders ← ctx.motives.mapM fun (motiveName, motiveType) =>
-      (motiveName, BinderInfo.implicit, fun _ : Array Expr =>
+      return (motiveName, BinderInfo.implicit, fun _ : Array Expr =>
         instantiateForall motiveType vars.params)
     withLocalDecls motiveBuilders fun xs =>
       modifyBinders { vars with target := vars.target ++ xs, motives := xs } 0
@@ -141,7 +141,7 @@ where
       let innerType := mkAppN vars.indVal[belowIdx] $
         vars.params ++ vars.motives ++ args[ctx.numParams:] ++ #[hApp]
       let x ← mkForallFVars vars.target innerType
-      replaceTempVars vars x
+      return replaceTempVars vars x
 
   replaceTempVars (vars : Variables) (ctor : Expr) :=
     let levelParams :=
@@ -152,11 +152,11 @@ where
 
   checkCount (domain : Expr) : MetaM Bool := do
     let run (x : StateRefT Nat MetaM Expr) : MetaM (Expr × Nat) := StateRefT'.run x 0
-    let (_, cnt) ← run $ transform domain fun e => do
+    let (_, cnt) ← run <| transform domain fun e => do
       if let some name := e.constName? then
         if let some idx := ctx.typeInfos.findIdx? fun indVal => indVal.name == name then
           modify (. + 1)
-      TransformStep.visit e
+      return TransformStep.visit e
 
     if cnt > 1 then
       throwError "only arrows are allowed as premises. Multiple recursive occurrences detected:{indentExpr domain}"
@@ -225,21 +225,21 @@ def mkInductiveType
 
 def mkBelowDecl (ctx : Context) : MetaM Declaration := do
   let lparams := ctx.typeInfos[0].levelParams
-  Declaration.inductDecl
+  return Declaration.inductDecl
     lparams
     (ctx.numParams + ctx.motives.size)
     (←ctx.typeInfos.mapIdxM $ mkInductiveType ctx).toList
     ctx.typeInfos[0].isUnsafe
 
 partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do
-  if depth = 0 then false
+  if depth = 0 then return false
   else
     withMVarContext m do
     let lctx ← getLCtx
     let mTy ← getMVarType m
     lctx.anyM fun localDecl =>
       if localDecl.isAuxDecl then
-        false
+        return false
       else
         commitWhen do
         let (mvars, _, t) ← forallMetaTelescope localDecl.type
@@ -247,7 +247,7 @@ partial def backwardsChaining (m : MVarId) (depth : Nat) : MetaM Bool := do
           assignExprMVar m (mkAppN localDecl.toExpr mvars)
           mvars.allM fun v =>
             isExprMVarAssigned v.mvarId! <||> backwardsChaining v.mvarId! (depth - 1)
-        else false
+        else return false
 
 partial def proveBrecOn (ctx : Context) (indVal : InductiveVal) (type : Expr) : MetaM Expr := do
   let main ← mkFreshExprSyntheticOpaqueMVar type
@@ -270,8 +270,8 @@ where
 
   applyIH (m : MVarId) (vars : BrecOnVariables) : MetaM (List MVarId) := do
     match (← vars.indHyps.findSomeM?
-      fun ih => do try some $ (←apply m $ mkFVar ih) catch ex => none) with
-    | some goals => goals
+      fun ih => do try pure <| some <| (←apply m $ mkFVar ih) catch ex => pure none) with
+    | some goals => pure goals
     | none => throwError "cannot apply induction hypothesis: {MessageData.ofGoal m}"
 
   induction (m : MVarId) (vars : BrecOnVariables) : MetaM (List MVarId) := do
@@ -287,7 +287,7 @@ where
       if recursorInfo.numLevelParams > levelParams.length
       then levelZero::levelParams
       else levelParams
-    let recursor ← mkAppN (mkConst recursorInfo.name $ recLevels) $ params ++ motives
+    let recursor := mkAppN (mkConst recursorInfo.name $ recLevels) $ params ++ motives
     apply m recursor
 
   applyCtors (ms : List MVarId) : MetaM $ List MVarId := do
@@ -305,7 +305,7 @@ where
     return mss.foldr List.append []
 
   introNPRec (m : MVarId) : MetaM MVarId := do
-    if (← getMVarType m).isForall then introNPRec (←intro1P m).2 else m
+    if (← getMVarType m).isForall then introNPRec (←intro1P m).2 else return m
 
   closeGoal (vars : BrecOnVariables) (maxDepth : Nat) (m : MVarId) : MetaM Unit := do
     unless (← isExprMVarAssigned m) do
@@ -318,7 +318,7 @@ def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do
   let type ← mkType
   let indVal := ctx.typeInfos[idx]
   let name := indVal.name ++ brecOnSuffix
-  Declaration.thmDecl {
+  return Declaration.thmDecl {
     name := name
     levelParams := indVal.levelParams
     type := type
@@ -352,7 +352,7 @@ where
         let conclusion :=
           mkAppN motives[idx] ys
         mkForallFVars ys (←mkArrow premise conclusion)
-    (←name, mkDomain)
+    return (←name, mkDomain)
 
 /-- Given a constructor name, find the indices of the corresponding `below` version thereof. -/
 partial def getBelowIndices (ctorName : Name) : MetaM $ Array Nat := do
@@ -368,7 +368,7 @@ where
       (rest : Expr)
       (belowIndices : Array Nat)
       (xIdx yIdx : Nat) : MetaM $ Array Nat := do
-    if xIdx ≥ xs.size then belowIndices else
+    if xIdx ≥ xs.size then return belowIndices else
     let x := xs[xIdx]
     let xTy ← inferType x
     let yTy := rest.bindingDomain!
@@ -385,7 +385,7 @@ private def belowType (motive : Expr) (xs : Array Expr) (idx : Nat) : MetaM $ Na
     let indInfo ← getConstInfoInduct indName
     let belowArgs := args[:indInfo.numParams] ++ #[motive] ++ args[indInfo.numParams:] ++ #[xs[idx]]
     let belowType := mkAppN (mkConst (indName ++ `below) type.constLevels!) belowArgs
-    (indName, belowType)
+    return (indName, belowType)
 
 /-- This function adds an additional `below` discriminant to a matcher application.
     It is used for modifying the patterns, such that the structural recursion can use the new
@@ -414,7 +414,7 @@ partial def mkBelowMatcher
       withLocalDeclD (←mkFreshUserName `h_below) belowType fun h_below => do
       mkForallFVars (xs.push h_below) t
     let motive ← newMotive belowType xs
-    (indName, belowType.replaceFVars xs matcherApp.discrs, motive, matchType)
+    pure (indName, belowType.replaceFVars xs matcherApp.discrs, motive, matchType)
 
   let lhss ← mkMatcherInput.lhss.mapM $ addBelowPattern indName
   let alts ← mkMatcherInput.lhss.zip lhss |>.toArray.zip matcherApp.alts |>.mapIdxM fun idx ((oldLhs, lhs), alt) => do
@@ -431,12 +431,12 @@ partial def mkBelowMatcher
     trace[Meta.IndPredBelow.match] "xs = {xs}; oldFVars = {oldFVars.map (·.toExpr)}; fvars = {fvars}; new = {fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:]}"
     let newAlt ← mkLambdaFVars (fvars[:oldFVars.size] ++ xs[oldFVars.size:] ++ fvars[oldFVars.size:]) t
     trace[Meta.IndPredBelow.match] "alt {idx}:\n{alt} ↦ {newAlt}"
-    newAlt
+    pure newAlt
 
   let matcherName ← mkFreshUserName mkMatcherInput.matcherName
   withExistingLocalDecls (lhss.foldl (init := []) fun s v => s ++ v.fvarDecls) do
     for lhs in lhss do
-      trace[Meta.IndPredBelow.match] "{←lhs.patterns.mapM (·.toMessageData)}"
+      trace[Meta.IndPredBelow.match] "{lhs.patterns.map (·.toMessageData)}"
   let res ← Match.mkMatcher { matcherName, matchType, numDiscrs := (mkMatcherInput.numDiscrs + 1), lhss }
   res.addMatcher
   -- if a wrong index is picked, the resulting matcher can be type-incorrect.
@@ -446,7 +446,7 @@ partial def mkBelowMatcher
   let newApp := mkApp res.matcher motive
   let newApp := mkAppN newApp $ matcherApp.discrs.push below
   let newApp := mkAppN newApp alts
-  (newApp, res.addMatcher)
+  return (newApp, res.addMatcher)
 
 where
   addBelowPattern (indName : Name) (lhs : AltLHS) : MetaM AltLHS := do
@@ -457,7 +457,7 @@ where
     withExistingLocalDecls fVars.toList do
     let patterns := patterns.push belowPattern
     let patterns := patterns.set! idx (←toInaccessible originalPattern)
-    { lhs with patterns := patterns.toList, fvarDecls := lhs.fvarDecls ++ fVars.toList }
+    return { lhs with patterns := patterns.toList, fvarDecls := lhs.fvarDecls ++ fVars.toList }
 
   /--
     this function changes the type of the pattern from the original type to the `below` version thereof.
@@ -500,18 +500,18 @@ where
       withExistingLocalDecls additionalFVars.toList do
       let ctor := Pattern.ctor belowCtor.name us belowParams.toList belowFields.toList
       trace[Meta.IndPredBelow.match] "{originalPattern.toMessageData} ↦ {ctor.toMessageData}"
-      (additionalFVars, ctor)
+      return (additionalFVars, ctor)
     | Pattern.as varId p hId =>
       let (additionalFVars, p) ← convertToBelow indName p
-      (additionalFVars, Pattern.as varId p hId)
+      return (additionalFVars, Pattern.as varId p hId)
     | Pattern.var varId =>
       let var := mkFVar varId
       (←inferType var).withApp fun ind args => do
       let (_, tgtType) ← belowType belowMotive #[var] 0
       withLocalDeclD (←mkFreshUserName `h) tgtType fun h => do
       let localDecl ← getFVarLocalDecl h
-      (#[localDecl], Pattern.var h.fvarId!)
-    | p => (#[], p)
+      return (#[localDecl], Pattern.var h.fvarId!)
+    | p => return (#[], p)
 
   transformFields belowCtor indName belowFieldOpts :=
     let rec loop
@@ -519,7 +519,7 @@ where
       (belowFieldOpts : Array $ Option Pattern)
       (belowFields : Array Pattern)
       (additionalFVars : Array LocalDecl) : MetaM (Array LocalDecl × Array Pattern) := do
-      if belowFields.size ≥ belowFieldOpts.size then (additionalFVars, belowFields) else
+      if belowFields.size ≥ belowFieldOpts.size then pure (additionalFVars, belowFields) else
       if let some belowField := belowFieldOpts[belowFields.size] then
         let belowFieldExpr ← belowField.toExpr
         let belowCtor := mkApp belowCtor belowFieldExpr
@@ -545,17 +545,17 @@ where
     loop belowCtor belowFieldOpts #[] #[]
 
   toInaccessible : Pattern → MetaM Pattern
-  | Pattern.inaccessible p => Pattern.inaccessible p
-  | Pattern.var v => Pattern.var v
-  | p => do Pattern.inaccessible $ ←p.toExpr
+  | Pattern.inaccessible p => return Pattern.inaccessible p
+  | Pattern.var v => return Pattern.var v
+  | p => return Pattern.inaccessible $ ←p.toExpr
 
   newMotive (belowType : Expr) (ys : Array Expr) : MetaM Expr :=
     lambdaTelescope matcherApp.motive fun xs t => do
     let numDiscrs := matcherApp.discrs.size
-    withLocalDeclD (←mkFreshUserName `h_below) (←belowType.replaceFVars ys xs) fun h_below => do
+    withLocalDeclD (←mkFreshUserName `h_below) (belowType.replaceFVars ys xs) fun h_below => do
     let motive ← mkLambdaFVars (xs[:numDiscrs] ++ #[h_below] ++ xs[numDiscrs:]) t
     trace[Meta.IndPredBelow.match] "motive := {motive}"
-    motive
+    return motive
 
 def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat) := do
   xs.findSomeM? fun x => do
@@ -570,13 +570,13 @@ def findBelowIdx (xs : Array Expr) (motive : Expr) : MetaM $ Option (Expr × Nat
         trace[Meta.IndPredBelow.match] "{←Meta.ppGoal below.mvarId!}"
         if (← backwardsChaining below.mvarId! 10) then
           trace[Meta.IndPredBelow.match] "Found below term in the local context: {below}"
-          if (← xs.anyM (isDefEq below)) then none else (below, idx.val)
+          if (← xs.anyM (isDefEq below)) then pure none else pure (below, idx.val)
         else
           trace[Meta.IndPredBelow.match] "could not find below term in the local context"
-          none
-      catch _ => none
-    else none
-  | _, _ => none
+          pure none
+      catch _ => pure none
+    else pure none
+  | _, _ => pure none
 
 def mkBelow (declName : Name) : MetaM Unit := do
   if (← isInductivePredicate declName) then
diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean
index 14b73888b4..aedabf4b7d 100644
--- a/src/Lean/Meta/Injective.lean
+++ b/src/Lean/Meta/Injective.lean
@@ -46,7 +46,7 @@ private partial def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useE
             eqs := eqs.push (← mkEq arg1 arg2)
           else
             eqs := eqs.push (← mkHEq arg1 arg2)
-      if let some andEqs ← mkAnd? eqs then
+      if let some andEqs := mkAnd? eqs then
         let result ←
           if useEq then
             mkEq eq andEqs
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index bfa7811aed..84b7582813 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -41,7 +41,7 @@ def Instances.eraseCore (d : Instances) (declName : Name) : Instances :=
 def Instances.erase [Monad m] [MonadError m] (d : Instances) (declName : Name) : m Instances := do
   unless d.instanceNames.contains declName do
     throwError "'{declName}' does not have [instance] attribute"
-  d.eraseCore declName
+  return d.eraseCore declName
 
 builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry Instances ←
   registerSimpleScopedEnvExtension {
@@ -70,7 +70,7 @@ builtin_initialize
       let prio ← getAttrParamOptPrio stx[1]
       discard <| addInstance declName attrKind prio |>.run {} {}
     erase := fun declName => do
-      let s ← instanceExtension.getState (← getEnv)
+      let s := instanceExtension.getState (← getEnv)
       let s ← s.erase declName
       modifyEnv fun env => instanceExtension.modifyState env fun _ => s
   }
diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean
index 0e93b64579..42674114b9 100644
--- a/src/Lean/Meta/LevelDefEq.lean
+++ b/src/Lean/Meta/LevelDefEq.lean
@@ -66,7 +66,7 @@ mutual
         return LBool.true
       else
         return LBool.undef
-    | _, Level.mvar .. => LBool.undef -- Let `solve v u` to handle this case
+    | _, Level.mvar .. => return LBool.undef -- Let `solve v u` to handle this case
     | Level.zero _, Level.max v₁ v₂ _ =>
       Bool.toLBool <$> (isLevelDefEqAux levelZero v₁ <&&> isLevelDefEqAux levelZero v₂)
     | Level.zero _, Level.imax _ v₂ _ =>
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index e20a63e0f0..75ed558f7b 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -186,7 +186,7 @@ private def processAsPattern (p : Problem) : MetaM Problem :=
           we the pattern `(vec.cons n h t)`. TODO: try to find a cleaner solution.
          -/
         let r ← mkEqRefl x
-        { alt with patterns := p :: ps }.replaceFVarId fvarId x |>.replaceFVarId h r
+        pure <| { alt with patterns := p :: ps }.replaceFVarId fvarId x |>.replaceFVarId h r
       | _ => pure alt
     pure { p with alts := alts }
 
@@ -715,7 +715,7 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
   let mkMatcherConst name :=
     mkAppN (mkConst name result.levelArgs.toList) result.exprArgs
   match (matcherExt.getState env).find? (result.value, compile) with
-  | some nameNew => (mkMatcherConst nameNew, none)
+  | some nameNew => pure (mkMatcherConst nameNew, none)
   | none =>
     let decl := Declaration.defnDecl {
       name
@@ -733,8 +733,7 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
       setInlineAttribute name
       if compile then
         compileDecl decl
-    (mkMatcherConst name, some addMatcher)
-
+    return (mkMatcherConst name, some addMatcher)
 
 structure MkMatcherInput where
   matcherName : Name
@@ -798,7 +797,7 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult :=
           altNumParams := minors.map Prod.snd,
           uElimPos? }
         |> addMatcher
-      | none => ()
+      | none => pure ()
 
     trace[Meta.Match.debug] "matcher: {matcher}"
     let unusedAltIdxs := lhss.length.fold (init := []) fun i r =>
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index b1f7262b49..86c190b4f5 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -103,7 +103,7 @@ where
         let typeNew := b.instantiate1 y
         if let some (_, lhs, rhs) ← matchEq? d then
           if lhs.isFVar && ys.contains lhs && args.contains lhs && isNamedPatternProof typeNew y then
-             let some i  ← ys.getIdx? lhs | unreachable!
+             let some i  := ys.getIdx? lhs | unreachable!
              let ys      := ys.eraseIdx i
              let mask    := mask.set! i false
              let args    := args.map fun arg => if arg == lhs then rhs else arg
@@ -445,7 +445,7 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
       let splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew
       let splitterType ← mkForallFVars splitterParams matchResultType
       trace[Meta.Match.matchEqs] "splitterType: {splitterType}"
-      let template ← mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
+      let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
       let template ← deltaExpand template (. == constInfo.name)
       let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew altArgMasks)
       let splitterName := baseName ++ `splitter
diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean
index cabaa53194..14c9b2830c 100644
--- a/src/Lean/Meta/Offset.lean
+++ b/src/Lean/Meta/Offset.lean
@@ -99,8 +99,8 @@ private partial def isOffset : Expr → OptionT MetaM (Expr × Nat)
 
 private def isNatZero (e : Expr) : MetaM Bool := do
   match (← evalNat e) with
-  | some v => v == 0
-  | _      => false
+  | some v => return v == 0
+  | _      => return false
 
 private def mkOffset (e : Expr) (offset : Nat) : MetaM Expr := do
   if offset == 0 then
diff --git a/src/Lean/Meta/Reduce.lean b/src/Lean/Meta/Reduce.lean
index d371a1296b..4589d494dc 100644
--- a/src/Lean/Meta/Reduce.lean
+++ b/src/Lean/Meta/Reduce.lean
@@ -12,9 +12,9 @@ namespace Lean.Meta
 partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : MetaM Expr :=
   let rec visit (e : Expr) : MonadCacheT Expr Expr MetaM Expr :=
     checkCache e fun _ => Core.withIncRecDepth do
-      if (← (skipTypes <&&> isType e)) then
+      if (← (pure skipTypes <&&> isType e)) then
         return e
-      else if (← (skipProofs <&&> isProof e)) then
+      else if (← (pure skipProofs <&&> isProof e)) then
         return e
       else
         let e ← whnf e
diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean
index c06d1e078e..1619f847db 100644
--- a/src/Lean/Meta/SizeOf.lean
+++ b/src/Lean/Meta/SizeOf.lean
@@ -17,7 +17,7 @@ where
       let param := params[i]
       let paramType ← inferType param
       let instType? ← forallTelescopeReducing paramType fun xs _ => do
-        let type ← mkAppN param xs
+        let type := mkAppN param xs
         try
           let sizeOf ← mkAppM `SizeOf #[type]
           let instType ← mkForallFVars xs sizeOf
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 15cdef8d9b..e70612d742 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -396,7 +396,7 @@ def isNewAnswer (oldAnswers : Array Answer) (answer : Answer) : Bool :=
 
 private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
   withMCtx cNode.mctx do
-    traceM `Meta.synthInstance.newAnswer do m!"size: {cNode.size}, {← inferType cNode.mvar}"
+    traceM `Meta.synthInstance.newAnswer do pure m!"size: {cNode.size}, {← inferType cNode.mvar}"
     let val ← instantiateMVars cNode.mvar
     trace[Meta.synthInstance.newAnswer] "val: {val}"
     let result ← abstractMVars val -- assignable metavariables become parameters
@@ -409,7 +409,7 @@ private def mkAnswer (cNode : ConsumerNode) : MetaM Answer :=
   And then, store it in the tabled entries map, and wakeup waiters. -/
 def addAnswer (cNode : ConsumerNode) : SynthM Unit := do
   if cNode.size ≥ (← read).maxResultSize then
-    traceM `Meta.synthInstance.discarded do withMCtx cNode.mctx do m!"size: {cNode.size} ≥ {(← read).maxResultSize}, {← inferType cNode.mvar}"
+    traceM `Meta.synthInstance.discarded do withMCtx cNode.mctx do pure m!"size: {cNode.size} ≥ {(← read).maxResultSize}, {← inferType cNode.mvar}"
     return ()
   else
     let answer ← mkAnswer cNode
@@ -487,7 +487,7 @@ def consume (cNode : ConsumerNode) : SynthM Unit :=
        match (← removeUnusedArguments? cNode.mctx mvar) with
        | none => newSubgoal cNode.mctx key mvar waiter
        | some (mvarType', transformer) =>
-         let key' ← mkTableKey cNode.mctx mvarType'
+         let key' := mkTableKey cNode.mctx mvarType'
          match (← findEntry? key') with
          | none => do
            let (mctx', mvar') ← withMCtx cNode.mctx do
@@ -498,7 +498,7 @@ def consume (cNode : ConsumerNode) : SynthM Unit :=
            let answers' ← entry'.answers.mapM fun a => withMCtx cNode.mctx do
              let trAnswr := Expr.betaRev transformer #[← instantiateMVars a.result.expr]
              let trAnswrType ← inferType trAnswr
-             { a with result.expr := trAnswr, resultType := trAnswrType }
+             pure { a with result.expr := trAnswr, resultType := trAnswrType }
            modify fun s =>
              { s with
                resumeStack  := answers'.foldl (fun s answer => s.push (cNode, answer)) s.resumeStack,
diff --git a/src/Lean/Meta/Tactic/AuxLemma.lean b/src/Lean/Meta/Tactic/AuxLemma.lean
index 1db2403fa4..95c72863a7 100644
--- a/src/Lean/Meta/Tactic/AuxLemma.lean
+++ b/src/Lean/Meta/Tactic/AuxLemma.lean
@@ -25,7 +25,7 @@ builtin_initialize auxLemmasExt : EnvExtension AuxLemmas ← registerEnvExtensio
 -/
 def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) : MetaM Name := do
   let env ← getEnv
-  let s ← auxLemmasExt.getState env
+  let s := auxLemmasExt.getState env
   let mkNewAuxLemma := do
     let auxName := Name.mkNum (env.mainModule ++ `_auxLemma) s.idx
     addDecl <| Declaration.thmDecl {
@@ -40,4 +40,4 @@ def mkAuxLemma (levelParams : List Name) (type : Expr) (value : Expr) : MetaM Na
   | some (name, levelParams') => if levelParams == levelParams' then return name else mkNewAuxLemma
   | none => mkNewAuxLemma
 
-end Lean.Meta
\ No newline at end of file
+end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/Delta.lean b/src/Lean/Meta/Tactic/Delta.lean
index f7a0e18665..0e8a4f3505 100644
--- a/src/Lean/Meta/Tactic/Delta.lean
+++ b/src/Lean/Meta/Tactic/Delta.lean
@@ -20,8 +20,8 @@ def delta? (e : Expr) (p : Name → Bool := fun _ => true) : CoreM (Option Expr)
 def deltaExpand (e : Expr) (p : Name → Bool) : CoreM Expr :=
   Core.transform e fun e => do
     match (← delta? e p) with
-    | some e' => TransformStep.visit e'
-    | none    => TransformStep.visit e
+    | some e' => return TransformStep.visit e'
+    | none    => return TransformStep.visit e
 
 def deltaTarget (mvarId : MVarId) (p : Name → Bool) : MetaM MVarId :=
   withMVarContext mvarId do
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 5af55f90e0..ee55250c33 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -361,7 +361,7 @@ where
     let q := e.bindingBody!
     let rp ← simp p
     trace[Debug.Meta.Tactic.simp] "arrow [{(← getConfig).contextual}] {p} [{← isProp p}] -> {q} [{← isProp q}]"
-    if (← (← getConfig).contextual <&&> isProp p <&&> isProp q) then
+    if (← pure (← getConfig).contextual <&&> isProp p <&&> isProp q) then
       trace[Debug.Meta.Tactic.simp] "ctx arrow {rp.expr} -> {q}"
       withLocalDeclD e.bindingName! rp.expr fun h => do
         let s ← getSimpLemmas
@@ -392,7 +392,7 @@ where
       return { expr := (← dsimp e) }
 
   simpLet (e : Expr) : M Result := do
-    let Expr.letE n t v b _ ← e | unreachable!
+    let Expr.letE n t v b _ := e | unreachable!
     if (← getConfig).zeta then
       return { expr := b.instantiate1 v }
     else
@@ -598,7 +598,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
       let type ← instantiateMVars localDecl.type
       let ctx ← match fvarIdToLemmaId.find? localDecl.fvarId with
         | none => pure ctx
-        | some lemmaId => pure { ctx with simpLemmas := (← ctx.simpLemmas.eraseCore lemmaId) }
+        | some lemmaId => pure { ctx with simpLemmas := ctx.simpLemmas.eraseCore lemmaId }
       match (← simpStep mvarId (mkFVar fvarId) type ctx discharge?) with
       | none => return none
       | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 11d139b345..94d799a9ed 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -181,11 +181,11 @@ def rewriteUsingDecide? (e : Expr) : MetaM (Option Result) := withReducibleAndIn
     x
 
 def rewritePre (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
-  let lemmas ← (← read).simpLemmas
+  let lemmas := (← read).simpLemmas
   return Step.visit (← rewrite e lemmas.pre lemmas.erased discharge? (tag := "pre"))
 
 def rewritePost (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step := do
-  let lemmas ← (← read).simpLemmas
+  let lemmas := (← read).simpLemmas
   return Step.visit (← rewrite e lemmas.post lemmas.erased discharge? (tag := "post"))
 
 def preDefault (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM Step :=
diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
index cb33b50673..a124832c92 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpAll.lean
@@ -50,7 +50,7 @@ private partial def loop : M Bool := do
     let entry := (← get).entries[i]
     let ctx := (← get).ctx
     -- We disable the current entry to prevent it to be simplified to `True`
-    let simpLemmasWithoutEntry ← (← getSimpLemmas).eraseCore entry.id
+    let simpLemmasWithoutEntry := (← getSimpLemmas).eraseCore entry.id
     let ctx := { ctx with simpLemmas := simpLemmasWithoutEntry }
     match (← simpStep (← get).mvarId entry.proof entry.type ctx) with
     | none => return true -- closed the goal
diff --git a/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean b/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
index bae1c3c0eb..cce66f757f 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
@@ -92,7 +92,7 @@ partial def SimpLemmas.eraseCore (d : SimpLemmas) (declName : Name) : SimpLemmas
 def SimpLemmas.erase [Monad m] [MonadError m] (d : SimpLemmas) (declName : Name) : m SimpLemmas := do
   unless d.isLemma declName || d.isDeclToUnfold declName || d.toUnfoldThms.contains declName do
     throwError "'{declName}' does not have [simp] attribute"
-  d.eraseCore declName
+  return d.eraseCore declName
 
 private partial def isPerm : Expr → Expr → MetaM Bool
   | Expr.app f₁ a₁ _, Expr.app f₂ a₂ _ => isPerm f₁ f₂ <&&> isPerm a₁ a₂
@@ -103,8 +103,8 @@ private partial def isPerm : Expr → Expr → MetaM Bool
   | Expr.lam n₁ d₁ b₁ _, Expr.lam n₂ d₂ b₂ _ => isPerm d₁ d₂ <&&> withLocalDeclD n₁ d₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
   | Expr.letE n₁ t₁ v₁ b₁ _, Expr.letE n₂ t₂ v₂ b₂ _ =>
     isPerm t₁ t₂ <&&> isPerm v₁ v₂ <&&> withLetDecl n₁ t₁ v₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
-  | Expr.proj _ i₁ b₁ _, Expr.proj _ i₂ b₂ _ => i₁ == i₂ <&&> isPerm b₁ b₂
-  | s, t => s == t
+  | Expr.proj _ i₁ b₁ _, Expr.proj _ i₂ b₂ _ => pure (i₁ == i₂) <&&> isPerm b₁ b₂
+  | s, t => return s == t
 
 private def checkBadRewrite (lhs rhs : Expr) : MetaM Unit := do
   let lhs ← DiscrTree.whnfDT lhs (root := true)
@@ -201,7 +201,7 @@ private def mkSimpLemmasFromConst (declName : Name) (post : Bool) (inv : Bool) (
         r := r.push <| (← mkSimpLemmaCore (mkConst auxName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst auxName) post prio declName)
       return r
     else
-      #[← mkSimpLemmaCore (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio declName]
+      return #[← mkSimpLemmaCore (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio declName]
 
 inductive SimpEntry where
   | lemma    : SimpLemma → SimpEntry
@@ -244,7 +244,7 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension) : IO
           throwError "invalid 'simp', it is not a proposition nor a definition (to unfold)"
       discard <| go.run {} {}
     erase := fun declName => do
-      let s ← ext.getState (← getEnv)
+      let s := ext.getState (← getEnv)
       let s ← s.erase declName
       modifyEnv fun env => ext.modifyState env fun _ => s
   }
@@ -285,7 +285,7 @@ def SimpLemma.getValue (simpLemma : SimpLemma) : MetaM Expr := do
       return simpLemma.proof.updateConst! (← info.levelParams.mapM (fun _ => mkFreshLevelMVar))
   else
     let us ← simpLemma.levelParams.mapM fun _ => mkFreshLevelMVar
-    simpLemma.proof.instantiateLevelParamsArray simpLemma.levelParams us
+    return simpLemma.proof.instantiateLevelParamsArray simpLemma.levelParams us
 
 private def preprocessProof (val : Expr) (inv : Bool) : MetaM (Array Expr) := do
   let type ← inferType val
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index da62a598fb..35ab03baa8 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -508,13 +508,13 @@ where
     match e with
     | Expr.letE n t v b _ => withLetDecl n t (← go v) fun x => do mkLetFVars #[x] (← go (b.instantiate1 x))
     | Expr.lam .. => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← go b)
-    | Expr.app f a .. => mkApp (← go f) (← go a)
-    | Expr.proj _ _ s _ => e.updateProj! (← go s)
+    | Expr.app f a .. => return mkApp (← go f) (← go a)
+    | Expr.proj _ _ s _ => return e.updateProj! (← go s)
     | Expr.mdata _ b _  =>
       if let some m := smartUnfoldingMatch? e then
         goMatch m
       else
-        e.updateMData! (← go b)
+        return e.updateMData! (← go b)
     | _ => return e
 
   goMatch (e : Expr) : OptionT MetaM Expr := do
@@ -706,9 +706,9 @@ def reduceNat? (e : Expr) : MetaM (Option Expr) :=
     return false
   else
     match (← getConfig).transparency with
-    | TransparencyMode.default => true
-    | TransparencyMode.all     => true
-    | _                        => false
+    | TransparencyMode.default => return true
+    | TransparencyMode.all     => return true
+    | _                        => return false
 
 @[inline] private def cached? (useCache : Bool) (e : Expr) : MetaM (Option Expr) := do
   if useCache then
diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
index 85c2706bfc..f1fb67acb5 100644
--- a/src/Lean/MonadEnv.lean
+++ b/src/Lean/MonadEnv.lean
@@ -77,7 +77,7 @@ def getConstInfo [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m Co
 
 def mkConstWithLevelParams [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m Expr := do
   let info ← getConstInfo constName
-  mkConst constName (info.levelParams.map mkLevelParam)
+  return mkConst constName (info.levelParams.map mkLevelParam)
 
 def getConstInfoInduct [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m InductiveVal := do
   match (← getConstInfo constName) with
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index dc4d5cbce2..defb470b9e 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -313,7 +313,7 @@ private def ParserExtension.OLeanEntry.toEntry (s : State) : OLeanEntry → Impo
   | category c l => return Entry.category c l
   | parser catName declName prio => do
     let (leading, p) ← mkParserOfConstant s.categories declName
-    Entry.parser catName declName leading p prio
+    return Entry.parser catName declName leading p prio
 
 builtin_initialize parserExtension : ParserExtension ←
   registerScopedEnvExtension {
@@ -341,8 +341,8 @@ def leadingIdentBehavior (env : Environment) (catName : Name) : LeadingIdentBeha
 unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s => unsafeBaseIO do
   let categories := (parserExtension.getState ctx.env).categories
   match (← (mkParserOfConstant categories declName { env := ctx.env, opts := ctx.options }).toBaseIO) with
-  | Except.ok (bool, p) => p.fn ctx s
-  | Except.error e => s.mkUnexpectedError e.toString
+  | Except.ok (bool, p) => return p.fn ctx s
+  | Except.error e => return s.mkUnexpectedError e.toString
 
 @[implementedBy evalParserConstUnsafe]
 constant evalParserConst (declName : Name) : ParserFn
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index 4517c1f6e8..12be7dcff2 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -35,7 +35,7 @@ open Meta Parser in
 /-- Takes an expression of type `Parser`, and determines the syntax kind of the root node it produces. -/
 partial def parserNodeKind? (e : Expr) : MetaM (Option Name) := do
   let reduceEval? e : MetaM (Option Name) := do
-    try some (← reduceEval e) catch _ => none
+    try pure <| some (← reduceEval e) catch _ => pure none
   let e ← whnfCore e
   if e matches Expr.lam .. then
     lambdaLetTelescope e fun xs e => parserNodeKind? e
@@ -46,7 +46,7 @@ partial def parserNodeKind? (e : Expr) : MetaM (Option Name) := do
   else if e.isAppOfArity ``leadingNode 3 || e.isAppOfArity ``trailingNode 4 || e.isAppOfArity ``node 2 then
     reduceEval? (e.getArg! 0)
   else
-    none
+    return none
 
 section
 open Meta
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index b724e3eb33..b01cb17886 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -138,10 +138,10 @@ def getExprKind : DelabM Name := do
 def getOptionsAtCurrPos : DelabM Options := do
   let ctx ← read
   let mut opts := ctx.defaultOptions
-  if let some opts' ← ctx.optionsPerPos.find? (← getPos) then
+  if let some opts' := ctx.optionsPerPos.find? (← getPos) then
     for (k, v) in opts' do
       opts := opts.insert k v
-  opts
+  return opts
 
 /-- Evaluate option accessor, using subterm-specific options if set. -/
 def getPPOption (opt : Options → Bool) : DelabM Bool := do
@@ -158,8 +158,8 @@ def whenNotPPOption (opt : Options → Bool) (d : Delab) : Delab := do
 def annotatePos (pos : Nat) (stx : Syntax) : Syntax :=
   stx.setInfo (SourceInfo.synthetic pos pos)
 
-def annotateCurPos (stx : Syntax) : Delab := do
-  annotatePos (← getPos) stx
+def annotateCurPos (stx : Syntax) : Delab :=
+  return annotatePos (← getPos) stx
 
 def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do
   -- Use a nicer binder name than `[anonymous]`. We probably shouldn't do this in all LocalContext use cases, so do it here.
@@ -193,7 +193,7 @@ def addTermInfo (pos : Pos) (stx : Syntax) (e : Expr) (isBinder : Bool := false)
   let info ← mkTermInfo stx e isBinder
   modify fun s => { s with infos := s.infos.insert pos info }
 where
-  mkTermInfo stx e isBinder := do Info.ofTermInfo {
+  mkTermInfo stx e isBinder := return Info.ofTermInfo {
     elaborator := `Delab,
     stx := stx,
     lctx := (← getLCtx),
@@ -206,7 +206,7 @@ def addFieldInfo (pos : Pos) (projName fieldName : Name) (stx : Syntax) (val : E
   let info ← mkFieldInfo projName fieldName stx val
   modify fun s => { s with infos := s.infos.insert pos info }
 where
-  mkFieldInfo projName fieldName stx val := do Info.ofFieldInfo {
+  mkFieldInfo projName fieldName stx val := return Info.ofFieldInfo {
     projName := projName,
     fieldName := fieldName,
     lctx := (← getLCtx),
@@ -220,7 +220,7 @@ partial def delabFor : Name → Delab
     (do let stx ← (delabAttribute.getValues (← getEnv) k).firstM id
         let stx ← annotateCurPos stx
         addTermInfo (← getPos) stx (← getExpr)
-        stx)
+        pure stx)
     -- have `app.Option.some` fall back to `app` etc.
     <|> if k.isAtomic then failure else delabFor k.getRoot
 
@@ -229,7 +229,7 @@ partial def delab : Delab := do
   let e ← getExpr
 
   -- no need to hide atomic proofs
-  if ← !e.isAtomic <&&> !(← getPPOption getPPProofs) <&&> (try Meta.isProof e catch ex => false) then
+  if ← pure !e.isAtomic <&&> pure !(← getPPOption getPPProofs) <&&> (try Meta.isProof e catch ex => pure false) then
     if ← getPPOption getPPProofsWithType then
       let stx ← withType delab
       return ← ``((_ : $stx))
@@ -237,10 +237,11 @@ partial def delab : Delab := do
       return ← ``(_)
   let k ← getExprKind
   let stx ← delabFor k <|> (liftM $ show MetaM Syntax from throwError "don't know how to delaborate '{k}'")
-  if ← getPPOption getPPAnalyzeTypeAscriptions <&&> getPPOption getPPAnalysisNeedsType <&&> !e.isMData then
+  if ← getPPOption getPPAnalyzeTypeAscriptions <&&> getPPOption getPPAnalysisNeedsType <&&> pure !e.isMData then
     let typeStx ← withType delab
     `(($stx:term : $typeStx:term)) >>= annotateCurPos
-  else stx
+  else
+    return stx
 
 unsafe def mkAppUnexpanderAttribute : IO (KeyedDeclsAttribute Unexpander) :=
   KeyedDeclsAttribute.init {
@@ -267,11 +268,11 @@ def delabCore (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (opt
   if pp.proofs.get? opts == none then
     try if ← Meta.isProof e then opts := pp.proofs.set opts true
     catch _ => pure ()
-  let e ← if getPPInstantiateMVars opts then ← Meta.instantiateMVars e else e
+  let e ← if getPPInstantiateMVars opts then Meta.instantiateMVars e else pure e
   let optionsPerPos ←
     if !getPPAll opts && getPPAnalyze opts && optionsPerPos.isEmpty then
       withTheReader Core.Context (fun ctx => { ctx with options := opts }) do topDownAnalyze e
-    else optionsPerPos
+    else pure optionsPerPos
   let (stx, {infos := infos, ..}) ← catchInternalId Delaborator.delabFailureId
     (Delaborator.delab
       { defaultOptions := opts
@@ -286,7 +287,7 @@ def delabCore (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (opt
 /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
 def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do
   let (stx, _) ← delabCore currNamespace openDecls e optionsPerPos
-  stx
+  return stx
 
 builtin_initialize registerTraceClass `PrettyPrinter.delab
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index b151ccbecf..2ca7e719f4 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -15,7 +15,7 @@ open Lean.Parser.Term
 open SubExpr
 
 def maybeAddBlockImplicit (ident : Syntax) : DelabM Syntax := do
-  if ← getPPOption getPPAnalysisBlockImplicit then `(@$ident:ident) else ident
+  if ← getPPOption getPPAnalysisBlockImplicit then `(@$ident:ident) else pure ident
 
 def unfoldMDatas : Expr → Expr
   | Expr.mdata _ e _ => unfoldMDatas e
@@ -100,7 +100,7 @@ def delabConst : Delab := do
           c := `_root_ ++ c
         else
           c := c₀
-      mkIdent c
+      pure <| mkIdent c
     else
       `($(mkIdent c).{$[$(ls.toArray.map quote)],*})
 
@@ -108,7 +108,7 @@ def delabConst : Delab := do
   if (← getPPOption getPPTagAppFns) then
     stx ← annotateCurPos stx
     addTermInfo (← getPos) stx (← getExpr)
-  stx
+  return stx
 
 def withMDataOptions [Inhabited α] (x : DelabM α) : DelabM α := do
   match ← getExpr with
@@ -179,15 +179,15 @@ def delabAppExplicit : Delab := do
                      if ← getPPOption getPPInstanceTypes then
                        let typeStx ← withType delab
                        `(($stx : $typeStx))
-                     else stx
+                     else pure stx
                    else delab
       pure (fnStx, paramKinds.tailD [], argStxs.push argStx))
-  Syntax.mkApp fnStx argStxs
+  return Syntax.mkApp fnStx argStxs
 
 def shouldShowMotive (motive : Expr) (opts : Options) : MetaM Bool := do
-  getPPMotivesAll opts
-  <||> (← getPPMotivesPi opts <&&> returnsPi motive)
-  <||> (← getPPMotivesNonConst opts <&&> isNonConstFun motive)
+  pure (getPPMotivesAll opts)
+  <||> (pure (getPPMotivesPi opts) <&&> returnsPi motive)
+  <||> (pure (getPPMotivesNonConst opts) <&&> isNonConstFun motive)
 
 def isRegularApp : DelabM Bool := do
   let e ← getExpr
@@ -198,8 +198,8 @@ def isRegularApp : DelabM Bool := do
   return true
 
 def unexpandRegularApp (stx : Syntax) : Delab := do
-  let Expr.const c .. ← pure (unfoldMDatas (← getExpr).getAppFn) | unreachable!
-  let fs ← appUnexpanderAttribute.getValues (← getEnv) c
+  let Expr.const c .. := (unfoldMDatas (← getExpr).getAppFn) | unreachable!
+  let fs := appUnexpanderAttribute.getValues (← getEnv) c
   let ref ← getRef
   fs.firstM fun f =>
     match f stx |>.run ref |>.run () with
@@ -209,10 +209,10 @@ def unexpandRegularApp (stx : Syntax) : Delab := do
 -- abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β
 -- abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
 def unexpandCoe (stx : Syntax) : Delab := whenPPOption getPPCoercions do
-  if not (← isCoe (← getExpr)) then failure
+  if not (isCoe (← getExpr)) then failure
   let e ← getExpr
   match stx with
-  | `($fn $arg)   => arg
+  | `($fn $arg)   => return arg
   | `($fn $args*) => `($(args.get! 0) $(args.eraseIdx 0)*)
   | _             => failure
 
@@ -256,8 +256,8 @@ def delabAppImplicit : Delab := do
   -- This is e.g. necessary for `@Eq`.
   let isImplicitApp ← try
       let ty ← whnf (← inferType (← getExpr))
-      ty.isForall && (ty.binderInfo == BinderInfo.implicit || ty.binderInfo == BinderInfo.instImplicit)
-    catch _ => false
+      pure <| ty.isForall && (ty.binderInfo == BinderInfo.implicit || ty.binderInfo == BinderInfo.instImplicit)
+    catch _ => pure false
   if isImplicitApp then failure
 
   let (fnStx, _, argStxs) ← withAppFnArgs
@@ -266,7 +266,7 @@ def delabAppImplicit : Delab := do
       let arg ← getExpr
       let opts ← getOptions
       let mkNamedArg (name : Name) (argStx : Syntax) : DelabM Syntax := do
-        `(Parser.Term.namedArgument| ($(← mkIdent name):ident := $argStx:term))
+        `(Parser.Term.namedArgument| ($(mkIdent name):ident := $argStx:term))
       let argStx? : Option Syntax ←
         if ← getPPOption getPPAnalysisSkip then pure none
         else if ← getPPOption getPPAnalysisHole then `(_)
@@ -276,9 +276,9 @@ def delabAppImplicit : Delab := do
           | param :: rest =>
             if param.defVal.isSome && rest.isEmpty then
               let v := param.defVal.get!
-              if !v.hasLooseBVars && v == arg then none else delab
+              if !v.hasLooseBVars && v == arg then pure none else delab
             else if !param.isRegularExplicit && param.defVal.isNone then
-              if ← getPPOption getPPAnalysisNamedArg <||> (param.name == `motive <&&> shouldShowMotive arg opts) then mkNamedArg param.name (← delab) else none
+              if ← getPPOption getPPAnalysisNamedArg <||> (pure (param.name == `motive) <&&> shouldShowMotive arg opts) then mkNamedArg param.name (← delab) else pure none
             else delab
       let argStxs := match argStx? with
         | none => argStxs
@@ -339,7 +339,7 @@ where
     | 0,   varNames => x varNames
     | n+1, varNames => do
       let rec visitLambda : DelabM α := do
-        let varName ← (← getExpr).bindingName!.eraseMacroScopes
+        let varName := (← getExpr).bindingName!.eraseMacroScopes
         -- Pattern variables cannot shadow each other
         if varNames.contains varName then
           let varName := (← getLCtx).getUnusedName varName
@@ -379,7 +379,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
     (do
       let (Expr.const c us _) ← getExpr | failure
       let (some info) ← getMatcherInfo? c | failure
-      { matcherTy := (← getConstInfo c).instantiateTypeLevelParams us, info := info : AppMatchState })
+      return { matcherTy := (← getConstInfo c).instantiateTypeLevelParams us, info := info : AppMatchState })
     (fun st => do
       if st.params.size < st.info.numParams then
         pure { st with params := st.params.push (← getExpr) }
@@ -411,7 +411,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
   match st.discrs, st.rhss with
   | #[discr], #[] =>
     let stx ← `(nomatch $discr)
-    Syntax.mkApp stx st.moreArgs
+    return Syntax.mkApp stx st.moreArgs
   | _,        #[] => failure
   | _,        _   =>
     let pats ← delabPatterns st
@@ -419,11 +419,11 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat
       let (piStx, lamMotive) := st.motive.get!
       let opts ← getOptions
       -- TODO: disable the match if other implicits are needed?
-      if ← st.motiveNamed <||> shouldShowMotive lamMotive opts then
+      if ← pure st.motiveNamed <||> shouldShowMotive lamMotive opts then
         `(match $[$st.discrs:term],* : $piStx with $[| $pats,* => $st.rhss]*)
       else
         `(match $[$st.discrs:term],* with $[| $pats,* => $st.rhss]*)
-    Syntax.mkApp stx st.moreArgs
+    return Syntax.mkApp stx st.moreArgs
 
 /--
   Delaborate applications of the form `(fun x => b) v` as `let_fun x := v; b`
@@ -501,7 +501,7 @@ private partial def delabBinders (delabGroup : Array Syntax → Syntax → Delab
       withBindingBodyUnusedName fun stxN => delabBinders delabGroup (curNames.push stxN)
     else
       -- don't group => delab body and prepend current binder group
-      let (stx, stxN) ← withBindingBodyUnusedName fun stxN => do (← delab, stxN)
+      let (stx, stxN) ← withBindingBodyUnusedName fun stxN => return (← delab, stxN)
       delabGroup (curNames.push stxN) stx
 
 @[builtinDelab lam]
@@ -511,7 +511,7 @@ def delabLam : Delab :=
     let stxT ← withBindingDomain delab
     let ppTypes ← getPPOption getPPFunBinderTypes
     let expl ← getPPOption getPPExplicit
-    let usedDownstream ← curNames.any (fun n => hasIdent n.getId stxBody)
+    let usedDownstream := curNames.any (fun n => hasIdent n.getId stxBody)
 
     -- leave lambda implicit if possible
     -- TODO: for now we just always block implicit lambdas when delaborating. We can revisit.
@@ -561,7 +561,7 @@ def delabLam : Delab :=
 def delabForall : Delab :=
   delabBinders fun curNames stxBody => do
     let e ← getExpr
-    let prop ← try isProp e catch _ => false
+    let prop ← try isProp e catch _ => pure false
     let stxT ← withBindingDomain delab
     let group ← match e.binderInfo with
     | BinderInfo.implicit       => `(bracketedBinderF|{$curNames* : $stxT})
@@ -745,7 +745,7 @@ partial def delabDoElems : DelabM (List Syntax) := do
         prependAndRec `(doElem|let $(mkIdent n) : $stxT := $stxV)
   else
     let stx ← delab
-    [←`(doElem|$stx:term)]
+    return [←`(doElem|$stx:term)]
   where
     prependAndRec x : DelabM _ := List.cons <$> x <*> delabDoElems
 
@@ -757,18 +757,16 @@ def delabDo : Delab := whenPPOption getPPNotation do
   `(do $items:doSeqItem*)
 
 def reifyName : Expr → DelabM Name
-  | Expr.const ``Lean.Name.anonymous .. => Name.anonymous
-  | Expr.app (Expr.app (Expr.const ``Lean.Name.mkStr ..) n _) (Expr.lit (Literal.strVal s) _) _ => do
-    (← reifyName n).mkStr s
-  | Expr.app (Expr.app (Expr.const ``Lean.Name.mkNum ..) n _) (Expr.lit (Literal.natVal i) _) _ => do
-    (← reifyName n).mkNum i
+  | Expr.const ``Lean.Name.anonymous .. => return Name.anonymous
+  | Expr.app (Expr.app (Expr.const ``Lean.Name.mkStr ..) n _) (Expr.lit (Literal.strVal s) _) _ => return (← reifyName n).mkStr s
+  | Expr.app (Expr.app (Expr.const ``Lean.Name.mkNum ..) n _) (Expr.lit (Literal.natVal i) _) _ => return (← reifyName n).mkNum i
   | _ => failure
 
 @[builtinDelab app.Lean.Name.mkStr]
 def delabNameMkStr : Delab := whenPPOption getPPNotation do
   let n ← reifyName (← getExpr)
   -- not guaranteed to be a syntactically valid name, but usually more helpful than the explicit version
-  mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{n}"]
+  return mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{n}"]
 
 @[builtinDelab app.Lean.Name.mkNum]
 def delabNameMkNum : Delab := delabNameMkStr
diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
index cbf061690b..25bd627ac8 100644
--- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean
@@ -41,8 +41,8 @@ variable [MonadLiftT IO m]
 
 def mkRoot (e : Expr) : SubExpr := ⟨e, 1⟩
 
-def getExpr : m Expr := do (← readThe SubExpr).expr
-def getPos  : m Pos  := do (← readThe SubExpr).pos
+def getExpr : m Expr := return (← readThe SubExpr).expr
+def getPos  : m Pos  := return (← readThe SubExpr).pos
 
 def descend (child : Expr) (childIdx : Pos) (x : m α) : m α :=
   withTheReader SubExpr (fun cfg => { cfg with expr := child, pos := cfg.pos * maxChildren + childIdx }) x
@@ -128,7 +128,7 @@ def nextExtraPos : m Pos := do
   let iter ← getThe HoleIterator
   let pos := iter.toPos
   modifyThe HoleIterator HoleIterator.next
-  pos
+  return pos
 
 end Hole
 end SubExpr
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index b3fb50ef08..808638c6e3 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -134,24 +134,24 @@ def getPPAnalysisBlockImplicit   (o : Options) : Bool := o.get `pp.analysis.bloc
 namespace PrettyPrinter.Delaborator
 
 def returnsPi (motive : Expr) : MetaM Bool := do
-  lambdaTelescope motive fun xs b => b.isForall
+  lambdaTelescope motive fun xs b => return b.isForall
 
 def isNonConstFun (motive : Expr) : MetaM Bool := do
   match motive with
   | Expr.lam name d b _ => isNonConstFun b
-  | _ => motive.hasLooseBVars
+  | _ => return motive.hasLooseBVars
 
-def isSimpleHOFun (motive : Expr) : MetaM Bool := do
-  not (← returnsPi motive) && not (← isNonConstFun motive)
+def isSimpleHOFun (motive : Expr) : MetaM Bool :=
+  return not (← returnsPi motive) && not (← isNonConstFun motive)
 
 def isType2Type (motive : Expr) : MetaM Bool := do
   match ← inferType motive with
-  | Expr.forallE _ (Expr.sort ..) (Expr.sort ..) .. => true
-  | _ => false
+  | Expr.forallE _ (Expr.sort ..) (Expr.sort ..) .. => return true
+  | _ => return false
 
 def isFOLike (motive : Expr) : MetaM Bool := do
   let f := motive.getAppFn
-  f.isFVar || f.isConst
+  return f.isFVar || f.isConst
 
 def isIdLike (arg : Expr) : Bool :=
   -- TODO: allow `id` constant as well?
@@ -168,21 +168,21 @@ def isCoe (e : Expr) : Bool :=
 
 def isStructureInstance (e : Expr) : MetaM Bool := do
   match e.isConstructorApp? (← getEnv) with
-  | some s => isStructure (← getEnv) s.induct
-  | none   => false
+  | some s => return isStructure (← getEnv) s.induct
+  | none   => return false
 
 namespace TopDownAnalyze
 
 partial def hasMVarAtCurrDepth (e : Expr) : MetaM Bool := do
   let mctx ← getMCtx
-  Option.isSome $ e.findMVar? fun mvarId =>
+  return Option.isSome <| e.findMVar? fun mvarId =>
     match mctx.findDecl? mvarId with
     | some mdecl => mdecl.depth == mctx.depth
     | _ => false
 
 partial def hasLevelMVarAtCurrDepth (e : Expr) : MetaM Bool := do
   let mctx ← getMCtx
-  Option.isSome $ e.findLevelMVar? fun mvarId =>
+  return Option.isSome <| e.findLevelMVar? fun mvarId =>
     mctx.findLevelDepth? mvarId == some mctx.depth
 
 private def valUnknown (e : Expr) : MetaM Bool := do
@@ -225,10 +225,10 @@ def checkpointDefEq (t s : Expr) : MetaM Bool := do
     isDefEqAssigning t s
 
 def isHigherOrder (type : Expr) : MetaM Bool := do
-  forallTelescopeReducing type fun xs b => xs.size > 0 && b.isSort
+  forallTelescopeReducing type fun xs b => return xs.size > 0 && b.isSort
 
 def isFunLike (e : Expr) : MetaM Bool := do
-  forallTelescopeReducing (← inferType e) fun xs b => xs.size > 0
+  forallTelescopeReducing (← inferType e) fun xs b => return xs.size > 0
 
 def isSubstLike (e : Expr) : Bool :=
   e.isAppOfArity `Eq.ndrec 6 || e.isAppOfArity `Eq.rec 6
@@ -241,8 +241,8 @@ where
     | Name.num ..   => true
     | Name.anonymous => false
 
-def mvarName (mvar : Expr) : MetaM Name := do
-  (← getMVarDecl mvar.mvarId!).userName
+def mvarName (mvar : Expr) : MetaM Name :=
+  return (← getMVarDecl mvar.mvarId!).userName
 
 def containsBadMax : Level → Bool
   | Level.succ u ..   => containsBadMax u
@@ -312,7 +312,7 @@ partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat :=
   -- These are incomplete (and possibly unsound) heuristics.
   -- TODO: do I need to snapshot the state before calling this?
   match fuel with
-  | 0 => false
+  | 0 => return false
   | fuel + 1 =>
     if ← isTrivialBottomUp e then return true
     let f := e.getAppFn
@@ -323,10 +323,10 @@ partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat :=
     for i in [:mvars.size] do
       if bInfos[i] == BinderInfo.instImplicit then
         inspectOutParams args[i] mvars[i]
-      else if ← bInfos[i] == BinderInfo.default then
+      else if bInfos[i] == BinderInfo.default then
         if ← isTrivialBottomUp args[i] then tryUnify args[i] mvars[i]
         else if ← typeUnknown mvars[i] <&&> canBottomUp args[i] mvars[i] fuel then tryUnify args[i] mvars[i]
-    if ← (isHBinOp e <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then tryUnify mvars[0] mvars[1]
+    if ← (pure (isHBinOp e) <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then tryUnify mvars[0] mvars[1]
     if mvar?.isSome then tryUnify resultType (← inferType mvar?.get!)
     return !(← valUnknown resultType)
 
@@ -371,7 +371,7 @@ mutual
     trace[pp.analyze] "{(← read).knowsType}.{(← read).knowsLevel}"
     let e ← getExpr
     let opts ← getOptions
-    if ← !e.isAtomic <&&> !(getPPProofs opts) <&&> (try Meta.isProof e catch ex => false) then
+    if ← (pure !e.isAtomic) <&&> pure !(getPPProofs opts) <&&> (try Meta.isProof e catch ex => pure false) then
       if getPPProofsWithType opts then
         withType $ withKnowing true true $ analyze
       return ()
@@ -398,7 +398,7 @@ mutual
         withType $ withKnowing true false $ analyze
         willKnowType := true
 
-      else if ← (!(← read).knowsType <||> (← read).inBottomUp) <&&> isStructureInstance (← getExpr) then
+      else if ← (pure !(← read).knowsType <||> pure (← read).inBottomUp) <&&> isStructureInstance (← getExpr) then
         withType do
           annotateBool `pp.structureInstanceTypes
           withKnowing true false $ analyze
@@ -515,7 +515,7 @@ mutual
 
     hBinOpHeuristic := do
       let { args, mvars, bInfos, ..} ← read
-      if ← (isHBinOp (← getExpr) <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then
+      if ← (pure (isHBinOp (← getExpr)) <&&> (valUnknown mvars[0] <||> valUnknown mvars[1])) then
         tryUnify mvars[0] mvars[1]
 
     collectTrivialBottomUps := do
@@ -536,7 +536,7 @@ mutual
         | Expr.lam .., Expr.forallE n t b .. =>
           let mut annotated := false
           for i in [:argIdx] do
-            if ← bInfos[i] == BinderInfo.implicit <&&> valUnknown mvars[i] <&&> withNewMCtxDepth (checkpointDefEq t mvars[i]) then
+            if ← pure (bInfos[i] == BinderInfo.implicit) <&&> valUnknown mvars[i] <&&> withNewMCtxDepth (checkpointDefEq t mvars[i]) then
               annotateBool `pp.funBinderTypes
               tryUnify args[i] mvars[i]
               -- Note: currently we always analyze the lambda binding domains in `analyzeLam`
@@ -549,7 +549,7 @@ mutual
         | _, _ => return false
 
       for i in [:args.size] do
-        if ← bInfos[i] == BinderInfo.default then
+        if bInfos[i] == BinderInfo.default then
           let b ← withNaryArg i (core i (← inferType mvars[i]))
           if b then modify fun s => { s with funBinders := s.funBinders.set! i true }
 
@@ -569,7 +569,7 @@ mutual
       let argType ← inferType arg
 
       let processNaturalImplicit : AnalyzeAppM Unit := do
-        if (← valUnknown mvars[i] <||> higherOrders[i]) && !forceRegularApp then
+        if (← valUnknown mvars[i] <||> pure higherOrders[i]) && !forceRegularApp then
           annotateNamedArg (← mvarName mvars[i])
           modify fun s => { s with provideds := s.provideds.set! i true }
         else
@@ -580,7 +580,7 @@ mutual
 
           match bInfos[i] with
           | BinderInfo.default =>
-            if ← getPPAnalyzeExplicitHoles (← getOptions) <&&> !(← valUnknown mvars[i]) <&&> !(← readThe Context).inBottomUp <&&> !(← isFunLike arg) <&&> !funBinders[i] <&&> checkpointDefEq mvars[i] arg then
+            if ← pure (getPPAnalyzeExplicitHoles (← getOptions)) <&&> pure !(← valUnknown mvars[i]) <&&> pure !(← readThe Context).inBottomUp <&&> pure !(← isFunLike arg) <&&> pure !funBinders[i] <&&> checkpointDefEq mvars[i] arg then
               annotateBool `pp.analysis.hole
             else
               modify fun s => { s with provideds := s.provideds.set! i true }
@@ -596,7 +596,7 @@ mutual
               annotateBool `pp.analysis.skip
               provided := false
             else if getPPAnalyzeCheckInstances (← getOptions) then
-              let instResult ← try trySynthInstance argType catch _ => LOption.undef
+              let instResult ← try trySynthInstance argType catch _ => pure LOption.undef
               match instResult with
               | LOption.some inst =>
                 if ← checkpointDefEq inst arg then annotateBool `pp.analysis.skip; provided := false
@@ -628,7 +628,7 @@ def topDownAnalyze (e : Expr) : MetaM OptionsPerPos := do
   let s₀ ← get
   traceCtx `pp.analyze do
     withReader (fun ctx => { ctx with config := Elab.Term.setElabConfig ctx.config }) do
-      let ϕ : AnalyzeM OptionsPerPos := do withNewMCtxDepth analyze; (← get).annotations
+      let ϕ : AnalyzeM OptionsPerPos := do withNewMCtxDepth analyze; pure (← get).annotations
       try
         let knowsType := getPPAnalyzeKnowsType (← getOptions)
         ϕ { knowsType := knowsType, knowsLevel := knowsType, subExpr := mkRoot e }
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 17cbfdf3d9..2783bcfb87 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -297,9 +297,9 @@ def trailingNode.formatter (k : SyntaxNodeKind) (_ _ : Nat) (p : Formatter) : Fo
     -- leading term, not actually produced by `p`
     categoryParser.formatter `foo
 
-def parseToken (s : String) : FormatterM ParserState := do
+def parseToken (s : String) : FormatterM ParserState :=
   -- include comment tokens, e.g. when formatting `- -0`
-  (Parser.andthenFn Parser.whitespace (Parser.tokenFn [])) {
+  return (Parser.andthenFn Parser.whitespace (Parser.tokenFn [])) {
     input := s,
     fileName := "",
     fileMap := FileMap.ofString "",
diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean
index d834dd8136..3209f4c955 100644
--- a/src/Lean/ReducibilityAttrs.lean
+++ b/src/Lean/ReducibilityAttrs.lean
@@ -40,12 +40,12 @@ def setReducibleAttribute [Monad m] [MonadEnv m] (declName : Name) : m Unit := d
 
 def isReducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   match (← getReducibilityStatus declName) with
-  | ReducibilityStatus.reducible => true
-  | _ => false
+  | ReducibilityStatus.reducible => return true
+  | _ => return false
 
 def isIrreducible [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   match (← getReducibilityStatus declName) with
-  | ReducibilityStatus.irreducible => true
-  | _ => false
+  | ReducibilityStatus.irreducible => return true
+  | _ => return false
 
 end Lean
diff --git a/src/Lean/Server/AsyncList.lean b/src/Lean/Server/AsyncList.lean
index 496b8b740f..ced5406875 100644
--- a/src/Lean/Server/AsyncList.lean
+++ b/src/Lean/Server/AsyncList.lean
@@ -51,7 +51,7 @@ partial def unfoldAsync (f : StateT σ (EIO ε) $ Option α) (init : σ)
         return cons aNext $ asyncTail tNext
 
   let tInit ← EIO.asTask (step init)
-  asyncTail tInit
+  return asyncTail tInit
 
 /-- The computed, synchronous list. If an async tail was present, returns also
 its terminating value. -/
@@ -70,14 +70,14 @@ partial def waitAll (p : α → Bool := fun _ => true) : AsyncList ε α → Bas
   | cons hd tl => do
     if p hd then
       let t ← tl.waitAll p
-      t.map fun ⟨l, e?⟩ => ⟨hd :: l, e?⟩
+      return t.map fun ⟨l, e?⟩ => ⟨hd :: l, e?⟩
     else
       return Task.pure ⟨[hd], none⟩
   | nil => return Task.pure ⟨[], none⟩
   | asyncTail tl => do
     BaseIO.bindTask tl fun
       | Except.ok tl   => tl.waitAll p
-      | Except.error e => Task.pure ⟨[], some e⟩
+      | Except.error e => return Task.pure ⟨[], some e⟩
 
 /-- Spawns a `Task` acting like `List.find?` but which will wait for tail evalution
 when necessary to traverse the list. If the tail terminates before a matching element
@@ -90,7 +90,7 @@ partial def waitFind? (p : α → Bool) : AsyncList ε α → BaseIO (Task $ Exc
   | asyncTail tl => do
     BaseIO.bindTask tl fun
       | Except.ok tl   => tl.waitFind? p
-      | Except.error e => Task.pure <| Except.error e
+      | Except.error e => return Task.pure <| Except.error e
 
 /-- Extends the `finishedPrefix` as far as possible. If computation was ongoing
 and has finished, also returns the terminating value. -/
diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index 2ef3e3fbba..d7cba3b320 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -26,11 +26,11 @@ def addToBlackList (env : Environment) (declName : Name) : Environment :=
 
 private def isBlackListed (declName : Name) : MetaM Bool := do
   let env ← getEnv
-  (declName.isInternal && !isPrivateName declName)
-  <||> isAuxRecursor env declName
-  <||> isNoConfusion env declName
+  (pure (declName.isInternal && !isPrivateName declName))
+  <||> (pure <| isAuxRecursor env declName)
+  <||> (pure <| isNoConfusion env declName)
   <||> isRec declName
-  <||> completionBlackListExt.isTagged env declName
+  <||> (pure <| completionBlackListExt.isTagged env declName)
   <||> isMatcher declName
 
 private partial def consumeImplicitPrefix (e : Expr) (k : Expr → MetaM α) : MetaM α := do
@@ -76,7 +76,7 @@ structure State where
 abbrev M := OptionT $ StateRefT State MetaM
 
 private def addCompletionItem (label : Name) (type : Expr) (expectedType? : Option Expr) (declName? : Option Name) (kind : CompletionItemKind) : M Unit := do
-  let docString? ← if let some declName := declName? then findDocString? (← getEnv) declName else none
+  let docString? ← if let some declName := declName? then findDocString? (← getEnv) declName else pure none
   let item ← mkCompletionItem label type docString? kind
   if (← isTypeApplicable  type expectedType?) then
     modify fun s => { s with itemsMain := s.itemsMain.push item }
@@ -88,7 +88,7 @@ private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionIt
   if constInfo.isCtor then
     return CompletionItemKind.constructor
   else if constInfo.isInductive then
-    if (← isClass env constInfo.name) then
+    if isClass env constInfo.name then
       return CompletionItemKind.class
     else if (← isEnumType constInfo.name) then
       return CompletionItemKind.enum
@@ -102,7 +102,7 @@ private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionIt
     return CompletionItemKind.constant
 
 private def addCompletionItemForDecl (label : Name) (declName : Name) (expectedType? : Option Expr) : M Unit := do
-  if let some c ← (← getEnv).find? declName then
+  if let some c := (← getEnv).find? declName then
     addCompletionItem label c.type expectedType? (some declName) (← getCompletionKindForDecl c)
 
 private def addKeywordCompletionItem (keyword : String) : M Unit := do
@@ -160,7 +160,7 @@ private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName :
           return some s₂
         else
           return none
-      | _, _ => none
+      | _, _ => return none
     else
       return none
 
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 688bf39b23..31acbe4d3c 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -134,7 +134,7 @@ section Elab
       -- followup errors
       publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
       publishIleanInfoFinal m ctx.hOut #[headerSnap]
-      AsyncList.nil
+      pure AsyncList.nil
     else
       -- This will overwrite existing ilean info for the file since this has a
       -- higher version number.
@@ -199,7 +199,7 @@ section Initialization
     let (headerStx, headerParserState, msgLog) ← Parser.parseHeader inputCtx
     let mut srcSearchPath ← initSrcSearchPath (← getBuildDir)
     let lakePath ← match (← IO.getEnv "LAKE") with
-      | some path => System.FilePath.mk path
+      | some path => pure <| System.FilePath.mk path
       | none =>
         let lakePath :=
           -- backward compatibility, kill when `leanpkg` is removed
@@ -208,7 +208,7 @@ section Initialization
         let lakePath ← match (← IO.getEnv "LEAN_SYSROOT") with
           | some path => pure <| System.FilePath.mk path / "bin" / lakePath
           | _         => pure <| (← appDir) / lakePath
-        lakePath.withExtension System.FilePath.exeExtension
+        pure <| lakePath.withExtension System.FilePath.exeExtension
     let (headerEnv, msgLog) ← try
       if let some path := m.uri.toPath? then
         -- NOTE: we assume for now that `lakefile.lean` does not have any non-stdlib deps
@@ -224,7 +224,7 @@ section Initialization
     try
       if let some path := m.uri.toPath? then
         headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none)
-    catch _ => ()
+    catch _ => pure ()
     let cmdState := Elab.Command.mkState headerEnv msgLog opts
     let cmdState := { cmdState with infoState := {
       enabled := true
@@ -316,7 +316,7 @@ section Updates
           else newHeaderSnap
         let newLastStx ← parseNextCmd newMeta.text.source preLastSnap
         if newLastStx != lastSnap.stx then
-          validSnaps ← validSnaps.dropLast
+          validSnaps := validSnaps.dropLast
         let cancelTk ← CancelToken.new
         let newSnaps ← unfoldCmdSnaps newMeta newHeaderSnap validSnaps.toArray cancelTk ctx
         let newCmdSnaps := AsyncList.ofList validSnaps ++ newSnaps
@@ -437,13 +437,13 @@ section MainLoop
     let msg ← ctx.hIn.readLspMessage
     let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
         : IO PendingRequestMap := do
-      if (←hasFinished task) then
+      if (← hasFinished task) then
         /- Handler tasks are constructed so that the only possible errors here
         are failures of writing a response into the stream. -/
         if let Except.error e := task.get then
           throwServerError s!"Failed responding to request {id}: {e}"
-        acc.erase id
-      else acc
+        pure <| acc.erase id
+      else pure acc
     let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests
     st := { st with pendingRequests }
 
@@ -459,7 +459,7 @@ section MainLoop
       handleRequest id method (toJson params)
       mainLoop
     | Message.notification "exit" none =>
-      let doc ← (←get).doc
+      let doc := (←get).doc
       doc.cancelTk.set
       return ()
     | Message.notification method (some params) =>
@@ -480,7 +480,7 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
     so if we get the line number correct it shouldn't matter that there
     is a CR there. -/
   let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩
-  let e ← e.withPrefix s!"[{param.textDocument.uri}] "
+  let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try
     let (ctx, st) ← initializeWorker meta i o e initParams.param opts
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index a77ffe5a34..ad31df69b0 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -132,7 +132,7 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
           let mut expr := ti.expr
           if kind == type then
             expr ← ci.runMetaM i.lctx do
-              Expr.getAppFn (← Meta.instantiateMVars (← Meta.inferType expr))
+              return Expr.getAppFn (← Meta.instantiateMVars (← Meta.inferType expr))
           match expr with
           | Expr.const n .. => return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
           | Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder snap.infoTree i id
@@ -177,7 +177,7 @@ open Elab in
 partial def handlePlainGoal (p : PlainGoalParams)
     : RequestM (RequestTask (Option PlainGoal)) := do
   let t ← getInteractiveGoals p
-  t.map <| Except.map <| Option.map <| fun ⟨goals⟩ =>
+  return t.map <| Except.map <| Option.map <| fun ⟨goals⟩ =>
     if goals.isEmpty then
       { goals := #[], rendered := "no goals" }
     else
@@ -210,7 +210,7 @@ partial def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
 def handlePlainTermGoal (p : PlainTermGoalParams)
     : RequestM (RequestTask (Option PlainTermGoal)) := do
   let t ← getInteractiveTermGoal p
-  t.map <| Except.map <| Option.map fun goal =>
+  return t.map <| Except.map <| Option.map fun goal =>
     { goal := toString goal.toInteractiveGoal.pretty
       range := goal.range
     }
@@ -246,7 +246,7 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams)
   withWaitFindSnap doc (fun s => s.endPos > pos)
     (notFoundX := pure #[]) fun snap => do
       let (snaps, _) ← doc.allSnaps.updateFinishedPrefix
-      if let some his ← highlightRefs? snaps.finishedPrefix.toArray p.position then
+      if let some his := highlightRefs? snaps.finishedPrefix.toArray p.position then
         return his
       if let some hi := highlightReturn? none snap.stx then
         return #[hi]
@@ -265,7 +265,7 @@ partial def handleDocumentSymbol (p : DocumentSymbolParams)
       throw RequestError.fileChanged
     | some (ElabTaskError.ioError e) =>
       throw (e : RequestError)
-    | _ => ()
+    | _ => pure ()
 
     let lastSnap := cmdSnaps.finishedPrefix.getLastD doc.headerSnap
     stxs := stxs ++ (← parseAhead doc.meta.text.source lastSnap).toList
diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index 604c128e2a..5fc46bbc9d 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -43,11 +43,11 @@ builtin_initialize
       i.ctx.runMetaM i.info.lctx do
         let type? ← match (← i.info.type?) with
           | some type => some <$> exprToInteractive type
-          | none => none
+          | none => pure none
         let exprExplicit? ← match i.info with
           | Elab.Info.ofTermInfo ti => some <$> exprToInteractiveExplicit ti.expr
-          | Elab.Info.ofFieldInfo fi => some (TaggedText.text fi.fieldName.toString)
-          | _ => none
+          | Elab.Info.ofFieldInfo fi => pure <| some (TaggedText.text fi.fieldName.toString)
+          | _ => pure none
         return {
           type := type?
           exprExplicit := exprExplicit?
@@ -76,17 +76,17 @@ structure GetInteractiveDiagnosticsParams where
 open RequestM in
 def getInteractiveDiagnostics (params : GetInteractiveDiagnosticsParams) : RequestM (RequestTask (Array InteractiveDiagnostic)) := do
   let doc ← readDoc
-  let rangeEnd ← params.lineRange?.map fun range =>
+  let rangeEnd := params.lineRange?.map fun range =>
     doc.meta.text.lspPosToUtf8Pos ⟨range.«end», 0⟩
   let t ← doc.cmdSnaps.waitAll fun snap => rangeEnd.all (snap.beginPos < ·)
-  t.map fun (snaps, _) =>
+  pure <| t.map fun (snaps, _) =>
     let diags? := snaps.getLast?.map fun snap =>
       snap.interactiveDiags.toArray.filter fun diag =>
         params.lineRange?.all fun ⟨s, e⟩ =>
           -- does [s,e) intersect [diag.fullRange.start.line,diag.fullRange.end.line)?
           s ≤ diag.fullRange.start.line ∧ diag.fullRange.start.line < e ∨
           diag.fullRange.start.line ≤ s ∧ s < diag.fullRange.end.line
-    diags?.getD #[]
+    pure <| diags?.getD #[]
 
 builtin_initialize
   registerRpcCallHandler
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 44669da11c..0c2f72cad6 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -163,9 +163,9 @@ def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do
     if let some m ← i.docString? then
       fmts := fmts.push m
     if fmts.isEmpty then
-      none
+      return none
     else
-      f!"\n***\n".joinSep fmts.toList
+      return f!"\n***\n".joinSep fmts.toList
 
 where
   fmtTerm? : MetaM (Option Format) := do
diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean
index c64d7d5e8d..c29111657c 100644
--- a/src/Lean/Server/References.lean
+++ b/src/Lean/Server/References.lean
@@ -234,7 +234,7 @@ def referringTo (self : References) (ident : RefIdent) (srcSearchPath : SearchPa
             result := result.push ⟨uri, range⟩
         for range in info.usages do
           result := result.push ⟨uri, range⟩
-  result
+  return result
 
 def definitionOf? (self : References) (ident : RefIdent) (srcSearchPath : SearchPath)
     : IO (Option Location) := do
diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean
index 2008ad59ea..bf3809c55a 100644
--- a/src/Lean/Server/Requests.lean
+++ b/src/Lean/Server/Requests.lean
@@ -76,7 +76,7 @@ open FileWorker
 open Snapshots
 
 def readDoc : RequestM EditableDocument := fun rc =>
-  rc.doc
+  return rc.doc
 
 def asTask (t : RequestM α) : RequestM (RequestTask α) := fun rc => do
   let t ← EIO.asTask <| t rc
@@ -146,12 +146,12 @@ def registerLspRequestHandler (method : String)
   let handle := fun j => do
     let params ← liftExcept <| parseRequestParams paramType j
     let t ← handler params
-    t.map <| Except.map ToJson.toJson
+    pure <| t.map <| Except.map ToJson.toJson
 
   requestHandlers.modify fun rhs => rhs.insert method { fileSource, handle }
 
-def lookupLspRequestHandler (method : String) : IO (Option RequestHandler) := do
-  (← requestHandlers.get).find? method
+def lookupLspRequestHandler (method : String) : IO (Option RequestHandler) :=
+  return (← requestHandlers.get).find? method
 
 /-- NB: This method may only be called in `builtin_initialize` blocks.
 
@@ -169,11 +169,11 @@ def chainLspRequestHandler (method : String)
   if let some oldHandler ← lookupLspRequestHandler method then
     let handle := fun j => do
       let t ← oldHandler.handle j
-      let t ← t.map fun x => x.bind fun j => FromJson.fromJson? j |>.mapError fun e =>
+      let t := t.map fun x => x.bind fun j => FromJson.fromJson? j |>.mapError fun e =>
         IO.userError s!"Failed to parse original LSP response for `{method}` when chaining: {e}"
       let params ← liftExcept <| parseRequestParams paramType j
       let t ← handler params t
-      t.map <| Except.map ToJson.toJson
+      pure <| t.map <| Except.map ToJson.toJson
 
     requestHandlers.modify fun rhs => rhs.insert method {oldHandler with handle}
   else
diff --git a/src/Lean/Server/Rpc/Basic.lean b/src/Lean/Server/Rpc/Basic.lean
index 31fa53666b..1d1c5f93c0 100644
--- a/src/Lean/Server/Rpc/Basic.lean
+++ b/src/Lean/Server/Rpc/Basic.lean
@@ -52,10 +52,10 @@ instance [FromJson α] [ToJson α] : RpcEncoding α α where
 
 instance [RpcEncoding α β] : RpcEncoding (Option α) (Option β) where
   rpcEncode v := match v with
-    | none => none
+    | none => pure none
     | some v => some <$> rpcEncode v
   rpcDecode v := match v with
-    | none => none
+    | none => pure none
     | some v => some <$> rpcDecode v
 
 -- TODO(WN): instance [RpcEncoding α β] [Traversable t] : RpcEncoding (t α) (t β)
@@ -98,7 +98,7 @@ protected unsafe def decodeUnsafeAs (α) (typeName : Name) (r : Lsp.RpcRef) : Ex
     | some (nm, obj) =>
       if nm != typeName then
         throw s!"RPC call type mismatch in reference '{r}'\nexpected '{typeName}', got '{nm}'"
-      WithRpcRef.mk <| @unsafeCast NonScalar α obj
+      return WithRpcRef.mk <| @unsafeCast NonScalar α obj
 
 end WithRpcRef
 end Lean.Server
diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean
index ff44f57f4c..20ee017686 100644
--- a/src/Lean/Server/Rpc/Deriving.lean
+++ b/src/Lean/Server/Rpc/Deriving.lean
@@ -48,7 +48,7 @@ private def deriveWithRefInstance (typeNm : Name) : CommandElabM Bool := do
 by their `RpcEncoding` and uses that to instantiate `RpcEncoding α LspPacket`. -/
 private def deriveInstance (typeName : Name) : CommandElabM Bool := do
   let env ← getEnv
-  if !(← isStructure env typeName) then
+  if !isStructure env typeName then
     throwError "only structures are supported"
   let indVal ← getConstInfoInduct typeName
   if indVal.all.length ≠ 1 then
@@ -69,7 +69,7 @@ private def deriveInstance (typeName : Name) : CommandElabM Bool := do
           throwError "failed to construct 'RpcEncoding {tp} {β}':\n{ex.toMessageData}"
       match (← trySynthInstance clTp) with
       | LOption.some _ => instantiateMVars β
-      | _ => none
+      | _ => pure none
 
     forallTelescopeReducing ctorVal.type fun xs _ => do
       if xs.size != numParams + fields.size then
diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean
index 603cb7d06a..2ec83fa743 100644
--- a/src/Lean/Server/Rpc/RequestHandling.lean
+++ b/src/Lean/Server/Rpc/RequestHandling.lean
@@ -19,7 +19,7 @@ builtin_initialize rpcProcedures : IO.Ref (Std.PersistentHashMap Name RpcProcedu
 
 private def handleRpcCall (p : Lsp.RpcCallParams) : RequestM (RequestTask Json) := do
   let rc ← read
-  let some proc ← (← rpcProcedures.get).find? p.method
+  let some proc := (← rpcProcedures.get).find? p.method
     | throwThe RequestError { code := JsonRpc.ErrorCode.methodNotFound
                               message := s!"No RPC method '{p.method}' bound" }
   proc.wrapper p.sessionId p.params
@@ -41,7 +41,7 @@ def registerRpcCallHandler (method : Name)
   let wrapper seshId j := do
     let rc ← read
 
-    let some seshRef ← rc.rpcSessions.find? seshId
+    let some seshRef := rc.rpcSessions.find? seshId
       | throwThe RequestError { code := JsonRpc.ErrorCode.rpcNeedsReconnect
                                 message := s!"Outdated RPC session" }
     let t ← RequestM.asTask do
@@ -62,7 +62,7 @@ def registerRpcCallHandler (method : Name)
       | Except.error e => throw e
       | Except.ok ret => do
         let act := rpcEncode (α := respType) (β := respLspType) (m := StateM FileWorker.RpcSession) ret
-        toJson (← seshRef.modifyGet act.run)
+        return toJson (← seshRef.modifyGet act.run)
 
   rpcProcedures.modify fun ps => ps.insert method ⟨wrapper⟩
 
diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean
index 73016a3a5d..d93ded7097 100644
--- a/src/Lean/Server/Snapshots.lean
+++ b/src/Lean/Server/Snapshots.lean
@@ -75,7 +75,7 @@ def parseNextCmd (contents : String) (snap : Snapshot) : IO Syntax := do
   let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
   let (cmdStx, _, _) :=
     Parser.parseCommand inputCtx pmctx snap.mpState snap.msgLog
-  cmdStx
+  return cmdStx
 
 /--
   Parse remaining file without elaboration. NOTE that doing so can lead to parse errors or even wrong syntax objects,
@@ -90,7 +90,7 @@ partial def parseAhead (contents : String) (snap : Snapshot) : IO (Array Syntax)
     go inputCtx pmctx cmdParserState stxs := do
       let (cmdStx, cmdParserState, _) := Parser.parseCommand inputCtx pmctx cmdParserState snap.msgLog
       if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then
-        stxs.push cmdStx
+        return stxs.push cmdStx
       else
         go inputCtx pmctx cmdParserState (stxs.push cmdStx)
 
@@ -115,7 +115,7 @@ def compileNextCmd (text : FileMap) (snap : Snapshot) (hasWidgets : Bool) : IO S
       cmdState := snap.cmdState
       interactiveDiags := ← withNewInteractiveDiags msgLog
     }
-    endSnap
+    return endSnap
   else
     let cmdStateRef ← IO.mkRef { snap.cmdState with messages := msgLog }
     let cmdCtx : Elab.Command.Context := {
@@ -145,7 +145,7 @@ def compileNextCmd (text : FileMap) (snap : Snapshot) (hasWidgets : Bool) : IO S
       cmdState := postCmdState
       interactiveDiags := ← withNewInteractiveDiags postCmdState.messages
     }
-    postCmdSnap
+    return postCmdSnap
 
 where
   /-- Compute the current interactive diagnostics log by finding a "diff" relative to the parent
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index 70a6f5a5d3..a908f7583c 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -188,8 +188,8 @@ section ServerM
   def updateFileWorkers (val : FileWorker) : ServerM Unit := do
     (←read).fileWorkersRef.modify (fun fileWorkers => fileWorkers.insert val.doc.meta.uri val)
 
-  def findFileWorker? (uri : DocumentUri) : ServerM (Option FileWorker) := do
-    (←(←read).fileWorkersRef.get).find? uri
+  def findFileWorker? (uri : DocumentUri) : ServerM (Option FileWorker) :=
+    return (← (←read).fileWorkersRef.get).find? uri
 
   def findFileWorker! (uri : DocumentUri) : ServerM FileWorker := do
     let some fw ← findFileWorker? uri
@@ -262,7 +262,7 @@ section ServerM
           return WorkerEvent.crashed err
       loop
     let task ← IO.asTask (loop $ ←read) Task.Priority.dedicated
-    task.map fun
+    return task.map fun
       | Except.ok ev   => ev
       | Except.error e => WorkerEvent.ioError e
 
@@ -384,7 +384,7 @@ def handleReference (p : ReferenceParams) : ServerM (Array Location) := do
       let references ← (← read).references.get
       if let some ident := references.findAt? module p.position then
         return ← references.referringTo ident srcSearchPath p.context.includeDeclaration
-  #[]
+  return #[]
 
 -- TODO Better matching https://github.com/leanprover/lean4/issues/960
 def handleWorkspaceSymbol (p : WorkspaceSymbolParams) : ServerM (Array SymbolInformation) := do
@@ -398,7 +398,7 @@ def handleWorkspaceSymbol (p : WorkspaceSymbolParams) : ServerM (Array SymbolInf
       else
         none
   -- TODO Sort symbols by some useful metric?
-  symbols.map fun (name, location) =>
+  return symbols.map fun (name, location) =>
     { name, kind := SymbolKind.constant, location }
 where
   containsCaseInsensitive (value : String) : String → Bool :=
@@ -500,12 +500,12 @@ section MessageHandling
       -- This request is handled specially.
       if method == "$/lean/rpc/connect" then
         let ps ← parseParams Lsp.RpcConnectParams params
-        fileSource ps
+        pure <| fileSource ps
       else match (← routeLspRequest method params) with
       | Except.error e =>
         (←read).hOut.writeLspResponseError <| e.toLspResponseError id
         return
-      | Except.ok uri => uri
+      | Except.ok uri => pure uri
     let some fw ← findFileWorker? uri
       /- Clients may send requests to closed files, which we respond to with an error.
       For example, VSCode sometimes sends requests just after closing a file,
@@ -585,7 +585,7 @@ section MainLoop
     let readMsgAction : IO ServerEvent := do
       /- Runs asynchronously. -/
       let msg ← st.hIn.readLspMessage
-      ServerEvent.clientMsg msg
+      pure <| ServerEvent.clientMsg msg
     let clientTask := (← IO.asTask readMsgAction).map fun
       | Except.ok ev   => ev
       | Except.error e => ServerEvent.clientError e
@@ -641,7 +641,7 @@ section MainLoop
                 code := ErrorCode.contentModified
                 message := "File changed."
               }
-            | _ => () -- notifications do not need to be cancelled
+            | _ => pure () -- notifications do not need to be cancelled
         | _ =>
           let t ← fw.runEditsSignalTask
           fw.groupedEditsRef.modify (Option.map fun ge => { ge with signalTask := t } )
@@ -719,7 +719,7 @@ def findWorkerPath : IO System.FilePath := do
     workerPath := System.FilePath.mk path / "bin" / "lean" |>.withExtension System.FilePath.exeExtension
   if let some path := (←IO.getEnv "LEAN_WORKER_PATH") then
     workerPath := System.FilePath.mk path
-  workerPath
+  return workerPath
 
 def loadReferences : IO References := do
   let oleanSearchPath ← Lean.searchPathRef.get
@@ -732,7 +732,7 @@ def loadReferences : IO References := do
       -- ilean load errors should not be fatal, but we *should* log them
       -- when we add logging to the server
       pure ()
-  refs
+  return refs
 
 def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
   let workerPath ← findWorkerPath
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 9f671a1368..3b88626634 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -349,7 +349,7 @@ def goRight               : m Unit := @modify _ _ t.st (fun t => t.right)
 
 def getIdx : m Nat := do
   let st ← t.st.get
-  st.idxs.back?.getD 0
+  return st.idxs.back?.getD 0
 
 end MonadTraverser
 end Syntax
diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean
index 88d2657158..5b2a04be12 100644
--- a/src/Lean/Util/Path.lean
+++ b/src/Lean/Util/Path.lean
@@ -13,8 +13,8 @@ import Lean.Data.Name
 namespace Lean
 open System
 
-def realPathNormalized (p : FilePath) : IO FilePath := do
-  (← IO.FS.realPath p).normalize
+def realPathNormalized (p : FilePath) : IO FilePath :=
+  return (← IO.FS.realPath p).normalize
 
 def modToFilePath (base : FilePath) (mod : Name) (ext : String) : FilePath :=
   go mod |>.withExtension ext
@@ -50,7 +50,7 @@ def findAllWithExt (sp : SearchPath) (ext : String) : IO (Array FilePath) := do
   for p in sp do
     if (← p.isDir) then
       paths := paths ++ (← p.walkDir).filter (·.extension == some ext)
-  paths
+  return paths
 
 end SearchPath
 
@@ -69,7 +69,7 @@ def getLibDir (leanSysroot : FilePath) : IO FilePath := do
   -- use stage1 stdlib with stage0 executable (which should never be distributed outside of the build directory)
   if isStage0 () then
     buildDir := buildDir / ".." / "stage1"
-  buildDir / "lib" / "lean"
+  return buildDir / "lib" / "lean"
 
 def getBuiltinSearchPath (leanSysroot : FilePath) : IO SearchPath :=
   return [← getLibDir leanSysroot]
@@ -102,7 +102,7 @@ partial def findOLean (mod : Name) : IO FilePath := do
     let rec maybeThisOne dir := do
       if ← (dir / pkg).isDir then
         return some s!"\nYou might need to open '{dir}' as a workspace in your editor"
-      if let some dir ← dir.parent then
+      if let some dir := dir.parent then
         maybeThisOne dir
       else
        return none
@@ -134,8 +134,8 @@ def searchModuleNameOfFileName (fname : FilePath) (rootDirs : SearchPath) : IO (
       return some <| ← moduleNameOfFileName fname <| some rootDir
     catch
       -- Try the next one
-      | e => ()
-  none
+      | e => pure ()
+  return none
 
 /--
   Find the system root of the given `lean` command
@@ -153,6 +153,6 @@ def findSysroot? (lean := "lean") : IO FilePath := do
     cmd := lean
     args := #["--print-prefix"]
   }
-  out.trim
+  return out.trim
 
 end Lean
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index 04b091e1d7..6fc29526ad 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -46,7 +46,7 @@ where
 
   go (addr : List Nat) (lctx : LocalContext) (e : Expr) : MetaM (LocalContext × Expr) := do
     match addr with
-    | [] => (lctx, e)
+    | [] => return (lctx, e)
     | a::as => do
       let go' (e' : Expr) := do
         go as (← getLCtx) e'
@@ -69,7 +69,7 @@ where
             go' (e₃.instantiate1 fvar)
         | 0, mdata _ e₁ _  => go' e₁
         | 0, proj _ _ e₁ _ => go' e₁
-        | _, _             => (lctx, e) -- panic! s!"cannot descend {a} into {e.expr}"
+        | _, _             => return (lctx, e) -- panic! s!"cannot descend {a} into {e.expr}"
 
 -- TODO(WN): should the two fns below go in `Lean.PrettyPrinter` ?
 open PrettyPrinter in
@@ -116,7 +116,7 @@ def exprToInteractive (e : Expr) : MetaM CodeWithInfos := do
     openDecls := ← getOpenDecls
     fileMap := default
   }
-  tagExprInfos ctx infos tt
+  return tagExprInfos ctx infos tt
 
 def exprToInteractiveExplicit (e : Expr) : MetaM CodeWithInfos := do
   let (fmt, infos) ← formatExplicitInfos e
@@ -130,6 +130,6 @@ def exprToInteractiveExplicit (e : Expr) : MetaM CodeWithInfos := do
     fileMap := default
   }
   let infos := infos.erase 1 -- remove highlight for entire expression in popups
-  tagExprInfos ctx infos tt
+  return tagExprInfos ctx infos tt
 
 end Lean.Widget
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index 5aecebc666..6cfdf627fa 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -115,12 +115,12 @@ where
     return Format.tag t fmt
 
   go : NamingContext → Option MessageDataContext → MessageData → MsgFmtM Format
-  | _,    _,         ofFormat fmt             => withIgnoreTags fmt
-  | _,    _,         ofLevel u                => format u
-  | _,    _,         ofName n                 => format n
+  | _,    _,         ofFormat fmt             => withIgnoreTags (pure fmt)
+  | _,    _,         ofLevel u                => return format u
+  | _,    _,         ofName n                 => return format n
   | nCtx, some ctx,  ofSyntax s               => withIgnoreTags (ppTerm (mkPPContext nCtx ctx) s) -- HACK: might not be a term
-  | _,    none,      ofSyntax s               => withIgnoreTags s.formatStx
-  | _,    none,      ofExpr e                 => format (toString e)
+  | _,    none,      ofSyntax s               => withIgnoreTags (pure s.formatStx)
+  | _,    none,      ofExpr e                 => return format (toString e)
   | nCtx, some ctx,  ofExpr e                 => do
     let ci : Elab.ContextInfo := {
       env := ctx.env
@@ -144,7 +144,7 @@ where
       -- take significant resources to pretty-print.
       if hasWidgets then
         let f ← pushEmbed <| EmbedFmt.lazyTrace nCtx ctx cls d
-        Format.tag f s!"[{cls}] (trace hidden)"
+        return Format.tag f s!"[{cls}] (trace hidden)"
       else
         go nCtx ctx d
     else
@@ -165,7 +165,7 @@ partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent
     match embeds.get! n with
     | EmbedFmt.expr ctx infos =>
       let subTt' := tagExprInfos ctx infos subTt
-      TaggedText.tag (MsgEmbed.expr subTt') (TaggedText.text subTt.stripTags)
+      return TaggedText.tag (MsgEmbed.expr subTt') (TaggedText.text subTt.stripTags)
     | EmbedFmt.goal ctx lctx g =>
       -- TODO(WN): use InteractiveGoal types here
       unreachable!
@@ -174,8 +174,8 @@ partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent
         match ctx? with
         | some ctx => MessageData.withNamingContext nCtx <| MessageData.withContext ctx m
         | none     => MessageData.withNamingContext nCtx m
-      TaggedText.tag (MsgEmbed.lazyTrace col cls ⟨msg⟩) (TaggedText.text subTt.stripTags)
-    | EmbedFmt.ignoreTags => TaggedText.text subTt.stripTags
+      return TaggedText.tag (MsgEmbed.lazyTrace col cls ⟨msg⟩) (TaggedText.text subTt.stripTags)
+    | EmbedFmt.ignoreTags => return TaggedText.text subTt.stripTags
 
 /-- Transform a Lean Message concerning the given text into an LSP Diagnostic. -/
 def msgToInteractiveDiagnostic (text : FileMap) (m : Message) (hasWidgets : Bool) : IO InteractiveDiagnostic := do
@@ -201,7 +201,7 @@ def msgToInteractiveDiagnostic (text : FileMap) (m : Message) (hasWidgets : Bool
   let message ← try
       msgToInteractive m.data hasWidgets
     catch ex =>
-      TaggedText.text s!"[error when printing message: {ex.toString}]"
+      pure <| TaggedText.text s!"[error when printing message: {ex.toString}]"
   pure {
     range := range
     fullRange := fullRange
diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean
index f5064d6f86..961bad568e 100644
--- a/src/Lean/Widget/InteractiveGoal.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -79,7 +79,7 @@ def addInteractiveHypothesis (hyps : Array InteractiveHypothesis) (ids : Array N
 open Meta in
 /-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
 def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
-  let some mvarDecl ← (← getMCtx).findDecl? mvarId
+  let some mvarDecl := (← getMCtx).findDecl? mvarId
     | throwError "unknown goal {mvarId.name}"
   let ppAuxDecls := pp.auxDecls.get (← getOptions)
   let lctx := mvarDecl.lctx
diff --git a/src/Lean/Widget/TaggedText.lean b/src/Lean/Widget/TaggedText.lean
index 7b1992c1d3..58dffd911c 100644
--- a/src/Lean/Widget/TaggedText.lean
+++ b/src/Lean/Widget/TaggedText.lean
@@ -46,9 +46,9 @@ partial def map : TaggedText α → TaggedText β
 
 variable [Monad m] (f : α → m β) in
 partial def mapM : TaggedText α → m (TaggedText β)
-  | text s => text s
-  | append as => do append (← as.mapM mapM)
-  | tag t a => do tag (← f t) (← mapM a)
+  | text s => return text s
+  | append as => return append (← as.mapM mapM)
+  | tag t a => return tag (← f t) (← mapM a)
 
 variable (f : α → TaggedText α → TaggedText β) in
 partial def rewrite : TaggedText α → TaggedText β
@@ -59,8 +59,8 @@ partial def rewrite : TaggedText α → TaggedText β
 variable [Monad m] (f : α → TaggedText α → m (TaggedText β)) in
 /-- Like `mapM` but allows rewriting the whole subtree at `tag` nodes. -/
 partial def rewriteM : TaggedText α → m (TaggedText β)
-  | text s => text s
-  | append as => do append (← as.mapM rewriteM)
+  | text s => return text s
+  | append as => return append (← as.mapM rewriteM)
   | tag t a => f t a
 
 instance [RpcEncoding α β] : RpcEncoding (TaggedText α) (TaggedText β) where
diff --git a/src/Leanc.lean b/src/Leanc.lean
index 61f1a69358..976d764dee 100644
--- a/src/Leanc.lean
+++ b/src/Leanc.lean
@@ -18,8 +18,8 @@ Beware of the licensing consequences since GMP is LGPL."
     return 1
 
   let root ← match (← IO.getEnv "LEAN_SYSROOT") with
-    | some root => System.FilePath.mk root
-    | none      => (← IO.appDir).parent.get!
+    | some root => pure <| System.FilePath.mk root
+    | none      => pure <| (← IO.appDir).parent.get!
   let rootify s := s.replace "ROOT" root.toString
 
   let compileOnly := args.contains "-c"
@@ -39,7 +39,7 @@ Beware of the licensing consequences since GMP is LGPL."
     | "--print-ldflags" =>
       IO.println <| " ".intercalate ((cflags ++ ldflags).map rootify |>.toList)
       return 0
-    | _ => ()
+    | _ => pure ()
 
   let mut cc := "@LEANC_CC@"
   if let some cc' ← IO.getEnv "LEAN_CC" then
diff --git a/src/Leanpkg.lean b/src/Leanpkg.lean
index 7587ab1d23..b7e15e4c51 100644
--- a/src/Leanpkg.lean
+++ b/src/Leanpkg.lean
@@ -54,7 +54,7 @@ partial def withLockFile (x : IO α) : IO α := do
 def getRootPart (pkg : FilePath := ".") : IO Lean.Name := do
   let entries ← pkg.readDir
   match entries.filter (FilePath.extension ·.fileName == "lean") with
-  | #[rootFile] => FilePath.withExtension rootFile.fileName "" |>.toString
+  | #[rootFile] => pure <| FilePath.withExtension rootFile.fileName "" |>.toString
   | #[]         => throw <| IO.userError s!"no '.lean' file found in {← IO.FS.realPath "."}"
   | _           => throw <| IO.userError s!"{← IO.FS.realPath "."} must contain a unique '.lean' file as the package root"
 
diff --git a/src/Leanpkg/Build.lean b/src/Leanpkg/Build.lean
index 8b396d7d6c..49580f5645 100644
--- a/src/Leanpkg/Build.lean
+++ b/src/Leanpkg/Build.lean
@@ -57,7 +57,7 @@ partial def buildModule (mod : Name) : BuildM Result := do
   let deps ← localImports.mapM fun i =>
     withReader (fun ctx => { ctx with parents := mod :: ctx.parents }) <|
       buildModule i.module
-  let depMTimes ← deps.mapM (·.maxMTime)
+  let depMTimes := deps.map (·.maxMTime)
   let maxMTime := List.maximum? (leanMData.modified :: ctx.moreDepsMTime :: depMTimes) |>.get!
 
   -- check whether we have an up-to-date .olean
diff --git a/src/Leanpkg/Git.lean b/src/Leanpkg/Git.lean
index 55ce109228..a323e6cbb8 100644
--- a/src/Leanpkg/Git.lean
+++ b/src/Leanpkg/Git.lean
@@ -18,7 +18,7 @@ def gitdefaultRevision : Option String → String
 
 def gitParseRevision (gitRepo : FilePath) (rev : String) : IO String := do
   let rev ← IO.Process.run {cmd := "git", args := #["rev-parse", "-q", "--verify", rev], cwd := gitRepo}
-  rev.trim -- remove newline at end
+  pure rev.trim -- remove newline at end
 
 def gitHeadRevision (gitRepo : FilePath) : IO String :=
   gitParseRevision gitRepo "HEAD"
@@ -34,7 +34,7 @@ def gitLatestOriginRevision (gitRepo : FilePath) (branch : Option String) : IO S
 def gitRevisionExists (gitRepo : FilePath) (rev : String) : IO Bool := do
   try
     discard <| gitParseRevision gitRepo (rev ++ "^{commit}")
-    true
-  catch _ => false
+    pure true
+  catch _ => pure false
 
 end Leanpkg
diff --git a/src/Leanpkg/Manifest.lean b/src/Leanpkg/Manifest.lean
index e993564abb..15e8613160 100644
--- a/src/Leanpkg/Manifest.lean
+++ b/src/Leanpkg/Manifest.lean
@@ -18,12 +18,12 @@ namespace Source
 
 def fromToml (v : Toml.Value) : OptionM Source :=
   (do let Toml.Value.str dir ← v.lookup "path" | none
-      path ⟨dir⟩) <|>
+      pure <| path ⟨dir⟩) <|>
   (do let Toml.Value.str url ← v.lookup "git" | none
       let Toml.Value.str rev ← v.lookup "rev" | none
       match v.lookup "branch" with
-      | none                         => git url rev none
-      | some (Toml.Value.str branch) => git url rev (some branch)
+      | none                         => pure <| git url rev none
+      | some (Toml.Value.str branch) => pure <| git url rev (some branch)
       | _ => none)
 
 def toToml : Source → Toml.Value
@@ -69,7 +69,7 @@ def fromToml (t : Toml.Value) : Option Manifest := OptionM.run do
     | none => some none
     | _ => none
   let Toml.Value.table deps ← t.lookup "dependencies" <|> some (Toml.Value.table []) | none
-  let deps ← deps.mapM fun ⟨n, src⟩ => do Dependency.mk n (← Source.fromToml src)
+  let deps ← deps.mapM fun ⟨n, src⟩ => return Dependency.mk n (← Source.fromToml src)
   return { name := n, version := ver, leanVersion := leanVer,
            path := path, dependencies := deps, timeout := tm }
 
@@ -78,7 +78,7 @@ def fromFile (fn : System.FilePath) : IO Manifest := do
   let toml ← Toml.parse cnts
   let some manifest ← pure (fromToml toml)
     | throw <| IO.userError s!"cannot read manifest from {fn}"
-  manifest
+  return manifest
 
 end Manifest
 
diff --git a/src/Leanpkg/Resolve.lean b/src/Leanpkg/Resolve.lean
index 57f76c1b02..f81712cc9c 100644
--- a/src/Leanpkg/Resolve.lean
+++ b/src/Leanpkg/Resolve.lean
@@ -29,12 +29,12 @@ end Assignment
 
 abbrev Solver := StateT Assignment IO
 
-def notYetAssigned (d : String) : Solver Bool := do
-  ¬ (← get).contains d
+def notYetAssigned (d : String) : Solver Bool :=
+  return ! (← get).contains d
 
 def resolvedPath (d : String) : Solver FilePath := do
   let some path ← pure ((← get).lookup d) | unreachable!
-  path
+  return path
 
 def materialize (relpath : FilePath) (dep : Dependency) : Solver Unit :=
   match dep.src with
@@ -72,10 +72,10 @@ def solveDepsCore (relPath : FilePath) (d : Manifest) : (maxDepth : Nat) → Sol
 
 def solveDeps (d : Manifest) : IO Assignment := do
   let (_, assg) ← (solveDepsCore ⟨"."⟩ d 1024).run <| Assignment.empty.insert d.name ⟨"."⟩
-  assg
+  return assg
 
 def constructPathCore (depname : String) (dirname : FilePath) : IO FilePath := do
-  let path ← Manifest.effectivePath (← Manifest.fromFile <| dirname / leanpkgTomlFn)
+  let path := Manifest.effectivePath (← Manifest.fromFile <| dirname / leanpkgTomlFn)
   return dirname / path
 
 def constructPath (assg : Assignment) : IO (List FilePath) := do
diff --git a/src/Leanpkg/Toml.lean b/src/Leanpkg/Toml.lean
index 31d910a63e..4a3f7173e2 100644
--- a/src/Leanpkg/Toml.lean
+++ b/src/Leanpkg/Toml.lean
@@ -65,7 +65,7 @@ def parse (input : String) : IO Value := do
   if s.hasError then
     throw <| IO.userError (s.toErrorMsg c)
   else if input.atEnd s.pos then
-    ofSyntax s.stxStack.back
+    return ofSyntax s.stxStack.back
   else
     throw <| IO.userError ((s.mkError "end of input").toErrorMsg c)