diff --git a/Std/Data/Array/Basic.lean b/Std/Data/Array/Basic.lean
index c000df3524..5570b51f8c 100644
--- a/Std/Data/Array/Basic.lean
+++ b/Std/Data/Array/Basic.lean
@@ -155,11 +155,11 @@ namespace Subarray
 The empty subarray.
 -/
 protected def empty : Subarray α where
-  as := #[]
+  array := #[]
   start := 0
   stop := 0
-  h₁ := Nat.le_refl 0
-  h₂ := Nat.le_refl 0
+  start_le_stop := Nat.le_refl 0
+  stop_le_array_size := Nat.le_refl 0
 
 instance : EmptyCollection (Subarray α) :=
   ⟨Subarray.empty⟩
@@ -192,7 +192,7 @@ def popHead? (as : Subarray α) : Option (α × Subarray α) :=
       let tail :=
         { as with
           start := as.start + 1
-          h₁ := Nat.le_of_lt_succ $ Nat.succ_lt_succ h  }
+          start_le_stop := Nat.le_of_lt_succ $ Nat.succ_lt_succ h  }
       some (head, tail)
     else
       none
diff --git a/lean-toolchain b/lean-toolchain
index b12b17b955..5f75567a01 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-04-12
+leanprover/lean4-pr-releases:pr-release-3851