diff --git a/Cache/IO.lean b/Cache/IO.lean
index 8e2426b276df96..55b829b9b2c17e 100644
--- a/Cache/IO.lean
+++ b/Cache/IO.lean
@@ -503,8 +503,6 @@ def lookup (hashMap : ModuleHashMap) (modules : List Name) : IO Unit := do
       println! "  comment: {line}"
   if err then IO.Process.exit 1
 
-open private Lake.Glob.ofString? from Lake.Load.Toml in
-
 /--
 Parse a string as either a path or a Lean module name.
 If the argument describes a folder, use `walkDir` to find all `.lean` files within.
diff --git a/Mathlib/Data/String/Lemmas.lean b/Mathlib/Data/String/Lemmas.lean
index bc240b9cafb430..fd79a3afd2a5c3 100644
--- a/Mathlib/Data/String/Lemmas.lean
+++ b/Mathlib/Data/String/Lemmas.lean
@@ -28,10 +28,10 @@ lemma length_eq_list_length (l : List Char) : (String.ofList l).length = l.lengt
   to the larger of `n` and `s.length` -/
 @[simp] lemma length_leftpad (n : ℕ) (c : Char) :
     ∀ (s : String), (leftpad n c s).length = max n s.length
-  | s => by simp [leftpad, Nat.sub_add_eq_max]
+  | s => by simp [leftpad, length_toList, Nat.sub_add_eq_max]
 
 lemma leftpad_prefix (n : ℕ) (c : Char) : ∀ s, IsPrefix (replicate (n - length s) c) (leftpad n c s)
-  | s => by simp [leftpad, IsPrefix, replicate]
+  | s => by simp [leftpad, IsPrefix, replicate, length_toList]
 
 lemma leftpad_suffix (n : ℕ) (c : Char) : ∀ s, IsSuffix s (leftpad n c s)
   | s => by simp [leftpad, IsSuffix]
diff --git a/lake-manifest.json b/lake-manifest.json
index 54f6bf9494c50c..b46adb2b83409c 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cdab3938ccabbdb044be6896e251b5814bec932e",
+   "rev": "fd70b40073aeca8fa60fe0fb492f189d3b12c0ef",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "25a8b1685158cc5b463b2cdf3d06f16846a3b919",
+   "rev": "8e1db9dde3100736e39943b355d076c6f3b38fff",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
diff --git a/lean-toolchain b/lean-toolchain
index 24588e1238c82c..14c276dd90f460 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-05-07
+leanprover/lean4:nightly-2026-05-10