diff --git a/.github/workflows/check-prelude.yml b/.github/workflows/check-prelude.yml
new file mode 100644
index 0000000000..ef497467b0
--- /dev/null
+++ b/.github/workflows/check-prelude.yml
@@ -0,0 +1,26 @@
+name: Check for modules that should use `prelude`
+
+on: [pull_request]
+
+jobs:
+  check-prelude:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          # the default is to use a virtual merge commit between the PR and master: just use the PR
+          ref: ${{ github.event.pull_request.head.sha }}
+          sparse-checkout: src/Lean
+      - name: Check Prelude
+        run: |
+          failed_files=""
+          while IFS= read -r -d '' file; do
+            if ! grep -q "^prelude$" "$file"; then
+              failed_files="$failed_files$file\n"
+            fi
+          done < <(find src/Lean -name '*.lean' -print0)
+          if [ -n "$failed_files" ]; then
+            echo -e "The following files use 'prelude':\n$failed_files"
+            exit 1
+          fi
\ No newline at end of file
diff --git a/src/Lean/Elab/Tactic/NormCast.lean b/src/Lean/Elab/Tactic/NormCast.lean
index 1a63c52d99..f6bfcc97d9 100644
--- a/src/Lean/Elab/Tactic/NormCast.lean
+++ b/src/Lean/Elab/Tactic/NormCast.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Paul-Nicolas Madelaine. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
 -/
+prelude
 import Lean.Meta.Tactic.NormCast
 import Lean.Elab.Tactic.Conv.Simp
 import Lean.Elab.ElabRules
diff --git a/src/Lean/Elab/Tactic/Omega.lean b/src/Lean/Elab/Tactic/Omega.lean
index dbd52aea42..f8f6bed5e1 100644
--- a/src/Lean/Elab/Tactic/Omega.lean
+++ b/src/Lean/Elab/Tactic/Omega.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+prelude
 import Lean.Elab.Tactic.Omega.Frontend
 
 /-!
diff --git a/src/Lean/Elab/Tactic/Omega/Core.lean b/src/Lean/Elab/Tactic/Omega/Core.lean
index dc199c72f1..36c6cfb8a3 100644
--- a/src/Lean/Elab/Tactic/Omega/Core.lean
+++ b/src/Lean/Elab/Tactic/Omega/Core.lean
@@ -3,6 +3,8 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+prelude
+import Init.Omega.Constraint
 import Lean.Elab.Tactic.Omega.OmegaM
 import Lean.Elab.Tactic.Omega.MinNatAbs
 
diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean
index 79fbc206a7..0c78d70947 100644
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+prelude
 import Lean.Elab.Tactic.Omega.Core
 import Lean.Elab.Tactic.FalseOrByContra
 import Lean.Meta.Tactic.Cases
diff --git a/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean b/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean
index c569d7b564..3f97d2ecc2 100644
--- a/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean
+++ b/src/Lean/Elab/Tactic/Omega/MinNatAbs.lean
@@ -3,6 +3,10 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+prelude
+import Init.BinderPredicates
+import Init.Data.List
+import Init.Data.Option
 
 /-!
 # `List.nonzeroMinimum`, `List.minNatAbs`, `List.maxNatAbs`
diff --git a/src/Lean/Elab/Tactic/Omega/OmegaM.lean b/src/Lean/Elab/Tactic/Omega/OmegaM.lean
index bbc1908950..5397e938e3 100644
--- a/src/Lean/Elab/Tactic/Omega/OmegaM.lean
+++ b/src/Lean/Elab/Tactic/Omega/OmegaM.lean
@@ -3,6 +3,10 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
+prelude
+import Init.Omega.LinearCombo
+import Init.Omega.Int
+import Init.Omega.Logic
 import Lean.Meta.AppBuilder
 
 /-!
diff --git a/src/Lean/Elab/Tactic/SimpTrace.lean b/src/Lean/Elab/Tactic/SimpTrace.lean
index eb1f2c595f..4a0adc45da 100644
--- a/src/Lean/Elab/Tactic/SimpTrace.lean
+++ b/src/Lean/Elab/Tactic/SimpTrace.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+prelude
 import Lean.Elab.ElabRules
 import Lean.Elab.Tactic.Simp
 import Lean.Meta.Tactic.TryThis
diff --git a/src/Lean/Elab/Tactic/Simpa.lean b/src/Lean/Elab/Tactic/Simpa.lean
index 267f8a7fa9..79d441460d 100644
--- a/src/Lean/Elab/Tactic/Simpa.lean
+++ b/src/Lean/Elab/Tactic/Simpa.lean
@@ -3,6 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino, Gabriel Ebner, Mario Carneiro
 -/
+prelude
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.TryThis
 import Lean.Elab.Tactic.Simp
diff --git a/src/Lean/Meta/CompletionName.lean b/src/Lean/Meta/CompletionName.lean
index ef2a96c3de..c83e33f5b3 100644
--- a/src/Lean/Meta/CompletionName.lean
+++ b/src/Lean/Meta/CompletionName.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-
+prelude
 import Lean.Meta.Basic
 import Lean.Meta.Match.MatcherInfo
 
diff --git a/src/Lean/Meta/Tactic/NormCast.lean b/src/Lean/Meta/Tactic/NormCast.lean
index b6d3bf76b9..c0cc81cf22 100644
--- a/src/Lean/Meta/Tactic/NormCast.lean
+++ b/src/Lean/Meta/Tactic/NormCast.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Paul-Nicolas Madelaine. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
 -/
+prelude
 import Lean.Meta.CongrTheorems
 import Lean.Meta.Tactic.Simp.SimpTheorems
 import Lean.Meta.CoeAttr
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean
index 211ddac2aa..b05242b891 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.ToExpr
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
 
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean
index 6c94b0b516..72eba30ff1 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+prelude
 import Lean.ToExpr
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char