From 2a7d650484103b911b23844492582979ccd3b4a5 Mon Sep 17 00:00:00 2001
From: kebekus <5110976+kebekus@users.noreply.github.com>
Date: Mon, 19 Oct 2026 09:51:18 +0000
Subject: [PATCH] Update Mathlib

---
 docbuild/lakefile.toml |  2 +-
 lake-manifest.json     | 20 ++++++++++----------
 lean-toolchain         |  2 +-
 3 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/docbuild/lakefile.toml b/docbuild/lakefile.toml
index 5a8f6ab..f0d2ffa 100644
--- a/docbuild/lakefile.toml
+++ b/docbuild/lakefile.toml
@@ -16,7 +16,7 @@ packagesDir = "../.lake/packages"
 [[require]]
 scope = "leanprover"
 name = "doc-gen4"
-rev = "v4.35.0-rc4"
+rev = "v4.36.0-rc1"
 
 [[require]]
 name = "VD"
diff --git a/lake-manifest.json b/lake-manifest.json
index ec75d8d..df55dd0 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "074063781836922cb02701cd12943c9f51731afa",
+   "rev": "02aea1d03062d67719ebe7b538ec4899bb9401b7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dfa4f38190d07c37e315953e08b90fe2d95b3c24",
+   "rev": "c2d7840c65673533e15b499f25beecdc6227f7d8",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d6b4c7be5be75ec4917c873ac50c756dc1436372",
+   "rev": "9d39f9bb0c30aa2f6200808805ff16e6ce950890",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a41f0e9a4dea23188ea9cc1c41ac9f8bbafe0b93",
+   "rev": "b3cc36c295aa5e3e3c0197b09a6556298e710447",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "df72b022e558978a1c50264cfc4d7fec86fa8e04",
+   "rev": "17137fad38a2cc782ff00b323a13c3a991d085ab",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4a174c490d8707121c4a9290800489f105d85e07",
+   "rev": "cbdde3aa2665915fb286c48bcd4cdf885c629511",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dce0ad79c486cb1fb504af04f953c3466b0c6db8",
+   "rev": "6d26f8bb4b2bb78f929ad160feac508866821316",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "66e469188fe07963e5cf666c7d4433f45b8131c5",
+   "rev": "4453b52d2468f4c346a8711d728c0742e7483c9b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "c24fe6078c630e89b489bffe59b3e20ac30d12c8",
+   "rev": "34d2efffcb6dc8d5f3537cf6a7f88bfaa999ec49",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0",
+   "inputRev": "v4.36.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "VD",
diff --git a/lean-toolchain b/lean-toolchain
index d87704e..2afd387 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.35.0
\ No newline at end of file
+leanprover/lean4:v4.36.0-rc1