diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 464bc3f9e5..827535fff0 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -742,43 +742,6 @@ def isMonadApp (type : Expr) : TermElabM Bool := do
   let some (m, _) ← isTypeApp? type | pure false
   return (← isMonad? m) |>.isSome
 
-/--
-  Try to coerce `a : α` into `m β` by first coercing `a : α` into ‵β`, and then using `pure`.
-  The method is only applied if `α` is not monadic (e.g., `Nat → IO Unit`), and the head symbol
-  of the resulting type is not a metavariable (e.g., `?m Unit` or `Bool → ?m Nat`).
-
-  The main limitation of the approach above is polymorphic code. As usual, coercions and polymorphism
-  do not interact well. In the example above, the lift is successfully applied to `true`, `false` and `!y`
-  since none of them is polymorphic
-  ```
-  def f (x : Bool) : IO Bool := do
-  let y ← if x == 0 then IO.println "hello"; true else false;
-  !y
-  ```
-  On the other hand, the following fails since `+` is polymorphic
-  ```
-  def f (x : Bool) : IO Nat := do
-  IO.prinln x
-  x + x  -- Error: failed to synthesize `Add (IO Nat)`
-  ```
--/
-private def tryPureCoe? (errorMsgHeader? : Option String) (m β α a : Expr) : TermElabM (Option Expr) :=
-  commitWhenSome? do
-    let doIt : TermElabM (Option Expr) := do
-      try
-        let aNew ← tryCoe errorMsgHeader? β α a none
-        let aNew ← mkPure m aNew
-        pure (some aNew)
-      catch _ =>
-        pure none
-    forallTelescope α fun _ α => do
-      if (← isMonadApp α) then
-        pure none
-      else if !α.getAppFn.isMVar  then
-        doIt
-      else
-        pure none
-
 /-
 Try coercions and monad lifts to make sure `e` has type `expectedType`.
 
@@ -787,13 +750,6 @@ Otherwise, we just use the basic `tryCoe`.
 
 Extensions for monads.
 
-Given an expected type of the form `n β`, if `eType` is of the form `α`, but not `m α`
-
-1 - Try to coerce ‵α` into ‵β`, and use `pure` to lift it to `n α`.
-    It only works if `n` implements `Pure`
-
-If `eType` is of the form `m α`. We use the following approaches.
-
 1- Try to unify `n` and `m`. If it succeeds, then we use
    ```
    coeM {m : Type u → Type v} {α β : Type u} [∀ a, CoeT α a β] [Monad m] (x : m α) : m β
