diff --git a/.github/workflows/check-prelude.yml b/.github/workflows/check-prelude.yml
index 049aad9b2439..cec957f6366f 100644
--- a/.github/workflows/check-prelude.yml
+++ b/.github/workflows/check-prelude.yml
@@ -14,6 +14,7 @@ jobs:
           sparse-checkout: |
             src/Lean
             src/Std
+            src/lake/Lake
       - name: Check Prelude
         run: |
           failed_files=""
@@ -21,7 +22,7 @@ jobs:
             if ! grep -q "^prelude$" "$file"; then
               failed_files="$failed_files$file\n"
             fi
-          done < <(find src/Lean src/Std -name '*.lean' -print0)
+          done < <(find src/Lean src/Std src/lake/Lake -name '*.lean' -print0)
           if [ -n "$failed_files" ]; then
             echo -e "The following files should use 'prelude':\n$failed_files"
             exit 1
diff --git a/src/lake/Lake.lean b/src/lake/Lake.lean
index 09633bb52453..57ff3aa4fb0c 100644
--- a/src/lake/Lake.lean
+++ b/src/lake/Lake.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build
 import Lake.Config
 import Lake.DSL
diff --git a/src/lake/Lake/Build.lean b/src/lake/Lake/Build.lean
index 528d75cdaddd..2bc56f42c067 100644
--- a/src/lake/Lake/Build.lean
+++ b/src/lake/Lake/Build.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Run
 import Lake.Build.Module
 import Lake.Build.Package
diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean
index afb7bdb5384c..30388d933a34 100644
--- a/src/lake/Lake/Build/Actions.lean
+++ b/src/lake/Lake/Build/Actions.lean
@@ -3,6 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone, Siddharth Bhat
 -/
+prelude
 import Lake.Util.Proc
 import Lake.Util.NativeLib
 import Lake.Util.IO
diff --git a/src/lake/Lake/Build/Basic.lean b/src/lake/Lake/Build/Basic.lean
index 446264f8aa0e..c18e5c764c0b 100644
--- a/src/lake/Lake/Build/Basic.lean
+++ b/src/lake/Lake/Build/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Log
 import Lake.Util.Exit
 import Lake.Util.Lift
diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index 4917f5ad181a..7658b3483fc6 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/src/lake/Lake/Build/Common.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Config.Monad
 import Lake.Build.Actions
 import Lake.Util.JsonObject
diff --git a/src/lake/Lake/Build/Data.lean b/src/lake/Lake/Build/Data.lean
index 799f105e23bc..77f4d4276c7a 100644
--- a/src/lake/Lake/Build/Data.lean
+++ b/src/lake/Lake/Build/Data.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Key
 import Lake.Util.Family
 
diff --git a/src/lake/Lake/Build/Executable.lean b/src/lake/Lake/Build/Executable.lean
index ff8ec5239136..53999a4b2be7 100644
--- a/src/lake/Lake/Build/Executable.lean
+++ b/src/lake/Lake/Build/Executable.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Common
 
 namespace Lake
diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean
index bf9bb43eb838..9299dee7255b 100644
--- a/src/lake/Lake/Build/Facets.lean
+++ b/src/lake/Lake/Build/Facets.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Job
 import Lake.Build.Data
 
diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean
index 4359122c41bc..38e9dc7a010f 100644
--- a/src/lake/Lake/Build/Fetch.lean
+++ b/src/lake/Lake/Build/Fetch.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Error
 import Lake.Util.Cycle
 import Lake.Util.EquipT
diff --git a/src/lake/Lake/Build/Imports.lean b/src/lake/Lake/Build/Imports.lean
index bfe43cfd56ca..efbb03ca3897 100644
--- a/src/lake/Lake/Build/Imports.lean
+++ b/src/lake/Lake/Build/Imports.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Module
 
 /-!
diff --git a/src/lake/Lake/Build/Index.lean b/src/lake/Lake/Build/Index.lean
index 73a1db2ca3f1..b696f7db814b 100644
--- a/src/lake/Lake/Build/Index.lean
+++ b/src/lake/Lake/Build/Index.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Executable
 import Lake.Build.Topological
 
diff --git a/src/lake/Lake/Build/Info.lean b/src/lake/Lake/Build/Info.lean
index 405f19763268..115cd88bd696 100644
--- a/src/lake/Lake/Build/Info.lean
+++ b/src/lake/Lake/Build/Info.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Config.LeanExe
 import Lake.Config.ExternLib
 import Lake.Build.Facets
diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean
index 4bc441c18e05..bcff6b3ea010 100644
--- a/src/lake/Lake/Build/Job.lean
+++ b/src/lake/Lake/Build/Job.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Task
 import Lake.Build.Basic
 
diff --git a/src/lake/Lake/Build/Key.lean b/src/lake/Lake/Build/Key.lean
index 6619ecc32d82..97b6329fe88e 100644
--- a/src/lake/Lake/Build/Key.lean
+++ b/src/lake/Lake/Build/Key.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Name
 
 namespace Lake
diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean
index 27db61dad0b7..8849b403dc0f 100644
--- a/src/lake/Lake/Build/Library.lean
+++ b/src/lake/Lake/Build/Library.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Common
 import Lake.Build.Targets
 
diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index 03ca79436beb..253c78dd900a 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/src/lake/Lake/Build/Module.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Mac Malone, Siddharth Bhat
 -/
+prelude
 import Lake.Util.OrdHashSet
 import Lake.Util.List
 import Lean.Elab.ParseImportsFast
diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean
index ec8185b0ffc3..35ee042fdc89 100644
--- a/src/lake/Lake/Build/Package.lean
+++ b/src/lake/Lake/Build/Package.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Git
 import Lake.Util.Sugar
 import Lake.Build.Common
diff --git a/src/lake/Lake/Build/Run.lean b/src/lake/Lake/Build/Run.lean
index 6ca3671a9b48..43bf3f92b9dc 100644
--- a/src/lake/Lake/Build/Run.lean
+++ b/src/lake/Lake/Build/Run.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone, Gabriel Ebner, Sebastian Ullrich
 -/
+prelude
 import Lake.Util.Lock
 import Lake.Build.Index
 
