diff --git a/Projects/MathlibDemo/MathlibDemo/Logic.lean b/Projects/MathlibDemo/MathlibDemo/Logic.lean
index ddcfe43f..7d4f60e8 100644
--- a/Projects/MathlibDemo/MathlibDemo/Logic.lean
+++ b/Projects/MathlibDemo/MathlibDemo/Logic.lean
@@ -1,4 +1,4 @@
-import Mathlib.Logic.Basic -- basic facts in logic
+import Mathlib.Basic.Logic.Basic -- basic facts in logic
 -- theorems in Lean's mathematics library
 
 -- Let P and Q be true-false statements
diff --git a/Projects/MathlibDemo/lake-manifest.json b/Projects/MathlibDemo/lake-manifest.json
index 87cef242..251d0d08 100644
--- a/Projects/MathlibDemo/lake-manifest.json
+++ b/Projects/MathlibDemo/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0cd048027c8b0239cdfe206691bbf2c0a0970078",
+   "rev": "3a8a89422e16d67b7ae57698f6d96e389e4d4202",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d54dddc581e08be364c278052863524bff7a99a9",
+   "rev": "7e23602c91bc04586b2b06de2708a041853e4681",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",