bump toolchain to 2026-02-01 nightly (#221)

Author: datokrat

HumanEvalLean/HumanEval110.lean

@@ -3,8 +3,8 @@ module
 public import Std
 
 public def isExchangePossible (xs ys : Array Int) : String :=
-  let need := xs.iter.filter (· % 2 == 1) |>.count
-  let available := ys.iter.filter (· % 2 == 0) |>.count
+  let need := xs.iter.filter (· % 2 == 1) |>.length
+  let available := ys.iter.filter (· % 2 == 0) |>.length
   if need ≤ available then "YES" else "NO"
 
 /-!
@@ -134,7 +134,7 @@ public theorem isExchangePossible_correct {xs ys : Array Int} :
   generalize h : VectorPair.mk xs.toVector ys.toVector = p
   simp only [show xs = p.1.toArray by grind, show ys = p.2.toArray by grind]
   -- prove the actual statement
-  simp [isExchangePossible, ← Std.Iter.length_toList_eq_count,
+  simp [isExchangePossible, ← Std.Iter.length_toList_eq_length,
     ← List.countP_eq_length_filter, VectorPair.countP_le_countP_iff_exists]
 
 /-!

HumanEvalLean/HumanEval114.lean

@@ -141,7 +141,7 @@ theorem isMinSubarraySum₀_append_singleton_eq {xs : List Int} {x minSum minSuf
         · grind
         · simp only [heq, List.toList_mkSlice_rco, List.take_length]
           have := h₂.2 i (by grind)
-          grind [List.drop_append_of_le_length]
+          grind
       · have := h₁.2 i j (by grind) (by grind)
         grind [List.take_append_of_le_length]
 
@@ -163,16 +163,16 @@ theorem isMinSuffixSum₀_append_singleton_eq {xs : List Int} {x minSuff : Int}
       by_cases hieq : i = (xs ++ [x]).length
       · grind
       · simp only [IsMinSuffixSum₀] at h
-        grind [List.drop_append_of_le_length]
+        grind
   · rw [show min 0 (minSuff + x) = minSuff + x by grind]
     apply And.intro
     · simp only [IsMinSuffixSum₀] at h
-      grind [List.drop_append_of_le_length]
+      grind
     · intro i hi
       by_cases hieq : i = (xs ++ [x]).length
       · grind
       · simp only [IsMinSuffixSum₀] at h
-        grind [List.drop_append_of_le_length]
+        grind
 
 theorem List.zero_le_min_of_zero_le_sum {xs : List Int} (hne : xs ≠ []) (h : xs.sum ≤ 0) :
     xs.min hne ≤ 0 := by

HumanEvalLean/HumanEval115.lean

@@ -44,25 +44,6 @@ actions needed.
 
 attribute [grind =] Vector.sum_mk List.zip_cons_cons List.zip_nil_right List.zip_nil_left
 
--- this is in Mathlib
-theorem Nat.div_add_div_le_add_div (a b c : Nat) : a / c + b / c ≤ (a + b) / c := by
-  by_cases h : 0 < c
-  · rw [← (Nat.mul_le_mul_right_iff (show 0 < c by grind)), Nat.add_mul]
-    simp only [Nat.div_mul_self_eq_mod_sub_self]
-    have (a b c d : Nat) (h : b ≤ a) (h' : d ≤ c) : (a - b) + (c - d) = (a + c) - (b + d) := by grind
-    rw [this, Nat.sub_le_sub_iff_left]
-    · rw [Nat.add_mod]
-      apply Nat.mod_le
-    · apply Nat.mod_le
-    · apply Nat.mod_le
-    · apply Nat.mod_le
-  · grind
-
-theorem Nat.le_mul_iff_le_left (hc : 0 < z) :
-    x ≤ y * z ↔ (x + z - 1) / z ≤ y := by
-  rw [Nat.div_le_iff_le_mul hc]
-  omega
-
 @[simp, grind =]
 theorem Vector.sum_toList {xs : Vector Nat α} :
     xs.toList.sum = xs.sum := by

HumanEvalLean/HumanEval123.lean

@@ -460,11 +460,11 @@ example : oddCollatz₂ 1 = [1] := by native_decide
 We'll verify `oddCollatz₂` by proving it equivalent to `oddCollatz₁`.
 -/
 
-theorem oddCollatz₂_pairwise_distinct {n : Nat} (h : Acc CollatzRel n) :
+theorem oddCollatz₂_pairwise_distinct {n : Nat} :
     (oddCollatz₂ n).Pairwise (· ≠ ·) := by
   simpa [oddCollatz₂] using TreeSet.distinct_toList (α := Nat) (cmp := compare)
 
-theorem oddCollatz₂_pairwise_lt {n : Nat} (h : Acc CollatzRel n) :
+theorem oddCollatz₂_pairwise_lt {n : Nat} :
     (oddCollatz₂ n).Pairwise (· < ·) := by
   simpa [oddCollatz₁, compare_eq_lt] using TreeSet.ordered_toList (α := Nat) (cmp := compare)
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-01-28
+leanprover/lean4:nightly-2026-02-01