diff --git a/.github/workflows/check-prelude.yml b/.github/workflows/check-prelude.yml
index 5c4f2ab54d9c..049aad9b2439 100644
--- a/.github/workflows/check-prelude.yml
+++ b/.github/workflows/check-prelude.yml
@@ -11,7 +11,9 @@ jobs:
         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
+          sparse-checkout: |
+            src/Lean
+            src/Std
       - name: Check Prelude
         run: |
           failed_files=""
@@ -19,8 +21,8 @@ jobs:
             if ! grep -q "^prelude$" "$file"; then
               failed_files="$failed_files$file\n"
             fi
-          done < <(find src/Lean -name '*.lean' -print0)
+          done < <(find src/Lean src/Std -name '*.lean' -print0)
           if [ -n "$failed_files" ]; then
             echo -e "The following files should use 'prelude':\n$failed_files"
             exit 1
-          fi
\ No newline at end of file
+          fi
diff --git a/src/Std/Sat/AIG.lean b/src/Std/Sat/AIG.lean
index f835d56631c1..c2889442e1fb 100644
--- a/src/Std/Sat/AIG.lean
+++ b/src/Std/Sat/AIG.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.LawfulOperator
 import Std.Sat.AIG.Lemmas
diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean
index 2cdcbb2d9747..86c06caebf79 100644
--- a/src/Std/Sat/AIG/Basic.lean
+++ b/src/Std/Sat/AIG/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Data.HashMap
 import Std.Data.HashSet
 
diff --git a/src/Std/Sat/AIG/CNF.lean b/src/Std/Sat/AIG/CNF.lean
index 7e7c9d7696ea..c81f3dee528e 100644
--- a/src/Std/Sat/AIG/CNF.lean
+++ b/src/Std/Sat/AIG/CNF.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.CNF
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.Lemmas
diff --git a/src/Std/Sat/AIG/Cached.lean b/src/Std/Sat/AIG/Cached.lean
index 542130d97db2..18b9d30e56e9 100644
--- a/src/Std/Sat/AIG/Cached.lean
+++ b/src/Std/Sat/AIG/Cached.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.Lemmas
 
diff --git a/src/Std/Sat/AIG/CachedGates.lean b/src/Std/Sat/AIG/CachedGates.lean
index b81c0f1e1f41..ab846563d1ea 100644
--- a/src/Std/Sat/AIG/CachedGates.lean
+++ b/src/Std/Sat/AIG/CachedGates.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Cached
 import Std.Sat.AIG.CachedLemmas
 
diff --git a/src/Std/Sat/AIG/CachedGatesLemmas.lean b/src/Std/Sat/AIG/CachedGatesLemmas.lean
index 17f53957a152..f17df1aa34f7 100644
--- a/src/Std/Sat/AIG/CachedGatesLemmas.lean
+++ b/src/Std/Sat/AIG/CachedGatesLemmas.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.CachedGates
 import Std.Sat.AIG.LawfulOperator
 
diff --git a/src/Std/Sat/AIG/CachedLemmas.lean b/src/Std/Sat/AIG/CachedLemmas.lean
index ca95c15d3eac..29d518404866 100644
--- a/src/Std/Sat/AIG/CachedLemmas.lean
+++ b/src/Std/Sat/AIG/CachedLemmas.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Cached
 
 /-!
diff --git a/src/Std/Sat/AIG/If.lean b/src/Std/Sat/AIG/If.lean
index 201a8a994d86..0e1ec1810c37 100644
--- a/src/Std/Sat/AIG/If.lean
+++ b/src/Std/Sat/AIG/If.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.CachedGatesLemmas
 import Std.Sat.AIG.LawfulVecOperator
 
diff --git a/src/Std/Sat/AIG/LawfulOperator.lean b/src/Std/Sat/AIG/LawfulOperator.lean
index 2de496c571b8..f7bd85297ede 100644
--- a/src/Std/Sat/AIG/LawfulOperator.lean
+++ b/src/Std/Sat/AIG/LawfulOperator.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Basic
 
 /-!
