diff --git a/HumanEvalLean/HumanEval0.lean b/HumanEvalLean/HumanEval0.lean
index cb77f87..29d904d 100644
--- a/HumanEvalLean/HumanEval0.lean
+++ b/HumanEvalLean/HumanEval0.lean
@@ -12,178 +12,12 @@ set_option mvcgen.warning false
 ## Missing API
 -/
 
-namespace Array
-
-def MergeSort.merge (xs ys : Array α) (le : α → α → Bool := by exact (· ≤ ·)) : Array α :=
-  if hxs : 0 < xs.size then
-    if hys : 0 < ys.size then
-      go xs[*...*] ys[*...*] (by simp only [Array.size_mkSlice_rii]; omega) (by simp only [Array.size_mkSlice_rii]; omega) (Array.emptyWithCapacity (xs.size + ys.size))
-    else
-      xs
-  else
-    ys
-where
-  go (xs ys : Subarray α) (hxs : 0 < xs.size) (hys : 0 < ys.size) (acc : Array α) : Array α :=
-    let x := xs[0]
-    let y := ys[0]
-    if le x y then
-      if hi : 1 < xs.size then
-        go (xs.drop 1) ys (by simp only [Subarray.size_drop]; omega) hys (acc.push x)
-      else
-        ys.foldl (init := acc.push x) (fun acc y => acc.push y)
-    else
-      if hj : 1 < ys.size then
-        go xs (ys.drop 1) hxs (by simp only [Subarray.size_drop]; omega) (acc.push y)
-      else
-        xs.foldl (init := acc.push y) (fun acc x => acc.push x)
-  termination_by xs.size + ys.size
-
-def _root_.Subarray.mergeSort (xs : Subarray α) (le : α → α → Bool := by exact (· ≤ ·)) : Array α :=
-    if h : 1 < xs.size then
-      let splitIdx := (xs.size + 1) / 2 -- We follow the same splitting convention as `List.mergeSort`
-      let left := xs[*...splitIdx]
-      let right := xs[splitIdx...*]
-      MergeSort.merge (mergeSort left le) (mergeSort right le) le
-    else
-      xs
-termination_by xs.size
-decreasing_by
-  · simp only [Subarray.size_mkSlice_rio]; omega
-  · simp only [Subarray.size_mkSlice_rci]; omega
-
-def mergeSort (xs : Array α) (le : α → α → Bool := by exact (· ≤ ·)) : Array α :=
-    xs[*...*].mergeSort le
-
-end Array
-
-theorem Array.MergeSort.merge.go_eq_listMerge {xs ys : Subarray α} {hxs hys le acc} :
-    (Array.MergeSort.merge.go le xs ys hxs hys acc).toList = acc.toList ++ List.merge xs.toList ys.toList le := by
-  fun_induction Array.MergeSort.merge.go le xs ys hxs hys acc
-  · rename_i xs ys _ _ _ _ _ _ _ _
-    rw [List.merge.eq_def]
-    split
-    · have : xs.size = 0 := by simp [← Subarray.length_toList, *]
-      omega
-    · have : ys.size = 0 := by simp [← Subarray.length_toList, *]
-      omega
-    · rename_i x' xs' y' ys' _ _
-      simp +zetaDelta only at *
-      have h₁ : x' = xs[0] := by simp [Subarray.getElem_eq_getElem_toList, *]
-      have h₂ : y' = ys[0] := by simp [Subarray.getElem_eq_getElem_toList, *]
-      cases h₁
-      cases h₂
-      simp [Subarray.toList_drop, *]
-  · rename_i xs ys _ _ _ _ _ _ _
-    rw [List.merge.eq_def]
-    split
-    · have : xs.size = 0 := by simp [← Subarray.length_toList, *]
-      omega
-    · have : ys.size = 0 := by simp [← Subarray.length_toList, *]
-      omega
-    · rename_i x' xs' y' ys' _ _
-      simp +zetaDelta only at *
-      have h₁ : x' = xs[0] := by simp [Subarray.getElem_eq_getElem_toList, *]
-      have h₂ : y' = ys[0] := by simp [Subarray.getElem_eq_getElem_toList, *]
-      cases h₁
-      cases h₂
-      simp [*]
-      have : xs.size = xs'.length + 1 := by simp [← Subarray.length_toList, *]
-      have : xs' = [] := List.eq_nil_of_length_eq_zero (by omega)
-      simp [this]
-      rw [← Subarray.foldl_toList]
-      simp [*]
-  · rename_i xs ys _ _ _ _ _ _ _ _
-    rw [List.merge.eq_def]
-    split
-    · have : xs.size = 0 := by simp [← Subarray.length_toList, *]
-      omega
-    · have : ys.size = 0 := by simp [← Subarray.length_toList, *]
-      omega
-    · rename_i x' xs' y' ys' _ _
-      simp +zetaDelta only at *
-      have h₁ : x' = xs[0] := by simp [Subarray.getElem_eq_getElem_toList, *]
-      have h₂ : y' = ys[0] := by simp [Subarray.getElem_eq_getElem_toList, *]
-      cases h₁
-      cases h₂
-      simp [Subarray.toList_drop, *]
-  · rename_i xs ys _ _ _ _ _ _ _
-    rw [List.merge.eq_def]
-    split
-    · have : xs.size = 0 := by simp [← Subarray.length_toList, *]
-      omega
-    · have : ys.size = 0 := by simp [← Subarray.length_toList, *]
-      omega
-    · rename_i x' xs' y' ys' _ _
-      simp +zetaDelta only at *
-      have h₁ : x' = xs[0] := by simp [Subarray.getElem_eq_getElem_toList, *]
-      have h₂ : y' = ys[0] := by simp [Subarray.getElem_eq_getElem_toList, *]
-      cases h₁
-      cases h₂
-      simp [*]
-      have : ys.size = ys'.length + 1 := by simp [← Subarray.length_toList, *]
-      have : ys' = [] := List.eq_nil_of_length_eq_zero (by omega)
-      simp [this]
-      rw [← Subarray.foldl_toList]
-      simp [*]
-
-theorem Array.MergeSort.merge_eq_listMerge {xs ys : Array α} {le} :
-    (Array.MergeSort.merge xs ys le).toList = List.merge xs.toList ys.toList le := by
-  rw [Array.MergeSort.merge]
-  split <;> rename_i heq₁
-  · split <;> rename_i heq₂
-    · simp [Array.MergeSort.merge.go_eq_listMerge]
-    · have : ys.toList = [] := by simp_all
-      simp [this]
-  · have : xs.toList = [] := by simp_all
-    simp [this]
-
-theorem List.mergeSort_eq_merge_mkSlice {xs : List α} :
-    xs.mergeSort le =
-      if 1 < xs.length then
-        merge (xs[*...((xs.length + 1) / 2)].toList.mergeSort le) (xs[((xs.length + 1) / 2)...*].toList.mergeSort le) le
-      else
-        xs := by
-  fun_cases xs.mergeSort le
-  · simp
-  · simp
-  · rename_i x y ys lr hl hr
-    simp [lr]
-
-theorem Subarray.toList_mergeSort {xs : Subarray α} {le : α → α → Bool} :
-    (xs.mergeSort le).toList = xs.toList.mergeSort le := by
-  fun_induction xs.mergeSort le
-  · rw [List.mergeSort_eq_merge_mkSlice]
-    simp +zetaDelta [Array.MergeSort.merge_eq_listMerge, *]
-  · simp [List.mergeSort_eq_merge_mkSlice, *]
-
-theorem Array.toList_mergeSort {xs : Array α} {le : α → α → Bool} :
-    (xs.mergeSort le).toList = xs.toList.mergeSort le := by
-  rw [Array.mergeSort, Subarray.toList_mergeSort, Array.toList_mkSlice_rii]
-
 theorem Nat.eq_add_of_toList_rio_eq_append_cons {a : Nat} {pref cur suff}
     (h : (*...a).toList = pref ++ cur :: suff) :
     cur = pref.length := by
   have := Rio.eq_succMany?_of_toList_eq_append_cons h
   simpa [PRange.UpwardEnumerable.least, PRange.least?] using this
 
