From 4af9cc05924d81e1d5dd35105fdce007c5bbc2e8 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Thu, 15 Jan 2026 17:43:10 +0100
Subject: [PATCH] feat: add `grind` annotations for list and array slices
 (#11993)

This PR adds `grind` annotations to the lemmas about `Subarray` and
`ListSlice`.
---
 src/Init/Data/Slice/Array/Iterator.lean |   1 +
 src/Init/Data/Slice/Array/Lemmas.lean   | 112 ++++++++++++++-------
 src/Init/Data/Slice/List/Lemmas.lean    | 124 ++++++++++++++++++++----
 tests/lean/run/slice.lean               |  37 +++++++
 4 files changed, 221 insertions(+), 53 deletions(-)

diff --git a/src/Init/Data/Slice/Array/Iterator.lean b/src/Init/Data/Slice/Array/Iterator.lean
index 9f2728b8f7..ddfd7ce8a4 100644
--- a/src/Init/Data/Slice/Array/Iterator.lean
+++ b/src/Init/Data/Slice/Array/Iterator.lean
@@ -148,6 +148,7 @@ theorem Subarray.copy_eq_toArray {s : Subarray α} :
     s.copy = s.toArray :=
   (rfl)
 
+@[grind =]
 theorem Subarray.sliceToArray_eq_toArray {s : Subarray α} :
     Slice.toArray s = s.toArray :=
   (rfl)
diff --git a/src/Init/Data/Slice/Array/Lemmas.lean b/src/Init/Data/Slice/Array/Lemmas.lean
index 8ad92f8329..dd8e1bfbf4 100644
--- a/src/Init/Data/Slice/Array/Lemmas.lean
+++ b/src/Init/Data/Slice/Array/Lemmas.lean
@@ -119,6 +119,13 @@ public theorem forIn_toList {α : Type u} {s : Subarray α}
     ForIn.forIn s.toList init f = ForIn.forIn s init f :=
   Slice.forIn_toList
 
+@[grind =]
+public theorem forIn_eq_forIn_toList {α : Type u} {s : Subarray α}
+    {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
+    {f : α → γ → m (ForInStep γ)} :
+    ForIn.forIn s init f = ForIn.forIn s.toList init f :=
+  forIn_toList.symm
+
 @[simp]
 public theorem forIn_toArray {α : Type u} {s : Subarray α}
     {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ}
@@ -167,22 +174,22 @@ public theorem Array.toSubarray_eq_min {xs : Array α} {lo hi : Nat} :
   simp only [Array.toSubarray]
   split <;> split <;> simp [Nat.min_eq_right (Nat.le_of_not_ge _), *]
 
-@[simp]
+@[simp, grind =]
 public theorem Array.array_toSubarray {xs : Array α} {lo hi : Nat} :
     (xs.toSubarray lo hi).array = xs := by
   simp [toSubarray_eq_min, Subarray.array]
 
-@[simp]
+@[simp, grind =]
 public theorem Array.start_toSubarray {xs : Array α} {lo hi : Nat} :
     (xs.toSubarray lo hi).start = min lo (min hi xs.size) := by
   simp [toSubarray_eq_min, Subarray.start]
 
-@[simp]
+@[simp, grind =]
 public theorem Array.stop_toSubarray {xs : Array α} {lo hi : Nat} :
     (xs.toSubarray lo hi).stop = min hi xs.size := by
   simp [toSubarray_eq_min, Subarray.stop]
 
-theorem Subarray.toList_eq {xs : Subarray α} :
+public theorem Subarray.toList_eq {xs : Subarray α} :
     xs.toList = (xs.array.extract xs.start xs.stop).toList := by
   let aslice := xs
   obtain ⟨⟨array, start, stop, h₁, h₂⟩⟩ := xs
@@ -199,45 +206,46 @@ theorem Subarray.toList_eq {xs : Subarray α} :
       simp [Subarray.array, Subarray.start, Subarray.stop]
   simp [this, ListSlice.toList_eq, lslice]
 
+@[grind =]
 public theorem Subarray.size_eq {xs : Subarray α} :
     xs.size = xs.stop - xs.start := by
   simp [Subarray.size]
 
-@[simp]
+@[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]
+@[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]
+@[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]
+@[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]
 
 namespace Array
 
-@[simp]
+@[simp, grind =]
 public theorem array_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...hi].array = xs := by
   simp [Std.Rco.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
 
-@[simp]
+@[simp, grind =]
 public theorem start_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...hi].start = min lo (min hi xs.size) := by
   simp [Std.Rco.Sliceable.mkSlice]
 
-@[simp]
+@[simp, grind =]
 public theorem stop_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...hi].stop = min hi xs.size := by
   simp [Std.Rco.Sliceable.mkSlice]
