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..0de8e8d 100644
--- a/HumanEvalLean/HumanEval114.lean
+++ b/HumanEvalLean/HumanEval114.lean
@@ -163,6 +163,10 @@ 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]
 
+-- 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}
     (h : IsMinSuffixSum₀ xs minSuff) :
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