diff --git a/MathPuzzles/Meta/ProblemExtraction.lean b/MathPuzzles/Meta/ProblemExtraction.lean
index cd80dfe2..f8617b3a 100644
--- a/MathPuzzles/Meta/ProblemExtraction.lean
+++ b/MathPuzzles/Meta/ProblemExtraction.lean
@@ -1,6 +1,5 @@
 import Lean.Elab.Command
 import Lean.Meta.Basic
-import Mathlib.Tactic.LabelAttr
 import Std.Lean.NameMapAttribute
 
 /-!
diff --git a/lake-manifest.json b/lake-manifest.json
index a267e175..8677ccdf 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,10 +4,10 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "e70f8800f70f89b102ad7469128ace674213e1e5",
+    "rev": "172bfffa8f5dac91317780938797c609c373541e",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "e70f8800f70f89b102ad7469128ace674213e1e5",
+    "inputRev?": "172bfffa8f5dac91317780938797c609c373541e",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",
@@ -44,7 +44,7 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "524aae5c8000f6e38433ee0ad95bdae3cfa88fee",
+    "rev": "67855403d60daf181775fa1ec63b04e70bcc3921",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
diff --git a/lakefile.lean b/lakefile.lean
index 7b945910..d28633f3 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -12,4 +12,4 @@ lean_exe buildWebpage where
   root := `scripts.buildWebpage
   supportInterpreter := true
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "e70f8800f70f89b102ad7469128ace674213e1e5"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "172bfffa8f5dac91317780938797c609c373541e"