diff --git a/src/lake/Lake/Build/Store.lean b/src/lake/Lake/Build/Store.lean
index 40b534c64d94..ba1a3fa0faeb 100644
--- a/src/lake/Lake/Build/Store.lean
+++ b/src/lake/Lake/Build/Store.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Data
 import Lake.Util.StoreInsts
 
diff --git a/src/lake/Lake/Build/Targets.lean b/src/lake/Lake/Build/Targets.lean
index 4901eca6edb9..9a51def55f5b 100644
--- a/src/lake/Lake/Build/Targets.lean
+++ b/src/lake/Lake/Build/Targets.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Config.Monad
 
 /-! # Build Target Fetching
diff --git a/src/lake/Lake/Build/Topological.lean b/src/lake/Lake/Build/Topological.lean
index b5bb54ee00c4..b6e5962ca664 100644
--- a/src/lake/Lake/Build/Topological.lean
+++ b/src/lake/Lake/Build/Topological.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Cycle
 import Lake.Util.Store
 import Lake.Util.EquipT
diff --git a/src/lake/Lake/Build/Trace.lean b/src/lake/Lake/Build/Trace.lean
index 2552f6e3e254..3980b6e1741a 100644
--- a/src/lake/Lake/Build/Trace.lean
+++ b/src/lake/Lake/Build/Trace.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.IO
 import Lean.Data.Json
 
diff --git a/src/lake/Lake/CLI.lean b/src/lake/Lake/CLI.lean
index 2695b6a4cf4d..da2a7ade7272 100644
--- a/src/lake/Lake/CLI.lean
+++ b/src/lake/Lake/CLI.lean
@@ -3,4 +3,5 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.CLI.Main
diff --git a/src/lake/Lake/CLI/Actions.lean b/src/lake/Lake/CLI/Actions.lean
index a627be0d6612..732a0a5f42fe 100644
--- a/src/lake/Lake/CLI/Actions.lean
+++ b/src/lake/Lake/CLI/Actions.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Run
 import Lake.Build.Targets
 import Lake.CLI.Build
diff --git a/src/lake/Lake/CLI/Build.lean b/src/lake/Lake/CLI/Build.lean
index 9f47c117f284..05aaa760a6c1 100644
--- a/src/lake/Lake/CLI/Build.lean
+++ b/src/lake/Lake/CLI/Build.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Index
 import Lake.CLI.Error
 
diff --git a/src/lake/Lake/CLI/Error.lean b/src/lake/Lake/CLI/Error.lean
index 221b91193e02..37d97c541dd1 100644
--- a/src/lake/Lake/CLI/Error.lean
+++ b/src/lake/Lake/CLI/Error.lean
@@ -3,6 +3,9 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Data.ToString
+import Init.System.FilePath
 
 namespace Lake
 open Lean (Name)
diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean
index 1ef1390e24f5..26a4f44005fb 100644
--- a/src/lake/Lake/CLI/Help.lean
+++ b/src/lake/Lake/CLI/Help.lean
@@ -3,6 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
+prelude
 import Lake.Version
 
 namespace Lake
diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean
index a36ca4792020..9b2bbacda722 100644
--- a/src/lake/Lake/CLI/Init.lean
+++ b/src/lake/Lake/CLI/Init.lean
@@ -3,6 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
+prelude
 import Lake.Util.Git
 import Lake.Util.Sugar
 import Lake.Util.Version
diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean
index ec27ba1b129f..b333732aed21 100644
--- a/src/lake/Lake/CLI/Main.lean
+++ b/src/lake/Lake/CLI/Main.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Load
 import Lake.Build.Imports
 import Lake.Util.Error
diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean
index eab1b99439b0..4598b7206e94 100644
--- a/src/lake/Lake/CLI/Serve.lean
+++ b/src/lake/Lake/CLI/Serve.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Load
 import Lake.Build
 import Lake.Util.MainM
diff --git a/src/lake/Lake/CLI/Translate.lean b/src/lake/Lake/CLI/Translate.lean
index 9a75e638cfd9..943b4d195bbd 100644
--- a/src/lake/Lake/CLI/Translate.lean
+++ b/src/lake/Lake/CLI/Translate.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Config.Lang
 import Lake.Config.Package
 import Lake.CLI.Translate.Toml
diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean
index 0319dd77d01b..ad00fe069120 100644
--- a/src/lake/Lake/CLI/Translate/Lean.lean
+++ b/src/lake/Lake/CLI/Translate/Lean.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.DSL
 import Lake.Config.Package
 import Lean.Parser.Module
diff --git a/src/lake/Lake/CLI/Translate/Toml.lean b/src/lake/Lake/CLI/Translate/Toml.lean
index 50a7c58a830c..5f75fa843091 100644
--- a/src/lake/Lake/CLI/Translate/Toml.lean
+++ b/src/lake/Lake/CLI/Translate/Toml.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Toml.Encode
 import Lake.Config.Package
 
diff --git a/src/lake/Lake/Config.lean b/src/lake/Lake/Config.lean
index cc67357d0adb..0677dbc6c978 100644
--- a/src/lake/Lake/Config.lean
+++ b/src/lake/Lake/Config.lean
@@ -3,4 +3,5 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Config.Monad
diff --git a/src/lake/Lake/Config/Context.lean b/src/lake/Lake/Config/Context.lean
index b3bdb799c227..01fc2c4dd2c5 100644
--- a/src/lake/Lake/Config/Context.lean
+++ b/src/lake/Lake/Config/Context.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Config.Opaque
 import Lake.Config.InstallPath
 
diff --git a/src/lake/Lake/Config/Defaults.lean b/src/lake/Lake/Config/Defaults.lean
index 60ff94095f2f..36ea4f8a02c2 100644
--- a/src/lake/Lake/Config/Defaults.lean
+++ b/src/lake/Lake/Config/Defaults.lean
@@ -3,7 +3,11 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.System.FilePath
+
 namespace Lake
+
 open System (FilePath)
 
 /--
diff --git a/src/lake/Lake/Config/Dependency.lean b/src/lake/Lake/Config/Dependency.lean
index 6ee9ee701e1c..246c4b68d565 100644
--- a/src/lake/Lake/Config/Dependency.lean
+++ b/src/lake/Lake/Config/Dependency.lean
@@ -3,6 +3,8 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
+prelude
+import Init.System.FilePath
 import Lean.Data.NameMap
 
 /- # Package Dependency Configuration