@@ -246,14 +254,14 @@ public theorem mkSlice_rco_eq_mkSlice_rco_min {xs : Array α} {lo hi : Nat} :
     xs[lo...hi] = xs[(min lo (min hi xs.size))...(min hi xs.size)] := by
   simp [Std.Rco.Sliceable.mkSlice, Array.toSubarray_eq_min]
 
-@[simp]
+@[simp, grind =]
 public theorem toList_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
   rw [List.take_eq_take_min, List.drop_eq_drop_min]
   simp [Std.Rco.Sliceable.mkSlice, Subarray.toList_eq, List.take_drop,
     Nat.add_sub_of_le (Nat.min_le_right _ _)]
 
-@[simp]
+@[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...hi].toArray = xs.extract lo hi := by
   simp only [← Subarray.toArray_toList, toList_mkSlice_rco]
@@ -266,12 +274,12 @@ public theorem toArray_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     · simp; omega
     · simp; omega
 
-@[simp]
+@[simp, grind =]
 public theorem size_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...hi].size = min hi xs.size - lo := by
   simp [← Subarray.length_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo...=hi] = xs[lo...(hi + 1)] := by
   simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -280,7 +288,7 @@ public theorem mkSlice_rcc_eq_mkSlice_rco_min {xs : Array α} {lo hi : Nat} :
     xs[lo...=hi] = xs[(min lo (min (hi + 1) xs.size))...(min (hi + 1) xs.size)] := by
   simp [mkSlice_rco_eq_mkSlice_rco_min]
 