@@ -853,14 +809,7 @@ private def tryLiftAndCoe (errorMsgHeader? : Option String) (expectedType : Expr
   let tryCoeSimple : TermElabM Expr :=
     tryCoe errorMsgHeader? expectedType eType e f?
   let some (n, β) ← isTypeApp? expectedType | tryCoeSimple
-  let tryPureCoeAndSimple : TermElabM Expr := do
-    if autoLift.get (← getOptions) then
-      match (← tryPureCoe? errorMsgHeader? n β eType e) with
-      | some eNew => pure eNew
-      | none      => tryCoeSimple
-    else
-      tryCoeSimple
-  let some (m, α) ← isTypeApp? eType | tryPureCoeAndSimple
+  let some (m, α) ← isTypeApp? eType | tryCoeSimple
   if (← isDefEq m n) then
     let some monadInst ← isMonad? n | tryCoeSimple
     try expandCoe (← mkAppOptM ``Lean.Internal.coeM #[m, α, β, none, monadInst, e]) catch _ => throwMismatch
@@ -887,13 +836,8 @@ private def tryLiftAndCoe (errorMsgHeader? : Option String) (expectedType : Expr
         unless (← isDefEq expectedType eNewType) do throwMismatch
         return eNew -- approach 3 worked
     catch _ =>
-      /-
-        If `m` is not a monad, then we try to use `tryPureCoe?` and then `tryCoe?`.
-        Otherwise, we just try `tryCoe?`.
-      -/
-      match (← isMonad? m) with
-      | none   => tryPureCoeAndSimple
-      | some _ => tryCoeSimple
+      /- If `m` is not a monad, then we try to use `tryCoe?`. -/
+      tryCoeSimple
   else
     tryCoeSimple
 
diff --git a/tests/bench/liasolver.lean b/tests/bench/liasolver.lean
index 5183d2f9e7..15da39814c 100644
--- a/tests/bench/liasolver.lean
+++ b/tests/bench/liasolver.lean
@@ -72,7 +72,7 @@ namespace Std.HashMap
     return false
 
   def mapValsM [Monad m] (f : β → m γ) (xs : HashMap α β) : m (HashMap α γ) :=
-    mkHashMap (capacity := xs.size) |> xs.foldM fun acc k v => do acc.insert k (←f v)
+    mkHashMap (capacity := xs.size) |> xs.foldM fun acc k v => return acc.insert k (←f v)
 
   def mapVals (f : β → γ) (xs : HashMap α β) : HashMap α γ :=
     mkHashMap (capacity := xs.size) |> xs.fold fun acc k v => acc.insert k (f v)
@@ -341,17 +341,17 @@ def error (msg : String) : IO α :=
   throw <| IO.userError s!"Error: {msg}."
 
 def Array.ithVal (xs : Array String) (i : Nat) (name : String) : IO Int := do
-  let some unparsed ← xs.get? i
+  let some unparsed := xs.get? i
     | error s!"Missing {name}"
-  let some parsed ← String.toInt? unparsed
+  let some parsed := String.toInt? unparsed
     | error s!"Invalid {name}: `{unparsed}`"
   return parsed
 
 def main (args : List String) : IO UInt32 := do
-  let some path ← args.head?
+  let some path := args.head?
     | error "Usage: liasolver <input file>"
   let lines ← IO.FS.lines path <&> Array.filter (¬·.isEmpty)
-  let some headerLine ← lines.get? 0
+  let some headerLine := lines.get? 0
     | error "No header line"
   let header := headerLine.splitOn.toArray
   let nEquations ← header.ithVal 0 "amount of equations"
diff --git a/tests/lean/448.lean b/tests/lean/448.lean
index aefaf7c764..404a08d322 100644
--- a/tests/lean/448.lean
+++ b/tests/lean/448.lean
@@ -6,7 +6,7 @@ structure M (α : Type) where
 instance : Monad M where
   pure x   := { σ := pure x }
   bind x f := { σ := do (f (← x.σ)).σ }
-  map f x  := { σ := do f (← x.σ) }
+  map f x  := { σ := return f (← x.σ) }
 
 instance : MonadLiftT IO M where
   monadLift {α : Type} (act : IO α) : M α :=
diff --git a/tests/lean/474.lean b/tests/lean/474.lean
index 7ca5b35f92..c409238f4d 100644
--- a/tests/lean/474.lean
+++ b/tests/lean/474.lean
@@ -5,7 +5,7 @@ open Lean Meta
   let e ← withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do
     let m ← mkFreshExprMVar (mkConst ``Nat)
     assignExprMVar m.mvarId! y
-    let e ← mkApp2 (mkConst ``Nat.add) m y
+    let e := mkApp2 (mkConst ``Nat.add) m y
     -- goal: construct λ y, e
     dbg_trace (← ppExpr (← mkLambdaFVars #[y] e)) -- doesn't work: creates let
     dbg_trace (← ppExpr (← instantiateMVars <| -- doesn't work: contains free variable
@@ -18,7 +18,7 @@ open Lean Meta
   withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do
     let m ← mkFreshExprMVar (mkConst ``Nat)
     assignExprMVar m.mvarId! y
-    let e ← mkApp2 (mkConst ``Nat.add) m y
+    let e := mkApp2 (mkConst ``Nat.add) m y
     -- goal: construct λ y, e
      dbg_trace (← instantiateMVars <| -- doesn't work: contains free variable
       mkLambda `y BinderInfo.default (mkConst ``Nat) (← abstract e #[y]))
@@ -26,7 +26,7 @@ open Lean Meta
 #eval show MetaM Unit from do
   let (e, m) ← withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do
     let m ← mkFreshExprMVar (mkConst ``Nat) (kind := MetavarKind.syntheticOpaque)
-    let e ← mkApp2 (mkConst ``Nat.add) m y
+    let e := mkApp2 (mkConst ``Nat.add) m y
     dbg_trace (← ppExpr e)
     dbg_trace (← ppExpr (← abstract e #[y]))
     let e ← instantiateMVars <| -- doesn't work: contains free variable
diff --git a/tests/lean/679.lean b/tests/lean/679.lean
index d043ecbdbc..80fe376610 100644
--- a/tests/lean/679.lean
+++ b/tests/lean/679.lean
@@ -2,7 +2,7 @@ import Lean
 open Lean
 
 def encodeDecode [ToJson α] [FromJson α] (x : α) : Except String α := do
-  let json ← toJson x
+  let json := toJson x
   fromJson? json
 
 #eval encodeDecode Name.anonymous
diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean
index 0af82cda0d..03f0d9ccf9 100644
--- a/tests/lean/StxQuot.lean
+++ b/tests/lean/StxQuot.lean
@@ -69,26 +69,26 @@ def f' (stx : Syntax) : Unhygienic Syntax := match stx with
 open Parser.Term
 #eval run do
   match ← `(structInstField|a := b) with
-  | `(Parser.Term.structInstField| $lhs:ident := $rhs) => #[lhs, rhs]
+  | `(Parser.Term.structInstField| $lhs:ident := $rhs) => pure #[lhs, rhs]
   | _ => unreachable!
 
 #eval run do
   match ← `({ a := a : a }) with
-  | `({ $f:ident := $e : 0 })      => "0"
-  | `({ $f:ident := $e $[: $a?]?}) => "1"
-  | stx                    => "2"
+  | `({ $f:ident := $e : 0 })      => pure "0"
+  | `({ $f:ident := $e $[: $a?]?}) => pure "1"
+  | stx                    => pure "2"
 
 #eval run `(sufficesDecl|x from x)
 
 #eval run do
   match ← `([1, 2, 3, 4]) with
-    | `([$x, $ys,*, $z]) => #[x, mkNullNode ys, z]
+    | `([$x, $ys,*, $z]) => pure #[x, mkNullNode ys, z]
     | _ => unreachable!
 
 #eval run do
   match ← `([1, 2]) with
-    | `([$x, $y, $zs,*]) => zs.getElems
-    | `([$x, $ys,*])     => ys.getElems
+    | `([$x, $y, $zs,*]) => pure zs.getElems
+    | `([$x, $ys,*])     => pure ys.getElems
     | _ => unreachable!
 
 #check (match · with | `([1, $ys,*, 2, $zs,*, 3]) => _)
@@ -110,6 +110,6 @@ syntax "foo" term : term
 
 #eval run do
   match mkIdent `b with
-  | `(a) => "0"
-  | `(b) => "1"
-  | _    => "2"
+  | `(a) => pure "0"
+  | `(b) => pure "1"
+  | _    => pure "2"
diff --git a/tests/lean/doIssue.lean b/tests/lean/doIssue.lean
index ba487ccb8b..3c84a0d74e 100644
--- a/tests/lean/doIssue.lean
+++ b/tests/lean/doIssue.lean
@@ -3,7 +3,7 @@ def f (x : Nat) : IO Unit := do
   IO.println x
 
 def f' (x : Nat) : IO Unit := do
-  discard x
+  discard (pure x)
   IO.println x
 
 def g (xs : Array Nat) : IO Unit := do
@@ -11,7 +11,7 @@ def g (xs : Array Nat) : IO Unit := do
   IO.println xs
 
 def g' (xs : Array Nat) : IO Unit := do
-  discard <| xs.set! 0 1 -- Error
+  discard <| pure (xs.set! 0 1)
   IO.println xs
 
 def h (xs : Array Nat) : IO Unit := do
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index 1217ec022a..f20073889f 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -42,7 +42,7 @@ example : True := by
 
 
 /-- My notation -/
-macro "mynota" e:term : term => e
+macro "mynota" e:term : term => pure e
 
 #check mynota 1
      --^ textDocument/hover
diff --git a/tests/lean/interactive/plainTermGoal.lean b/tests/lean/interactive/plainTermGoal.lean
index 109a3540e0..0520208125 100644
--- a/tests/lean/interactive/plainTermGoal.lean
+++ b/tests/lean/interactive/plainTermGoal.lean
@@ -9,7 +9,7 @@ example : 0 < 2 :=
 
 example : OptionM Unit := do
   let y : Int ← none
-  let x ← Nat.zero
+  let x := Nat.zero
         --^ $/lean/plainTermGoal
   return ()
 
diff --git a/tests/lean/interactive/plainTermGoal.lean.expected.out b/tests/lean/interactive/plainTermGoal.lean.expected.out
index d761e97d4b..f3c1f64bb7 100644
--- a/tests/lean/interactive/plainTermGoal.lean.expected.out
+++ b/tests/lean/interactive/plainTermGoal.lean.expected.out
@@ -26,8 +26,8 @@
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 11, "character": 10}}
 {"range":
- {"start": {"line": 11, "character": 10}, "end": {"line": 11, "character": 18}},
- "goal": "y : Int\n⊢ OptionM Nat"}
+ {"start": {"line": 9, "character": 26}, "end": {"line": 13, "character": 11}},
+ "goal": "⊢ OptionM Unit"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 16, "character": 17}}
 {"range":
diff --git a/tests/lean/nonReserved.lean b/tests/lean/nonReserved.lean
index 35de65221f..41e0653949 100644
--- a/tests/lean/nonReserved.lean
+++ b/tests/lean/nonReserved.lean
@@ -1,7 +1,7 @@
 syntax "foo" &"bla" term : term
 
 macro_rules
-  | `(foo bla $x) => x
+  | `(foo bla $x) => pure x
 
 -- bla is still a valid identifier
 def bla := 10
diff --git a/tests/lean/run/498.lean b/tests/lean/run/498.lean
index 79b336c483..2d2f301465 100644
--- a/tests/lean/run/498.lean
+++ b/tests/lean/run/498.lean
@@ -53,9 +53,9 @@ inductive Kind
   (msg       : String :=
     let complementaryName? : Option String := OptionM.run do
       if inputFlag.isShort then
-        s!" (`--{flag.longName}`)"
+        pure s!" (`--{flag.longName}`)"
       else
-        s!" (`-{← flag.shortName?}`)"
+        pure s!" (`-{← flag.shortName?}`)"
     s!"Duplicate flag `{inputFlag}`.")
 | redundantFlagArg
   (flag       : Flag)
diff --git a/tests/lean/run/646.lean b/tests/lean/run/646.lean
index 71b49d0a9e..813392ea35 100644
--- a/tests/lean/run/646.lean
+++ b/tests/lean/run/646.lean
@@ -6,7 +6,7 @@ def build (n : Nat) : Array Unit := Id.run <| do
 
 @[noinline] def size : IO Nat := pure 50000
 
-def bench (f : ∀ {α : Type}, α → IO Unit := fun _ => ()) : IO Unit := do
+def bench (f : ∀ {α : Type}, α → IO Unit := fun _ => pure ()) : IO Unit := do
   let n ← size
   let arr := build n
   timeit "time" $
diff --git a/tests/lean/run/677.lean b/tests/lean/run/677.lean
index 46302b5cea..da44566e0d 100644
--- a/tests/lean/run/677.lean
+++ b/tests/lean/run/677.lean
@@ -2,7 +2,7 @@ import Lean
 open Lean
 
 def encodeDecode [ToJson α] [FromJson α] (x : α) : Except String α := do
-  let json ← toJson x
+  let json := toJson x
   fromJson? json
 
 #eval IO.ofExcept <| encodeDecode (Name.mkNum Name.anonymous 5)
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index a29c6b4bf1..54c51f5c8e 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -26,7 +26,7 @@ def checkDelab (e : Expr) (tgt? : Option Syntax) (name? : Option Name := none) :
       let e' ← instantiateMVars e'
       -- let ⟨e', _⟩ ← levelMVarToParam e'
       throwErrorIfErrors
-      e'
+      pure e'
     catch ex => throwError "{pfix} failed to re-elaborate,\n{stx}\n{← ex.toMessageData.toString}"
 
   withTheReader Core.Context (fun ctx => { ctx with options := ctx.options.setBool `pp.all true }) do
@@ -54,7 +54,7 @@ syntax (name := testDelabTDN) "#testDelabN " ident : command
   | `(#testDelabN $name:ident) => liftTermElabM `delabTD do
     let name := name.getId
     let [name] ← resolveGlobalConst (mkIdent name) | throwError "cannot resolve name"
-    let some cInfo ← (← getEnv).find? name | throwError "no decl for name"
+    let some cInfo := (← getEnv).find? name | throwError "no decl for name"
     let some value ← pure cInfo.value? | throwError "decl has no value"
     modify fun s => { s with levelNames := cInfo.levelParams }
     withTheReader Core.Context (fun ctx => { ctx with currNamespace := name.getPrefix, openDecls := [] }) do
@@ -270,7 +270,7 @@ set_option pp.proofs.withType false in
 #testDelab ∀ (α : Type u) (vals vals_1 : List α), { data := vals : Array α } = { data := vals_1 : Array α }
   expecting ∀ (α : Type u) (vals vals_1 : List α), { data := vals : Array α } = { data := vals_1 }
 
-#testDelab (do let ctxCore ← readThe Core.Context; ctxCore.currNamespace : MetaM Name)
+#testDelab (do let ctxCore ← readThe Core.Context; pure ctxCore.currNamespace : MetaM Name)
   expecting do
     let ctxCore ← readThe Core.Context
     pure ctxCore.currNamespace
diff --git a/tests/lean/run/doNotation2.lean b/tests/lean/run/doNotation2.lean
index 4a5e059b0e..4989812923 100644
--- a/tests/lean/run/doNotation2.lean
+++ b/tests/lean/run/doNotation2.lean
@@ -116,8 +116,8 @@ theorem ex8 : split [1, 2, 3, 4] = ([2, 4], [1, 3]) :=
 rfl
 
 def f3 (x : Nat) : IO Bool := do
-let y ← cond (x == 0) (do IO.println "hello"; true) false;
-!y
+let y ← cond (x == 0) (do IO.println "hello"; pure true) (pure false);
+pure !y
 
 def f4 (x y : Nat) : Nat × Nat := Id.run <| do
   let mut (x, y) := (x, y)
diff --git a/tests/lean/run/doNotation3.lean b/tests/lean/run/doNotation3.lean
index 34f802e45f..b31ca5087a 100644
--- a/tests/lean/run/doNotation3.lean
+++ b/tests/lean/run/doNotation3.lean
@@ -6,7 +6,7 @@ theorem zero_lt_of_lt : {a b : Nat} → a < b → 0 < b
 
 def fold {m α β} [Monad m] (as : Array α) (b : β) (f : α → β → m β) : m β := do
 let rec loop : (i : Nat) → i ≤ as.size → β → m β
-  | 0,   h, b => b
+  | 0,   h, b => pure b
   | i+1, h, b => do
     have h' : i < as.size          := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
     have : as.size - 1 < as.size     := Nat.sub_lt (zero_lt_of_lt h') (by decide)
diff --git a/tests/lean/run/irCompilerBug.lean b/tests/lean/run/irCompilerBug.lean
index 08d6f5649d..4e76ce9a1c 100644
--- a/tests/lean/run/irCompilerBug.lean
+++ b/tests/lean/run/irCompilerBug.lean
@@ -7,7 +7,7 @@ structure Payload :=
 
 
 @[noinline] def get? (p : Payload) (k : Nat) : OptionM Nat :=
-if p.key == k then p.val else none
+if p.key == k then pure p.val else failure
 
 inductive T
 | a (i : Nat)
diff --git a/tests/lean/run/isDefEqCheckAssignmentBug.lean b/tests/lean/run/isDefEqCheckAssignmentBug.lean
index 8d33cc220a..bc13c13b8e 100644
--- a/tests/lean/run/isDefEqCheckAssignmentBug.lean
+++ b/tests/lean/run/isDefEqCheckAssignmentBug.lean
@@ -18,7 +18,7 @@ def tst : MetaM Unit := do
     trace[Meta.debug] "{m2} : {← inferType m2}"
     trace[Meta.debug] "{m1} : {← inferType m1}"
     let e ← mkForallFVars #[x] m2 -- `forall (x : f ?m2), ?m2`
-    trace[Meta.debug] "{e} : {← e}"
+    trace[Meta.debug] "{e} : {← inferType e}"
     return ()
 
 set_option trace.Meta.isDefEq true
diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean
index 01f1625316..e11768707c 100644
--- a/tests/lean/run/match1.lean
+++ b/tests/lean/run/match1.lean
@@ -8,11 +8,11 @@ def checkWithMkMatcherInput (matcher : Lean.Name) : Lean.MetaM Unit :=
     throwError "matcher name not reconstructed correctly: {matcher} ≟ {input.matcherName}"
 
   let lCtx ← Lean.getLCtx
-  let fvars ← Lean.collectFVars {} res.matcher
-  let closure ← Lean.Meta.Closure.mkLambda (fvars.fvarSet.toList.toArray.map lCtx.get!) res.matcher
+  let fvars := Lean.collectFVars {} res.matcher
+  let closure := Lean.Meta.Closure.mkLambda (fvars.fvarSet.toList.toArray.map lCtx.get!) res.matcher
 
   let origTy := origMatcher.value!
-  let newTy ← closure
+  let newTy := closure
   if not <| ←Lean.Meta.isDefEq origTy newTy then
     throwError "matcher {matcher} does not round-trip correctly:\n{origTy} ≟ {newTy}"
 
diff --git a/tests/lean/run/maze.lean b/tests/lean/run/maze.lean
index 220784e180..1587c5c357 100644
--- a/tests/lean/run/maze.lean
+++ b/tests/lean/run/maze.lean
@@ -103,7 +103,7 @@ def extractXY : Lean.Expr → Lean.MetaM Coords
   let y ← Lean.Meta.whnf sizeArgs[1]
   let numCols := (Lean.Expr.natLit? x).get!
   let numRows := (Lean.Expr.natLit? y).get!
-  Coords.mk numCols numRows
+  return Coords.mk numCols numRows
 
 partial def extractWallList : Lean.Expr → Lean.MetaM (List Coords)
 | exp => do
@@ -113,8 +113,8 @@ partial def extractWallList : Lean.Expr → Lean.MetaM (List Coords)
   then let consArgs := Lean.Expr.getAppArgs exp'
        let rest ← extractWallList consArgs[2]
        let ⟨wallCol, wallRow⟩ ← extractXY consArgs[1]
-       (Coords.mk wallCol wallRow) :: rest
-  else [] -- "List.nil"
+       return (Coords.mk wallCol wallRow) :: rest
+  else return [] -- "List.nil"
 
 partial def extractGameState : Lean.Expr → Lean.MetaM GameState
 | exp => do
diff --git a/tests/lean/run/toFromJson.lean b/tests/lean/run/toFromJson.lean
index 0ecec5fa8d..a138a3f9f9 100644
--- a/tests/lean/run/toFromJson.lean
+++ b/tests/lean/run/toFromJson.lean
@@ -12,8 +12,8 @@ syntax "json " json : term
 
 /- declare a micro json parser, so we can write our tests in a more legible way. -/
 open Json in macro_rules
-  | `(json $s:strLit) => s
-  | `(json $n:numLit) => n
+  | `(json $s:strLit) => pure s
+  | `(json $n:numLit) => pure n
   | `(json { $[$ns : $js],* }) => do
     let mut fields := #[]
     for n in ns, j in js do
@@ -28,15 +28,15 @@ open Json in macro_rules
 def checkToJson [ToJson α] (obj : α) (rhs : Json) : MetaM Unit :=
   let lhs := (obj |> toJson).pretty
   if lhs == rhs.pretty then
-    ()
+    pure ()
   else
     throwError "{lhs} ≟ {rhs}"
 
-def checkRoundTrip [Repr α] [BEq α] [ToJson α] [FromJson α] (obj : α) : MetaM Unit :=
+def checkRoundTrip [Repr α] [BEq α] [ToJson α] [FromJson α] (obj : α) : MetaM Unit := do
   let roundTripped := obj |> toJson |> fromJson?
-  if let some roundTripped := roundTripped then
+  if let Except.ok roundTripped := roundTripped then
     if obj == roundTripped then
-      ()
+      pure ()
     else
       throwError "{repr obj} ≟ {repr roundTripped}"
   else
diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean
index 694b771188..e9fca46871 100644
--- a/tests/lean/run/trace.lean
+++ b/tests/lean/run/trace.lean
@@ -39,7 +39,7 @@ do traceCtx `module $ do {
    -- if `trace.slow is active.
    trace[slow] (m!"slow message: " ++ toString (slow b))
    -- This is true even if it is a monad computation:
-   trace[slow] (m!"slow message: " ++ (← toString (slow b)))
+   trace[slow] (m!"slow message: " ++ (toString (slow b)))
 
 def run (x : M Unit) : M Unit :=
 withReader
diff --git a/tests/lean/run/tryPureCoe.lean b/tests/lean/run/tryPureCoe.lean
deleted file mode 100644
index 4aac1b5979..0000000000
--- a/tests/lean/run/tryPureCoe.lean
+++ /dev/null
@@ -1,47 +0,0 @@
-def m1 : IO Bool :=
-pure true
-
-def p (x : Nat) : Bool :=
-x > 0
-
-def tst1 : IO Bool :=
-true <&&> m1
-
-def tst2 (x : Nat) : IO Bool :=
-x = 0 <&&> m1
-
-def tst3 (x : Nat) : IO Unit := do
-if ← (m1 <&&> x > 0) then
-  throw $ IO.userError "test"
-
-def tst4 (x : Nat) : IO Unit := do
-if x > 0 && (← m1) then
-  throw $ IO.userError "test"
-
-def tst5 (x : Nat) : IO Unit := do
-if ← (p x <&&> m1) then
-  throw $ IO.userError "test"
-
-def tst6 (x : Nat) : IO Unit := do
-if ← (p x <&&> id m1) then
-  throw $ IO.userError "test"
-
-def tst7 (x : Nat) : IO Unit := do
-if (← m1) && x > 0 then
-  throw $ IO.userError "test"
-
-def tst8 (x : Nat) : IO Unit := do
-if x > 0 && (← m1) then
-  throw $ IO.userError "test"
-
-def tst9 (x : Nat) : IO Unit := do
-if p x && (← m1) then
-  throw $ IO.userError "test"
-
-def tst10 (x : Nat) : IO Unit := do
-if p x && (← id m1) then
-  throw $ IO.userError "test"
-
-def tst11 (x : Nat) : IO Unit := do
-if p x && id (← m1) then
-  throw $ IO.userError "test"
diff --git a/tests/lean/runSTBug.lean b/tests/lean/runSTBug.lean
index 18d1b6acdf..bf0d6425f9 100644
--- a/tests/lean/runSTBug.lean
+++ b/tests/lean/runSTBug.lean
@@ -6,7 +6,7 @@ def f (xs : List Nat) (delta : Nat) : List Nat :=
   runST (fun ω => visit xs |>.run)
 where
   visit {ω} : List Nat → MonadCacheT Nat Nat (ST ω) (List Nat)
-    | []    => []
+    | []    => return []
     | a::as => do
       let b ← checkCache a fun _ => return a + delta
       return b :: (← visit as)
diff --git a/tests/lean/server/diags.lean b/tests/lean/server/diags.lean
index 71895faf51..64e50227f6 100644
--- a/tests/lean/server/diags.lean
+++ b/tests/lean/server/diags.lean
@@ -18,7 +18,7 @@ def main : IO Unit := do
       let diag := diags.getLast!
       FS.writeFile "content_diag.json.produced" (toString <| toJson (diag : JsonRpc.Message))
 
-      if let some (refDiag : JsonRpc.Notification PublishDiagnosticsParams) :=
+      if let Except.ok (refDiag : JsonRpc.Notification PublishDiagnosticsParams) :=
         (Json.parse $ ←FS.readFile "content_diag.json") >>= fromJson?
       then
         assert! (diag == refDiag)
diff --git a/tests/lean/server/edits.lean b/tests/lean/server/edits.lean
index e3d84fe494..a215e5d3e8 100644
--- a/tests/lean/server/edits.lean
+++ b/tests/lean/server/edits.lean
@@ -23,7 +23,7 @@ def main : IO Unit := do
       let diag := diags.getLast!
       FS.writeFile "edits_diag.json.produced" (toString <| toJson (diag : JsonRpc.Message))
 
-      if let some (refDiag : JsonRpc.Notification PublishDiagnosticsParams) :=
+      if let Except.ok (refDiag : JsonRpc.Notification PublishDiagnosticsParams) :=
         (Json.parse $ ←FS.readFile "edits_diag.json") >>= fromJson?
       then
         assert! (diag == refDiag)
diff --git a/tests/lean/syntaxInNamespacesAndPP.lean b/tests/lean/syntaxInNamespacesAndPP.lean
index effec3aa65..251ba3301d 100644
--- a/tests/lean/syntaxInNamespacesAndPP.lean
+++ b/tests/lean/syntaxInNamespacesAndPP.lean
@@ -3,7 +3,7 @@ namespace Foo
 syntax "foo" term : term
 
 macro_rules
-  | `(foo $x) => x
+  | `(foo $x) => pure x
 
 set_option trace.Elab true in
 #check foo true
@@ -15,7 +15,7 @@ namespace Bla
 syntax (name := bla) "bla" term : term
 
 macro_rules
-  | `(bla $x) => x
+  | `(bla $x) => pure x
 
 set_option trace.Elab true in
 #check bla true
diff --git a/tests/leanpkg/builtin_attr/UserAttr/BlaAttr.lean b/tests/leanpkg/builtin_attr/UserAttr/BlaAttr.lean
index 6fb03c4e86..a931e061e7 100644
--- a/tests/leanpkg/builtin_attr/UserAttr/BlaAttr.lean
+++ b/tests/leanpkg/builtin_attr/UserAttr/BlaAttr.lean
@@ -7,5 +7,5 @@ open Lean
 initialize registerBuiltinAttribute {
     name := `bar,
     descr := "",
-    add := fun _ _ _ => ()
+    add := fun _ _ _ => pure ()
   }
diff --git a/tests/leanpkg/user_attr_app/UserAttr.lean b/tests/leanpkg/user_attr_app/UserAttr.lean
index 219093ee95..5eebfc9430 100644
--- a/tests/leanpkg/user_attr_app/UserAttr.lean
+++ b/tests/leanpkg/user_attr_app/UserAttr.lean
@@ -13,4 +13,4 @@ def tst : MetaM Unit := do
 
 unsafe def main : IO Unit := do
   initSearchPath (← Lean.findSysroot?) ["build"]
-  withImportModules [{ module := `UserAttr.Tst : Import }] {} 0 fun env => ()
+  withImportModules [{ module := `UserAttr.Tst : Import }] {} 0 fun env => pure ()