diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean
index 7658450..a70b07e 100644
--- a/REPL/Frontend.lean
+++ b/REPL/Frontend.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean.Elab.Frontend
-import REPL.Util.TermUnsafe
 
 open Lean Elab
 
diff --git a/REPL/Main.lean b/REPL/Main.lean
index be515cf..23345d5 100644
--- a/REPL/Main.lean
+++ b/REPL/Main.lean
@@ -6,7 +6,6 @@ Authors: Scott Morrison
 import REPL.JSON
 import REPL.Frontend
 import REPL.Util.Path
-import REPL.Util.TermUnsafe
 import REPL.Lean.ContextInfo
 import REPL.Lean.Environment
 import REPL.Lean.InfoTree
diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean
index a67bd63..206b22a 100644
--- a/REPL/Snapshots.lean
+++ b/REPL/Snapshots.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean.Replay
+import Lean.Elab.Command
 import REPL.Util.Pickle
 
 open Lean Elab
diff --git a/REPL/Util/Pickle.lean b/REPL/Util/Pickle.lean
index eba3338..e3a4c9e 100644
--- a/REPL/Util/Pickle.lean
+++ b/REPL/Util/Pickle.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import REPL.Util.TermUnsafe
+import Lean.Environment
 
 /-!
 # Pickling and unpickling objects
diff --git a/REPL/Util/TermUnsafe.lean b/REPL/Util/TermUnsafe.lean
deleted file mode 100644
index e790347..0000000
--- a/REPL/Util/TermUnsafe.lean
+++ /dev/null
@@ -1,63 +0,0 @@
-/-
-Copyright (c) 2021 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Gabriel Ebner
--/
-import Lean.Elab.ElabRules
-import Lean.Meta.Closure
-import Lean.Compiler.ImplementedByAttr
-
--- This has been duplicated from Std4 to avoid a dependency.
-
-/-!
-Defines term syntax to call unsafe functions.
-
-```
-def cool :=
-  unsafe (unsafeCast () : Nat)
-
-#eval cool
-```
--/
-
-namespace Std.TermUnsafe
-open Lean Meta Elab Term
-
-/-- Construct an auxiliary name based on the current declaration name and the given `hint` base. -/
-def mkAuxName (hint : Name) : TermElabM Name :=
-  withFreshMacroScope do
-    let name := (← getDeclName?).getD Name.anonymous ++ hint
-    pure $ addMacroScope (← getMainModule) name (← getCurrMacroScope)
-
-/--
-`unsafe t : α` is an expression constructor which allows using unsafe declarations inside the
-body of `t : α`, by creating an auxiliary definition containing `t` and using `implementedBy` to
-wrap it in a safe interface. It is required that `α` is nonempty for this to be sound,
-but even beyond that, an `unsafe` block should be carefully inspected for memory safety because
-the compiler is unable to guarantee the safety of the operation.
-
-For example, the `evalExpr` function is unsafe, because the compiler cannot guarantee that when
-you call ```evalExpr Foo ``Foo e``` that the type `Foo` corresponds to the name `Foo`, but in a
-particular use case, we can ensure this, so `unsafe (evalExpr Foo ``Foo e)` is a correct usage.
--/
-elab "unsafe " t:term : term <= expectedType => do
-  let mut t ← elabTerm t expectedType
-  t ← instantiateMVars t
-  if t.hasExprMVar then
-    synthesizeSyntheticMVarsNoPostponing
-    t ← instantiateMVars t
-  if ← logUnassignedUsingErrorInfos (← getMVars t) then throwAbortTerm
-  t ← mkAuxDefinitionFor (← mkAuxName `unsafe) t
-  let Expr.const unsafeFn unsafeLvls .. := t.getAppFn | unreachable!
-  let ConstantInfo.defnInfo unsafeDefn ← getConstInfo unsafeFn | unreachable!
-  let implName ← mkAuxName `impl
-  addDecl <| Declaration.defnDecl {
-    name := implName
-    type := unsafeDefn.type
-    levelParams := unsafeDefn.levelParams
-    value := ← mkOfNonempty unsafeDefn.type
-    hints := ReducibilityHints.opaque
-    safety := DefinitionSafety.safe
-  }
-  setImplementedBy implName unsafeFn
-  pure $ mkAppN (mkConst implName unsafeLvls) t.getAppArgs
diff --git a/lean-toolchain b/lean-toolchain
index 5026204..6b26dd5 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.0
+leanprover/lean4:v4.7.0-rc1
diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json
index 95669a7..812c31d 100644
--- a/test/Mathlib/lake-manifest.json
+++ b/test/Mathlib/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
+   "rev": "ff9850c4726f6b9fb8d8e96980c3fcb2900be8bd",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -22,19 +22,19 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b",
+   "rev": "056ca0fa8f5585539d0b940f532d9750c3a2270f",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "16cae05860b208925f54e5581ec5fd264823440c",
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.29",
+   "inputRev": "v0.0.30",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -58,10 +58,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb",
+   "rev": "fa48894a5d2780c6593a224003a660ca039e3e8f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "v4.7.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«repl-mathlib-tests»",
diff --git a/test/Mathlib/lakefile.lean b/test/Mathlib/lakefile.lean
index 879e707..cb7a21e 100644
--- a/test/Mathlib/lakefile.lean
+++ b/test/Mathlib/lakefile.lean
@@ -3,7 +3,7 @@ open Lake DSL
 
 package «repl-mathlib-tests» where
   -- add package configuration options here
-  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.6.0"
+  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.7.0-rc1"
 
 @[default_target]
 lean_lib «ReplMathlibTests» where
diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain
index 5026204..6b26dd5 100644
--- a/test/Mathlib/lean-toolchain
+++ b/test/Mathlib/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.0
+leanprover/lean4:v4.7.0-rc1
diff --git a/test/Mathlib/test/20240209.expected.out b/test/Mathlib/test/20240209.expected.out
index b043371..b83ff66 100644
--- a/test/Mathlib/test/20240209.expected.out
+++ b/test/Mathlib/test/20240209.expected.out
@@ -1,5 +1,3 @@
-{"env": 0}
-
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 22},
@@ -10,7 +8,7 @@
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
    "data": "declaration uses 'sorry'"}],
