From 5cf1cc445cdfc1d2646b3c98353428095c6b4295 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Wed, 7 Oct 2026 06:20:48 +0000
Subject: [PATCH] chore: bump mathlib to v4.35.0-rc4: chore: bump toolchain to
 v4.35.0-rc4 (#44557) (2026-10-06)

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

diff --git a/lake-manifest.json b/lake-manifest.json
index 072f6455..fb1b62d4 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7d6757bc18680044fc0ff6efc8ee20494b408556",
+   "rev": "1f414401f69059aa7eead47b53ee40bd38455eeb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "7d6757bc18680044fc0ff6efc8ee20494b408556",
+   "inputRev": "1f414401f69059aa7eead47b53ee40bd38455eeb",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "afc2695efcb6855264d85a45632db1ddc56c8774",
+   "rev": "aef59637faa9e85fa2486acaaf906ce3f572af7c",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "50cd21bc62f2c8357c4f269d1185921cbfcdfc90",
+   "rev": "234d9e074fbd6e911b920baf32db5291c3125be0",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7ad9f2e325aa6cec3dacaa97c2653a98032750eb",
+   "rev": "579f558774c4ac6840e715ba60dabf3030619349",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "87dfe779d5dfd03142ee4fe158911b8eb553ec98",
+   "rev": "d5ad4a0b79fa7f9818fe1380d05a3f6143823c09",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "36cb0105a76ff3de70add8ae91afb6cfc57fafe3",
+   "rev": "04879b1e1de744d5c9777c8cf63fa55a8f652e5e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d93a8a0622807953d1e424f0fe2a5f5b5520c12e",
+   "rev": "e7c4cdd2f1bf9df361ef7f621b4d6867012ab65e",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "914928598160c128affd7a42640b4237b7e4d912",
+   "rev": "b71aaf60877e673fdb921f06f20987d12ee8a290",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a",
+   "rev": "82c11b9717083154aefc5fe8d4cba4bbf046298f",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0-rc3",
+   "inputRev": "v4.35.0-rc4",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/illuminate",
diff --git a/lakefile.toml b/lakefile.toml
index 05ede8a3..503f44f3 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -17,7 +17,7 @@ rev = "v4.35.0-rc3"
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "7d6757bc18680044fc0ff6efc8ee20494b408556"
+rev = "1f414401f69059aa7eead47b53ee40bd38455eeb"
 
 [[lean_lib]]
 name = "LeanMachineLearning"
diff --git a/lean-toolchain b/lean-toolchain
index 9d74fe15..e5b681cf 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.35.0-rc3
\ No newline at end of file
+leanprover/lean4:v4.35.0-rc4
\ No newline at end of file