diff --git a/src/lake/Lake/Config/Env.lean b/src/lake/Lake/Config/Env.lean
index e50343c480e1..1f99bb5c4797 100644
--- a/src/lake/Lake/Config/Env.lean
+++ b/src/lake/Lake/Config/Env.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Name
 import Lake.Util.NativeLib
 import Lake.Config.InstallPath
diff --git a/src/lake/Lake/Config/ExternLib.lean b/src/lake/Lake/Config/ExternLib.lean
index cbda507695e6..92020e374ade 100644
--- a/src/lake/Lake/Config/ExternLib.lean
+++ b/src/lake/Lake/Config/ExternLib.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Config.Package
 
 namespace Lake
diff --git a/src/lake/Lake/Config/ExternLibConfig.lean b/src/lake/Lake/Config/ExternLibConfig.lean
index fbc52a051a0e..16644168f1f6 100644
--- a/src/lake/Lake/Config/ExternLibConfig.lean
+++ b/src/lake/Lake/Config/ExternLibConfig.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Job
 import Lake.Build.Data
 
diff --git a/src/lake/Lake/Config/FacetConfig.lean b/src/lake/Lake/Config/FacetConfig.lean
index 63d1090b05f9..ffb3609e39ae 100644
--- a/src/lake/Lake/Config/FacetConfig.lean
+++ b/src/lake/Lake/Config/FacetConfig.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone, Mario Carneiro
 -/
+prelude
 import Lake.Build.Fetch
 
 namespace Lake
diff --git a/src/lake/Lake/Config/Glob.lean b/src/lake/Lake/Config/Glob.lean
index 26637af7e7de..15d893b6663a 100644
--- a/src/lake/Lake/Config/Glob.lean
+++ b/src/lake/Lake/Config/Glob.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Mac Malone
 -/
+prelude
 import Lean.Util.Path
 import Lake.Util.Name
 
diff --git a/src/lake/Lake/Config/InstallPath.lean b/src/lake/Lake/Config/InstallPath.lean
index a0877ef9316f..b9ffc6e0c2ca 100644
--- a/src/lake/Lake/Config/InstallPath.lean
+++ b/src/lake/Lake/Config/InstallPath.lean
@@ -3,6 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Control.Option
 import Lake.Util.NativeLib
 import Lake.Config.Defaults
 
diff --git a/src/lake/Lake/Config/Lang.lean b/src/lake/Lake/Config/Lang.lean
index d12e9b0fdc99..b686dada0749 100644
--- a/src/lake/Lake/Config/Lang.lean
+++ b/src/lake/Lake/Config/Lang.lean
@@ -3,6 +3,9 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Data.ToString.Basic
+
 namespace Lake
 
 /-- Lake configuration language identifier. -/
diff --git a/src/lake/Lake/Config/LeanConfig.lean b/src/lake/Lake/Config/LeanConfig.lean
index 464b9907f61d..6c2337c83111 100644
--- a/src/lake/Lake/Config/LeanConfig.lean
+++ b/src/lake/Lake/Config/LeanConfig.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Util.LeanOptions
 
 namespace Lake
diff --git a/src/lake/Lake/Config/LeanExe.lean b/src/lake/Lake/Config/LeanExe.lean
index dc880b08e5c6..fcef19affe04 100644
--- a/src/lake/Lake/Config/LeanExe.lean
+++ b/src/lake/Lake/Config/LeanExe.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Compiler.FFI
 import Lake.Config.Module
 
diff --git a/src/lake/Lake/Config/LeanExeConfig.lean b/src/lake/Lake/Config/LeanExeConfig.lean
index 347383c6ad79..51598dc1ec9b 100644
--- a/src/lake/Lake/Config/LeanExeConfig.lean
+++ b/src/lake/Lake/Config/LeanExeConfig.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Facets
 import Lake.Config.LeanConfig
 
diff --git a/src/lake/Lake/Config/LeanLib.lean b/src/lake/Lake/Config/LeanLib.lean
index 7a6af946ec8d..50f76f061b57 100644
--- a/src/lake/Lake/Config/LeanLib.lean
+++ b/src/lake/Lake/Config/LeanLib.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Config.Package
 
 namespace Lake
diff --git a/src/lake/Lake/Config/LeanLibConfig.lean b/src/lake/Lake/Config/LeanLibConfig.lean
index 0bae37ff3f12..7b28084bd949 100644
--- a/src/lake/Lake/Config/LeanLibConfig.lean
+++ b/src/lake/Lake/Config/LeanLibConfig.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Casing
 import Lake.Build.Facets
 import Lake.Config.InstallPath
diff --git a/src/lake/Lake/Config/Module.lean b/src/lake/Lake/Config/Module.lean
index 51e9e6a1c5b4..a0a3124e20d5 100644
--- a/src/lake/Lake/Config/Module.lean
+++ b/src/lake/Lake/Config/Module.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Trace
 import Lake.Config.LeanLib
 import Lake.Util.OrdHashSet
diff --git a/src/lake/Lake/Config/Monad.lean b/src/lake/Lake/Config/Monad.lean
index a548520a303b..8f426c846e88 100644
--- a/src/lake/Lake/Config/Monad.lean
+++ b/src/lake/Lake/Config/Monad.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Config.Context
 import Lake.Config.Workspace
 
diff --git a/src/lake/Lake/Config/Opaque.lean b/src/lake/Lake/Config/Opaque.lean
index 9f3e2eba19de..bcf5c32c3a1f 100644
--- a/src/lake/Lake/Config/Opaque.lean
+++ b/src/lake/Lake/Config/Opaque.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Name
 import Lake.Util.Opaque
 
diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean
index 16498576bf9a..4bbdec2886c0 100644
--- a/src/lake/Lake/Config/Package.lean
+++ b/src/lake/Lake/Config/Package.lean
@@ -3,6 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
+prelude
 import Lake.Config.Opaque
 import Lake.Config.Defaults
 import Lake.Config.LeanLibConfig
diff --git a/src/lake/Lake/Config/Script.lean b/src/lake/Lake/Config/Script.lean
index b80f37a6696a..becd5ecf3728 100644
--- a/src/lake/Lake/Config/Script.lean
+++ b/src/lake/Lake/Config/Script.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Exit
 import Lake.Config.Context
 
