diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index 08738ae2a8..1cc925fcf1 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -7,7 +7,7 @@ module
 
 prelude
 public import Init.Data.Array.Basic
-public import Init.Data.Slice.Basic
+public import Init.Data.Slice.Operations
 
 public section
 
@@ -76,15 +76,17 @@ def Subarray.stop_le_array_size (xs : Subarray α) : xs.stop ≤ xs.array.size :
 
 namespace Subarray
 
-/--
-Computes the size of the subarray.
--/
-def size (s : Subarray α) : Nat :=
-  s.stop - s.start
+instance : SliceSize (Internal.SubarrayData α) where
+  size s := s.internalRepresentation.stop - s.internalRepresentation.start
+
+@[grind =, suggest_for Subarray.size]
+public theorem size_eq {xs : Subarray α} :
+    xs.size = xs.stop - xs.start := by
+  simp [Std.Slice.size, SliceSize.size, start, stop]
 
 theorem size_le_array_size {s : Subarray α} : s.size ≤ s.array.size := by
   let ⟨{array, start, stop, start_le_stop, stop_le_array_size}⟩ := s
-  simp only [size, ge_iff_le]
+  simp only [ge_iff_le, size_eq]
   apply Nat.le_trans (Nat.sub_le stop start)
   assumption
 
diff --git a/src/Init/Data/Slice/Array/Iterator.lean b/src/Init/Data/Slice/Array/Iterator.lean
index f566abdbf6..2412081f79 100644
--- a/src/Init/Data/Slice/Array/Iterator.lean
+++ b/src/Init/Data/Slice/Array/Iterator.lean
@@ -62,9 +62,6 @@ attribute [instance] Subarray.instToIterator
 
 universe v w
 
-instance : SliceSize (Internal.SubarrayData α) where
-  size s := s.internalRepresentation.stop - s.internalRepresentation.start
-
 instance {α : Type u} {m : Type v → Type w} [Monad m] : ForIn m (Subarray α) α :=
   inferInstance
 
@@ -76,45 +73,6 @@ explicitly provide the wrapper function `Subarray.foldlM` for `Slice.foldlM`, pr
 specific docstring.
 -/
 
-/--
-Folds a monadic operation from left to right over the elements in a subarray.
-An accumulator of type `β` is constructed by starting with `init` and monadically combining each
-element of the subarray with the current accumulator value in turn. The monad in question may permit
-early termination or repetition.
-Examples:
-```lean example
-#eval #["red", "green", "blue"].toSubarray.foldlM (init := "") fun acc x => do
-  let l ← Option.guard (· ≠ 0) x.length
-  return s!"{acc}({l}){x} "
-```
-```output
-some "(3)red (5)green (4)blue "
-```
-```lean example
-#eval #["red", "green", "blue"].toSubarray.foldlM (init := 0) fun acc x => do
-  let l ← Option.guard (· ≠ 5) x.length
-  return s!"{acc}({l}){x} "
-```
-```output
-none
-```
--/
-@[inline]
-def Subarray.foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (as : Subarray α) : m β :=
-  Slice.foldlM f (init := init) as
-
-/--
-Folds an operation from left to right over the elements in a subarray.
-An accumulator of type `β` is constructed by starting with `init` and combining each
-element of the subarray with the current accumulator value in turn.
-Examples:
- * `#["red", "green", "blue"].toSubarray.foldl (· + ·.length) 0 = 12`
- * `#["red", "green", "blue"].toSubarray.popFront.foldl (· + ·.length) 0 = 9`
--/
-@[inline]
-def Subarray.foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) (as : Subarray α) : β :=
-  Slice.foldl f (init := init) as
-
 /--
 The implementation of `ForIn.forIn` for `Subarray`, which allows it to be used with `for` loops in
 `do`-notation.
@@ -126,16 +84,12 @@ def Subarray.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
 /--
 Allocates a new array that contains the contents of the subarray.
 -/
-@[coe]
-def Subarray.toArray (s : Subarray α) : Array α :=
+@[expose, coe]
+def Subarray.copy (s : Subarray α) : Array α :=
   Slice.toArray s
 
 instance instCoeSubarrayArray : Coe (Subarray α) (Array α) :=
-  ⟨Subarray.toArray⟩
-
-@[inherit_doc Subarray.toArray]
-def Subarray.copy (s : Subarray α) : Array α :=
-  Slice.toArray s
+  ⟨Subarray.copy⟩
 
 @[simp]
 theorem Subarray.copy_eq_toArray {s : Subarray α} :
@@ -149,7 +103,7 @@ theorem Subarray.sliceToArray_eq_toArray {s : Subarray α} :
 
 namespace Array
 
-@[inherit_doc Subarray.toArray]
+@[inherit_doc Subarray.copy]
 def ofSubarray (s : Subarray α) : Array α :=
   Slice.toArray s
 
diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean
index 680ba83638..6194119bea 100644
--- a/src/Init/Data/Slice/Array/Lemmas.lean
+++ b/src/Init/Data/Slice/Array/Lemmas.lean
@@ -121,7 +121,7 @@ public instance : LawfulSliceSize (Internal.SubarrayData α) where
 
 public theorem toArray_eq_sliceToArray {α : Type u} {s : Subarray α} :
     s.toArray = Slice.toArray s := by
-  simp [Subarray.toArray]
+  simp [Std.Slice.toArray]
 
 @[simp]
 public theorem forIn_toList {α : Type u} {s : Subarray α}
@@ -156,11 +156,11 @@ public theorem sliceFoldl_eq_foldl {α : Type u} {s : Subarray α} {f : β → 
 public theorem foldlM_toList {m} [Monad m] {α : Type u} {s : Subarray α} {f}
     [LawfulMonad m] :
     s.toList.foldlM (init := init) f = s.foldlM (m := m) (init := init) f := by
-  simp [Std.Slice.foldlM_toList, sliceFoldlM_eq_foldlM]
+  simp [Std.Slice.foldlM_toList]
 
 public theorem foldl_toList {α : Type u} {s : Subarray α} {f} :
     s.toList.foldl (init := init) f = s.foldl (init := init) f := by
-  simp [Std.Slice.foldl_toList, sliceFoldl_eq_foldl]
+  simp [Std.Slice.foldl_toList]
 
 end Subarray
 
@@ -251,21 +251,16 @@ public theorem Subarray.toList_eq_drop_take {xs : Subarray α} :
     xs.toList = (xs.array.toList.take xs.stop).drop xs.start := by
   rw [Subarray.toList_eq, Array.toList_extract, Std.Internal.List.extract_eq_drop_take']
 
-@[grind =]
-public theorem Subarray.size_eq {xs : Subarray α} :
-    xs.size = xs.stop - xs.start := by
-  simp [Subarray.size]
-
 @[simp, grind =]
 public theorem Subarray.size_drop {xs : Subarray α} :
     (xs.drop i).size = xs.size - i := by
-  simp only [size, stop, drop, start]
+  simp only [size_eq, stop, drop, start]
   omega
 
 @[simp, grind =]
 public theorem Subarray.size_take {xs : Subarray α} :
     (xs.take i).size = min i xs.size := by
-  simp only [size, stop, take, start]
+  simp only [size_eq, stop, take, start]
   omega
 
 public theorem Subarray.sliceSize_eq_size {xs : Subarray α} :
@@ -273,7 +268,7 @@ public theorem Subarray.sliceSize_eq_size {xs : Subarray α} :
   rfl
 
 public theorem Subarray.getElem_eq_getElem_array {xs : Subarray α} {h : i < xs.size} :
-    xs[i] = xs.array[xs.start + i]'(by simp only [size] at h; have := xs.stop_le_array_size; omega) := by
+    xs[i] = xs.array[xs.start + i]'(by simp only [size_eq] at h; have := xs.stop_le_array_size; omega) := by
   rfl
 
 public theorem Subarray.getElem_toList {xs : Subarray α} {h : i < xs.toList.length} :
@@ -297,24 +292,24 @@ public theorem Subarray.toList_take {xs : Subarray α} :
 @[simp, grind =]
 public theorem Subarray.toArray_toList {xs : Subarray α} :
     xs.toList.toArray = xs.toArray := by
-  simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
+  simp [Std.Slice.toList, Std.Slice.toArray, Std.Slice.toArray]
 
 @[simp, grind =]
 public theorem Subarray.toList_toArray {xs : Subarray α} :
     xs.toArray.toList = xs.toList := by
-  simp [Std.Slice.toList, Subarray.toArray, Std.Slice.toArray]
+  simp [Std.Slice.toList, Std.Slice.toArray, Std.Slice.toArray]
 
 @[simp, grind =]
 public theorem Subarray.length_toList {xs : Subarray α} :
     xs.toList.length = xs.size := by
   have : xs.start ≤ xs.stop := xs.internalRepresentation.start_le_stop
   have : xs.stop ≤ xs.array.size := xs.internalRepresentation.stop_le_array_size
-  simp [Subarray.toList_eq, Subarray.size]; omega
+  simp [Subarray.toList_eq, Subarray.size_eq]; omega
 
 @[simp, grind =]
 public theorem Subarray.size_toArray {xs : Subarray α} :
     xs.toArray.size = xs.size := by
-  simp [← Subarray.toArray_toList, Subarray.size, Slice.size, SliceSize.size, start, stop]
+  simp [← Subarray.toArray_toList, Subarray.size_eq, start, stop]
 
 namespace Array
 
@@ -708,7 +703,7 @@ public theorem toList_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     Array.start_toSubarray, Array.stop_toSubarray, Array.toList_extract, List.take_drop,
     List.take_take]
   rw [Nat.add_sub_cancel' (by omega)]
-  simp [Subarray.size, ← Array.length_toList, ← List.take_eq_take_min, Nat.add_comm xs.start]
+  simp [Subarray.size_eq, ← Array.length_toList, ← List.take_eq_take_min, Nat.add_comm xs.start]
 
 @[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
@@ -718,7 +713,7 @@ public theorem toArray_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     xs[lo...hi].size = min hi xs.size - lo := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     xs[lo...=hi] = xs[lo...(hi + 1)] := by
@@ -738,7 +733,7 @@ public theorem toArray_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
     xs[lo...=hi].size = min (hi + 1) xs.size - lo := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_rci_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} :
     xs[lo...*] = xs[lo...xs.size] := by
@@ -758,7 +753,7 @@ public theorem toArray_mkSlice_rci {xs : Subarray α} {lo : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_rci {xs : Subarray α} {lo : Nat} :
     xs[lo...*].size = xs.size - lo := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_roc_eq_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[lo<...(hi + 1)] := by
@@ -787,7 +782,7 @@ public theorem toArray_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...hi].size = min hi xs.size - (lo + 1) := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_roc_eq_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[(lo + 1)...=hi] := by
@@ -806,7 +801,7 @@ public theorem toArray_mkSlice_roc {xs : Subarray α} {lo hi : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_roc {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...=hi].size = min (hi + 1) xs.size - (lo + 1) := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_roi_eq_mkSlice_rci {xs : Subarray α} {lo : Nat} :
     xs[lo<...*] = xs[(lo + 1)...*] := by
@@ -830,7 +825,7 @@ public theorem toArray_mkSlice_roi {xs : Subarray α} {lo : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_roi {xs : Subarray α} {lo : Nat} :
     xs[lo<...*].size = xs.size - (lo + 1) := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_ric_eq_mkSlice_rio {xs : Subarray α} {hi : Nat} :
     xs[*...=hi] = xs[*...(hi + 1)] := by
@@ -859,7 +854,7 @@ public theorem toArray_mkSlice_rio {xs : Subarray α} {hi : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_rio {xs : Subarray α} {hi : Nat} :
     xs[*...hi].size = min hi xs.size := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 public theorem mkSlice_ric_eq_mkSlice_rcc {xs : Subarray α} {hi : Nat} :
     xs[*...=hi] = xs[0...=hi] := by
@@ -880,7 +875,7 @@ public theorem toArray_mkSlice_ric {xs : Subarray α} {hi : Nat} :
 @[simp, grind =]
 public theorem size_mkSlice_ric {xs : Subarray α} {hi : Nat} :
     xs[*...=hi].size = min (hi + 1) xs.size := by
-  simp [← Subarray.length_toList]
+  simp [← length_toList, - length_toList_eq_size]
 
 @[simp, grind =, grind =]
 public theorem mkSlice_rii {xs : Subarray α} :
diff --git a/src/Init/Data/Slice/Operations.lean b/src/Init/Data/Slice/Operations.lean
index b790424b16..03b047bba7 100644
--- a/src/Init/Data/Slice/Operations.lean
+++ b/src/Init/Data/Slice/Operations.lean
@@ -51,12 +51,12 @@ Returns the number of elements with distinct indices in the given slice.
 
 Example: `#[1, 1, 1][0...2].size = 2`.
 -/
-@[always_inline, inline]
+@[expose, always_inline, inline, suggest_for Subarray.size]
 def size (s : Slice γ) [SliceSize γ] :=
   SliceSize.size s
 
 /-- Allocates a new array that contains the elements of the slice. -/
-@[always_inline, inline]
+@[always_inline, inline, suggest_for Subarray.toArray]
 def toArray [ToIterator (Slice γ) Id α β] [Iterator α Id β]
     (s : Slice γ) : Array β :=
   Internal.iter s |>.toArray
@@ -103,7 +103,7 @@ some "(3)red (5)green (4)blue "
 none
 ```
 -/
-@[always_inline, inline]
+@[always_inline, inline, suggest_for Subarray.foldlM]
 def foldlM {γ : Type u} {β : Type v}
     {δ : Type w} {m : Type w → Type w'} [Monad m] (f : δ → β → m δ) (init : δ)
     [ToIterator (Slice γ) Id α β] [Iterator α Id β]
@@ -119,7 +119,7 @@ Examples for the special case of subarrays:
  * `#["red", "green", "blue"].toSubarray.foldl (· + ·.length) 0 = 12`
  * `#["red", "green", "blue"].toSubarray.popFront.foldl (· + ·.length) 0 = 9`
 -/
-@[always_inline, inline]
+@[always_inline, inline, suggest_for Subarray.foldl]
 def foldl {γ : Type u} {β : Type v}
     {δ : Type w} (f : δ → β → δ) (init : δ)
     [ToIterator (Slice γ) Id α β] [Iterator α Id β]