From 663ab597b858232b471f9093341d1b80a785e652 Mon Sep 17 00:00:00 2001
From: Seasawher <47292598+Seasawher@users.noreply.github.com>
Date: Thu, 6 Feb 2025 11:10:12 +0000
Subject: [PATCH] [create-pull-request] automated change

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

diff --git a/lake-manifest.json b/lake-manifest.json
index ca03f99..97caed1 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1ed9fcd0377fe21c629eed68e254255012cfd7d6",
+   "rev": "acdf3213f3a9d3a5c22d7061b3a3adb20dcfc7ea",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9571e4aeb3689e34e89f18bba35fda5ae7a1fcd5",
+   "rev": "d0f3f20e087f980c83ac3a167aeeae6e55d1c417",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d835296a6149acb9bd2ff65ec01b728b9cc99a1c",
+   "rev": "c53b3371dd0fe5f3dd75a2df543c3550e246465a",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,10 +45,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
+   "rev": "59a8514bb0ee5bae2689d8be717b5272c9b3dc1c",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc1",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
+   "rev": "5013810061a18ca1f5510106172b94c6fbd0a2fc",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,37 +75,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
+   "rev": "8fff3f074da9237cd4e179fd6dd89be6c4022d41",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.50",
+   "inputRev": "v0.0.52-pre",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
+   "rev": "ba9a63be53f16b3b6e4043641c6bad4883e650b4",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc1",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
+   "rev": "7b3b0c8327b3c0214ac49ca6d6922edbb81ab8c9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9a3a71e5626f03b45c7533ce625dc7ba7f46d6ab",
+   "rev": "3766e2340b4f89b1173910f0161ca8eded9b0902",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index 2ffc30c..3ca992c 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.16.0-rc2
\ No newline at end of file
+leanprover/lean4:v4.17.0-rc1