diff --git a/src/lake/Lake/Config/TargetConfig.lean b/src/lake/Lake/Config/TargetConfig.lean
index db754244e260..4169990b40c9 100644
--- a/src/lake/Lake/Config/TargetConfig.lean
+++ b/src/lake/Lake/Config/TargetConfig.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Build.Fetch
 
 namespace Lake
diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean
index 29638b2c9df5..eddf6dba5964 100644
--- a/src/lake/Lake/Config/Workspace.lean
+++ b/src/lake/Lake/Config/Workspace.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Util.Paths
 import Lake.Config.FacetConfig
 import Lake.Config.TargetConfig
diff --git a/src/lake/Lake/Config/WorkspaceConfig.lean b/src/lake/Lake/Config/WorkspaceConfig.lean
index b5250d953672..cd4d16b54b0e 100644
--- a/src/lake/Lake/Config/WorkspaceConfig.lean
+++ b/src/lake/Lake/Config/WorkspaceConfig.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Config.Defaults
 
 open System
diff --git a/src/lake/Lake/DSL.lean b/src/lake/Lake/DSL.lean
index ec4003ad61bc..4240392b199e 100644
--- a/src/lake/Lake/DSL.lean
+++ b/src/lake/Lake/DSL.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.DSL.DeclUtil
 import Lake.DSL.Attributes
 import Lake.DSL.Extensions
diff --git a/src/lake/Lake/DSL/Attributes.lean b/src/lake/Lake/DSL/Attributes.lean
index 7c89acd56cb8..ad9ef0e3e5fb 100644
--- a/src/lake/Lake/DSL/Attributes.lean
+++ b/src/lake/Lake/DSL/Attributes.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.DSL.AttributesCore
 
 open Lean
diff --git a/src/lake/Lake/DSL/AttributesCore.lean b/src/lake/Lake/DSL/AttributesCore.lean
index ad5a00878c30..89784b9eeb7b 100644
--- a/src/lake/Lake/DSL/AttributesCore.lean
+++ b/src/lake/Lake/DSL/AttributesCore.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.OrderedTagAttribute
 
 open Lean
diff --git a/src/lake/Lake/DSL/Config.lean b/src/lake/Lake/DSL/Config.lean
index 1ea682f2b70d..20c9bd8ccb83 100644
--- a/src/lake/Lake/DSL/Config.lean
+++ b/src/lake/Lake/DSL/Config.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Elab.ElabRules
 import Lake.DSL.Extensions
 
diff --git a/src/lake/Lake/DSL/DeclUtil.lean b/src/lake/Lake/DSL/DeclUtil.lean
index ce098a62d9b4..6bff854c2f6f 100644
--- a/src/lake/Lake/DSL/DeclUtil.lean
+++ b/src/lake/Lake/DSL/DeclUtil.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.DSL.Config
 import Lake.Util.Binder
 import Lake.Util.Name
diff --git a/src/lake/Lake/DSL/Extensions.lean b/src/lake/Lake/DSL/Extensions.lean
index 453f840009c3..150805a4f9e4 100644
--- a/src/lake/Lake/DSL/Extensions.lean
+++ b/src/lake/Lake/DSL/Extensions.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Environment
 
 open Lean
diff --git a/src/lake/Lake/DSL/Meta.lean b/src/lake/Lake/DSL/Meta.lean
index 91cb3540bddf..8251cf7bde73 100644
--- a/src/lake/Lake/DSL/Meta.lean
+++ b/src/lake/Lake/DSL/Meta.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Elab.Eval
 import Lean.Elab.ElabRules
 import Lake.Util.FilePath
diff --git a/src/lake/Lake/DSL/Package.lean b/src/lake/Lake/DSL/Package.lean
index 25c42390d463..ac51c26fdf16 100644
--- a/src/lake/Lake/DSL/Package.lean
+++ b/src/lake/Lake/DSL/Package.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Config.Package
 import Lake.DSL.Attributes
 import Lake.DSL.DeclUtil
diff --git a/src/lake/Lake/DSL/Require.lean b/src/lake/Lake/DSL/Require.lean
index 76a0dd4ca04c..7fec264f741d 100644
--- a/src/lake/Lake/DSL/Require.lean
+++ b/src/lake/Lake/DSL/Require.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Parser.Command
 import Lake.Config.Dependency
 import Lake.DSL.Extensions
diff --git a/src/lake/Lake/DSL/Script.lean b/src/lake/Lake/DSL/Script.lean
index 9eb3f9417e80..9565f0cf88cf 100644
--- a/src/lake/Lake/DSL/Script.lean
+++ b/src/lake/Lake/DSL/Script.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Config.Package
 import Lake.DSL.Attributes
 import Lake.DSL.DeclUtil
diff --git a/src/lake/Lake/DSL/Targets.lean b/src/lake/Lake/DSL/Targets.lean
index 650ae2207062..c8c4bc36920c 100644
--- a/src/lake/Lake/DSL/Targets.lean
+++ b/src/lake/Lake/DSL/Targets.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.DSL.DeclUtil
 import Lake.Build.Index
 
diff --git a/src/lake/Lake/Load.lean b/src/lake/Lake/Load.lean
index 9b71d35bb7c7..bfc557c1af95 100644
--- a/src/lake/Lake/Load.lean
+++ b/src/lake/Lake/Load.lean
@@ -3,4 +3,5 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Load.Workspace
diff --git a/src/lake/Lake/Load/Config.lean b/src/lake/Lake/Load/Config.lean
index d5929bf8cd4b..f9027af7fe68 100644
--- a/src/lake/Lake/Load/Config.lean
+++ b/src/lake/Lake/Load/Config.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Data.Name
 import Lean.Data.Options
 import Lake.Config.Defaults
diff --git a/src/lake/Lake/Load/Lean.lean b/src/lake/Lake/Load/Lean.lean
index 08aab790c347..c95e6a24e3b8 100644
--- a/src/lake/Lake/Load/Lean.lean
+++ b/src/lake/Lake/Load/Lean.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Load.Lean.Elab
 import Lake.Load.Lean.Eval
 