-@[simp, grind =]
-theorem Array.size_mergeSort {xs : Array α} :
-    (xs.mergeSort le).size = xs.size := by
-  rw [← length_toList, Array.toList_mergeSort, List.length_mergeSort, length_toList]
-
-theorem Array.mergeSort_perm {xs : Array α} :
-    (xs.mergeSort le).Perm xs := by
-  simpa only [perm_iff_toList_perm, Array.toList_mergeSort] using List.mergeSort_perm _ _
-
-theorem Array.pairwise_mergeSort
-    (trans : ∀ (a b c : α), le a b → le b c → le a c)
-    (total : ∀ (a b : α), le a b || le b a) :
-    (l : Array α) → (mergeSort l le).toList.Pairwise (le · ·) := by
-  intro xs
-  simpa [toList_mergeSort] using List.pairwise_mergeSort trans total _
-
-attribute [simp, grind =] Rio.mem_iff
-
 /-!
 ## Implementation
 -/
diff --git a/HumanEvalLean/HumanEval20.lean b/HumanEvalLean/HumanEval20.lean
index 8a577fc..9477329 100644
--- a/HumanEvalLean/HumanEval20.lean
+++ b/HumanEvalLean/HumanEval20.lean
@@ -15,8 +15,8 @@ public section
 increasing order.
 -/
 def findClosestElements (xs : Array Rat) (h : 2 ≤ xs.size := by grind) : Rat × Rat := Id.run do
