diff --git a/lake-manifest.json b/lake-manifest.json
index f5cb61a..d9011b2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1a5c8fe51b870f5c4ffd6fe44936e09a776d8f3e",
+   "rev": "2df2f0150c275ad53cb3c90f7c98ec15a56a1a67",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0-rc2",
+   "inputRev": "v4.26.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fde3fc21dd68a10791dea22b6f5b53c5a5a5962d",
+   "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,60 +35,60 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "856a8cb8908af109aac3ce13e2b4f866f3d75199",
+   "rev": "e9f31324f15ead11048b1443e62c5deaddd055d2",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2d6d124aedc3023506a67e50bfd5582384d6bd17",
+   "rev": "b4fb2aa5290ebf61bc5f80a5375ba642f0a49192",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.63-pre",
+   "inputRev": "v0.0.83",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a1b5d59f433c6ec2b318192bd910c257a3c62be8",
+   "rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "56047303fce0d07dcae7e3e91b17eef67d11f6f4",
+   "rev": "9312503909aa8e8bb392530145cc1677a6298574",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bfd7f60186ea20946cc36288f83ad3659520f0ce",
+   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "1604206fcd0462da9a241beeac0e2df471647435",
+   "rev": "933fce7e893f65969714c60cdb4bd8376786044e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.26.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "ExtTreeMapLemmas",
diff --git a/lakefile.lean b/lakefile.lean
index ffaceda..a62030c 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,7 +4,7 @@ open System Lake DSL
 
 package ExtTreeMapLemmas where version := v!"0.1.0"
 
-require "leanprover-community" / mathlib @ git "v4.22.0-rc2"
+require "leanprover-community" / mathlib @ git "v4.26.0"
 
 @[default_target]
 lean_lib ExtTreeMapLemmas
diff --git a/lean-toolchain b/lean-toolchain
index 52782c4..2654c20 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.22.0-rc2
\ No newline at end of file
+leanprover/lean4:v4.26.0
\ No newline at end of file