diff --git a/src/lake/Lake/Load/Lean/Elab.lean b/src/lake/Lake/Load/Lean/Elab.lean
index 20d5334464cb..c83fe093df16 100644
--- a/src/lake/Lake/Load/Lean/Elab.lean
+++ b/src/lake/Lake/Load/Lean/Elab.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Elab.Frontend
 import Lake.DSL.Extensions
 import Lake.DSL.Attributes
diff --git a/src/lake/Lake/Load/Lean/Eval.lean b/src/lake/Lake/Load/Lean/Eval.lean
index 67ed546e412b..244ae86c8213 100644
--- a/src/lake/Lake/Load/Lean/Eval.lean
+++ b/src/lake/Lake/Load/Lean/Eval.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.DSL.Attributes
 import Lake.Config.Workspace
 import Lean.DocString
diff --git a/src/lake/Lake/Load/Manifest.lean b/src/lake/Lake/Load/Manifest.lean
index 3aa23a7c0044..f15b70f781d5 100644
--- a/src/lake/Lake/Load/Manifest.lean
+++ b/src/lake/Lake/Load/Manifest.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone, Gabriel Ebner
 -/
+prelude
 import Lake.Util.Log
 import Lake.Util.Name
 import Lake.Util.FilePath
diff --git a/src/lake/Lake/Load/Materialize.lean b/src/lake/Lake/Load/Materialize.lean
index b8a7268082a4..c3c514dcbff3 100644
--- a/src/lake/Lake/Load/Materialize.lean
+++ b/src/lake/Lake/Load/Materialize.lean
@@ -3,6 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
+prelude
 import Lake.Util.Git
 import Lake.Load.Manifest
 import Lake.Config.Dependency
diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean
index fc6b970ee1a6..173bc972ba10 100644
--- a/src/lake/Lake/Load/Package.lean
+++ b/src/lake/Lake/Load/Package.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Load.Lean
 import Lake.Load.Toml
 
diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean
index 9d4888aae026..f52d06b01330 100644
--- a/src/lake/Lake/Load/Resolve.lean
+++ b/src/lake/Lake/Load/Resolve.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone, Gabriel Ebner
 -/
+prelude
 import Lake.Config.Monad
 import Lake.Util.StoreInsts
 import Lake.Build.Topological
diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean
index 59955be78855..ce0271df81a1 100644
--- a/src/lake/Lake/Load/Toml.lean
+++ b/src/lake/Lake/Load/Toml.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Toml.Load
 import Lake.Toml.Decode
 import Lake.Config.Package
diff --git a/src/lake/Lake/Load/Workspace.lean b/src/lake/Lake/Load/Workspace.lean
index c17adecbc17a..32d2a84cae30 100644
--- a/src/lake/Lake/Load/Workspace.lean
+++ b/src/lake/Lake/Load/Workspace.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Load.Resolve
 import Lake.Build.Module
 import Lake.Build.Package
diff --git a/src/lake/Lake/Reservoir.lean b/src/lake/Lake/Reservoir.lean
index 2ed295344164..8ebfc93213cb 100644
--- a/src/lake/Lake/Reservoir.lean
+++ b/src/lake/Lake/Reservoir.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Log
 import Lake.Util.Proc
 import Lake.Util.JsonObject
diff --git a/src/lake/Lake/Toml.lean b/src/lake/Lake/Toml.lean
index df3e653e59d7..1fb1f0a4e690 100644
--- a/src/lake/Lake/Toml.lean
+++ b/src/lake/Lake/Toml.lean
@@ -3,4 +3,5 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Toml.Load
diff --git a/src/lake/Lake/Toml/Data.lean b/src/lake/Lake/Toml/Data.lean
index 04ef0bc18185..f97a045e9dea 100644
--- a/src/lake/Lake/Toml/Data.lean
+++ b/src/lake/Lake/Toml/Data.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Toml.Data.Value
 
 /-!
diff --git a/src/lake/Lake/Toml/Data/DateTime.lean b/src/lake/Lake/Toml/Data/DateTime.lean
index 4b4c9a7b3856..da77dae5c984 100644
--- a/src/lake/Lake/Toml/Data/DateTime.lean
+++ b/src/lake/Lake/Toml/Data/DateTime.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Date
 
 /-!
diff --git a/src/lake/Lake/Toml/Data/Dict.lean b/src/lake/Lake/Toml/Data/Dict.lean
index de40e3163bed..ae5476f55cd8 100644
--- a/src/lake/Lake/Toml/Data/Dict.lean
+++ b/src/lake/Lake/Toml/Data/Dict.lean
@@ -3,7 +3,9 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Data.NameMap
+import Init.Data.Nat.Fold
 
 /-! # Red-Black Dictionary
 
@@ -33,11 +35,10 @@ instance : EmptyCollection (RBDict α β cmp) := ⟨RBDict.empty⟩
 def mkEmpty (capacity : Nat) : RBDict α β cmp :=
   {items := .mkEmpty capacity, indices := {}}
 
-def ofArray (items : Array (α × β)) : RBDict α β cmp := Id.run do
-  let mut indices := mkRBMap α Nat cmp
-  for h : i in [0:items.size] do
-    indices := indices.insert items[i].1 i
-  return {items, indices}
+def ofArray (items : Array (α × β)) : RBDict α β cmp :=
+  let indices := items.size.fold (init := mkRBMap α Nat cmp) fun i _ indices =>
+    indices.insert items[i].1 i
+  {items, indices}
 
 protected def beq [BEq (α × β)] (self other : RBDict α β cmp) : Bool :=
   self.items == other.items
diff --git a/src/lake/Lake/Toml/Data/Value.lean b/src/lake/Lake/Toml/Data/Value.lean
index be64ef8d875d..b76ed30cf8c1 100644
--- a/src/lake/Lake/Toml/Data/Value.lean
+++ b/src/lake/Lake/Toml/Data/Value.lean
@@ -3,6 +3,8 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Data.Float
 import Lake.Toml.Data.Dict
 import Lake.Toml.Data.DateTime
 
diff --git a/src/lake/Lake/Toml/Decode.lean b/src/lake/Lake/Toml/Decode.lean
index 309db6f697a4..1d2e1b46cd64 100644
--- a/src/lake/Lake/Toml/Decode.lean
+++ b/src/lake/Lake/Toml/Decode.lean
@@ -3,6 +3,8 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.System.FilePath
 import Lake.Toml.Data
 
 /-!
