From 19342a8bb34f75f53d45e8945a9b607a2a694d95 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Sun, 22 Oct 2023 09:30:29 +1100
Subject: [PATCH 1/2] chore: bump lean-toolchain to v4.2.0-rc4

Fixes a potential data loss bug. All projects should update their toolchain as soon as possible.

Please see https://github.com/leanprover/lean4/releases/tag/v4.2.0-rc4
and the [zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Potential.20data.20loss.20from.20.60lake.20clean.60.20with.204.2E2.2E0-rc2.2F3/near/397875701) for more information.
---
 lean-toolchain | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lean-toolchain b/lean-toolchain
index a61d2828..183a307e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc3
+leanprover/lean4:v4.2.0-rc4

From 79cd731453b6a0d26fd31adb368fe36d03084404 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 22 Oct 2023 11:10:31 +0900
Subject: [PATCH 2/2] =?UTF-8?q?mathlib=E3=81=AE=E3=83=90=E3=83=BC=E3=82=B8?=
 =?UTF-8?q?=E3=83=A7=E3=83=B3=E3=82=92=E4=B8=8A=E3=81=92=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/lake-manifest.json b/lake-manifest.json
index 23a4f3ca..93c4f2f5 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "ae7ec61a7b0e120ac9bdbeda6f0047c8059f754f",
+    "rev": "3ce43c18f614b76e161f911b75a3e1ef641620ff",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "ae7ec61a7b0e120ac9bdbeda6f0047c8059f754f",
+    "inputRev?": "3ce43c18f614b76e161f911b75a3e1ef641620ff",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "dd2549f76ff763c897fe997061e2625a7d628eaf",
+    "rev": "727fa6aa1113c376ea1873812d1ab5c17a24f1d2",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
diff --git a/lakefile.lean b/lakefile.lean
index 53e8c1c4..152c60a6 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -8,7 +8,7 @@ package examples {
 }
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "ae7ec61a7b0e120ac9bdbeda6f0047c8059f754f"
+  "https://github.com/leanprover-community/mathlib4.git" @ "3ce43c18f614b76e161f911b75a3e1ef641620ff"
 
 @[default_target]
 lean_lib Examples {