From 4f4d398b1a8d5fd77594b9f0d60bc3812f53a80a Mon Sep 17 00:00:00 2001
From: Moritz Doll <moritz.doll@googlemail.com>
Date: Mon, 20 Jul 2026 12:35:01 +1000
Subject: [PATCH] update mathlib

---
 lake-manifest.json | 30 +++++++++++++++---------------
 lakefile.toml      |  4 ++--
 lean-toolchain     |  2 +-
 3 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 6091b1e..24fcaaa 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4a7edd35ec64de7117995da659e9d4d80e6cca19",
+   "rev": "79d0395a1825a6264ad5d269e35e60537518955e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "4a7edd35ec64de7117995da659e9d4d80e6cca19",
+   "inputRev": "v4.33.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "8cb04559a9b9feb8efab43e135f662514561f668",
+   "rev": "6af30619664960f9c816b27157dff3ceb1500dcf",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.32.0-rc1",
+   "inputRev": "v4.33.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
+   "rev": "b1c4a69a7e247ab7df20460212001673d74f08c0",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "41f407a8e85b0fdc00910633a8f14754139b63f4",
+   "rev": "18a90119a5d316358fde6c86e0ca24e59212e32c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93",
+   "rev": "b1436dc749e722c9920036b52cdc43b3451d0b69",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "24fa6b3599743c23e6debd53d5fd09ebfa587d29",
+   "rev": "57d3325be72a842920813bcb40f96a6f7393c185",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
+   "rev": "ee41917ae11d38479fb8fb24745f7ca4bf0a784d",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dfb6d7e9949d1bb0706f651e330176bc66fc6f3d",
+   "rev": "31a49105f960721073a9adfc82b261f5d0f2ce1e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ae95e7e7d01c072421732d0b84cf63ff903f4f0e",
+   "rev": "56958b3901ca108830de34fbce6cecd4b5757c1f",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
+   "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0bd508e8362f56d4a05cbf63614d4c97db954041",
+   "rev": "0076a9e8a3670d83c54c93414b2b26d3a8aba08d",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -125,10 +125,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "406ebb8c8e2f7e852a1b47764b42494022ce652c",
+   "rev": "da07ca808b6718cb2aed14dba154e5a08b8f8ecf",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.32.0-rc1",
+   "inputRev": "v4.33.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "DynamicalSystems",
diff --git a/lakefile.toml b/lakefile.toml
index 1cb587b..4c8b19c 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -14,12 +14,12 @@ warn.sorry = false
 [[require]]
 name = "verso"
 scope = "leanprover"
-rev = "v4.32.0-rc1"
+rev = "v4.33.0-rc1"
 
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "4a7edd35ec64de7117995da659e9d4d80e6cca19"
+rev = "v4.33.0-rc1"
 
 [[lean_lib]]
 name = "DynamicalSystems"
diff --git a/lean-toolchain b/lean-toolchain
index 63f51ea..1770ccd 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.32.0-rc1
\ No newline at end of file
+leanprover/lean4:v4.33.0-rc1
\ No newline at end of file