From 5c26ee53c2c879195d74f699db57b067786991f1 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Thu, 2 Jul 2026 08:48:32 +0000
Subject: [PATCH] chore: bump mathlib to v4.31.0-rc1: chore: bump toolchain to
 v4.31.0-rc1 (#39980) (2026-05-29)

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

diff --git a/lake-manifest.json b/lake-manifest.json
index de3823b..47111ca 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,17 +15,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "81343555dae873c8de2de2b27bbabf7bc4d8d97a",
+   "rev": "d568c8c09630de097a046763c17b9ea99f95f950",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "d568c8c09630de097a046763c17b9ea99f95f950",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
+   "rev": "d575be693add4fe9cb996968968ce42ce75c5ccd",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
+   "rev": "6db47de43aa7f516708053ae2fdadd29dd9baaaa",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,50 +55,50 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
+   "rev": "85bb7e7637e84a7d9803be7d954579fdae42c64b",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.99",
+   "inputRev": "v0.0.100",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "558915ae105bfd8074e22d597613d1961822adc2",
+   "rev": "fafca80479ff95e041d84373dda7122adf1295f2",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "v4.31.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
+   "rev": "8d33324ee877e9735d2829bc6f1f439e60cf98b1",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "v4.31.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "32dc18cde3684679f3c003de608743b57498c56f",
+   "rev": "708b057842c4cd0845fba132bd94b08493f6fc42",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.31.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
+   "rev": "48bdcff4c5fa27e09028f9f330e59baa0d4640cf",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.30.0",
+   "inputRev": "v4.31.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "Statlib",
diff --git a/lakefile.toml b/lakefile.toml
index 4dba6a2..df89cc9 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -13,7 +13,7 @@ weak.linter.mathlibStandardSet = true
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "master"
+rev = "d568c8c09630de097a046763c17b9ea99f95f950"
 
 [[require]]
 name = "subverso"
diff --git a/lean-toolchain b/lean-toolchain
index 5a8f161..7217ff5 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.30.0
\ No newline at end of file
+leanprover/lean4:v4.31.0-rc1
\ No newline at end of file