-@[simp]
+@[simp, grind =]
 public theorem array_mkSlice_rcc {xs : Array α} {lo hi : Nat} :
     xs[lo...=hi].array = xs := by
   simp [Std.Rcc.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
@@ -325,7 +333,7 @@ public theorem stop_mkSlice_rci {xs : Array α} {lo : Nat} :
     xs[lo...*].stop = xs.size := by
   simp [Std.Rci.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rci_eq_mkSlice_rco {xs : Array α} {lo : Nat} :
     xs[lo...*] = xs[lo...xs.size] := by
   simp [Std.Rci.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice, Std.Rci.HasRcoIntersection.intersection]
@@ -344,7 +352,7 @@ public theorem toArray_mkSlice_rci {xs : Array α} {lo : Nat} :
     xs[lo...*].toArray = xs.extract lo := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem size_mkSlice_rci {xs : Array α} {lo : Nat} :
     xs[lo...*].size = xs.size - lo := by
   simp [← Subarray.length_toList]
@@ -364,7 +372,7 @@ public theorem stop_mkSlice_roo {xs : Array α} {lo hi : Nat} :
     xs[lo<...hi].stop = min hi xs.size := by
   simp [Std.Roo.Sliceable.mkSlice]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_roo_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
     xs[lo<...hi] = xs[(lo + 1)...hi] := by
   simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -408,6 +416,11 @@ public theorem mkSlice_roc_eq_mkSlice_roo {xs : Array α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[lo<...(hi + 1)] := by
   simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice]
 
+@[grind =]
+public theorem mkSlice_roc_eq_mkSlice_rco {xs : Array α} {lo hi : Nat} :
+    xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
+  simp
+
 public theorem mkSlice_roc_eq_mkSlice_roo_min {xs : Array α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[(min (lo + 1) (min (hi + 1) xs.size))...(min (hi + 1) xs.size)] := by
   simp [mkSlice_rco_eq_mkSlice_rco_min]
@@ -452,6 +465,11 @@ public theorem mkSlice_roi_eq_mkSlice_roo {xs : Array α} {lo : Nat} :
     xs[lo<...*] = xs[lo<...xs.size] := by
   simp [mkSlice_rci_eq_mkSlice_rco]
 
+@[grind =]
+public theorem mkSlice_roi_eq_mkSlice_rco {xs : Array α} {lo : Nat} :
+    xs[lo<...*] = xs[(lo + 1)...xs.size] := by
+  simp [mkSlice_rci_eq_mkSlice_rco]
+
 public theorem mkSlice_roi_eq_mkSlice_roo_min {xs : Array α} {lo : Nat} :
     xs[lo<...*] = xs[(min (lo + 1) xs.size)...xs.size] := by
   simp [mkSlice_rco_eq_mkSlice_rco_min]
@@ -476,7 +494,7 @@ public theorem array_mkSlice_rio {xs : Array α} {hi : Nat} :
     xs[*...hi].array = xs := by
   simp [Std.Rio.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
 
-@[simp]
+@[simp, grind =]
 public theorem start_mkSlice_rio {xs : Array α} {hi : Nat} :
     xs[*...hi].start = 0 := by
   simp [Std.Rio.Sliceable.mkSlice]
@@ -486,7 +504,7 @@ public theorem stop_mkSlice_rio {xs : Array α} {hi : Nat} :
     xs[*...hi].stop = min hi xs.size := by
   simp [Std.Rio.Sliceable.mkSlice]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rio_eq_mkSlice_rco {xs : Array α} {hi : Nat} :
     xs[*...hi] = xs[0...hi] := by
   simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -515,7 +533,7 @@ public theorem array_mkSlice_ric {xs : Array α} {hi : Nat} :
     xs[*...=hi].array = xs := by
   simp [Std.Ric.Sliceable.mkSlice, Array.toSubarray, apply_dite, Subarray.array]
 
-@[simp]
+@[simp, grind =]
 public theorem start_mkSlice_ric {xs : Array α} {hi : Nat} :
     xs[*...=hi].start = 0 := by
   simp [Std.Ric.Sliceable.mkSlice]
@@ -530,6 +548,11 @@ public theorem mkSlice_ric_eq_mkSlice_rio {xs : Array α} {hi : Nat} :
     xs[*...=hi] = xs[*...(hi + 1)] := by
   simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice]
 
+@[grind =]
+public theorem mkSlice_ric_eq_mkSlice_rco {xs : Array α} {hi : Nat} :
+    xs[*...=hi] = xs[0...(hi + 1)] := by
+  simp
+
 public theorem mkSlice_ric_eq_mkSlice_rio_min {xs : Array α} {hi : Nat} :
     xs[*...=hi] = xs[*...(min (hi + 1) xs.size)] := by
   simp [mkSlice_rco_eq_mkSlice_rco_min]
@@ -559,11 +582,16 @@ public theorem mkSlice_rii_eq_mkSlice_rio {xs : Array α} :
     xs[*...*] = xs[*...xs.size] := by
   simp [mkSlice_rci_eq_mkSlice_rco]
 
+@[grind =]
+public theorem mkSlice_rii_eq_mkSlice_rco {xs : Array α} :
+    xs[*...*] = xs[0...xs.size] := by
+  simp
+
 public theorem mkSlice_rii_eq_mkSlice_rio_min {xs : Array α} :
     xs[*...*] = xs[*...xs.size] := by
   simp [mkSlice_rco_eq_mkSlice_rco_min]
 
-@[simp]
+@[simp, grind =]
 public theorem toList_mkSlice_rii {xs : Array α} :
     xs[*...*].toList = xs.toList := by
   rw [mkSlice_rii_eq_mkSlice_rci, toList_mkSlice_rci, List.drop_zero]
@@ -573,7 +601,7 @@ public theorem toArray_mkSlice_rii {xs : Array α} :
     xs[*...*].toArray = xs := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem size_mkSlice_rii {xs : Array α} :
     xs[*...*].size = xs.size := by
   simp [← Subarray.length_toList]
@@ -583,12 +611,12 @@ public theorem array_mkSlice_rii {xs : Array α} :
     xs[*...*].array = xs := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem start_mkSlice_rii {xs : Array α} :
     xs[*...*].start = 0 := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem stop_mkSlice_rii {xs : Array α} :
     xs[*...*].stop = xs.size := by
   simp [Std.Rii.Sliceable.mkSlice]
@@ -599,7 +627,7 @@ section SubarraySlices
 
 namespace Subarray
 
-@[simp]
+@[simp, grind =]
 public theorem toList_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
   simp only [Std.Rco.Sliceable.mkSlice, Std.Rco.HasRcoIntersection.intersection, toList_eq,
@@ -608,12 +636,12 @@ public theorem toList_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
   rw [Nat.add_sub_cancel' (by omega)]
   simp [Subarray.size, ← Array.length_toList, ← List.take_eq_take_min, Nat.add_comm xs.start]
 
-@[simp]
+@[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     xs[lo...hi].toArray = xs.toArray.extract lo hi := by
   simp [← Subarray.toArray_toList, List.drop_take]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rcc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     xs[lo...=hi] = xs[lo...(hi + 1)] := by
   simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
@@ -629,7 +657,7 @@ public theorem toArray_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
     xs[lo...=hi].toArray = xs.toArray.extract lo (hi + 1) := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rci_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} :
     xs[lo...*] = xs[lo...xs.size] := by
   simp [Std.Rci.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
@@ -651,12 +679,17 @@ public theorem mkSlice_roc_eq_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
   simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice,
     Std.Roc.HasRcoIntersection.intersection, Std.Roo.HasRcoIntersection.intersection]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_roo_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...hi] = xs[(lo + 1)...hi] := by
   simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
     Std.Roo.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
 
+@[grind =]
+public theorem mkSlice_roc_eq_mkSlice_rco {xs : Subarray α} {lo hi : Nat} :
+    xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...hi].toList = (xs.toList.take hi).drop (lo + 1) := by
@@ -670,8 +703,7 @@ public theorem toArray_mkSlice_roo {xs : Subarray α} {lo hi : Nat} :
 @[simp]
 public theorem mkSlice_roc_eq_mkSlice_rcc {xs : Subarray α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[(lo + 1)...=hi] := by
-  simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
-    Std.Roc.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
+  simp
 
 @[simp]
 public theorem toList_mkSlice_roc {xs : Subarray α} {lo hi : Nat} :
@@ -689,6 +721,11 @@ public theorem mkSlice_roi_eq_mkSlice_rci {xs : Subarray α} {lo : Nat} :
   simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice,
     Std.Roi.HasRcoIntersection.intersection, Std.Rci.HasRcoIntersection.intersection]
 
+@[grind =]
+public theorem mkSlice_roi_eq_mkSlice_rco {xs : Subarray α} {lo : Nat} :
+    xs[lo<...*] = xs[(lo + 1)...xs.size] := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_roi {xs : Subarray α} {lo : Nat} :
     xs[lo<...*].toList = xs.toList.drop (lo + 1) := by
@@ -705,12 +742,17 @@ public theorem mkSlice_ric_eq_mkSlice_rio {xs : Subarray α} {hi : Nat} :
   simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice,
     Std.Ric.HasRcoIntersection.intersection, Std.Rio.HasRcoIntersection.intersection]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rio_eq_mkSlice_rco {xs : Subarray α} {hi : Nat} :
     xs[*...hi] = xs[0...hi] := by
   simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice,
     Std.Rio.HasRcoIntersection.intersection, Std.Rco.HasRcoIntersection.intersection]
 
+@[grind =]
+public theorem mkSlice_ric_eq_mkSlice_rco {xs : Subarray α} {hi : Nat} :
+    xs[*...=hi] = xs[0...(hi + 1)] := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_rio {xs : Subarray α} {hi : Nat} :
     xs[*...hi].toList = xs.toList.take hi := by
@@ -737,7 +779,7 @@ public theorem toArray_mkSlice_ric {xs : Subarray α} {hi : Nat} :
     xs[*...=hi].toArray = xs.toArray.extract 0 (hi + 1) := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rii {xs : Subarray α} :
     xs[*...*] = xs := by
   simp [Std.Rii.Sliceable.mkSlice]
diff --git a/src/Init/Data/Slice/List/Lemmas.lean b/src/Init/Data/Slice/List/Lemmas.lean
index fe7165095a..6678085516 100644
--- a/src/Init/Data/Slice/List/Lemmas.lean
+++ b/src/Init/Data/Slice/List/Lemmas.lean
@@ -47,21 +47,28 @@ public theorem toList_eq {xs : ListSlice α} :
   simp only [Std.Slice.toList, toList_internalIter]
   rfl
 
+@[simp, grind =]
 public theorem toArray_toList {xs : ListSlice α} :
     xs.toList.toArray = xs.toArray := by
   simp [Std.Slice.toArray, Std.Slice.toList]
 
+@[simp, grind =]
 public theorem toList_toArray {xs : ListSlice α} :
     xs.toArray.toList = xs.toList := by
   simp [Std.Slice.toArray, Std.Slice.toList]
 
-@[simp]
+@[simp, grind =]
 public theorem length_toList {xs : ListSlice α} :
     xs.toList.length = xs.size := by
   simp [ListSlice.toList_eq, Std.Slice.size, Std.Slice.SliceSize.size, ← Iter.length_toList_eq_count,
     toList_internalIter]; rfl
 
-@[simp]
+@[grind =]
+public theorem size_eq_length_toList {xs : ListSlice α} :
+    xs.size = xs.toList.length :=
+  length_toList.symm
+
+@[simp, grind =]
 public theorem size_toArray {xs : ListSlice α} :
     xs.toArray.size = xs.size := by
   simp [← ListSlice.toArray_toList]
@@ -70,7 +77,7 @@ end ListSlice
 
 namespace List
 
-@[simp]
+@[simp, grind =]
 public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.take hi).drop lo := by
   rw [List.take_eq_take_min, List.drop_eq_drop_min]
