From 980eaefd249b5851941eed216d473f5ebf2e4d98 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 19 Jan 2026 08:41:17 +0100
Subject: [PATCH 1/2] wip

---
 HumanEvalLean/HumanEval102.lean | 4 ++--
 HumanEvalLean/HumanEval114.lean | 7 +++++++
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/HumanEvalLean/HumanEval102.lean b/HumanEvalLean/HumanEval102.lean
index 4bdf02d..cc383f4 100644
--- a/HumanEvalLean/HumanEval102.lean
+++ b/HumanEvalLean/HumanEval102.lean
@@ -28,7 +28,7 @@ macro "chooseNum_trivial" : tactic => `(tactic|(
   omega
 ))
 
-namespace Std.Range
+namespace Std.Legacy.Range
 
 -- A specification for `m` being the even maximum of range `r`.
 structure EvenMax (r : Range) (m : Nat) : Prop where
@@ -63,7 +63,7 @@ theorem not_iff_chooseNum : ¬(∃ m, [lo:hi + 1].EvenMax m) ↔ (chooseNum lo h
     · exact h ⟨hi, {}⟩
     · exact h ⟨hi, {}⟩
 
-end Std.Range.EvenMax
+end Std.Legacy.Range.EvenMax
 
 /-!
 ## Prompt
diff --git a/HumanEvalLean/HumanEval114.lean b/HumanEvalLean/HumanEval114.lean
index 4b57169..1eb1c8d 100644
--- a/HumanEvalLean/HumanEval114.lean
+++ b/HumanEvalLean/HumanEval114.lean
@@ -163,6 +163,11 @@ theorem isMinSubarraySum₀_append_singleton_eq {xs : List Int} {x minSum minSuf
       · have := h₁.2 i j (by grind) (by grind)
         grind [List.take_append_of_le_length]
 
+attribute [- grind] Subarray.sliceToArray_eq_toArray Subarray.forIn_eq_forIn_toList
+  Array.array_toSubarray Array.start_toSubarray Array.stop_toSubarray
+  ListSlice.toArray_toList ListSlice.toList_toArray
+  List.toList_mkSlice_rci_eq_toList_mkSlice_rco
+
 @[grind =>]
 theorem isMinSuffixSum₀_append_singleton_eq {xs : List Int} {x minSuff : Int}
     (h : IsMinSuffixSum₀ xs minSuff) :
@@ -177,6 +182,8 @@ theorem isMinSuffixSum₀_append_singleton_eq {xs : List Int} {x minSuff : Int}
       by_cases hieq : i = (xs ++ [x]).length
       · grind
       · simp only [IsMinSuffixSum₀] at h
+        rw [show Std.Slice.toList (Std.Rci.Sliceable.mkSlice (xs ++ [x]) i...*) = Std.Slice.toList (Std.Rco.Sliceable.mkSlice (xs ++ [x]) i...((xs ++ [x]).length)) by sorry]
+        --simp only [List.toList_mkSlice_rci_eq_toList_mkSlice_rco]
         grind [List.drop_append_of_le_length]
   · rw [show min 0 (minSuff + x) = minSuff + x by grind]
     apply And.intro

From 320774cb7ee891cffbd628c5c5344fca92e6666f Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 19 Jan 2026 11:33:21 +0100
Subject: [PATCH 2/2] bump

---
 HumanEvalLean/HumanEval114.lean | 9 +++------
 lean-toolchain                  | 2 +-
 2 files changed, 4 insertions(+), 7 deletions(-)

diff --git a/HumanEvalLean/HumanEval114.lean b/HumanEvalLean/HumanEval114.lean
index 1eb1c8d..0de8e8d 100644
--- a/HumanEvalLean/HumanEval114.lean
+++ b/HumanEvalLean/HumanEval114.lean
@@ -163,10 +163,9 @@ theorem isMinSubarraySum₀_append_singleton_eq {xs : List Int} {x minSum minSuf
       · have := h₁.2 i j (by grind) (by grind)
         grind [List.take_append_of_le_length]
 
-attribute [- grind] Subarray.sliceToArray_eq_toArray Subarray.forIn_eq_forIn_toList
-  Array.array_toSubarray Array.start_toSubarray Array.stop_toSubarray
-  ListSlice.toArray_toList ListSlice.toList_toArray
-  List.toList_mkSlice_rci_eq_toList_mkSlice_rco
+-- using this lemma would lead to complicated `take` expressions that are harder to solve for
+-- `grind`
+attribute [- grind] List.toList_mkSlice_rci_eq_toList_mkSlice_rco
 
 @[grind =>]
 theorem isMinSuffixSum₀_append_singleton_eq {xs : List Int} {x minSuff : Int}
@@ -182,8 +181,6 @@ theorem isMinSuffixSum₀_append_singleton_eq {xs : List Int} {x minSuff : Int}
       by_cases hieq : i = (xs ++ [x]).length
       · grind
       · simp only [IsMinSuffixSum₀] at h
-        rw [show Std.Slice.toList (Std.Rci.Sliceable.mkSlice (xs ++ [x]) i...*) = Std.Slice.toList (Std.Rco.Sliceable.mkSlice (xs ++ [x]) i...((xs ++ [x]).length)) by sorry]
-        --simp only [List.toList_mkSlice_rci_eq_toList_mkSlice_rco]
         grind [List.drop_append_of_le_length]
   · rw [show min 0 (minSuff + x) = minSuff + x by grind]
     apply And.intro
diff --git a/lean-toolchain b/lean-toolchain
index 105d472..385b58a 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2025-12-17
+leanprover/lean4:nightly-2026-01-16