diff --git a/src/Std/Sat/AIG/LawfulVecOperator.lean b/src/Std/Sat/AIG/LawfulVecOperator.lean
index 400765617511..f0f02301dcef 100644
--- a/src/Std/Sat/AIG/LawfulVecOperator.lean
+++ b/src/Std/Sat/AIG/LawfulVecOperator.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.LawfulOperator
 import Std.Sat.AIG.RefVec
 
diff --git a/src/Std/Sat/AIG/Lemmas.lean b/src/Std/Sat/AIG/Lemmas.lean
index d988d6ff19ac..afde41c6dae7 100644
--- a/src/Std/Sat/AIG/Lemmas.lean
+++ b/src/Std/Sat/AIG/Lemmas.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.LawfulOperator
 
diff --git a/src/Std/Sat/AIG/RefVec.lean b/src/Std/Sat/AIG/RefVec.lean
index 0d1099fc435a..4f02242ddeb0 100644
--- a/src/Std/Sat/AIG/RefVec.lean
+++ b/src/Std/Sat/AIG/RefVec.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.LawfulOperator
 import Std.Sat.AIG.CachedGatesLemmas
 
diff --git a/src/Std/Sat/AIG/RefVecOperator.lean b/src/Std/Sat/AIG/RefVecOperator.lean
index 611f5c6a0ebb..18ed5286f88f 100644
--- a/src/Std/Sat/AIG/RefVecOperator.lean
+++ b/src/Std/Sat/AIG/RefVecOperator.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.RefVecOperator.Map
 import Std.Sat.AIG.RefVecOperator.Zip
 import Std.Sat.AIG.RefVecOperator.Fold
diff --git a/src/Std/Sat/AIG/RefVecOperator/Fold.lean b/src/Std/Sat/AIG/RefVecOperator/Fold.lean
index b51cbcd3a804..19206d208c02 100644
--- a/src/Std/Sat/AIG/RefVecOperator/Fold.lean
+++ b/src/Std/Sat/AIG/RefVecOperator/Fold.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.RefVec
 import Std.Sat.AIG.LawfulVecOperator
 
diff --git a/src/Std/Sat/AIG/RefVecOperator/Map.lean b/src/Std/Sat/AIG/RefVecOperator/Map.lean
index 3512a56bbdd1..cf1b5c85a015 100644
--- a/src/Std/Sat/AIG/RefVecOperator/Map.lean
+++ b/src/Std/Sat/AIG/RefVecOperator/Map.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.RefVec
 import Std.Sat.AIG.LawfulVecOperator
 
diff --git a/src/Std/Sat/AIG/RefVecOperator/Zip.lean b/src/Std/Sat/AIG/RefVecOperator/Zip.lean
index 49c73e107bbd..58bdd28212b4 100644
--- a/src/Std/Sat/AIG/RefVecOperator/Zip.lean
+++ b/src/Std/Sat/AIG/RefVecOperator/Zip.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.RefVec
 import Std.Sat.AIG.LawfulVecOperator
 
diff --git a/src/Std/Sat/AIG/Relabel.lean b/src/Std/Sat/AIG/Relabel.lean
index f68cf0d9c435..f06433ffaae9 100644
--- a/src/Std/Sat/AIG/Relabel.lean
+++ b/src/Std/Sat/AIG/Relabel.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Basic
 import Std.Sat.AIG.Lemmas
 
diff --git a/src/Std/Sat/AIG/RelabelNat.lean b/src/Std/Sat/AIG/RelabelNat.lean
index d29e2f4195ce..bc78f4cc5761 100644
--- a/src/Std/Sat/AIG/RelabelNat.lean
+++ b/src/Std/Sat/AIG/RelabelNat.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
+prelude
 import Std.Sat.AIG.Relabel
 
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
index 38b96e65daeb..4e9e5bd87eca 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 prelude
+import Init.Data.AC
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Const
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Not