From ca8559b9dc13d3a0d2d5deb8236f077dbbc98663 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 26 Aug 2026 19:47:41 +1000
Subject: [PATCH] chore: bump toolchain to v4.33.1

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01C4AZKZ85yyEVqQby5CeBiR
---
 lake-manifest.json | 29 +++++++++++++++--------------
 lakefile.toml      |  1 +
 lean-toolchain     |  2 +-
 3 files changed, 17 insertions(+), 15 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 713962c..0192d41 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,21 +1,21 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365",
+   "rev": "0df444a360eaa60ab8c11dca51a86af692955474",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.28.0",
+   "inputRev": "v4.33.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3",
+   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e",
+   "rev": "16f02aa7642864af59f1ff0e384a015994db9118",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d",
+   "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.87",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1",
+   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3",
+   "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f",
+   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,11 +85,12 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e",
+   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.28.0",
+   "inputRev": "v4.33.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Project",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/lakefile.toml b/lakefile.toml
index 281da52..c38f079 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -9,6 +9,7 @@ relaxedAutoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
+rev = "v4.33.1"
 
 [[lean_lib]]
 name = "Project"
diff --git a/lean-toolchain b/lean-toolchain
index ea6ca7f..a8afa7d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.28.0
\ No newline at end of file
+leanprover/lean4:v4.33.1