chore: bump to Lean 4 nightly-2023-05-06 (#3817)

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
leanprover-community · May 6, 2023 · 9cf0d9b · 9cf0d9b
1 parent 38dbcd8
commit 9cf0d9b
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/Mathlib/Data/String/Basic.lean b/Mathlib/Data/String/Basic.lean
@@ -19,9 +19,7 @@ Supplementary theorems about the `String` type.
 
 namespace String
 
-open private utf8GetAux from Init.Data.String.Basic
-
-private lemma utf8GetAux.add_right_cancel (s : List Char) (i p n : ℕ) :
+lemma utf8GetAux.add_right_cancel (s : List Char) (i p n : ℕ) :
     utf8GetAux s ⟨i + n⟩ ⟨p + n⟩ = utf8GetAux s ⟨i⟩ ⟨p⟩ := by
   apply utf8InductionOn s ⟨i⟩ ⟨p⟩ (motive := fun s i ↦
     utf8GetAux s ⟨i.byteIdx + n⟩ ⟨p + n⟩ = utf8GetAux s i ⟨p⟩) <;>

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-04-20
+leanprover/lean4:nightly-2023-05-06