diff --git a/RustLeanModels/Basic.lean b/RustLeanModels/Basic.lean
index d153228..bef4189 100644
--- a/RustLeanModels/Basic.lean
+++ b/RustLeanModels/Basic.lean
@@ -1,6 +1,5 @@
 -- Copyright Kani Contributors
 -- SPDX-License-Identifier: Apache-2.0 OR MIT
-import Batteries.Data.List
 open String
 open List
 open Nat
diff --git a/lake-manifest.json b/lake-manifest.json
index a023141..c0b9293 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,15 +1,5 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
-   "name": "batteries",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "0f3e143",
-   "inherited": false,
-   "configFile": "lakefile.lean"}],
+ "packages": [],
  "name": "«rust-lean-models»",
  "lakeDir": ".lake"}
diff --git a/lakefile.toml b/lakefile.toml
index 5d91959..3951ecb 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -4,10 +4,5 @@ defaultTargets = ["RustLeanModels"]
 [leanOptions]
 pp.unicode.fun = true
 
-[[require]]
-name = "batteries"
-git = "https://github.com/leanprover-community/batteries"
-rev = "0f3e143"
-
 [[lean_lib]]
 name = "RustLeanModels"
diff --git a/lean-toolchain b/lean-toolchain
index 7f0ea50..5a9c76d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:v4.11.0