diff --git a/src/lake/Lake/Toml/Elab.lean b/src/lake/Lake/Toml/Elab.lean
index 7403d606e1b4..e953ee92ebb1 100644
--- a/src/lake/Lake/Toml/Elab.lean
+++ b/src/lake/Lake/Toml/Elab.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Toml.Elab.Expression
 
 /-!
diff --git a/src/lake/Lake/Toml/Elab/Expression.lean b/src/lake/Lake/Toml/Elab/Expression.lean
index 081a0b668423..9f13942f8975 100644
--- a/src/lake/Lake/Toml/Elab/Expression.lean
+++ b/src/lake/Lake/Toml/Elab/Expression.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Toml.Elab.Value
 
 /-!
diff --git a/src/lake/Lake/Toml/Elab/Value.lean b/src/lake/Lake/Toml/Elab/Value.lean
index 7ba4a9085f15..7970ff7fa6f0 100644
--- a/src/lake/Lake/Toml/Elab/Value.lean
+++ b/src/lake/Lake/Toml/Elab/Value.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.CoreM
 import Lake.Toml.Data.Value
 import Lake.Toml.Grammar
diff --git a/src/lake/Lake/Toml/Encode.lean b/src/lake/Lake/Toml/Encode.lean
index a3fde0ed4ead..e3e425df43c0 100644
--- a/src/lake/Lake/Toml/Encode.lean
+++ b/src/lake/Lake/Toml/Encode.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Toml.Data
 import Lake.Util.FilePath
 
diff --git a/src/lake/Lake/Toml/Grammar.lean b/src/lake/Lake/Toml/Grammar.lean
index 349d985bb206..805976e38a62 100644
--- a/src/lake/Lake/Toml/Grammar.lean
+++ b/src/lake/Lake/Toml/Grammar.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Toml.ParserUtil
 
 /-!
diff --git a/src/lake/Lake/Toml/Load.lean b/src/lake/Lake/Toml/Load.lean
index 919ff4e6941b..c5c518fae112 100644
--- a/src/lake/Lake/Toml/Load.lean
+++ b/src/lake/Lake/Toml/Load.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Toml.Elab
 import Lake.Util.Message
 
diff --git a/src/lake/Lake/Toml/ParserUtil.lean b/src/lake/Lake/Toml/ParserUtil.lean
index de874dc03549..b92cc1e42f18 100644
--- a/src/lake/Lake/Toml/ParserUtil.lean
+++ b/src/lake/Lake/Toml/ParserUtil.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Parser
 import Lean.PrettyPrinter.Formatter
 
diff --git a/src/lake/Lake/Util/Binder.lean b/src/lake/Lake/Util/Binder.lean
index 21adec6e6a0f..5ccc90bb6815 100644
--- a/src/lake/Lake/Util/Binder.lean
+++ b/src/lake/Lake/Util/Binder.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Parser.Term
 import Lean.Elab.Term
 import Lean.Expr
diff --git a/src/lake/Lake/Util/Casing.lean b/src/lake/Lake/Util/Casing.lean
index 662c339f6113..56be3909213d 100644
--- a/src/lake/Lake/Util/Casing.lean
+++ b/src/lake/Lake/Util/Casing.lean
@@ -3,7 +3,11 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Data.String.Basic
+
 namespace Lake
+
 open Lean (Name)
 
 /-- Converts a snake case, kebab case, or lower camel case `String` to upper camel case. -/
diff --git a/src/lake/Lake/Util/Cli.lean b/src/lake/Lake/Util/Cli.lean
index 4b8e5782b713..bb63bf9b00f0 100644
--- a/src/lake/Lake/Util/Cli.lean
+++ b/src/lake/Lake/Util/Cli.lean
@@ -3,6 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Data.Array.Basic
 
 namespace Lake
 
@@ -75,8 +77,18 @@ variable [Monad m] [MonadStateOf ArgList m]
 
 /-- Process a multiple short options grouped together (ex. `-xyz` as `x`, `y`, `z`). -/
 @[inline] def multiShortOption (handle : Char → m PUnit) (opt : String) : m PUnit := do
