From 761d3f566a25437e2cf2e90d9157ded623593b43 Mon Sep 17 00:00:00 2001
From: David Renshaw <dwrenshaw@gmail.com>
Date: Fri, 8 Sep 2023 08:20:26 -0400
Subject: [PATCH] update mathlib

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

diff --git a/lake-manifest.json b/lake-manifest.json
index 23bb3b59..5ec5ce56 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -20,10 +20,10 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "2c0daa9c00f4b974f91b16ff57c3a9ab6f687c08",
+    "rev": "2df6bb4167844ead7631ba547d6a44d465c0b37b",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "2c0daa9c00f4b974f91b16ff57c3a9ab6f687c08",
+    "inputRev?": "2df6bb4167844ead7631ba547d6a44d465c0b37b",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
diff --git a/lakefile.lean b/lakefile.lean
index 9c60cdc6..2ba87b55 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -12,4 +12,4 @@ lean_exe buildWebpage where
   root := `scripts.buildWebpage
   supportInterpreter := true
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "2c0daa9c00f4b974f91b16ff57c3a9ab6f687c08"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "2df6bb4167844ead7631ba547d6a44d465c0b37b"
diff --git a/lean-toolchain b/lean-toolchain
index 9b1d5d72..f0a6d660 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.0.0-rc4
+leanprover/lean4:v4.0.0