-  let sorted := xs.toList.mergeSort.toArray
-  have : 2 ≤ sorted.size := by grind [List.length_mergeSort]
+  let sorted := xs.mergeSort
+  have : 2 ≤ sorted.size := by grind [Array.size_mergeSort]
   let mut closest := (sorted[0], sorted[1])
   for hi : i in 1...(sorted.size - 1) do
     if (sorted[i + 1] - sorted[i]).abs < (closest.2 - closest.1).abs then
@@ -33,8 +33,6 @@ example : findClosestElements #[(1.1 : Rat), 2.2, 3.1, 4.1, 5.1] = (2.2, 3.1) :=
 
 /-! ## Missing API -/
 
--- TODO: As soon as `Array.mergeSort` is merged, use that one.
-
 theorem Nat.eq_add_of_toList_rco_eq_append_cons {a b : Nat} {pref cur suff}
     (h : (a...b).toList = pref ++ cur :: suff) :
     cur = a + pref.length := by
@@ -54,11 +52,11 @@ theorem sorted_findClosestElements {xs : Array Rat} {h : 2 ≤ xs.size} :
   invariants
   · ⇓⟨cur, closest⟩ => ⌜closest.1 ≤ closest.2⌝
   case vc1 sorted _ _ _ _ _ _ _ _ _ =>
-    have : sorted.toList.Pairwise (· ≤ ·) := by grind [List.pairwise_mergeSort]
+    have : sorted.toList.Pairwise (· ≤ ·) := by grind [Array.pairwise_mergeSort]
     simp only [List.pairwise_iff_getElem] at this
     grind
   case vc3 sorted _ _ =>
-    have : sorted.toList.Pairwise (· ≤ ·) := by grind [List.pairwise_mergeSort]
+    have : sorted.toList.Pairwise (· ≤ ·) := by grind [Array.pairwise_mergeSort]
     simp only [List.pairwise_iff_getElem] at this
     grind
 
@@ -69,8 +67,8 @@ The elements of the pair `findClosestElements xs` are located in two distinct po
 theorem exists_mem_findClosestElements {xs : Array Rat} {h : 2 ≤ xs.size} :
     ∃ (i j : Nat) (hi : i < xs.size) (hj : j < xs.size) (_hij : i ≠ j),
       findClosestElements xs = (xs[i], xs[j]) := by
-  suffices h' : ¬ xs.toList.mergeSort.Pairwise (fun x y => ¬ (findClosestElements xs = (x, y) ∨  findClosestElements xs = (y, x))) by
-    have := xs.toList.mergeSort_perm (· ≤ ·)
+  suffices h' : ¬ xs.mergeSort.toList.Pairwise (fun x y => ¬ (findClosestElements xs = (x, y) ∨  findClosestElements xs = (y, x))) by
+    have := xs.mergeSort_perm (le := (· ≤ ·))
     rw [this.pairwise_iff (by grind)] at h'
     grind [List.pairwise_iff_getElem]
   generalize hwp : findClosestElements xs = wp
@@ -79,9 +77,9 @@ theorem exists_mem_findClosestElements {xs : Array Rat} {h : 2 ≤ xs.size} :
   invariants
   | inv1 sorted _ _ => ⇓⟨cur, closest⟩ => ⌜∃ (i j : Nat) (hi : i < sorted.size) (hj : j < sorted.size) (hij : i ≠ j),
         closest = (sorted[i], sorted[j])⌝
-  case vc1 => grind [List.length_mergeSort, List.pairwise_iff_getElem]
+  case vc1 => grind [List.pairwise_iff_getElem]
   case vc3 => exact ⟨0, 1, by grind⟩
-  case vc4 => grind [List.length_mergeSort, List.pairwise_iff_getElem]
+  case vc4 => grind [List.pairwise_iff_getElem]
 
 /--
 This lemma is an intermediate step towards `pairwise_abs_findClosestElements_le`.
@@ -91,7 +89,7 @@ distance of any two consecutive elements in the *sorted* array.
 -/
 private theorem abs_findClosestElements_le_mergeSort {xs : Array Rat} {h : 2 ≤ xs.size} :
     letI closest := findClosestElements xs
