diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 86765aa384..cd519d2dd3 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -545,7 +545,7 @@ def getMax? (as : Array α) (lt : α → α → Bool) : Option α :=
     none
 
 @[inline]
-def partition (p : α → Bool) (as : Array α) : Array α × Array α := do
+def partition (p : α → Bool) (as : Array α) : Array α × Array α := Id.run <| do
   let mut bs := #[]
   let mut cs := #[]
   for a in as do
diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index 1dfcfd774a..76ca13608c 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -100,7 +100,7 @@ def toSubarray (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Suba
      else
        { as := as, start := as.size, stop := as.size, h₁ := Nat.le_refl _, h₂ := Nat.le_refl _ }
 
-def ofSubarray (s : Subarray α) : Array α := do
+def ofSubarray (s : Subarray α) : Array α := Id.run <| do
   let mut as := mkEmpty (s.stop - s.start)
   for a in s do
     as := as.push a
diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 14449194cf..f545cf2022 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -365,7 +365,7 @@ def mkIdent (val : Name) : Syntax :=
 @[inline] def mkGroupNode (args : Array Syntax := #[]) : Syntax :=
   mkNode groupKind args
 
-def mkSepArray (as : Array Syntax) (sep : Syntax) : Array Syntax := do
+def mkSepArray (as : Array Syntax) (sep : Syntax) : Array Syntax := Id.run <| do
   let mut i := 0
   let mut r := #[]
   for a in as do
diff --git a/src/Lean/Compiler/IR/Format.lean b/src/Lean/Compiler/IR/Format.lean
index 28eeaf0b04..464e8f8134 100644
--- a/src/Lean/Compiler/IR/Format.lean
+++ b/src/Lean/Compiler/IR/Format.lean
@@ -24,7 +24,7 @@ private def formatLitVal : LitVal → Format
 instance : ToFormat LitVal := ⟨formatLitVal⟩
 
 private def formatCtorInfo : CtorInfo → Format
-  | { name := name, cidx := cidx, usize := usize, ssize := ssize, .. } => do
+  | { name := name, cidx := cidx, usize := usize, ssize := ssize, .. } => Id.run <| do
     let mut r := f!"ctor_{cidx}"
     if usize > 0 || ssize > 0 then
       r := f!"{r}.{usize}.{ssize}"
diff --git a/src/Lean/Compiler/IR/SimpCase.lean b/src/Lean/Compiler/IR/SimpCase.lean
index f8b36e0771..6c59e7a18d 100644
--- a/src/Lean/Compiler/IR/SimpCase.lean
+++ b/src/Lean/Compiler/IR/SimpCase.lean
@@ -16,7 +16,7 @@ def ensureHasDefault (alts : Array Alt) : Array Alt :=
     let alts := alts.pop;
     alts.push (Alt.default last.body)
 
-private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := do
+private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run <| do
   let aBody := (alts.get! i).body
   let mut n := 1
   for j in [i+1:alts.size] do
@@ -24,7 +24,7 @@ private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := do
       n := n+1
   return n
 
-private def maxOccs (alts : Array Alt) : Alt × Nat := do
+private def maxOccs (alts : Array Alt) : Alt × Nat := Id.run <| do
   let mut maxAlt := alts[0]
   let mut max    := getOccsOf alts 0
   for i in [1:alts.size] do
diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean
index 6d61cf1658..612399b748 100644
--- a/src/Lean/Data/Json/Basic.lean
+++ b/src/Lean/Data/Json/Basic.lean
@@ -31,7 +31,7 @@ private partial def countDigits (n : Nat) : Nat :=
 
 -- convert mantissa * 10^-exponent to 0.mantissa * 10^exponent
 protected def normalize : JsonNumber → Int × Nat × Int
-  | ⟨m, e⟩ => do
+  | ⟨m, e⟩ => Id.run <| do
     if m = 0 then (0, 0, 0)
     else
       let sign : Int := if m > 0 then 1 else -1
@@ -165,7 +165,7 @@ instance : BEq Json where
 
 -- HACK(Marc): temporary ugliness until we can use RBMap for JSON objects
 def mkObj (o : List (String × Json)) : Json :=
-  obj $ do
+  obj <| Id.run <| do
     let mut kvPairs := RBNode.leaf
     for ⟨k, v⟩ in o do
       kvPairs := kvPairs.insert compare k v
diff --git a/src/Lean/Data/Json/Printer.lean b/src/Lean/Data/Json/Printer.lean
index 0753a7538b..89f1eaada5 100644
--- a/src/Lean/Data/Json/Printer.lean
+++ b/src/Lean/Data/Json/Printer.lean
@@ -37,7 +37,7 @@ private def escapeAux (acc : String) (c : Char) : String :=
       Nat.digitChar ((n % 256) / 16),
       Nat.digitChar (n % 16) ].asString
 
-def escape (s : String) : String := do
+def escape (s : String) : String :=
   s.foldl escapeAux ""
 
 def renderString (s : String) : String :=
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 1887bf550b..a85d689e52 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -332,7 +332,7 @@ def getBracketedBinderIds : Syntax → Array Name
   | `(bracketedBinder|[$ty])                         => #[Name.anonymous]
   | _                                                => #[]
 
-private def mkTermContext (ctx : Context) (s : State) (declName? : Option Name) : Term.Context := do
+private def mkTermContext (ctx : Context) (s : State) (declName? : Option Name) : Term.Context := Id.run <| do
   let scope      := s.scopes.head!
   let mut sectionVars := {}
   for id in scope.varDecls.concatMap getBracketedBinderIds, uid in scope.varUIds do
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 6747d1e0a6..e58e6672c0 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -390,7 +390,7 @@ private def updateParams (vars : Array Expr) (indTypes : List InductiveType) : T
       pure { ctor with type := ctorType }
     pure { indType with type := type, ctors := ctors }
 
-private def collectLevelParamsInInductive (indTypes : List InductiveType) : Array Name := do
+private def collectLevelParamsInInductive (indTypes : List InductiveType) : Array Name := Id.run <| do
   let mut usedParams : CollectLevelParams.State := {}
   for indType in indTypes do
     usedParams := collectLevelParams usedParams indType.type
@@ -398,7 +398,7 @@ private def collectLevelParamsInInductive (indTypes : List InductiveType) : Arra
       usedParams := collectLevelParams usedParams ctor.type
   return usedParams.params
 
-private def mkIndFVar2Const (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name) : ExprMap Expr := do
+private def mkIndFVar2Const (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name) : ExprMap Expr := Id.run <| do
   let levelParams := levelNames.map mkLevelParam;
   let mut m : ExprMap Expr := {}
   for i in [:views.size] do
@@ -427,7 +427,7 @@ private def replaceIndFVarsWithConsts (views : Array InductiveView) (indFVars :
 
 abbrev Ctor2InferMod := Std.HashMap Name Bool
 
-private def mkCtor2InferMod (views : Array InductiveView) : Ctor2InferMod := do
+private def mkCtor2InferMod (views : Array InductiveView) : Ctor2InferMod := Id.run <| do
   let mut m := {}
   for view in views do
     for ctorView in view.ctors do
diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index 57f1752881..0e84967de2 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -149,10 +149,10 @@ def ContextInfo.toPPContext (info : ContextInfo) (lctx : LocalContext) : PPConte
 def ContextInfo.ppSyntax (info : ContextInfo) (lctx : LocalContext) (stx : Syntax) : IO Format := do
   ppTerm (info.toPPContext lctx) stx
 
-private def formatStxRange (ctx : ContextInfo) (stx : Syntax) : Format := do
+private def formatStxRange (ctx : ContextInfo) (stx : Syntax) : Format :=
   let pos    := stx.getPos?.getD 0
   let endPos := stx.getTailPos?.getD pos
-  return f!"{fmtPos pos stx.getHeadInfo}-{fmtPos endPos stx.getTailInfo}"
+  f!"{fmtPos pos stx.getHeadInfo}-{fmtPos endPos stx.getTailInfo}"
 where fmtPos pos info :=
     let pos := format <| ctx.fileMap.toPosition pos
     match info with
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 17e0bbe8d9..5ddc047415 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -320,7 +320,7 @@ Note that `g` is not a free variable at `(let g : B := ?m₂; body)`. We recover
 `f` depends on `g` because it contains `m₂`
 -/
 private def mkInitialUsedFVarsMap (mctx : MetavarContext) (sectionVars : Array Expr) (mainFVarIds : Array FVarId) (letRecsToLift : List LetRecToLift)
-    : UsedFVarsMap := do
+    : UsedFVarsMap := Id.run <| do
   let mut sectionVarSet := {}
   for var in sectionVars do
     sectionVarSet := sectionVarSet.insert var.fvarId!
@@ -418,7 +418,7 @@ abbrev FreeVarMap := FVarIdMap (Array FVarId)
 
 private def mkFreeVarMap
     (mctx : MetavarContext) (sectionVars : Array Expr) (mainFVarIds : Array FVarId)
-    (recFVarIds : Array FVarId) (letRecsToLift : List LetRecToLift) : FreeVarMap := do
+    (recFVarIds : Array FVarId) (letRecsToLift : List LetRecToLift) : FreeVarMap := Id.run <| do
   let usedFVarsMap  := mkInitialUsedFVarsMap mctx sectionVars mainFVarIds letRecsToLift
   let letRecFVarIds := letRecsToLift.map fun toLift => toLift.fvarId
   let usedFVarsMap  := FixPoint.run letRecFVarIds usedFVarsMap
diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
index 39a8402dd5..f1d150ae6e 100644
--- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
@@ -8,7 +8,7 @@ import Lean.Elab.PreDefinition.Structural.Basic
 namespace Lean.Elab.Structural
 open Meta
 
-private def getIndexMinPos (xs : Array Expr) (indices : Array Expr) : Nat := do
+private def getIndexMinPos (xs : Array Expr) (indices : Array Expr) : Nat := Id.run <| do
   let mut minPos := xs.size
   for index in indices do
     match xs.indexOf? index with
diff --git a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
index d609761d73..172c397072 100644
--- a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
+++ b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean
@@ -13,7 +13,7 @@ open Meta
   Return an array containing its "elements".
   Example: `mkTupleElems a 4` returns `#[a.1, a.2.1, a.2.2.1, a.2.2.2]`.
   -/
-private def mkTupleElems (t : Expr) (arity : Nat) : Array Expr := do
+private def mkTupleElems (t : Expr) (arity : Nat) : Array Expr := Id.run <| do
   let mut result := #[]
   let mut t := t
   for i in [:arity - 1] do
diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
index 10cc9714d6..e4e265ae80 100644
--- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
+++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
@@ -48,7 +48,7 @@ def TerminationHint.erase (t : TerminationHint) (clique : Array Name) : Terminat
   match t with
   | TerminationHint.none   => TerminationHint.none
   | TerminationHint.one .. => TerminationHint.none
-  | TerminationHint.many m => do
+  | TerminationHint.many m => Id.run <| do
     for declName in clique do
       if m.contains declName then
         let m := m.erase declName
diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index 070af7e067..ca5c0b2a30 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -14,7 +14,7 @@ private def throwUnknownId (id : Name) : CommandElabM Unit :=
 private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
   match levelParams with
   | []    => ""
-  | u::us => do
+  | u::us => Id.run <| do
     let mut m := m!".\{{u}"
     for u in us do
       m := m ++ ", " ++ toMessageData u
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index c52e7f1332..5eda012301 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -31,7 +31,7 @@ private partial def floatOutAntiquotTerms : Syntax → StateT (Syntax → TermEl
     Syntax.node i k (← args.mapM floatOutAntiquotTerms)
   | stx => pure stx
 
-private def getSepFromSplice (splice : Syntax) : Syntax := do
+private def getSepFromSplice (splice : Syntax) : Syntax :=
   if let Syntax.atom _ sep := getAntiquotSpliceSuffix splice then
     Syntax.mkStrLit (sep.dropRight 1)
   else
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 32487b1c35..eee9f1f7c3 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -471,7 +471,7 @@ where
       | none => throwError "failed to copied fields from parent structure{indentExpr parentType}" -- TODO improve error message
     return result
 
-private partial def mkToParentName (parentStructName : Name) (p : Name → Bool) : Name := do
+private partial def mkToParentName (parentStructName : Name) (p : Name → Bool) : Name := Id.run <| do
   let base := Name.mkSimple $ "to" ++ parentStructName.eraseMacroScopes.getString!
   if p base then
     base
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index ce92ae8946..030b0f5a6d 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -374,7 +374,7 @@ def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVar
   for g in newGoals do
     if mctx.isAnonymousMVar g then
       numAnonymous := numAnonymous + 1
-  modifyMCtx fun mctx => do
+  modifyMCtx fun mctx => Id.run <| do
     let mut mctx := mctx
     let mut idx  := 1
     for g in newGoals do
diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean
index caa5aa31fb..e93593ebf8 100644
--- a/src/Lean/Meta/CongrTheorems.lean
+++ b/src/Lean/Meta/CongrTheorems.lean
@@ -32,14 +32,14 @@ structure CongrTheorem where
   proof    : Expr
   argKinds : Array CongrArgKind
 
-private def addPrimeToFVarUserNames (ys : Array Expr) (lctx : LocalContext) : LocalContext := do
+private def addPrimeToFVarUserNames (ys : Array Expr) (lctx : LocalContext) : LocalContext := Id.run <| do
   let mut lctx := lctx
   for y in ys do
     let decl := lctx.getFVar! y
     lctx := lctx.setUserName decl.fvarId (decl.userName.appendAfter "'")
   return lctx
 
-private def setBinderInfosD (ys : Array Expr) (lctx : LocalContext) : LocalContext := do
+private def setBinderInfosD (ys : Array Expr) (lctx : LocalContext) : LocalContext := Id.run <| do
   let mut lctx := lctx
   for y in ys do
     let decl := lctx.getFVar! y
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index ba64ea0146..502d3addc8 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -330,7 +330,7 @@ where
   /- Return true if there are let-declarions between `xs[0]` and `xs[xs.size-1]`.
      We use it a quick-check to avoid the more expensive collection procedure. -/
   hasLetDeclsInBetween : MetaM Bool := do
-    let check (lctx : LocalContext) : Bool := do
+    let check (lctx : LocalContext) : Bool := Id.run <| do
       let start := lctx.getFVar! xs[0] |>.index
       let stop  := lctx.getFVar! xs.back |>.index
       for i in [start+1:stop] do
diff --git a/src/Lean/Meta/Injective.lean b/src/Lean/Meta/Injective.lean
index d41049a593..14b73888b4 100644
--- a/src/Lean/Meta/Injective.lean
+++ b/src/Lean/Meta/Injective.lean
@@ -13,7 +13,7 @@ import Lean.Meta.Tactic.Assumption
 
 namespace Lean.Meta
 
-private def mkAnd? (args : Array Expr) : Option Expr := do
+private def mkAnd? (args : Array Expr) : Option Expr := Id.run <| do
   if args.isEmpty then
     return none
   else
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 0f05037546..ff7f295b02 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -136,7 +136,7 @@ private def isNatValueTransition (p : Problem) : Bool :=
 private def processSkipInaccessible (p : Problem) : Problem :=
   match p.vars with
   | []      => unreachable!
-  | x :: xs => do
+  | x :: xs =>
     let alts := p.alts.map fun alt => match alt.patterns with
       | Pattern.inaccessible _ :: ps => { alt with patterns := ps }
       | _       => unreachable!
@@ -537,7 +537,7 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
         let newAlts := p.alts.filter isFirstPatternVar
         pure { p with mvarId := subgoal.mvarId, alts := newAlts, vars := x::xs }
 
-private def expandNatValuePattern (p : Problem) : Problem := do
+private def expandNatValuePattern (p : Problem) : Problem :=
   let alts := p.alts.map fun alt => match alt.patterns with
     | Pattern.val (Expr.lit (Literal.natVal 0) _) :: ps     => { alt with patterns := Pattern.ctor `Nat.zero [] [] [] :: ps }
     | Pattern.val (Expr.lit (Literal.natVal (n+1)) _) :: ps => { alt with patterns := Pattern.ctor `Nat.succ [] [] [Pattern.val (mkRawNatLit n)] :: ps }
@@ -588,12 +588,12 @@ private def List.moveToFront [Inhabited α] (as : List α) (i : Nat) : List α :
   b :: bs
 
 /-- Move variable `#i` to the beginning of the to-do list `p.vars`. -/
-private def moveToFront (p : Problem) (i : Nat) : Problem := do
+private def moveToFront (p : Problem) (i : Nat) : Problem :=
   if i == 0 then
     p
   else if h : i < p.vars.length then
     let x := p.vars.get i h
-    return { p with
+    { p with
       vars := List.moveToFront p.vars i
       alts := p.alts.map fun alt => { alt with patterns := List.moveToFront alt.patterns i }
     }
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index 10224d6eb8..f12a081447 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -211,7 +211,7 @@ private partial def mkSplitterProof (matchDeclName : Name) (template : Expr) (al
     proveSubgoal mvarId
   instantiateMVars proof
 where
-  mkMap : FVarIdMap Expr := do
+  mkMap : FVarIdMap Expr := Id.run <| do
     let mut m := {}
     for alt in alts, altNew in altsNew do
       m := m.insert alt.fvarId! altNew
diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean
index 34de76d95f..f0fd2885f9 100644
--- a/src/Lean/Meta/PPGoal.lean
+++ b/src/Lean/Meta/PPGoal.lean
@@ -131,7 +131,7 @@ def collect (goalTarget : Expr) : MetaM (FVarIdSet × FVarIdSet) := do
     return ({}, {})
   else
     let lctx ← getLCtx
-    let hiddenInaccessible := lctx.foldl (init := {}) fun hiddenInaccessible localDecl => do
+    let hiddenInaccessible := lctx.foldl (init := {}) fun hiddenInaccessible localDecl => Id.run <| do
       if localDecl.userName.isInaccessibleUserName then
         hiddenInaccessible.insert localDecl.fvarId
       else
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 46ccdeb75a..d8541cacb4 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -390,7 +390,7 @@ def wakeUp (answer : Answer) : Waiter → SynthM Unit
     modify fun s => { s with resumeStack := s.resumeStack.push (cNode, answer) }
 
 def isNewAnswer (oldAnswers : Array Answer) (answer : Answer) : Bool :=
-  oldAnswers.all fun oldAnswer => do
+  oldAnswers.all fun oldAnswer =>
     -- Remark: isDefEq here is too expensive. TODO: if `==` is too imprecise, add some light normalization to `resultType` at `addAnswer`
     -- iseq ← isDefEq oldAnswer.resultType answer.resultType; pure (!iseq)
     oldAnswer.resultType != answer.resultType
diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean
index d1b6f7ccc0..42a42567ba 100644
--- a/src/Lean/Meta/Tactic/Induction.lean
+++ b/src/Lean/Meta/Tactic/Induction.lean
@@ -161,7 +161,7 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi
       let (indices', mvarId) ← introNP mvarId indices.size
       let (majorFVarId', mvarId) ← intro1P mvarId
       -- Create FVarSubst with indices
-      let baseSubst := do
+      let baseSubst := Id.run <| do
         let mut subst : FVarSubst := {}
         let mut i := 0
         for index in indices do
diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index f76f5b7e81..1910a4458a 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -121,7 +121,7 @@ partial def findSplit? (env : Environment) (e : Expr) : Option Expr :=
   else
     none
 where
-  isCandidate (e : Expr) : Bool := do
+  isCandidate (e : Expr) : Bool := Id.run <| do
     if e.isIte || e.isDIte then
       !(e.getArg! 1 5).hasLooseBVars
     else if let some info := isMatcherAppCore? env e then
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 3860b2970a..132b0b0c28 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -715,7 +715,7 @@ instance : MonadHashMapCacheAdapter ExprStructEq Expr M where
   modifyCache := fun f => modify fun s => { s with cache := f s.cache }
 
 /-- Return the local declaration of the free variable `x` in `xs` with the smallest index -/
-private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) : LocalDecl := do
+private def getLocalDeclWithSmallestIdx (lctx : LocalContext) (xs : Array Expr) : LocalDecl := Id.run <| do
   let mut d : LocalDecl := lctx.getFVar! xs[0]
   for i in [1:xs.size] do
     let curr := lctx.getFVar! xs[i]
diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
index 9ded9391ed..85c2706bfc 100644
--- a/src/Lean/MonadEnv.lean
+++ b/src/Lean/MonadEnv.lean
@@ -21,8 +21,8 @@ def isInductive [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
 
 def isRecCore (env : Environment) (declName : Name) : Bool :=
   match env.find? declName with
-  | some (ConstantInfo.recInfo ..) => return true
-  | _ => return false
+  | some (ConstantInfo.recInfo ..) => true
+  | _ => false
 
 def isRec [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
   return isRecCore (← getEnv) declName
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 7e6bba75b2..20b094acf8 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -598,7 +598,7 @@ def notFollowedByFn (p : ParserFn) (msg : String) : ParserFn := fun c s =>
   fn := notFollowedByFn p.fn msg
 }
 
-partial def manyAux (p : ParserFn) : ParserFn := fun c s => do
+partial def manyAux (p : ParserFn) : ParserFn := fun c s => Id.run <| do
   let iniSz  := s.stackSize
   let iniPos := s.pos
   let mut s  := p c s
@@ -631,7 +631,7 @@ partial def manyAux (p : ParserFn) : ParserFn := fun c s => do
 }
 
 private partial def sepByFnAux (p : ParserFn) (sep : ParserFn) (allowTrailingSep : Bool) (iniSz : Nat) (pOpt : Bool) : ParserFn :=
-  let rec parse (pOpt : Bool) (c s) := do
+  let rec parse (pOpt : Bool) (c s) := Id.run <| do
     let sz  := s.stackSize
     let pos := s.pos
     let mut s := p c s
@@ -1011,7 +1011,7 @@ def mkIdResult (startPos : Nat) (tk : Option Token) (val : Name) : ParserFn := f
     s.pushSyntax atom
 
 partial def identFnAux (startPos : Nat) (tk : Option Token) (r : Name) : ParserFn :=
-  let rec parse (r : Name) (c s) := do
+  let rec parse (r : Name) (c s) := Id.run <| do
     let input := c.input
     let i     := s.pos
     if input.atEnd i then
@@ -1392,7 +1392,7 @@ def invalidLongestMatchParser (s : ParserState) : ParserState :=
 
  Remark: `p` must produce exactly one syntax node.
  Remark: the `left?` is not none when we are processing trailing parsers. -/
-def runLongestMatchParser (left? : Option Syntax) (startLhsPrec : Nat) (p : ParserFn) : ParserFn := fun c s => do
+def runLongestMatchParser (left? : Option Syntax) (startLhsPrec : Nat) (p : ParserFn) : ParserFn := fun c s => Id.run <| do
   /-
     We assume any registered parser `p` has one of two forms:
     * a direct call to `leadingParser` or `trailingParser`
@@ -1694,7 +1694,7 @@ def pushNone : Parser :=
 def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbolNoAntiquot "(" >> decQuotDepth termParser >> symbolNoAntiquot ")")
 def antiquotExpr : Parser       := identNoAntiquot <|> antiquotNestedExpr
 
-@[inline] def tokenWithAntiquotFn (p : ParserFn) : ParserFn := fun c s => do
+@[inline] def tokenWithAntiquotFn (p : ParserFn) : ParserFn := fun c s => Id.run <| do
   let s := p c s
   if s.hasError || c.quotDepth == 0 then
     return s
@@ -1739,7 +1739,7 @@ def mkAntiquot (name : String) (kind : Option SyntaxNodeKind) (anonymous := true
     checkNoWsBefore "no space before spliced term" >> antiquotExpr >>
     nameP
 
-def tryAnti (c : ParserContext) (s : ParserState) : Bool := do
+def tryAnti (c : ParserContext) (s : ParserState) : Bool := Id.run <| do
   if c.quotDepth == 0 then
     return false
   let (s, stx) := peekToken c s
@@ -1768,7 +1768,7 @@ def mkAntiquotSplice (kind : SyntaxNodeKind) (p suffix : Parser) : Parser :=
     checkNoWsBefore "no space before spliced term" >> symbol "[" >> node nullKind p >> symbol "]" >>
     suffix
 
-@[inline] def withAntiquotSuffixSpliceFn (kind : SyntaxNodeKind) (p suffix : ParserFn) : ParserFn := fun c s => do
+@[inline] def withAntiquotSuffixSpliceFn (kind : SyntaxNodeKind) (p suffix : ParserFn) : ParserFn := fun c s => Id.run <| do
   let s := p c s
   if s.hasError || c.quotDepth == 0 || !s.stxStack.back.isAntiquot then
     return s
@@ -1869,7 +1869,7 @@ private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=
   if s.stackSize == iniSz + 1 then s
   else s.mkNode nullKind iniSz -- throw error instead?
 
-def leadingParserAux (kind : Name) (tables : PrattParsingTables) (behavior : LeadingIdentBehavior) : ParserFn := fun c s => do
+def leadingParserAux (kind : Name) (tables : PrattParsingTables) (behavior : LeadingIdentBehavior) : ParserFn := fun c s => Id.run <| do
   let iniSz   := s.stackSize
   let (s, ps) := indexed tables.leadingTable c s behavior
   if s.hasError then
@@ -1886,7 +1886,7 @@ def leadingParserAux (kind : Name) (tables : PrattParsingTables) (behavior : Lea
 def trailingLoopStep (tables : PrattParsingTables) (left : Syntax) (ps : List (Parser × Nat)) : ParserFn := fun c s =>
   longestMatchFn left (ps ++ tables.trailingParsers) c s
 
-partial def trailingLoop (tables : PrattParsingTables) (c : ParserContext) (s : ParserState) : ParserState := do
+partial def trailingLoop (tables : PrattParsingTables) (c : ParserContext) (s : ParserState) : ParserState := Id.run <| do
   let iniSz  := s.stackSize
   let iniPos := s.pos
   let (s, ps)       := indexed tables.trailingTable c s LeadingIdentBehavior.default
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 031751a827..c660225c17 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -385,7 +385,7 @@ def isValidSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Bool :=
   let kinds := (parserExtension.getState env).kinds
   kinds.contains k
 
-def getSyntaxNodeKinds (env : Environment) : List SyntaxNodeKind := do
+def getSyntaxNodeKinds (env : Environment) : List SyntaxNodeKind :=
   let kinds := (parserExtension.getState env).kinds
   kinds.foldl (fun ks k _ => k::ks) []
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index ab1396e0ea..65dc32a1f7 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -153,7 +153,7 @@ def isFOLike (motive : Expr) : MetaM Bool := do
   let f := motive.getAppFn
   f.isFVar || f.isConst
 
-def isIdLike (arg : Expr) : Bool := do
+def isIdLike (arg : Expr) : Bool :=
   -- TODO: allow `id` constant as well?
   match arg with
   | Expr.lam _ _ (Expr.bvar ..) .. => true
@@ -190,7 +190,7 @@ private def valUnknown (e : Expr) : MetaM Bool := do
 private def typeUnknown (e : Expr) : MetaM Bool := do
   valUnknown (← inferType e)
 
-def isHBinOp (e : Expr) : Bool := do
+def isHBinOp (e : Expr) : Bool := Id.run <| do
   -- TODO: instead of tracking these explicitly,
   -- consider a more general solution that checks for defaultInstances
   if e.getAppNumArgs != 6 then return false
diff --git a/src/Lean/ScopedEnvExtension.lean b/src/Lean/ScopedEnvExtension.lean
index e8387c5f5c..1316c56097 100644
--- a/src/Lean/ScopedEnvExtension.lean
+++ b/src/Lean/ScopedEnvExtension.lean
@@ -168,7 +168,7 @@ def ScopedEnvExtension.activateScoped (ext : ScopedEnvExtension α β σ) (env :
         match s.scopedEntries.map.find? namespaceName with
         | none =>
           { top with activeScopes := activeScopes }
-        | some bs => do
+        | some bs => Id.run <| do
           let mut state := top.state
           for b in bs do
             state := ext.descr.addEntry state b
diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index fd33db2bb3..d20c1f8508 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -311,11 +311,11 @@ where
       let ⟨line, _⟩ := fileMap.toPosition pos
       if line != hoverLine then best?
       else match best? with
-        | none => return (ctx, info)
+        | none => (ctx, info)
         | some (_, best) =>
           let dBest := best.occursBefore? hoverPos |>.get!
           if d < dBest || (d == dBest && info.isSmaller best) then
-            return (ctx, info)
+            (ctx, info)
           else
             best?
     else
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index bd665e30c9..9422a37974 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -168,11 +168,11 @@ partial def handleReferences (p : ReferenceParams)
       | Info.ofFieldInfo fi => some (RefIdent.const fi.projName, false)
       | _ => none
 
-    findReferences (doc : EditableDocument) (snaps : List Snapshot) : Array Reference := do
+    findReferences (doc : EditableDocument) (snaps : List Snapshot) : Array Reference := Id.run <| do
       let text := doc.meta.text
       let mut refs := #[]
       for snap in snaps do
-        refs := refs.appendList <| snap.infoTree.deepestNodes fun _ info _ => do
+        refs := refs.appendList <| snap.infoTree.deepestNodes fun _ info _ => Id.run <| do
           if let some (ident, isDeclaration) := identOf info then
             if let some range := info.range? then
               return some { ident, range := range.toLspRange text, isDeclaration }
@@ -279,7 +279,7 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams)
   let text := doc.meta.text
   let pos := text.lspPosToUtf8Pos p.position
   let rec highlightReturn? (doRange? : Option Range) : Syntax → Option DocumentHighlight
-    | stx@`(doElem|return%$i $e) => do
+    | stx@`(doElem|return%$i $e) => Id.run <| do
       if let some range := i.getRange? then
         if range.contains pos then
           return some { range := doRange?.getD (range.toLspRange text), kind? := DocumentHighlightKind.text }
@@ -319,7 +319,7 @@ partial def handleDocumentSymbol (p : DocumentSymbolParams)
       | `(namespace $id)  => sectionLikeToDocumentSymbols text stx stxs (id.getId.toString) SymbolKind.namespace id
       | `(section $(id)?) => sectionLikeToDocumentSymbols text stx stxs ((·.getId.toString) <$> id |>.getD "<section>") SymbolKind.namespace (id.getD stx)
       | `(end $(id)?) => ([], stx::stxs)
-      | _ => do
+      | _ => Id.run <| do
         let (syms, stxs') := toDocumentSymbols text stxs
         unless stx.isOfKind ``Lean.Parser.Command.declaration do
           return (syms, stxs')
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 59d89fbc60..a8d1865a06 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -119,8 +119,8 @@ def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextI
   infos.toArray.getMax? (fun a b => a.1 > b.1) |>.map fun (_, ci, i) => (ci, i)
 
 /-- Find an info node, if any, which should be shown on hover/cursor at position `hoverPos`. -/
-partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) : Option (ContextInfo × Info) := do
-  let res := t.smallestInfo? fun i => do
+partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) : Option (ContextInfo × Info) := Id.run <| do
+  let res := t.smallestInfo? fun i => Id.run <| do
     if i matches Info.ofFieldInfo _ || i.toElabInfo?.isSome then
       return i.contains hoverPos
     return false
@@ -205,7 +205,7 @@ structure GoalsAtResult where
   there is no nested tactic info (i.e. it is a leaf tactic; tactic combinators should decide for themselves
   where to show intermediate/final states)
 -/
-partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List GoalsAtResult := do
+partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List GoalsAtResult := Id.run <| do
   t.deepestNodes fun
     | ctx, i@(Info.ofTacticInfo ti), cs => OptionM.run do
       if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
@@ -220,7 +220,7 @@ partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String
     | _, _, _ => none
 where
   hasNestedTactic (pos tailPos) : InfoTree → Bool
-    | InfoTree.node i@(Info.ofTacticInfo _) cs => do
+    | InfoTree.node i@(Info.ofTacticInfo _) cs => Id.run <| do
       if let `(by $t) := i.stx then
         return false  -- ignore term-nested proofs such as in `simp [show p by ...]`
       if let (some pos', some tailPos') := (i.pos?, i.tailPos?) then
@@ -245,12 +245,12 @@ these head function symbols such as `f`,
 and later ignore identifiers at these positions.
 -/
 partial def InfoTree.termGoalAt? (t : InfoTree) (hoverPos : String.Pos) : Option (ContextInfo × Info) :=
-  let headFns : Std.HashSet String.Pos := t.foldInfo (init := {}) fun ctx i headFns => do
+  let headFns : Std.HashSet String.Pos := t.foldInfo (init := {}) fun ctx i headFns =>
     if let some pos := getHeadFnPos? i.stx then
       headFns.insert pos
     else
       headFns
-  t.smallestInfo? fun i => do
+  t.smallestInfo? fun i => Id.run <| do
     if i.contains hoverPos then
       if let Info.ofTermInfo ti := i then
         return !ti.stx.isIdent || !headFns.contains i.pos?.get!
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index e1f6c3faea..df78008e75 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -274,7 +274,7 @@ where
     -- guaranteed.
     | _                                => s!" {val} "
 
-def hasMissing (stx : Syntax) : Bool := do
+def hasMissing (stx : Syntax) : Bool := Id.run <| do
   for stx in stx.topDown do
     if stx.isMissing then
       return true
diff --git a/src/Lean/Widget/InteractiveGoal.lean b/src/Lean/Widget/InteractiveGoal.lean
index 8f179e1dc9..f5064d6f86 100644
--- a/src/Lean/Widget/InteractiveGoal.lean
+++ b/src/Lean/Widget/InteractiveGoal.lean
@@ -31,7 +31,7 @@ namespace InteractiveGoal
 private def addLine (fmt : Format) : Format :=
   if fmt.isNil then fmt else fmt ++ Format.line
 
-def pretty (g : InteractiveGoal) : Format := do
+def pretty (g : InteractiveGoal) : Format := Id.run <| do
   let indent := 2 -- Use option
   let mut ret := match g.userName? with
     | some userName => f!"case {userName}"
diff --git a/src/Std/Data/BinomialHeap.lean b/src/Std/Data/BinomialHeap.lean
index 8c63fa6759..9961fe5c0d 100644
--- a/src/Std/Data/BinomialHeap.lean
+++ b/src/Std/Data/BinomialHeap.lean
@@ -124,7 +124,7 @@ partial def toArrayUnordered (h : Heap α) : Array α :=
   go #[] h
   where
     go (acc : Array α) : Heap α → Array α
-      | heap ns => do
+      | heap ns => Id.run <| do
         let mut acc := acc
         for n in ns do
           acc := acc.push n.val