From 66df65c14b287d89129baa1446c49b4fa953f649 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Sat, 20 May 2023 11:11:27 -0600
Subject: [PATCH] Update toolchain and deps.

---
 Common/Real/Floor.lean | 4 ++--
 lake-manifest.json     | 8 ++++----
 lean-toolchain         | 2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Common/Real/Floor.lean b/Common/Real/Floor.lean
index fccedd5..e0356e1 100644
--- a/Common/Real/Floor.lean
+++ b/Common/Real/Floor.lean
@@ -55,7 +55,7 @@ theorem partition_subset_Ico_zero_one
     zero_lt_one,
     not_true,
     ge_iff_le,
-    Set.unionᵢ_subset_iff
+    Set.iUnion_subset_iff
   ]
   intro i hi x hx
   have hn : (0 : ℝ) < n := calc (0 : ℝ)
@@ -83,7 +83,7 @@ theorem partition_subset_Ico_zero_one
 theorem Ico_zero_one_subset_partition
   : Set.Ico 0 1 ⊆ (⋃ i ∈ Finset.range n, partition n i) := by
   intro x hx
-  simp only [Finset.mem_range, Set.mem_unionᵢ, exists_prop]
+  simp only [Finset.mem_range, Set.mem_iUnion, exists_prop]
   unfold partition
   exact fract_mem_partition x hx n
 
diff --git a/lake-manifest.json b/lake-manifest.json
index ff1f703..5f9f502 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -22,7 +22,7 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "eff4459bbf65f545383feac6b2a857a8b798d4dd",
+    "rev": "62e469416e55278c1a4bca000426539b578b7749",
     "name": "mathlib",
     "inputRev?": "master"}},
   {"git":
@@ -34,7 +34,7 @@
   {"git":
    {"url": "https://github.com/JLimperg/aesop",
     "subDir?": null,
-    "rev": "cdc00b640d0179910ebaa9c931e3b733a04b881c",
+    "rev": "409f3b050034337664d21e41fe1cc1bf7f5daec0",
     "name": "aesop",
     "inputRev?": "master"}},
   {"git":
@@ -52,12 +52,12 @@
   {"git":
    {"url": "https://github.com/leanprover/std4.git",
     "subDir?": null,
-    "rev": "f6525373c9fd639adffa259bcb98c17dfd00e61e",
+    "rev": "acb5ba1b6643269a37da88fa3ce5d30e27e66bad",
     "name": "std4",
     "inputRev?": "main"}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "6006307d2ceb8743fea7e00ba0036af8654d0347",
+    "rev": "3156cd5b375d1a932d590c918b7ad50e3be11947",
     "name": "std",
     "inputRev?": "main"}}]}
diff --git a/lean-toolchain b/lean-toolchain
index a7041bc..e7e8b2d 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-05-06
+leanprover/lean4:nightly-2023-05-16