diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 9379c2a448..f755ccc713 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -74,7 +74,8 @@ instance : MonadResolveName CoreM where
   getOpenDecls := return (← read).openDecls
 
 @[inline] def liftIOCore (x : IO α) : CoreM α := do
-  IO.toEIO (fun (err : IO.Error) => Exception.error (← getRef) (toString err)) x
+  let ref ← getRef
+  IO.toEIO (fun (err : IO.Error) => Exception.error ref (toString err)) x
 
 instance : MonadLift IO CoreM where
   monadLift := liftIOCore
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 07173b00b4..a8c438b9dd 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -131,7 +131,8 @@ private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : M
 @[inline] def liftEIO {α} (x : EIO Exception α) : CommandElabM α := liftM x
 
 @[inline] def liftIO {α} (x : IO α) : CommandElabM α := do
-  IO.toEIO (fun (ex : IO.Error) => Exception.error (← read).ref ex.toString) x
+  let ctx ← read
+  IO.toEIO (fun (ex : IO.Error) => Exception.error ctx.ref ex.toString) x
 
 instance : MonadLiftT IO CommandElabM where
   monadLift := liftIO
diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index 1fa0cfaa12..1abdeb5218 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -255,10 +255,12 @@ def mkInfoNode (info : Info) : m Unit := do
     Prod.fst <$> MonadFinally.tryFinally' x fun a? => do
       match a? with
       | none   => modifyInfoTrees fun _ => treesSaved
-      | some a => modifyInfoTrees fun trees =>
-        match (← mkInfo a) with
-        | Sum.inl info  => treesSaved.push <| InfoTree.node info trees
-        | Sum.inr mvaId => treesSaved.push <| InfoTree.hole mvaId
+      | some a =>
+        let info ← mkInfo a
+        modifyInfoTrees fun trees =>
+          match info with
+          | Sum.inl info  => treesSaved.push <| InfoTree.node info trees
+          | Sum.inr mvaId => treesSaved.push <| InfoTree.hole mvaId
   else
     x
 
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index e69fdbf9b2..9dcd2dea0e 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -114,7 +114,8 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
                 | none                 => Array.empty)
             | _ =>
               let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id $arr)) ids.back
-              `(Array.map (fun $(← mkTuple ids) => $(inner[0])) $arr)
+              let tuple ← mkTuple ids
+              `(Array.map (fun $tuple => $(inner[0])) $arr)
           let arr ←
             if k == `sepBy then
               `(mkSepArray $arr (mkAtom $(getSepFromSplice arg)))
diff --git a/src/Lean/Elab/SetOption.lean b/src/Lean/Elab/SetOption.lean
index 60c0880b2d..4bcfab4cfb 100644
--- a/src/Lean/Elab/SetOption.lean
+++ b/src/Lean/Elab/SetOption.lean
@@ -26,8 +26,9 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
     throwError "unexpected set_option value {val}"
 where
   setOption (optionName : Name) (val : DataValue) : m Options := do
-    let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error (← getRef) ex.toString) (getOptionDecl optionName)
+    let ref ← getRef
+    let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error ref ex.toString) (getOptionDecl optionName)
     unless decl.defValue.sameCtor val do throwError "type mismatch at set_option"
     return (← getOptions).insert optionName val
 
-end Lean.Elab
\ No newline at end of file
+end Lean.Elab
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 230895a5bc..ef60a800c9 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -113,8 +113,9 @@ where
       let candidates ← resolveGlobalConstWithInfos (← getRef) parserName
       /- 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 =>
-         match (← getEnv).find? c with
+         match env.find? c with
          | none      => none
          | some info =>
            match info.type with
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index ae128f47ba..960485c90d 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -128,7 +128,8 @@ partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array E
           addNewArg arg
         | _ =>
           let arg ← mkFreshExprSyntheticOpaqueMVar (← getArgExpectedType) (tag := appendTag tag binderName)
-          modify fun s => { s with alts := s.alts.push (← getBindingName, arg.mvarId!) }
+          let x   ← getBindingName
+          modify fun s => { s with alts := s.alts.push (x, arg.mvarId!) }
           addNewArg arg
       loop
     | _ =>
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 1b6f3193f7..8321f112ad 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1392,7 +1392,8 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List Stri
         throwError "invalid use of explicit universe parameters, '{e}' is a local"
       return [(e, projs)]
     -- check for section variable capture by a quotation
-    if let some (e, projs) := preresolved.findSome? fun (n, projs) => (← read).sectionFVars.find? n |>.map (·, projs) then
+    let ctx ← read
+    if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then
       return [(e, projs)]  -- section variables should shadow global decls
     if preresolved.isEmpty then
       process (← resolveGlobalName n)
diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean
index bfb68753c9..17d734a08a 100644
--- a/src/Lean/Meta/LevelDefEq.lean
+++ b/src/Lean/Meta/LevelDefEq.lean
@@ -82,7 +82,9 @@ private def solveSelfMax (mvarId : MVarId) (v : Level) : MetaM Unit := do
   assignLevelMVar mvarId <| mkMaxArgsDiff mvarId v n
 
 private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit := do
-  modifyPostponed fun postponed => postponed.push { lhs := lhs, rhs := rhs, ref := (← getRef), ctx? := (← read).defEqCtx? }
+  let ref ← getRef
+  let ctx ← read
+  modifyPostponed fun postponed => postponed.push { lhs := lhs, rhs := rhs, ref := ref, ctx? := ctx.defEqCtx? }
 
 mutual
 
diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean
index 93bf664cbb..1780df4624 100644
--- a/src/Lean/Meta/SizeOf.lean
+++ b/src/Lean/Meta/SizeOf.lean
@@ -79,7 +79,7 @@ private partial def mkSizeOfMinors {α} (motiveFVars : Array Expr) (minorFVars :
 where
   loop (i : Nat) (minors : Array Expr) : MetaM α := do
     if i < minorFVars.size then
-      forallTelescopeReducing (← inferType minorFVars[i]) fun xs _ =>
+      forallTelescopeReducing (← inferType minorFVars[i]) fun xs _ => do
       forallBoundedTelescope (← inferType minorFVars'[i]) xs.size fun xs' _ => do
         let mut minor ← mkNumeral (mkConst ``Nat) 1
         for x in xs, x' in xs' do