diff --git a/CODEOWNERS b/CODEOWNERS
index 4c58ab23c70b..9e97a85a616b 100644
--- a/CODEOWNERS
+++ b/CODEOWNERS
@@ -39,3 +39,5 @@
 /src/Lean/Elab/Tactic/Guard.lean @digama0
 /src/Init/Guard.lean @digama0
 /src/Lean/Server/CodeActions/ @digama0
+/src/Init/Data/Array/Subarray.lean @david-christiansen
+
diff --git a/RELEASES.md b/RELEASES.md
index ef21b2fce362..1308ddc1277c 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -112,6 +112,8 @@ fact.def :
 
 * The coercion from `String` to `Name` was removed. Previously, it was `Name.mkSimple`, which does not separate strings at dots, but experience showed that this is not always the desired coercion. For the previous behavior, manually insert a call to `Name.mkSimple`.
 
+* The `Subarray` fields `as`, `h₁` and `h₂` have been renamed to `array`, `start_le_stop`, and `stop_le_array_size`, respectively. This more closely follows standard Lean conventions. Deprecated aliases for the field projects were added; these will be removed in a future release.
+
 v4.7.0
 ---------
 
diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index 4ae0daf73ca9..b57d8eaace9f 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -9,11 +9,20 @@ import Init.Data.Array.Basic
 universe u v w
 
 structure Subarray (α : Type u)  where
-  as : Array α
+  array : Array α
   start : Nat
   stop : Nat
-  h₁ : start ≤ stop
-  h₂ : stop ≤ as.size
+  start_le_stop : start ≤ stop
+  stop_le_array_size : stop ≤ array.size
+
+@[deprecated Subarray.array]
+abbrev Subarray.as (s : Subarray α) : Array α := s.array
+
+@[deprecated Subarray.start_le_stop]
+theorem Subarray.h₁ (s : Subarray α) : s.start ≤ s.stop := s.start_le_stop
+
+@[deprecated Subarray.stop_le_array_size]
+theorem Subarray.h₂ (s : Subarray α) : s.stop ≤ s.as.size := s.stop_le_array_size
 
 namespace Subarray
 
@@ -21,13 +30,13 @@ def size (s : Subarray α) : Nat :=
   s.stop - s.start
 
 def get (s : Subarray α) (i : Fin s.size) : α :=
-  have : s.start + i.val < s.as.size := by
-   apply Nat.lt_of_lt_of_le _ s.h₂
+  have : s.start + i.val < s.array.size := by
+   apply Nat.lt_of_lt_of_le _ s.stop_le_array_size
    have := i.isLt
    simp [size] at this
    rw [Nat.add_comm]
    exact Nat.add_lt_of_lt_sub this
-  s.as[s.start + i.val]
+  s.array[s.start + i.val]
 
 instance : GetElem (Subarray α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get ⟨i, h⟩
@@ -42,7 +51,7 @@ abbrev get! [Inhabited α] (s : Subarray α) (i : Nat) : α :=
 
 def popFront (s : Subarray α) : Subarray α :=
   if h : s.start < s.stop then
-    { s with start := s.start + 1, h₁ := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) }
+    { s with start := s.start + 1, start_le_stop := Nat.le_of_lt_succ (Nat.add_lt_add_right h 1) }
   else
     s
 
@@ -50,7 +59,7 @@ def popFront (s : Subarray α) : Subarray α :=
   let sz := USize.ofNat s.stop
   let rec @[specialize] loop (i : USize) (b : β) : m β := do
     if i < sz then
-      let a := s.as.uget i lcProof
+      let a := s.array.uget i lcProof
       match (← f a b) with
       | ForInStep.done  b => pure b
       | ForInStep.yield b => loop (i+1) b
@@ -68,27 +77,27 @@ instance : ForIn m (Subarray α) α where
 
 @[inline]
 def foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Subarray α) : m β :=
-  as.as.foldlM f (init := init) (start := as.start) (stop := as.stop)
+  as.array.foldlM f (init := init) (start := as.start) (stop := as.stop)
 
 @[inline]
 def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (as : Subarray α) : m β :=
-  as.as.foldrM f (init := init) (start := as.stop) (stop := as.start)
+  as.array.foldrM f (init := init) (start := as.stop) (stop := as.start)
 
 @[inline]
 def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m Bool :=
-  as.as.anyM p (start := as.start) (stop := as.stop)
+  as.array.anyM p (start := as.start) (stop := as.stop)
 
 @[inline]
 def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Subarray α) : m Bool :=
-  as.as.allM p (start := as.start) (stop := as.stop)
+  as.array.allM p (start := as.start) (stop := as.stop)
 
 @[inline]
 def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnit :=
-  as.as.forM f (start := as.start) (stop := as.stop)
+  as.array.forM f (start := as.start) (stop := as.stop)
 
 @[inline]
 def forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Subarray α) : m PUnit :=
-  as.as.forRevM f (start := as.stop) (stop := as.start)
+  as.array.forRevM f (start := as.stop) (stop := as.start)
 
 @[inline]
 def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β :=
@@ -135,15 +144,25 @@ variable {α : Type u}
 
 def toSubarray (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Subarray α :=
   if h₂ : stop ≤ as.size then
-     if h₁ : start ≤ stop then
-       { as := as, start := start, stop := stop, h₁ := h₁, h₂ := h₂ }
-     else
-       { as := as, start := stop, stop := stop, h₁ := Nat.le_refl _, h₂ := h₂ }
+    if h₁ : start ≤ stop then
+      { array := as, start := start, stop := stop,
+        start_le_stop := h₁, stop_le_array_size := h₂ }
+    else
+      { array := as, start := stop, stop := stop,
+        start_le_stop := Nat.le_refl _, stop_le_array_size := h₂ }
   else
-     if h₁ : start ≤ as.size then
-       { as := as, start := start, stop := as.size, h₁ := h₁, h₂ := Nat.le_refl _ }
-     else
-       { as := as, start := as.size, stop := as.size, h₁ := Nat.le_refl _, h₂ := Nat.le_refl _ }
+    if h₁ : start ≤ as.size then
+      { array := as,
+        start := start,
+        stop := as.size,
+        start_le_stop := h₁,
+        stop_le_array_size := Nat.le_refl _ }
+    else
+      { array := as,
+        start := as.size,
+        stop := as.size,
+        start_le_stop := Nat.le_refl _,
+        stop_le_array_size := Nat.le_refl _ }
 
 @[coe]
 def ofSubarray (s : Subarray α) : Array α := Id.run do
diff --git a/src/Init/Data/Stream.lean b/src/Init/Data/Stream.lean
index 2eb2fb5143c7..f045327471fc 100644
--- a/src/Init/Data/Stream.lean
+++ b/src/Init/Data/Stream.lean
@@ -94,7 +94,8 @@ instance : Stream (Subarray α) α where
   next? s :=
     if h : s.start < s.stop then
       have : s.start + 1 ≤ s.stop := Nat.succ_le_of_lt h
-      some (s.as.get ⟨s.start, Nat.lt_of_lt_of_le h s.h₂⟩, { s with start := s.start + 1, h₁ := this })
+      some (s.as.get ⟨s.start, Nat.lt_of_lt_of_le h s.stop_le_array_size⟩,
+        { s with start := s.start + 1, start_le_stop := this })
     else
       none