-    letI sorted := xs.toList.mergeSort.toArray
+    letI sorted := xs.mergeSort
     ∀ (i : Nat) (hi : i + 1 < sorted.size),
       (closest.2 - closest.1).abs ≤ (sorted[i + 1] - sorted[i]).abs := by
   generalize hwp : findClosestElements xs = wp
@@ -109,7 +107,7 @@ private theorem abs_findClosestElements_le_mergeSort {xs : Array Rat} {h : 2 ≤
     by_cases i < cur <;> grind
   case vc3 => grind
   case vc4 h =>
-    simp +zetaDelta only [List.getElem!_toArray, List.getElem!_eq_getElem?_getD] at h
+    simp +zetaDelta only [Array.getElem!_eq_getD, Array.getD_eq_getD_getElem?] at h
     grind [Nat.length_toList_rco]
 
 /--
@@ -121,11 +119,11 @@ is at least as large as the distance between the components of `findClosestEleme
 theorem pairwise_abs_findClosestElements_le {xs : Array Rat} {h : 2 ≤ xs.size} :
     letI closest := findClosestElements xs
     xs.toList.Pairwise (fun x y => (closest.2 - closest.1).abs ≤ (y - x).abs) := by
-  have := xs.toList.mergeSort_perm (· ≤ ·)
+  have := xs.mergeSort_perm (le := (· ≤ ·))
   rw [← this.pairwise_iff (by grind [Rat.abs_sub_comm]), List.pairwise_iff_getElem]
   intro i j hi hj hij
   have := abs_findClosestElements_le_mergeSort (xs := xs) (h := h) i (by grind)
-  have h_sorted := xs.toList.pairwise_mergeSort (le := (· ≤ ·)) (by grind) (by grind)
+  have h_sorted := xs.pairwise_mergeSort (le := (· ≤ ·)) (by grind) (by grind)
   grind [List.pairwise_iff_getElem, Rat.abs_of_nonneg]
 
 /-!
diff --git a/HumanEvalLean/HumanEval47.lean b/HumanEvalLean/HumanEval47.lean
index 9ae9c72..b311a86 100644
--- a/HumanEvalLean/HumanEval47.lean
+++ b/HumanEvalLean/HumanEval47.lean
@@ -4,13 +4,9 @@ module
 
 public section
 
-@[grind =]
-def Array.mergeSort (xs : Array Int) : Array Int :=
-  xs.toList.mergeSort.toArray
-
 def median (xs : Array Int) (h : xs ≠ #[]) : Rat :=
   let sorted := xs.mergeSort
-  have : 0 < sorted.size := by grind [List.length_mergeSort]
+  have : 0 < sorted.size := by grind [Array.size_mergeSort]
   if xs.size % 2 = 1 then
     sorted[sorted.size / 2]
   else
@@ -27,14 +23,14 @@ example : median #[8, 1, 3, 9, 9, 2, 7] (by decide) = 7 := by native_decide
 /-! ## Verification -/
 
 theorem median_eq_getElem_of_odd {xs : Array Int} {h} (h' : xs.size % 2 = 1) :
-    median xs h = xs.mergeSort[xs.size / 2]'(by grind [List.length_mergeSort]) := by
-  grind [median, List.length_mergeSort]
+    median xs h = xs.mergeSort[xs.size / 2]'(by grind [Array.size_mergeSort]) := by
+  grind [median, Array.size_mergeSort]
 
 theorem two_mul_median_of_even {xs : Array Int} {h} (h' : xs.size % 2 = 0) :
     2 * median xs h =
-      xs.mergeSort[xs.size / 2 - 1]'(by grind [List.length_mergeSort]) +
-      xs.mergeSort[xs.size / 2]'(by grind [List.length_mergeSort]) := by
-  grind [median, List.length_mergeSort]
+      xs.mergeSort[xs.size / 2 - 1]'(by grind [Array.size_mergeSort]) +
+      xs.mergeSort[xs.size / 2]'(by grind [Array.size_mergeSort]) := by
+  grind [median, Array.size_mergeSort]
 
 /-!
 ### MergeSort properties
@@ -43,10 +39,10 @@ The following two library lemmas show that `Array.mergeSort` correctly sorts an
 -/
 
 example {xs : Array Int} : xs.mergeSort.toList.Pairwise (· ≤ ·) := by
-  grind [List.pairwise_mergeSort]
+  grind [Array.pairwise_mergeSort]
 
 example {xs : Array Int} : xs.mergeSort.Perm xs := by
-  grind [List.mergeSort_perm, Array.Perm]
+  grind [Array.mergeSort_perm, Array.Perm]
 
 /-!
 ## Prompt
diff --git a/lean-toolchain b/lean-toolchain
index fd31525..388919a 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-03-05
+leanprover/lean4:nightly-2026-03-07