diff --git a/HumanEvalLean/HumanEval15.lean b/HumanEvalLean/HumanEval15.lean
index 0a6bd48..6af8e0e 100644
--- a/HumanEvalLean/HumanEval15.lean
+++ b/HumanEvalLean/HumanEval15.lean
@@ -3,7 +3,7 @@ import Std.Data.Iterators.Producers.Range
 import Std
 
 def stringSequence (n : Nat) : String :=
-  Std.Iter.intercalateString.{0} " " ((0...=n).iter.map (String.toSlice ∘ Nat.repr))
+  Std.Iter.intercalateString " " ((0...=n).iter.map (String.toSlice ∘ Nat.repr))
 
 example : stringSequence 0 = "0" := by native_decide
 example : stringSequence 3 = "0 1 2 3" := by native_decide
diff --git a/HumanEvalLean/HumanEval27.lean b/HumanEvalLean/HumanEval27.lean
index 7b3edd2..330aca9 100644
--- a/HumanEvalLean/HumanEval27.lean
+++ b/HumanEvalLean/HumanEval27.lean
@@ -20,10 +20,6 @@ theorem toList_flipCase {string : String} : (flipCase string).toList = string.to
 
 namespace Char
 
-@[simp]
-theorem toNat_mk {val : UInt32} {h} : (Char.mk val h).toNat = val.toNat := by
-  simp [← toNat_val]
-
 theorem isUpper_flipCase {c : Char} : c.flipCase.isUpper ↔ c.isLower := by
   grind [flipCase, isUpper, isLower, toUpper, toLower]
 
diff --git a/HumanEvalLean/HumanEval50.lean b/HumanEvalLean/HumanEval50.lean
index abfc9ee..65f919a 100644
--- a/HumanEvalLean/HumanEval50.lean
+++ b/HumanEvalLean/HumanEval50.lean
@@ -12,10 +12,6 @@ def encodeShift (s : String) : String :=
 def decodeShift (s : String) : String :=
   s.map Char.unshiftByFive
 
-@[simp]
-theorem Char.toNat_mk {val : UInt32} {h} : (Char.mk val h).toNat = val.toNat := by
-  simp [← toNat_val]
-
 theorem Char.toNat_ofNat_of_isValidChar {n : Nat} (h : n.isValidChar) : (Char.ofNat n).toNat = n := by
   simp [ofNat, h, ofNatAux]
 
diff --git a/lean-toolchain b/lean-toolchain
index de7cb2b..b222dcb 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-03-24
+leanprover/lean4:nightly-2026-03-25