-  -- TODO: this code is assuming all characters are ASCII.
-  for i in [1:opt.length] do handle (opt.get ⟨i⟩)
+  let rec loop (p : String.Pos) := do
+    if h : opt.atEnd p then
+      return
+    else
+      handle (opt.get' p h)
+      loop (opt.next' p h)
+  termination_by opt.utf8ByteSize - p.byteIdx
+  decreasing_by
+    simp [String.atEnd] at h
+    apply Nat.sub_lt_sub_left h
+    simp [String.lt_next opt p]
+  loop ⟨1⟩
 
 /-- Splits a long option of the form `"--long foo bar"` into `--long` and `"foo bar"`. -/
 @[inline] def longOptionOrSpace (handle : String → m α) (opt : String) : m α :=
@@ -102,8 +114,9 @@ variable [Monad m] [MonadStateOf ArgList m]
 
 /-- Process a short option of the form `-x`, `-x=arg`, `-x arg`, or `-long`. -/
 @[inline] def shortOption
-(shortHandle : Char → m α) (longHandle : String → m α)
-(opt : String) : m α :=
+  (shortHandle : Char → m α) (longHandle : String → m α)
+  (opt : String)
+: m α :=
   if opt.length == 2 then -- `-x`
     shortHandle (opt.get ⟨1⟩)
   else -- `-c(.+)`
@@ -151,7 +164,9 @@ partial def processLeadingOptions (handle : String → m PUnit) : m PUnit := do
       processLeadingOptions handle
 
 /-- Process every option and collect the remaining arguments into an `Array`. -/
-partial def collectArgs (option : String → m PUnit) (args : Array String := #[]) : m (Array String) := do
+partial def collectArgs
+  (option : String → m PUnit) (args : Array String := #[])
+: m (Array String) := do
   if let some arg ← takeArg? then
     let len := arg.length
     if len > 1 && arg.get 0 == '-' then -- `-(.+)`
diff --git a/src/lake/Lake/Util/Compare.lean b/src/lake/Lake/Util/Compare.lean
index 8dec7bb51195..c26a11846a85 100644
--- a/src/lake/Lake/Util/Compare.lean
+++ b/src/lake/Lake/Util/Compare.lean
@@ -3,6 +3,8 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Data.Ord
 
 namespace Lake
 
diff --git a/src/lake/Lake/Util/Cycle.lean b/src/lake/Lake/Util/Cycle.lean
index 7187f2a111ab..9f308244186a 100644
--- a/src/lake/Lake/Util/Cycle.lean
+++ b/src/lake/Lake/Util/Cycle.lean
@@ -3,6 +3,9 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Control.Except
+import Init.Data.List.Basic
 
 namespace Lake
 
diff --git a/src/lake/Lake/Util/DRBMap.lean b/src/lake/Lake/Util/DRBMap.lean
index 722f44e513fd..3451ff161471 100644
--- a/src/lake/Lake/Util/DRBMap.lean
+++ b/src/lake/Lake/Util/DRBMap.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mac Malone
 -/
+prelude
 import Lean.Data.RBMap
 import Lake.Util.Compare
 
diff --git a/src/lake/Lake/Util/Date.lean b/src/lake/Lake/Util/Date.lean
index e49a21def12c..2775bcf5d26a 100644
--- a/src/lake/Lake/Util/Date.lean
+++ b/src/lake/Lake/Util/Date.lean
@@ -3,6 +3,8 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Data.Ord
 
 /-!
 #  Date
diff --git a/src/lake/Lake/Util/EStateT.lean b/src/lake/Lake/Util/EStateT.lean
index 36bc5eab9498..5fcf982b4c65 100644
--- a/src/lake/Lake/Util/EStateT.lean
+++ b/src/lake/Lake/Util/EStateT.lean
@@ -3,6 +3,8 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone, Leonardo de Moura, Mario Carneiro
 -/
+prelude
+import Init.Control.State
 
 namespace Lake
 
diff --git a/src/lake/Lake/Util/EquipT.lean b/src/lake/Lake/Util/EquipT.lean
index 59e27b1a2e4c..972c2c670ae2 100644
--- a/src/lake/Lake/Util/EquipT.lean
+++ b/src/lake/Lake/Util/EquipT.lean
@@ -3,6 +3,9 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Control.Except
+
 namespace Lake
 
 /--
diff --git a/src/lake/Lake/Util/Error.lean b/src/lake/Lake/Util/Error.lean
index 127242eceab9..0fac5a62639e 100644
--- a/src/lake/Lake/Util/Error.lean
+++ b/src/lake/Lake/Util/Error.lean
@@ -3,6 +3,9 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.System.IO
+
 namespace Lake
 
 class MonadError (m : Type u → Type v) where
diff --git a/src/lake/Lake/Util/Exit.lean b/src/lake/Lake/Util/Exit.lean
index 2ce22f9a23bf..9f3cad4769a6 100644
--- a/src/lake/Lake/Util/Exit.lean
+++ b/src/lake/Lake/Util/Exit.lean
@@ -3,6 +3,9 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Data.UInt.Basic
+
 namespace Lake
 
 /-- A process exit / return code. -/
diff --git a/src/lake/Lake/Util/Family.lean b/src/lake/Lake/Util/Family.lean
index 9418b4a196ac..e62d72c8c670 100644
--- a/src/lake/Lake/Util/Family.lean
+++ b/src/lake/Lake/Util/Family.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Parser.Command
 
 /-!
diff --git a/src/lake/Lake/Util/FilePath.lean b/src/lake/Lake/Util/FilePath.lean
index f4fa96a9d01f..6a4a5d103230 100644
--- a/src/lake/Lake/Util/FilePath.lean
+++ b/src/lake/Lake/Util/FilePath.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
-import Lean.ToExpr
+prelude
 import Lean.Data.Json
 
 open System Lean
diff --git a/src/lake/Lake/Util/Git.lean b/src/lake/Lake/Util/Git.lean
index cc365d053f05..53971647b813 100644
--- a/src/lake/Lake/Util/Git.lean
+++ b/src/lake/Lake/Util/Git.lean
@@ -3,6 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
+prelude
 import Lake.Util.Proc
 import Lake.Util.Lift
 
diff --git a/src/lake/Lake/Util/IO.lean b/src/lake/Lake/Util/IO.lean
index 7fae188e340b..d38c06c7e915 100644
--- a/src/lake/Lake/Util/IO.lean
+++ b/src/lake/Lake/Util/IO.lean
@@ -3,6 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.System.IO
 
 namespace Lake
 
diff --git a/src/lake/Lake/Util/JsonObject.lean b/src/lake/Lake/Util/JsonObject.lean
index 48fb2a5d6134..38af63fdb8a5 100644
--- a/src/lake/Lake/Util/JsonObject.lean
+++ b/src/lake/Lake/Util/JsonObject.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Data.Json
 
 open Lean
diff --git a/src/lake/Lake/Util/Lift.lean b/src/lake/Lake/Util/Lift.lean
index 7dd0a21f83f3..0e9c79de33ba 100644
--- a/src/lake/Lake/Util/Lift.lean
+++ b/src/lake/Lake/Util/Lift.lean
@@ -3,6 +3,10 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.System.IO
+import Init.Control.Option
+
 namespace Lake
 
 instance (priority := low) [Monad m] [MonadExceptOf PUnit m] : Alternative m where
diff --git a/src/lake/Lake/Util/List.lean b/src/lake/Lake/Util/List.lean
index 807082562819..ec0aae369a63 100644
--- a/src/lake/Lake/Util/List.lean
+++ b/src/lake/Lake/Util/List.lean
@@ -3,8 +3,8 @@ Copyright (c) 2023 Siddharth Bhat. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddharth Bhat
 -/
-
-open Lean
+prelude
+import Init.Data.List.Notation
 
 namespace Lake
 
@@ -15,5 +15,3 @@ def List.squeeze [BEq α] : List α → List α
   match List.squeeze xs with
   | [] => [x]
   | x' :: xs' => if x == x' then x' :: xs' else x :: x' :: xs'
-
-end Lake
diff --git a/src/lake/Lake/Util/Lock.lean b/src/lake/Lake/Util/Lock.lean
index 576e2e1c8d8f..3af80b2eaf78 100644
--- a/src/lake/Lake/Util/Lock.lean
+++ b/src/lake/Lake/Util/Lock.lean
@@ -3,6 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone, Gabriel Ebner, Sebastian Ullrich
 -/
+prelude
+import Init.System.IO
 
 /-! # Lock File Utilities
 
diff --git a/src/lake/Lake/Util/Log.lean b/src/lake/Lake/Util/Log.lean
index 8ed7f1123ce2..cb08f050d9bc 100644
--- a/src/lake/Lake/Util/Log.lean
+++ b/src/lake/Lake/Util/Log.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Error
 import Lake.Util.EStateT
 import Lake.Util.Lift
diff --git a/src/lake/Lake/Util/MainM.lean b/src/lake/Lake/Util/MainM.lean
index 24dcea7a0717..82582af71435 100644
--- a/src/lake/Lake/Util/MainM.lean
+++ b/src/lake/Lake/Util/MainM.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Log
 import Lake.Util.Exit
 import Lake.Util.Error
diff --git a/src/lake/Lake/Util/Message.lean b/src/lake/Lake/Util/Message.lean
index 0d7847fa6c98..a5954dfdaf69 100644
--- a/src/lake/Lake/Util/Message.lean
+++ b/src/lake/Lake/Util/Message.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Message
 import Lean.Exception
 import Lean.Parser.Basic
diff --git a/src/lake/Lake/Util/Name.lean b/src/lake/Lake/Util/Name.lean
index cfbd05f98d75..4c4c5e198ee0 100644
--- a/src/lake/Lake/Util/Name.lean
+++ b/src/lake/Lake/Util/Name.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Data.Json
 import Lean.Data.NameMap
 import Lake.Util.DRBMap
diff --git a/src/lake/Lake/Util/NativeLib.lean b/src/lake/Lake/Util/NativeLib.lean
index 672c3337485a..abdf6bd4412e 100644
--- a/src/lake/Lake/Util/NativeLib.lean
+++ b/src/lake/Lake/Util/NativeLib.lean
@@ -3,6 +3,8 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.System.IO
 
 open System
 namespace Lake
diff --git a/src/lake/Lake/Util/Opaque.lean b/src/lake/Lake/Util/Opaque.lean
index 9905ab59548b..f4f857cff85c 100644
--- a/src/lake/Lake/Util/Opaque.lean
+++ b/src/lake/Lake/Util/Opaque.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.Binder
 import Lean.Parser.Command
 
diff --git a/src/lake/Lake/Util/OrdHashSet.lean b/src/lake/Lake/Util/OrdHashSet.lean
index 003af356e14b..713813b7187c 100644
--- a/src/lake/Lake/Util/OrdHashSet.lean
+++ b/src/lake/Lake/Util/OrdHashSet.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Data.HashSet
 import Std.Data.HashSet.Basic
 
diff --git a/src/lake/Lake/Util/OrderedTagAttribute.lean b/src/lake/Lake/Util/OrderedTagAttribute.lean
index a486a380a28f..1e2ca66973aa 100644
--- a/src/lake/Lake/Util/OrderedTagAttribute.lean
+++ b/src/lake/Lake/Util/OrderedTagAttribute.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
+prelude
 import Lean.Attributes
 
 open Lean
diff --git a/src/lake/Lake/Util/Proc.lean b/src/lake/Lake/Util/Proc.lean
index 89cc5989eb64..eb0a86a3e5e0 100644
--- a/src/lake/Lake/Util/Proc.lean
+++ b/src/lake/Lake/Util/Proc.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
+prelude
 import Lake.Util.Log
 
 namespace Lake
diff --git a/src/lake/Lake/Util/RBArray.lean b/src/lake/Lake/Util/RBArray.lean
index 3794801f6c91..287e0fd4a46d 100644
--- a/src/lake/Lake/Util/RBArray.lean
+++ b/src/lake/Lake/Util/RBArray.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Data.RBMap
 
 namespace Lake
diff --git a/src/lake/Lake/Util/Store.lean b/src/lake/Lake/Util/Store.lean
index 123ea39296c4..446c34cb69f0 100644
--- a/src/lake/Lake/Util/Store.lean
+++ b/src/lake/Lake/Util/Store.lean
@@ -3,6 +3,9 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Notation
+
 namespace Lake
 
 /-- A monad equipped with a dependently typed key-value store for a particular key. -/
diff --git a/src/lake/Lake/Util/StoreInsts.lean b/src/lake/Lake/Util/StoreInsts.lean
index 05fb57090126..5ee67d98570d 100644
--- a/src/lake/Lake/Util/StoreInsts.lean
+++ b/src/lake/Lake/Util/StoreInsts.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lake.Util.DRBMap
 import Lake.Util.RBArray
 import Lake.Util.Family
diff --git a/src/lake/Lake/Util/Sugar.lean b/src/lake/Lake/Util/Sugar.lean
index 842c3977f22b..52db1339bf47 100644
--- a/src/lake/Lake/Util/Sugar.lean
+++ b/src/lake/Lake/Util/Sugar.lean
@@ -3,6 +3,9 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Notation
+
 namespace Lake
 
 macro "try " x:term " else " y:term : term =>
diff --git a/src/lake/Lake/Util/Task.lean b/src/lake/Lake/Util/Task.lean
index c986852fd11f..afe7a137e71c 100644
--- a/src/lake/Lake/Util/Task.lean
+++ b/src/lake/Lake/Util/Task.lean
@@ -3,6 +3,9 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Control.Option
+
 namespace Lake
 
 instance : Monad Task where
diff --git a/src/lake/Lake/Util/Version.lean b/src/lake/Lake/Util/Version.lean
index 8c16fec1e853..c3ca84018433 100644
--- a/src/lake/Lake/Util/Version.lean
+++ b/src/lake/Lake/Util/Version.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
 import Lean.Elab.Eval
 import Lake.Util.Date
 
diff --git a/src/lake/Lake/Version.lean b/src/lake/Lake/Version.lean
index 05b856e438f5..dba5c6c4dade 100644
--- a/src/lake/Lake/Version.lean
+++ b/src/lake/Lake/Version.lean
@@ -3,6 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+prelude
+import Init.Data.ToString
 
 namespace Lake
 
diff --git a/src/lake/LakeMain.lean b/src/lake/LakeMain.lean
index 620b9bd485f3..8fa420c697c6 100644
--- a/src/lake/LakeMain.lean
+++ b/src/lake/LakeMain.lean
@@ -3,6 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
+prelude
 import Lake
 import Lake.CLI