- "env": 1}
+ "env": 0}
 
 {"proofState": 1,
  "messages":
diff --git a/test/Mathlib/test/20240209.in b/test/Mathlib/test/20240209.in
index 738d727..08ebbb2 100644
--- a/test/Mathlib/test/20240209.in
+++ b/test/Mathlib/test/20240209.in
@@ -1,5 +1,3 @@
-{"cmd": "import Std.Tactic.Simpa"}
-
-{"cmd": "example : False := by sorry", "env": 0}
+{"cmd": "example : False := by sorry"}
 
 {"tactic": "simpa using show False by done", "proofState": 0}
diff --git a/test/Mathlib/test/exact.expected.out b/test/Mathlib/test/exact.expected.out.broken
similarity index 100%
rename from test/Mathlib/test/exact.expected.out
rename to test/Mathlib/test/exact.expected.out.broken
diff --git a/test/by_cases.expected.out b/test/by_cases.expected.out
index 0530ff9..e22198a 100644
--- a/test/by_cases.expected.out
+++ b/test/by_cases.expected.out
@@ -12,14 +12,14 @@
 
 {"proofState": 1,
  "goals":
- ["case inl\nx : Int\nh : x < 0\n⊢ x = x",
-  "case inr\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
+ ["case pos\nx : Int\nh : x < 0\n⊢ x = x",
+  "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
 
-{"proofState": 2, "goals": ["case inr\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
+{"proofState": 2, "goals": ["case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
 
 {"sorries":
- [{"proofState": 3, "goal": "case inl\nx : Int\nh : x < 0\n⊢ x = x"},
-  {"proofState": 4, "goal": "case inr\nx : Int\nh : ¬x < 0\n⊢ x = x"}],
+ [{"proofState": 3, "goal": "case pos\nx : Int\nh : x < 0\n⊢ x = x"},
+  {"proofState": 4, "goal": "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"}],
  "proofState": 5,
  "goals": []}
 
diff --git a/test/by_cases.in b/test/by_cases.in
index 9498c79..031c43f 100644
--- a/test/by_cases.in
+++ b/test/by_cases.in
@@ -2,7 +2,7 @@
 
 {"proofState" : 0, "tactic": "by_cases h : x < 0"}
 
-{"proofState" : 1, "tactic": "case inl => rfl"}
+{"proofState" : 1, "tactic": "case pos => rfl"}
 
 {"proofState" : 1, "tactic": "all_goals sorry"}
 
diff --git a/test/name_generator.expected.out b/test/name_generator.expected.out
index 33bb796..557d03b 100644
--- a/test/name_generator.expected.out
+++ b/test/name_generator.expected.out
@@ -23,11 +23,15 @@
  "proofState": 5,
  "goals": []}
 
-{"traces": ["[Meta.Tactic.simp.rewrite] h0:1000, x > 0 ==> True"],
+{"traces":
+ ["[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, x > 0 ==> 0 < x",
+  "[Meta.Tactic.simp.rewrite] h0:1000, 0 < x ==> True"],
  "proofState": 6,
  "goals": []}
 
-{"traces": ["[Meta.Tactic.simp.rewrite] h0:1000, x > 0 ==> True"],
+{"traces":
+ ["[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, x > 0 ==> 0 < x",
+  "[Meta.Tactic.simp.rewrite] h0:1000, 0 < x ==> True"],
  "proofState": 7,
  "goals": []}