From 898bbf8569b267024ee46e5dccc6d679d2ead1fa Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 18 Mar 2026 09:58:20 +0100
Subject: [PATCH] Update LEAN

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

diff --git a/lake-manifest.json b/lake-manifest.json
index ef01237..37b8a54 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d62eab0cc36ea522904895389c301cf8d844fd69",
+   "rev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "d62eab0cc36ea522904895389c301cf8d844fd69",
+   "inputRev": "8f9d9cff6bd728b17a24e163c9402775d9e6a365",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "304c5e2f490d546134c06bf8919e13b175272084",
+   "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f5e58ef1f58fc0cbd92296d18951f45216309e48",
+   "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "632ca63a94f47dbd5694cac3fd991354b82b8f7a",
+   "rev": "be3b2e63b1bbf496c478cef98b86972a37c1417d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.59",
+   "inputRev": "v0.0.87",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9264d548cf1ccf0ba454b82f931f44c37c299fc1",
+   "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "36ce5e17d6ab3c881e0cb1bb727982507e708130",
+   "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "78e1181c4752c7e10874d2ed5a6a15063f4a35b6",
+   "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664",
+   "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.28.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "aristotle",
diff --git a/lakefile.toml b/lakefile.toml
index 78641bb..b9a07f2 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -12,7 +12,7 @@ maxSynthPendingDepth = 3
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "d62eab0cc36ea522904895389c301cf8d844fd69"
+rev = "8f9d9cff6bd728b17a24e163c9402775d9e6a365"
 
 [[lean_lib]]
 name = "Aristotle"
diff --git a/lean-toolchain b/lean-toolchain
index cc6fba8..ea6ca7f 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.20.0-rc5
\ No newline at end of file
+leanprover/lean4:v4.28.0
\ No newline at end of file