diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index 7ddae63fddaa1..ca3359b3a58c7 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -79,10 +79,6 @@ jobs:
         run: |
           git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
-      - name: update MathlibExtras.lean
-        run: |
-          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
-
       - name: update Mathlib/Tactic.lean
         run: |
           git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
@@ -191,9 +187,6 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
-      - name: build library_search cache
-        run: lake build -KCI MathlibExtras
-
       - name: upload cache
         # We only upload the cache if the build ran (either succeeding or failing),
         # but not if it was skipped.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index d7f993dce4c22..56ec0d158b53b 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -86,10 +86,6 @@ jobs:
         run: |
           git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
-      - name: update MathlibExtras.lean
-        run: |
-          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
-
       - name: update Mathlib/Tactic.lean
         run: |
           git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
@@ -198,9 +194,6 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
-      - name: build library_search cache
-        run: lake build -KCI MathlibExtras
-
       - name: upload cache
         # We only upload the cache if the build ran (either succeeding or failing),
         # but not if it was skipped.
diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in
index 1e00355151e7f..b7e39ee04905b 100644
--- a/.github/workflows/build.yml.in
+++ b/.github/workflows/build.yml.in
@@ -65,10 +65,6 @@ jobs:
         run: |
           git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
-      - name: update MathlibExtras.lean
-        run: |
-          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
-
       - name: update Mathlib/Tactic.lean
         run: |
           git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
@@ -177,9 +173,6 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
-      - name: build library_search cache
-        run: lake build -KCI MathlibExtras
-
       - name: upload cache
         # We only upload the cache if the build ran (either succeeding or failing),
         # but not if it was skipped.
diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
index ee58e87f74de1..f8c27fb7900c4 100644
--- a/.github/workflows/build_fork.yml
+++ b/.github/workflows/build_fork.yml
@@ -83,10 +83,6 @@ jobs:
         run: |
           git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
-      - name: update MathlibExtras.lean
-        run: |
-          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
-
       - name: update Mathlib/Tactic.lean
         run: |
           git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean
@@ -195,9 +191,6 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
-      - name: build library_search cache
-        run: lake build -KCI MathlibExtras
-
       - name: upload cache
         # We only upload the cache if the build ran (either succeeding or failing),
         # but not if it was skipped.
diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml
index 01e828cb0f8bd..422eb5fb2c32f 100644
--- a/.github/workflows/lint_and_suggest_pr.yml
+++ b/.github/workflows/lint_and_suggest_pr.yml
@@ -61,10 +61,6 @@ jobs:
         run: |
           git ls-files 'Mathlib/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
-      - name: update MathlibExtras.lean
-        run: |
-          git ls-files 'MathlibExtras/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > MathlibExtras.lean
-
       - name: update Mathlib/Tactic.lean
         run: |
           git ls-files 'Mathlib/Tactic/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib/Tactic.lean