From 2fc5440694ed3d454fc22c838f2f1bff36b0b73a Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Mon, 11 Sep 2023 20:48:18 +0100
Subject: [PATCH] update mathlib

---
 lake-manifest.json | 12 ++++++------
 lakefile.lean      |  2 +-
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index f8f13e942..d81ef94f7 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -12,7 +12,7 @@
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
-    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+    "rev": "21dac2e9cc7e3cf7da5800814787b833e680b2fd",
     "opts": {},
     "name": "Cli",
     "inputRev?": "nightly",
@@ -20,15 +20,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "891adb329938ca3cd49a1d1208f691a98fb0896f",
+    "rev": "23cd2eabe45f28df8e1778c94ca00fd4287b6cf8",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "891adb3",
+    "inputRev?": "23cd2ea",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,
-    "rev": "81cc13c524a68d0072561dbac276cd61b65872a6",
+    "rev": "e75daed95ad1c92af4e577fea95e234d7a8401c1",
     "opts": {},
     "name": "Qq",
     "inputRev?": "master",
@@ -36,7 +36,7 @@
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "086c98bb129ca856381d4414dc0afd6e3e4ae2ef",
+    "rev": "1a0cded2be292b5496e659b730d2accc742de098",
     "opts": {},
     "name": "aesop",
     "inputRev?": "master",
@@ -44,7 +44,7 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "b5f7bd40d2162fe148e585543f284a5d8cc0ef26",
+    "rev": "e8c27f7d90ee71470558efd1bc197fe55068c748",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
diff --git a/lakefile.lean b/lakefile.lean
index 552f3a495..e2c46d936 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -37,7 +37,7 @@ lean_exe mlirnatural {
 
 -- NOTE: this must be 'm'mathlib, as indicated from:
 --  https://github.com/leanprover-community/mathlib4#using-mathlib4-as-a-dependency
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "891adb3"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "23cd2ea"
 
 require Cli from git "https://github.com/mhuisi/lean4-cli.git" @ "nightly"