From d3cf37b03527dd7b3cd449d7bc09182d5eb41ba5 Mon Sep 17 00:00:00 2001
From: Yongxi Lin <aaronlin@andrew.cmu.edu>
Date: Wed, 24 Jun 2026 19:32:26 -0700
Subject: [PATCH] bump mathlib

---
 lake-manifest.json | 24 ++++++++++++------------
 lean-toolchain     |  2 +-
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index de3823b..4be1cb6 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "81343555dae873c8de2de2b27bbabf7bc4d8d97a",
+   "rev": "ee89f2d4639074a91449870b8f7a0d0e401faba8",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
+   "rev": "f3c7bd5061bd81b4480295c524d4f245c8b7e4e2",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
+   "rev": "41f407a8e85b0fdc00910633a8f14754139b63f4",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,37 +55,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
+   "rev": "e6518a674e62de322b8f79eebeda7bcae2a36bc3",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.99",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "558915ae105bfd8074e22d597613d1961822adc2",
+   "rev": "b5b9e2bb45ce91e4bc44eaa738c3a8910404ab82",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
+   "rev": "7a62bd13860cd39ac98da16ffc8c24d601353f69",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "32dc18cde3684679f3c003de608743b57498c56f",
+   "rev": "7d1b02eb63b526dff04cb990cf05b06b38ccbd3f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
+   "rev": "406ebb8c8e2f7e852a1b47764b42494022ce652c",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "v4.32.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Statlib",
diff --git a/lean-toolchain b/lean-toolchain
index 5a8f161..2694eb7 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.30.0
\ No newline at end of file
+leanprover/lean4:v4.32.0-rc1