@@ -81,17 +88,17 @@ public theorem toList_mkSlice_rco {xs : List α} {lo hi : Nat} :
   · have : min hi xs.length ≤ lo := by omega
     simp [h, Nat.min_eq_right this]
 
-@[simp]
+@[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo...hi].toArray = ((xs.take hi).drop lo).toArray := by
   simp [← ListSlice.toArray_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem size_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo...hi].size = min hi xs.length - lo := by
   simp [← ListSlice.length_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rcc_eq_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo...=hi] = xs[lo...(hi + 1)] := by
   simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -122,12 +129,22 @@ public theorem toArray_mkSlice_rci {xs : List α} {lo : Nat} :
     xs[lo...*].toArray = (xs.drop lo).toArray := by
   simp [← ListSlice.toArray_toList]
 
+@[grind =]
+public theorem toList_mkSlice_rci_eq_toList_mkSlice_rco {xs : List α} {lo : Nat} :
+    xs[lo...*].toList = xs[lo...xs.length].toList := by
+  simp
+
+@[grind =]
+public theorem toArray_mkSlice_rci_eq_toArray_mkSlice_rco {xs : List α} {lo : Nat} :
+    xs[lo...*].toArray = xs[lo...xs.length].toArray := by
+  simp
+
 @[simp]
 public theorem size_mkSlice_rci {xs : List α} {lo : Nat} :
     xs[lo...*].size = xs.length - lo := by
   simp [← ListSlice.length_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_roo_eq_mkSlice_rco {xs : List α} {lo hi : Nat} :
     xs[lo<...hi] = xs[(lo + 1)...hi] := by
   simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -152,6 +169,11 @@ public theorem mkSlice_roc_eq_mkSlice_roo {xs : List α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[lo<...(hi + 1)] := by
   simp [Std.Roc.Sliceable.mkSlice, Std.Roo.Sliceable.mkSlice]
 
+@[simp, grind =]
+public theorem mkSlice_roc_eq_mkSlice_rco {xs : List α} {lo hi : Nat} :
+    xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_roc {xs : List α} {lo hi : Nat} :
     xs[lo<...=hi].toList = (xs.take (hi + 1)).drop (lo + 1) := by
@@ -167,11 +189,27 @@ public theorem size_mkSlice_roc {xs : List α} {lo hi : Nat} :
     xs[lo<...=hi].size = min (hi + 1) xs.length - (lo + 1) := by
   simp [← ListSlice.length_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_roi_eq_mkSlice_rci {xs : List α} {lo : Nat} :
     xs[lo<...*] = xs[(lo + 1)...*] := by
   simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice]
 
+public theorem toList_mkSlice_roi_eq_toList_mkSlice_roo {xs : List α} {lo : Nat} :
+    xs[lo<...*].toList = xs[lo<...xs.length].toList := by
+  simp
+
+public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_roo {xs : List α} {lo : Nat} :
+    xs[lo<...*].toArray = xs[lo<...xs.length].toArray := by
+  simp
+
+public theorem toList_mkSlice_roi_eq_toList_mkSlice_rco {xs : List α} {lo : Nat} :
+    xs[lo<...*].toList = xs[(lo + 1)...xs.length].toList := by
+  simp
+
+public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_rco {xs : List α} {lo : Nat} :
+    xs[lo<...*].toArray = xs[(lo + 1)...xs.length].toArray := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_roi {xs : List α} {lo : Nat} :
     xs[lo<...*].toList = xs.drop (lo + 1) := by
@@ -187,7 +225,7 @@ public theorem size_mkSlice_roi {xs : List α} {lo : Nat} :
     xs[lo<...*].size = xs.length - (lo + 1) := by
   simp [← ListSlice.length_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rio_eq_mkSlice_rco {xs : List α} {hi : Nat} :
     xs[*...hi] = xs[0...hi] := by
   simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -212,6 +250,11 @@ public theorem mkSlice_ric_eq_mkSlice_rio {xs : List α} {hi : Nat} :
     xs[*...=hi] = xs[*...(hi + 1)] := by
   simp [Std.Ric.Sliceable.mkSlice, Std.Rio.Sliceable.mkSlice]
 
+@[grind =]
+public theorem mkSlice_ric_eq_mkSlice_rco {xs : List α} {hi : Nat} :
+    xs[*...=hi] = xs[0...(hi + 1)] := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_ric {xs : List α} {hi : Nat} :
     xs[*...=hi].toList = xs.take (hi + 1) := by
@@ -227,11 +270,19 @@ public theorem size_mkSlice_ric {xs : List α} {hi : Nat} :
     xs[*...=hi].size = min (hi + 1) xs.length := by
   simp [← ListSlice.length_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rii_eq_mkSlice_rci {xs : List α} :
     xs[*...*] = xs[0...*] := by
   simp [Std.Rii.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice]
 
+public theorem toList_mkSlice_rii_eq_toList_mkSlice_rco {xs : List α} :
+    xs[*...*].toList = xs[0...xs.length].toList := by
+  simp
+
+public theorem toArray_mkSlice_rii_eq_toArray_mkSlice_rco {xs : List α} :
+    xs[*...*].toArray = xs[0...xs.length].toArray := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_rii {xs : List α} :
     xs[*...*].toList = xs := by
@@ -253,7 +304,7 @@ section ListSubslices
 
 namespace ListSlice
 
-@[simp]
+@[simp, grind =]
 public theorem toList_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...hi].toList = (xs.toList.take hi).drop lo := by
   simp only [instSliceableListSliceNat_1, List.toList_mkSlice_rco, ListSlice.toList_eq (xs := xs)]
@@ -262,12 +313,12 @@ public theorem toList_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
   · simp
   · simp [List.take_take, Nat.min_comm]
 
-@[simp]
+@[simp, grind =]
 public theorem toArray_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...hi].toArray = xs.toArray.extract lo hi := by
   simp [← toArray_toList, List.drop_take]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rcc_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
     xs[lo...=hi] = xs[lo...(hi + 1)] := by
   simp [Std.Rcc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -295,9 +346,19 @@ public theorem toArray_mkSlice_rci {xs : ListSlice α} {lo : Nat} :
     xs[lo...*].toArray = xs.toArray.extract lo := by
   simp only [← toArray_toList, toList_mkSlice_rci]
   rw (occs := [1]) [← List.take_length (l := List.drop lo xs.toList)]
+  simp [- toArray_toList]
+
+@[grind =]
+public theorem toList_mkSlice_rci_eq_toList_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
+    xs[lo...*].toList = xs[lo...xs.size].toList := by
+  simp [← length_toList, - Slice.length_toList_eq_size]
+
+@[grind =]
+public theorem toArray_mkSlice_rci_eq_toArray_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
+    xs[lo...*].toArray = xs[lo...xs.size].toArray := by
   simp
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_roo_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
     xs[lo<...hi] = xs[(lo + 1)...hi] := by
   simp [Std.Roo.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -322,6 +383,11 @@ public theorem mkSlice_roc_eq_mkSlice_rcc {xs : ListSlice α} {lo hi : Nat} :
     xs[lo<...=hi] = xs[(lo + 1)...=hi] := by
   simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
 
+@[simp, grind =]
+public theorem mkSlice_roc_eq_mkSlice_rco {xs : ListSlice α} {lo hi : Nat} :
+    xs[lo<...=hi] = xs[(lo + 1)...(hi + 1)] := by
+  simp [Std.Roc.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
+
 @[simp]
 public theorem toList_mkSlice_roc {xs : ListSlice α} {lo hi : Nat} :
     xs[lo<...=hi].toList = (xs.toList.take (hi + 1)).drop (lo + 1) := by
@@ -332,11 +398,28 @@ public theorem toArray_mkSlice_roc {xs : ListSlice α} {lo hi : Nat} :
     xs[lo<...=hi].toArray = xs.toArray.extract (lo + 1) (hi + 1) := by
   simp [← toArray_toList, List.drop_take]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_roi_eq_mkSlice_rci {xs : ListSlice α} {lo : Nat} :
     xs[lo<...*] = xs[(lo + 1)...*] := by
   simp [Std.Roi.Sliceable.mkSlice, Std.Rci.Sliceable.mkSlice]
 
+public theorem toList_mkSlice_roi_eq_toList_mkSlice_roo {xs : ListSlice α} {lo : Nat} :
+    xs[lo<...*].toList = xs[lo<...xs.size].toList := by
+  simp [← length_toList, - Slice.length_toList_eq_size]
+
+public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_roo {xs : ListSlice α} {lo : Nat} :
+    xs[lo<...*].toArray = xs[lo<...xs.size].toArray := by
+  simp only [mkSlice_roi_eq_mkSlice_rci, toArray_mkSlice_rci, size_toArray_eq_size,
+    mkSlice_roo_eq_mkSlice_rco, toArray_mkSlice_rco]
+
+public theorem toList_mkSlice_roi_eq_toList_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
+    xs[lo<...*].toList = xs[(lo + 1)...xs.size].toList := by
+  simp [← length_toList, - Slice.length_toList_eq_size]
+
+public theorem toArray_mkSlice_roi_eq_toArray_mkSlice_rco {xs : ListSlice α} {lo : Nat} :
+    xs[lo<...*].toArray = xs[(lo + 1)...xs.size].toArray := by
+  simp
+
 @[simp]
 public theorem toList_mkSlice_roi {xs : ListSlice α} {lo : Nat} :
     xs[lo<...*].toList = xs.toList.drop (lo + 1) := by
@@ -347,9 +430,9 @@ public theorem toArray_mkSlice_roi {xs : ListSlice α} {lo : Nat} :
     xs[lo<...*].toArray = xs.toArray.extract (lo + 1) := by
   simp only [← toArray_toList, toList_mkSlice_roi]
   rw (occs := [1]) [← List.take_length (l := List.drop (lo + 1) xs.toList)]
-  simp
+  simp [- toArray_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rio_eq_mkSlice_rco {xs : ListSlice α} {hi : Nat} :
     xs[*...hi] = xs[0...hi] := by
   simp [Std.Rio.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
@@ -374,6 +457,11 @@ public theorem mkSlice_ric_eq_mkSlice_rcc {xs : ListSlice α} {hi : Nat} :
     xs[*...=hi] = xs[0...=hi] := by
   simp [Std.Ric.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
 
+@[grind =]
+public theorem mkSlice_ric_eq_mkSlice_rco {xs : ListSlice α} {hi : Nat} :
+    xs[*...=hi] = xs[0...(hi + 1)] := by
+  simp [Std.Ric.Sliceable.mkSlice, Std.Rco.Sliceable.mkSlice]
+
 @[simp]
 public theorem toList_mkSlice_ric {xs : ListSlice α} {hi : Nat} :
     xs[*...=hi].toList = xs.toList.take (hi + 1) := by
@@ -384,7 +472,7 @@ public theorem toArray_mkSlice_ric {xs : ListSlice α} {hi : Nat} :
     xs[*...=hi].toArray = xs.toArray.extract 0 (hi + 1) := by
   simp [← toArray_toList]
 
-@[simp]
+@[simp, grind =]
 public theorem mkSlice_rii {xs : ListSlice α} :
     xs[*...*] = xs := by
   simp [Std.Rii.Sliceable.mkSlice]
diff --git a/tests/lean/run/slice.lean b/tests/lean/run/slice.lean
index 9b7c1733bf..054ad15ab0 100644
--- a/tests/lean/run/slice.lean
+++ b/tests/lean/run/slice.lean
@@ -121,3 +121,40 @@ example : [1, 2, 3, 4, 5][1...*][*...2].toArray = #[2, 3] := by simp
 example : [1, 2, 3, 4, 5][1...*][*...=2].toArray = #[2, 3, 4] := by simp
 example : [1, 2, 3, 4, 5][1...*][*...*].toArray = #[2, 3, 4, 5] := by simp
 example : [1, 2, 3][0...2][*...*].toArray = #[1, 2] := by simp
+
+example (xs : List α) : xs[*...5].size = xs[0...5].size := by
+  grind
+
+example {xs : List α} {lo hi : Nat} :
+    xs[lo...=hi].toList = (xs.take (hi + 1)).drop lo := by
+  grind
+
+-- verify that grind is powerful enough to prove some lemmas that are not grind-annotated
+example : type_of% @List.toList_mkSlice_rcc := by grind
+example : type_of% @List.toArray_mkSlice_rcc := by grind
+example : type_of% @List.size_mkSlice_rcc := by grind
+example : type_of% @List.toList_mkSlice_rci := by grind
+example : type_of% @List.toArray_mkSlice_rci := by grind
+example : type_of% @List.toArray_mkSlice_roi := by grind
+example : type_of% @List.toArray_mkSlice_ric := by grind
+example : type_of% @List.toArray_mkSlice_rii_eq_toArray_mkSlice_rco := by grind
+example : type_of% @List.toArray_mkSlice_roc := by grind
+example : type_of% @List.toList_mkSlice_ric := by grind
+
+example (xs : List Nat) : xs[1...=4][2...3].toList = xs[3...4].toList := by
+  grind [List.take_drop, List.drop_drop]
+
+example : type_of% @Array.toArray_mkSlice_rcc := by grind
+example : type_of% @Array.toArray_mkSlice_rcc := by grind
+example : type_of% @Array.size_mkSlice_rcc := by grind
+example : type_of% @Array.toArray_mkSlice_rci := by grind
+example : type_of% @Array.toArray_mkSlice_rci := by grind
+example : type_of% @Array.toArray_mkSlice_roi := by grind
+example : type_of% @Array.toArray_mkSlice_ric := by grind
+example : type_of% @Array.toArray_mkSlice_roc := by grind
+example : type_of% @Array.toArray_mkSlice_ric := by grind
+
+example (xs : Array Nat) : xs[1...=4][2...3].toList = xs[3...4].toList := by
+  grind [List.take_drop, List.drop_drop]
+
+example (xs : Array Nat) : xs[1...=4][2...3].toArray = xs[3...4].toArray := by grind