diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean
index a9f8bce381..b56889bea9 100644
--- a/src/Lean/Elab/GuardMsgs.lean
+++ b/src/Lean/Elab/GuardMsgs.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
+prelude
 import Lean.Server.CodeActions.Attr
 
 /-! `#guard_msgs` command for testing commands
diff --git a/src/Lean/Server/CodeActions.lean b/src/Lean/Server/CodeActions.lean
index 1a02fc26db..6642fb3372 100644
--- a/src/Lean/Server/CodeActions.lean
+++ b/src/Lean/Server/CodeActions.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: E.W.Ayers
 -/
+prelude
 import Lean.Server.CodeActions.Attr
 import Lean.Server.CodeActions.Basic
 import Lean.Server.CodeActions.Provider
diff --git a/src/Lean/Server/CodeActions/Attr.lean b/src/Lean/Server/CodeActions/Attr.lean
index f00975b02a..a751d7f56b 100644
--- a/src/Lean/Server/CodeActions/Attr.lean
+++ b/src/Lean/Server/CodeActions/Attr.lean
@@ -3,6 +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
 -/
+prelude
 import Lean.Server.CodeActions.Basic
 
 /-!
diff --git a/src/Lean/Server/CodeActions/Provider.lean b/src/Lean/Server/CodeActions/Provider.lean
index 6108768af5..13068794db 100644
--- a/src/Lean/Server/CodeActions/Provider.lean
+++ b/src/Lean/Server/CodeActions/Provider.lean
@@ -3,6 +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
 -/
+prelude
 import Lean.Elab.BuiltinTerm
 import Lean.Elab.BuiltinNotation
 import Lean.Server.InfoUtils