diff --git a/Aesop/Search/Expansion/Norm.lean b/Aesop/Search/Expansion/Norm.lean
index 058ef867..72015fb3 100644
--- a/Aesop/Search/Expansion/Norm.lean
+++ b/Aesop/Search/Expansion/Norm.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
+import Std.Data.Option.Basic
 import Aesop.RuleTac
 import Aesop.Search.Expansion.Basic
 import Aesop.Search.Expansion.Simp
diff --git a/Aesop/Util/EqualUpToIds.lean b/Aesop/Util/EqualUpToIds.lean
index 5615a692..ba9a0375 100644
--- a/Aesop/Util/EqualUpToIds.lean
+++ b/Aesop/Util/EqualUpToIds.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
+import Lean.Elab.Tactic.Basic
 import Std.Lean.Meta.SavedState
 
 open Lean Lean.Meta
diff --git a/Aesop/Util/Tactic.lean b/Aesop/Util/Tactic.lean
index 38731d2f..4b43b8ca 100644
--- a/Aesop/Util/Tactic.lean
+++ b/Aesop/Util/Tactic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
-
+import Lean.Meta.Tactic.Delta
 import Aesop.Util.Basic
 
 open Lean
diff --git a/lake-manifest.json b/lake-manifest.json
index baee9c8b..843316c7 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "ee49cf8fada1bf5a15592c399a925c401848227f",
+   "rev": "1972e073b3e6bc0776ad5b544bfa7db7fc3f7c36",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",