fix

src/Init/Data/Array/Attach.lean

@@ -56,15 +56,15 @@ well-founded recursion mechanism to prove that the function terminates.
 -/
 @[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id
 
-@[simp] theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} :
+@[simp, grind =] theorem _root_.List.attachWith_toArray {l : List α} {P : α → Prop} {H : ∀ x ∈ l.toArray, P x} :
     l.toArray.attachWith P H = (l.attachWith P (by simpa using H)).toArray := by
   simp [attachWith]
 
-@[simp] theorem _root_.List.attach_toArray {l : List α} :
+@[simp, grind =] theorem _root_.List.attach_toArray {l : List α} :
     l.toArray.attach = (l.attachWith (· ∈ l.toArray) (by simp)).toArray := by
   simp [attach]
 
-@[simp] theorem _root_.List.pmap_toArray {l : List α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l.toArray, P a} :
+@[simp, grind =] theorem _root_.List.pmap_toArray {l : List α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l.toArray, P a} :
     l.toArray.pmap f H = (l.pmap f (by simpa using H)).toArray := by
   simp [pmap]
 
@@ -590,7 +590,7 @@ def unattach {α : Type _} {p : α → Prop} (xs : Array { x // p x }) : Array
   unfold unattach
   simp
 
-@[simp] theorem _root_.List.unattach_toArray {p : α → Prop} {xs : List { x // p x }} :
+@[simp, grind =] theorem _root_.List.unattach_toArray {p : α → Prop} {xs : List { x // p x }} :
     xs.toArray.unattach = xs.unattach.toArray := by
   simp only [unattach, List.map_toArray, List.unattach]
 

src/Init/Data/Array/Basic.lean

@@ -88,11 +88,11 @@ theorem ext' {xs ys : Array α} (h : xs.toList = ys.toList) : xs = ys := by
 @[simp] theorem toArrayAux_eq {as : List α} {acc : Array α} : (as.toArrayAux acc).toList = acc.toList ++ as := by
   induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
 
-@[simp] theorem toArray_toList {xs : Array α} : xs.toList.toArray = xs := rfl
+@[simp, grind =] theorem toArray_toList {xs : Array α} : xs.toList.toArray = xs := rfl
 
-@[simp] theorem getElem_toList {xs : Array α} {i : Nat} (h : i < xs.size) : xs.toList[i] = xs[i] := rfl
+@[simp, grind =] theorem getElem_toList {xs : Array α} {i : Nat} (h : i < xs.size) : xs.toList[i] = xs[i] := rfl
 
-@[simp] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by
+@[simp, grind =] theorem getElem?_toList {xs : Array α} {i : Nat} : xs.toList[i]? = xs[i]? := by
   simp [getElem?_def]
 
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
@@ -107,7 +107,7 @@ instance : Membership α (Array α) where
 theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
-@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+@[simp, grind =] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [mem_def]
 
 @[simp, grind] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
@@ -127,18 +127,18 @@ theorem toList_toArray {as : List α} : as.toArray.toList = as := rfl
 @[deprecated toList_toArray (since := "2025-02-17")]
 abbrev _root_.Array.toList_toArray := @List.toList_toArray
 
-@[simp] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size]
+@[simp, grind] theorem size_toArray {as : List α} : as.toArray.size = as.length := by simp [Array.size]
 
 @[deprecated size_toArray (since := "2025-02-17")]
 abbrev _root_.Array.size_toArray := @List.size_toArray
 
-@[simp] theorem getElem_toArray {xs : List α} {i : Nat} (h : i < xs.toArray.size) :
+@[simp, grind =] theorem getElem_toArray {xs : List α} {i : Nat} (h : i < xs.toArray.size) :
     xs.toArray[i] = xs[i]'(by simpa using h) := rfl
 
-@[simp] theorem getElem?_toArray {xs : List α} {i : Nat} : xs.toArray[i]? = xs[i]? := by
+@[simp, grind =] theorem getElem?_toArray {xs : List α} {i : Nat} : xs.toArray[i]? = xs[i]? := by
   simp [getElem?_def]
 
-@[simp] theorem getElem!_toArray [Inhabited α] {xs : List α} {i : Nat} :
+@[simp, grind =] theorem getElem!_toArray [Inhabited α] {xs : List α} {i : Nat} :
     xs.toArray[i]! = xs[i]! := by
   simp [getElem!_def]
 

src/Init/Data/Array/Bootstrap.lean

@@ -55,12 +55,12 @@ theorem foldlM_toList.aux [Monad m]
     rfl
   · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
 
-@[simp] theorem foldlM_toList [Monad m]
+@[simp, grind =] theorem foldlM_toList [Monad m]
     {f : β → α → m β} {init : β} {xs : Array α} :
     xs.toList.foldlM f init = xs.foldlM f init := by
   simp [foldlM, foldlM_toList.aux]
 
-@[simp] theorem foldl_toList (f : β → α → β) {init : β} {xs : Array α} :
+@[simp, grind =] theorem foldl_toList (f : β → α → β) {init : β} {xs : Array α} :
     xs.toList.foldl f init = xs.foldl f init :=
   List.foldl_eq_foldlM .. ▸ foldlM_toList ..
 
@@ -79,32 +79,32 @@ theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init
   match xs, this with | _, .inl rfl => rfl | xs, .inr h => ?_
   simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
-@[simp] theorem foldrM_toList [Monad m]
+@[simp, grind =] theorem foldrM_toList [Monad m]
     {f : α → β → m β} {init : β} {xs : Array α} :
     xs.toList.foldrM f init = xs.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList, List.foldlM_reverse]
 
-@[simp] theorem foldr_toList (f : α → β → β) {init : β} {xs : Array α} :
+@[simp, grind =] theorem foldr_toList (f : α → β → β) {init : β} {xs : Array α} :
     xs.toList.foldr f init = xs.foldr f init :=
   List.foldr_eq_foldrM .. ▸ foldrM_toList ..
 
-@[simp] theorem push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by
+@[simp, grind =] theorem push_toList {xs : Array α} {a : α} : (xs.push a).toList = xs.toList ++ [a] := by
   simp [push, List.concat_eq_append]
 
-@[simp] theorem toListAppend_eq {xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l := by
+@[simp, grind =] theorem toListAppend_eq {xs : Array α} {l : List α} : xs.toListAppend l = xs.toList ++ l := by
   simp [toListAppend, ← foldr_toList]
 
-@[simp] theorem toListImpl_eq {xs : Array α} : xs.toListImpl = xs.toList := by
+@[simp, grind =] theorem toListImpl_eq {xs : Array α} : xs.toListImpl = xs.toList := by
   simp [toListImpl, ← foldr_toList]
 
-@[simp] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl
+@[simp, grind =] theorem toList_pop {xs : Array α} : xs.pop.toList = xs.toList.dropLast := rfl
 
 @[deprecated toList_pop (since := "2025-02-17")]
 abbrev pop_toList := @Array.toList_pop
 
 @[simp] theorem append_eq_append {xs ys : Array α} : xs.append ys = xs ++ ys := rfl
 
-@[simp] theorem toList_append {xs ys : Array α} :
+@[simp, grind =] theorem toList_append {xs ys : Array α} :
     (xs ++ ys).toList = xs.toList ++ ys.toList := by
   rw [← append_eq_append]; unfold Array.append
   rw [← foldl_toList]
@@ -112,13 +112,13 @@ abbrev pop_toList := @Array.toList_pop
 
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
-@[simp, grind] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by
+@[simp, grind =] theorem append_empty {xs : Array α} : xs ++ #[] = xs := by
   apply ext'; simp only [toList_append, toList_empty, List.append_nil]
 
 @[deprecated append_empty (since := "2025-01-13")]
 abbrev append_nil := @append_empty
 
-@[simp, grind] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
+@[simp, grind =] theorem empty_append {xs : Array α} : #[] ++ xs = xs := by
   apply ext'; simp only [toList_append, toList_empty, List.nil_append]
 
 @[deprecated empty_append (since := "2025-01-13")]
@@ -129,7 +129,7 @@ abbrev nil_append := @empty_append
 
 @[simp] theorem appendList_eq_append {xs : Array α} {l : List α} : xs.appendList l = xs ++ l := rfl
 
-@[simp] theorem toList_appendList {xs : Array α} {l : List α} :
+@[simp, grind =] theorem toList_appendList {xs : Array α} {l : List α} :
     (xs ++ l).toList = xs.toList ++ l := by
   rw [← appendList_eq_append]; unfold Array.appendList
   induction l generalizing xs <;> simp [*]

src/Init/Data/Array/Count.lean

@@ -25,7 +25,7 @@ section countP
 
 variable {p q : α → Bool}
 
-@[simp] theorem _root_.List.countP_toArray {l : List α} : countP p l.toArray = l.countP p := by
+@[simp, grind =] theorem _root_.List.countP_toArray {l : List α} : countP p l.toArray = l.countP p := by
   simp [countP]
   induction l with
   | nil => rfl
@@ -33,7 +33,7 @@ variable {p q : α → Bool}
     simp only [List.foldr_cons, ih, List.countP_cons]
     split <;> simp_all
 
-@[simp] theorem countP_toList {xs : Array α} : xs.toList.countP p = countP p xs := by
+@[simp, grind =] theorem countP_toList {xs : Array α} : xs.toList.countP p = countP p xs := by
   cases xs
   simp
 
@@ -164,10 +164,10 @@ section count
 
 variable [BEq α]
 
-@[simp] theorem _root_.List.count_toArray {l : List α} {a : α} : count a l.toArray = l.count a := by
+@[simp, grind =] theorem _root_.List.count_toArray {l : List α} {a : α} : count a l.toArray = l.count a := by
   simp [count, List.count_eq_countP]
 
-@[simp] theorem count_toList {xs : Array α} {a : α} : xs.toList.count a = xs.count a := by
+@[simp, grind =] theorem count_toList {xs : Array α} {a : α} : xs.toList.count a = xs.count a := by
   cases xs
   simp
 

src/Init/Data/Array/DecidableEq.lean

@@ -68,7 +68,7 @@ theorem isEqv_eq_decide (xs ys : Array α) (r) :
       Bool.not_eq_true]
     simpa [isEqv_iff_rel] using h'
 
-@[simp] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
+@[simp, grind =] theorem isEqv_toList [BEq α] (xs ys : Array α) : (xs.toList.isEqv ys.toList r) = (xs.isEqv ys r) := by
   simp [isEqv_eq_decide, List.isEqv_eq_decide]
 
 theorem eq_of_isEqv [DecidableEq α] (xs ys : Array α) (h : Array.isEqv xs ys (fun x y => x = y)) : xs = ys := by
@@ -99,17 +99,17 @@ theorem beq_eq_decide [BEq α] (xs ys : Array α) :
       decide (∀ (i : Nat) (h' : i < xs.size), xs[i] == ys[i]'(h ▸ h')) else false := by
   simp [BEq.beq, isEqv_eq_decide]
 
-@[simp] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
+@[simp, grind =] theorem beq_toList [BEq α] (xs ys : Array α) : (xs.toList == ys.toList) = (xs == ys) := by
   simp [beq_eq_decide, List.beq_eq_decide]
 
 end Array
 
 namespace List
 
-@[simp] theorem isEqv_toArray [BEq α] (as bs : List α) : (as.toArray.isEqv bs.toArray r) = (as.isEqv bs r) := by
+@[simp, grind =] theorem isEqv_toArray [BEq α] (as bs : List α) : (as.toArray.isEqv bs.toArray r) = (as.isEqv bs r) := by
   simp [isEqv_eq_decide, Array.isEqv_eq_decide]
 
-@[simp] theorem beq_toArray [BEq α] (as bs : List α) : (as.toArray == bs.toArray) = (as == bs) := by
+@[simp, grind =] theorem beq_toArray [BEq α] (as bs : List α) : (as.toArray == bs.toArray) = (as == bs) := by
   simp [beq_eq_decide, Array.beq_eq_decide]
 
 end List

src/Init/Data/Array/Lemmas.lean

@@ -39,10 +39,10 @@ namespace Array
 @[simp] theorem toList_eq_nil_iff {xs : Array α} : xs.toList = [] ↔ xs = #[] := by
   cases xs <;> simp
 
-@[simp] theorem mem_toList_iff {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := by
+@[simp, grind =] theorem mem_toList_iff {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := by
   cases xs <;> simp
 
-@[simp] theorem length_toList {xs : Array α} : xs.toList.length = xs.size := rfl
+@[simp, grind =] theorem length_toList {xs : Array α} : xs.toList.length = xs.size := rfl
 
 theorem eq_toArray : xs = List.toArray as ↔ xs.toList = as := by
   cases xs
@@ -527,7 +527,7 @@ theorem forall_getElem {xs : Array α} {p : α → Prop} :
   rcases xs with ⟨xs⟩
   simp
 
-@[simp] theorem isEmpty_toList {xs : Array α} : xs.toList.isEmpty = xs.isEmpty := by
+@[simp, grind =] theorem isEmpty_toList {xs : Array α} : xs.toList.isEmpty = xs.isEmpty := by
   rcases xs with ⟨_ | _⟩ <;> simp
 
 theorem isEmpty_eq_false_iff_exists_mem {xs : Array α} :
@@ -592,7 +592,7 @@ theorem anyM_loop_cons [Monad m] {p : α → m Bool} {a : α} {as : List α} {st
   · rw [dif_neg]
     omega
 
-@[simp] theorem anyM_toList [Monad m] {p : α → m Bool} {as : Array α} :
+@[simp, grind =] theorem anyM_toList [Monad m] {p : α → m Bool} {as : Array α} :
     as.toList.anyM p = as.anyM p :=
   match as with
   | ⟨[]⟩  => by simp [anyM, anyM.loop]
@@ -651,7 +651,7 @@ theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
   rw [Bool.eq_false_iff, Ne, any_eq_true]
   simp
 
-@[simp] theorem any_toList {p : α → Bool} {as : Array α} : as.toList.any p = as.any p := by
+@[simp, grind =] theorem any_toList {p : α → Bool} {as : Array α} : as.toList.any p = as.any p := by
   rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]
   simp only [List.mem_iff_getElem, getElem_toList]
   exact ⟨fun ⟨_, ⟨i, w, rfl⟩, h⟩ => ⟨i, w, h⟩, fun ⟨i, w, h⟩ => ⟨_, ⟨i, w, rfl⟩, h⟩⟩
@@ -661,7 +661,7 @@ theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] {p : α → m Bool} {as :
   dsimp [allM, anyM]
   simp
 
-@[simp] theorem allM_toList [Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α} :
+@[simp, grind =] theorem allM_toList [Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α} :
     as.toList.allM p = as.allM p := by
   rw [allM_eq_not_anyM_not]
   rw [← anyM_toList]
@@ -690,7 +690,7 @@ theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
   rw [Bool.eq_false_iff, Ne, all_eq_true]
   simp
 
-@[simp] theorem all_toList {p : α → Bool} {as : Array α} : as.toList.all p = as.all p := by
+@[simp, grind =] theorem all_toList {p : α → Bool} {as : Array α} : as.toList.all p = as.all p := by
   rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]
   simp only [List.mem_iff_getElem, getElem_toList]
   constructor
@@ -730,18 +730,18 @@ theorem all_eq_true_iff_forall_mem {xs : Array α} : xs.all p ↔ ∀ x, x ∈ x
   subst h
   rw [all_toList]
 
-theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} :
+@[grind] theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} :
     l.toArray.anyM p = l.anyM p := by
   rw [← anyM_toList]
 
-theorem _root_.List.any_toArray {p : α → Bool} {l : List α} : l.toArray.any p = l.any p := by
+@[grind] theorem _root_.List.any_toArray {p : α → Bool} {l : List α} : l.toArray.any p = l.any p := by
   rw [any_toList]
 
-theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} :
+@[grind] theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] {p : α → m Bool} {l : List α} :
     l.toArray.allM p = l.allM p := by
   rw [← allM_toList]
 
-theorem _root_.List.all_toArray {p : α → Bool} {l : List α} : l.toArray.all p = l.all p := by
+@[grind] theorem _root_.List.all_toArray {p : α → Bool} {l : List α} : l.toArray.all p = l.all p := by
   rw [all_toList]
 
 /-- Variant of `any_eq_true` in terms of membership rather than an array index. -/
@@ -807,7 +807,7 @@ theorem decide_forall_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
     decide (∀ x, x ∈ xs → p x) = xs.all p := by
   simp [all_eq']
 
-@[simp] theorem _root_.List.contains_toArray [BEq α] {l : List α} {a : α} :
+@[simp, grind =] theorem _root_.List.contains_toArray [BEq α] {l : List α} {a : α} :
     l.toArray.contains a = l.contains a := by
   simp [Array.contains, List.any_beq]
 
@@ -1205,7 +1205,7 @@ where
     induction l generalizing xs <;> simp [*]
   simp [H]
 
-@[simp] theorem _root_.List.map_toArray {f : α → β} {l : List α} :
+@[simp, grind =] theorem _root_.List.map_toArray {f : α → β} {l : List α} :
     l.toArray.map f = (l.map f).toArray := by
   apply ext'
   simp
@@ -1428,7 +1428,7 @@ theorem filter_congr {xs ys : Array α} (h : xs = ys)
   induction xs with simp
   | cons => split <;> simp [*]
 
-theorem toList_filter {p : α → Bool} {xs : Array α} :
+@[grind] theorem toList_filter {p : α → Bool} {xs : Array α} :
     (xs.filter p).toList = xs.toList.filter p := by
   simp
 
@@ -1437,7 +1437,7 @@ theorem toList_filter {p : α → Bool} {xs : Array α} :
   apply ext'
   simp [h]
 
-theorem _root_.List.filter_toArray {p : α → Bool} {l : List α} :
+@[grind] theorem _root_.List.filter_toArray {p : α → Bool} {l : List α} :
     l.toArray.filter p = (l.filter p).toArray := by
   simp
 
@@ -1602,7 +1602,7 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs)
   · simp_all [Id.run, List.filterMap_cons]
     split <;> simp_all
 
-theorem toList_filterMap {f : α → Option β} {xs : Array α} :
+@[grind] theorem toList_filterMap {f : α → Option β} {xs : Array α} :
     (xs.filterMap f).toList = xs.toList.filterMap f := by
   simp [toList_filterMap']
 
@@ -1612,7 +1612,7 @@ theorem toList_filterMap {f : α → Option β} {xs : Array α} :
   apply ext'
   simp [h]
 
-theorem _root_.List.filterMap_toArray {f : α → Option β} {l : List α} :
+@[grind] theorem _root_.List.filterMap_toArray {f : α → Option β} {l : List α} :
     l.toArray.filterMap f = (l.filterMap f).toArray := by
   simp
 
@@ -2097,7 +2097,7 @@ theorem append_eq_map_iff {f : α → β} :
 
 @[simp, grind] theorem flatten_empty : (#[] : Array (Array α)).flatten = #[] := by simp [flatten]; rfl
 
-@[simp] theorem toList_flatten {xss : Array (Array α)} :
+@[simp, grind] theorem toList_flatten {xss : Array (Array α)} :
     xss.flatten.toList = (xss.toList.map toList).flatten := by
   dsimp [flatten]
   simp only [← foldl_toList]
@@ -2124,7 +2124,7 @@ theorem append_eq_map_iff {f : α → β} :
   apply ext'
   simp
 
-@[simp] theorem size_flatten {xss : Array (Array α)} : xss.flatten.size = (xss.map size).sum := by
+@[simp, grind] theorem size_flatten {xss : Array (Array α)} : xss.flatten.size = (xss.map size).sum := by
   cases xss using array₂_induction
   simp [Function.comp_def]
 
@@ -2307,7 +2307,7 @@ theorem flatMap_toList {xs : Array α} {f : α → List β} :
   rcases xs with ⟨l⟩
   simp
 
-@[simp] theorem toList_flatMap {xs : Array α} {f : α → Array β} :
+@[simp, grind =] theorem toList_flatMap {xs : Array α} {f : α → Array β} :
     (xs.flatMap f).toList = xs.toList.flatMap fun a => (f a).toList := by
   rcases xs with ⟨l⟩
   simp
@@ -2322,7 +2322,7 @@ theorem flatMap_toArray_cons {β} {f : α → Array β} {a : α} {as : List α}
   intro cs
   induction as generalizing cs <;> simp_all
 
-@[simp] theorem flatMap_toArray {β} {f : α → Array β} {as : List α} :
+@[simp, grind =] theorem flatMap_toArray {β} {f : α → Array β} {as : List α} :
     as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by
   induction as with
   | nil => simp
@@ -2652,6 +2652,7 @@ abbrev sum_mkArray_nat := @sum_replicate_nat
 
 /-! ### Preliminaries about `swap` needed for `reverse`. -/
 
+@[grind]
 theorem getElem?_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i j hi hj)[k]? =
     if j = k then some xs[i] else if i = k then some xs[j] else xs[k]? := by
   simp [swap_def, getElem?_set]
@@ -2710,15 +2711,15 @@ theorem getElem?_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i
         true_and, Nat.not_lt] at h
       rw [List.getElem?_eq_none_iff.2 ‹_›, List.getElem?_eq_none_iff.2 (xs.toList.length_reverse ▸ ‹_›)]
 
-@[simp] theorem _root_.List.reverse_toArray {l : List α} : l.toArray.reverse = l.reverse.toArray := by
+@[simp, grind =] theorem _root_.List.reverse_toArray {l : List α} : l.toArray.reverse = l.reverse.toArray := by
   apply ext'
   simp only [toList_reverse]
 
-@[simp, grind] theorem reverse_push {xs : Array α} {a : α} : (xs.push a).reverse = #[a] ++ xs.reverse := by
+@[simp, grind =] theorem reverse_push {xs : Array α} {a : α} : (xs.push a).reverse = #[a] ++ xs.reverse := by
   cases xs
   simp
 
-@[simp, grind] theorem mem_reverse {x : α} {xs : Array α} : x ∈ xs.reverse ↔ x ∈ xs := by
+@[simp, grind =] theorem mem_reverse {x : α} {xs : Array α} : x ∈ xs.reverse ↔ x ∈ xs := by
   cases xs
   simp
 
@@ -3003,7 +3004,7 @@ theorem extract_empty_of_size_le_start {xs : Array α} {start stop : Nat} (h : x
   · simp
   · simp at h₁
 
-@[simp] theorem _root_.List.extract_toArray {l : List α} {start stop : Nat} :
+@[simp, grind =] theorem _root_.List.extract_toArray {l : List α} {start stop : Nat} :
     l.toArray.extract start stop = (l.extract start stop).toArray := by
   apply ext'
   simp
@@ -3742,25 +3743,25 @@ theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.contains a ↔ a ∈ xs := by
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_toList [BEq α] {xs : Array α} {x : α} :
     xs.toList.contains x = xs.contains x := by
   rcases xs with ⟨xs⟩
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_map [BEq β] {xs : Array α} {x : β} {f : α → β} :
     (xs.map f).contains x = xs.any (fun a => x == f a) := by
   rcases xs with ⟨xs⟩
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_filter [BEq α] {xs : Array α} {x : α} {p : α → Bool} :
     (xs.filter p).contains x = xs.any (fun a => x == a && p a) := by
   rcases xs with ⟨xs⟩
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_filterMap [BEq β] {xs : Array α} {x : β} {f : α → Option β} :
     (xs.filterMap f).contains x = xs.any (fun a => (f a).any fun b => x == b) := by
   rcases xs with ⟨xs⟩
@@ -3773,19 +3774,19 @@ theorem contains_append [BEq α] {xs ys : Array α} {x : α} :
   rcases ys with ⟨ys⟩
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_flatten [BEq α] {xs : Array (Array α)} {x : α} :
     (xs.flatten).contains x = xs.any fun xs => xs.contains x := by
   rcases xs with ⟨xs⟩
   simp [Function.comp_def]
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_reverse [BEq α] {xs : Array α} {x : α} :
     (xs.reverse).contains x = xs.contains x := by
   rcases xs with ⟨xs⟩
   simp
 
-@[simp, grind]
+@[simp, grind =]
 theorem contains_flatMap [BEq β] {xs : Array α} {f : α → Array β} {x : β} :
     (xs.flatMap f).contains x = xs.any fun a => (f a).contains x := by
   rcases xs with ⟨xs⟩
@@ -3798,7 +3799,7 @@ theorem pop_append {xs ys : Array α} :
     (xs ++ ys).pop = if ys.isEmpty then xs.pop else xs ++ ys.pop := by
   split <;> simp_all
 
-@[simp] theorem pop_replicate {n : Nat} {a : α} : (replicate n a).pop = replicate (n - 1) a := by
+@[simp, grind =] theorem pop_replicate {n : Nat} {a : α} : (replicate n a).pop = replicate (n - 1) a := by
   ext <;> simp
 
 @[deprecated pop_replicate (since := "2025-03-18")]
@@ -4096,6 +4097,7 @@ theorem getElem_swap' {xs : Array α} {i j : Nat} {hi hj} {k : Nat} (hk : k < xs
   · simp_all only [getElem_swap_left]
   · split <;> simp_all
 
+@[grind]
 theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
     (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) := by
   apply getElem_swap'
@@ -4361,7 +4363,10 @@ theorem foldl_toList_eq_map {l : List α} {acc : Array β} {G : α → β} :
 
 /-! # uset -/
 
-attribute [simp] uset
+-- For verification purposes, we use `simp` to replace `uset` with `set`.
+@[simp, grind =] theorem uset_eq_set {xs : Array α} {v : α} {i : USize} (h : i.toNat < xs.size) :
+    uset xs i v h = set xs i.toNat v h := by
+  simp [uset]
 
 theorem size_uset {xs : Array α} {v : α} {i : USize} (h : i.toNat < xs.size) :
     (uset xs i v h).size = xs.size := by
@@ -4378,7 +4383,7 @@ theorem getElem!_eq_getD [Inhabited α] {xs : Array α} {i} : xs[i]! = xs.getD i
 
 /-! # mem -/
 
-@[simp] theorem mem_toList {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := mem_def.symm
+@[simp, grind =] theorem mem_toList {a : α} {xs : Array α} : a ∈ xs.toList ↔ a ∈ xs := mem_def.symm
 
 @[deprecated not_mem_empty (since := "2025-03-25")]
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun
@@ -4421,12 +4426,12 @@ theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some
 
 /-! ### forIn -/
 
-@[simp] theorem forIn_toList [Monad m] {xs : Array α} {b : β} {f : α → β → m (ForInStep β)} :
+@[simp, grind =] theorem forIn_toList [Monad m] {xs : Array α} {b : β} {f : α → β → m (ForInStep β)} :
     forIn xs.toList b f = forIn xs b f := by
   cases xs
   simp
 
-@[simp] theorem forIn'_toList [Monad m] {xs : Array α} {b : β} {f : (a : α) → a ∈ xs.toList → β → m (ForInStep β)} :
+@[simp, grind =] theorem forIn'_toList [Monad m] {xs : Array α} {b : β} {f : (a : α) → a ∈ xs.toList → β → m (ForInStep β)} :
     forIn' xs.toList b f = forIn' xs b (fun a m b => f a (mem_toList.mpr m) b) := by
   cases xs
   simp
@@ -4439,7 +4444,7 @@ abbrev contains_def [DecidableEq α] {a : α} {xs : Array α} : xs.contains a
 
 /-! ### isPrefixOf -/
 
-@[simp] theorem isPrefixOf_toList [BEq α] {xs ys : Array α} :
+@[simp, grind =] theorem isPrefixOf_toList [BEq α] {xs ys : Array α} :
     xs.toList.isPrefixOf ys.toList = xs.isPrefixOf ys := by
   cases xs
   cases ys
@@ -4480,32 +4485,32 @@ abbrev contains_def [DecidableEq α] {a : α} {xs : Array α} : xs.contains a
 
 /-! ### findSomeM?, findM?, findSome?, find? -/
 
-@[simp] theorem findSomeM?_toList [Monad m] [LawfulMonad m] {p : α → m (Option β)} {xs : Array α} :
+@[simp, grind =] theorem findSomeM?_toList [Monad m] [LawfulMonad m] {p : α → m (Option β)} {xs : Array α} :
     xs.toList.findSomeM? p = xs.findSomeM? p := by
   cases xs
   simp
 
-@[simp] theorem findM?_toList [Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Array α} :
+@[simp, grind =] theorem findM?_toList [Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Array α} :
     xs.toList.findM? p = xs.findM? p := by
   cases xs
   simp
 
-@[simp] theorem findSome?_toList {p : α → Option β} {xs : Array α} :
+@[simp, grind =] theorem findSome?_toList {p : α → Option β} {xs : Array α} :
     xs.toList.findSome? p = xs.findSome? p := by
   cases xs
   simp
 
-@[simp] theorem find?_toList {p : α → Bool} {xs : Array α} :
+@[simp, grind =] theorem find?_toList {p : α → Bool} {xs : Array α} :
     xs.toList.find? p = xs.find? p := by
   cases xs
   simp
 
-@[simp] theorem finIdxOf?_toList [BEq α] {a : α} {xs : Array α} :
+@[simp, grind =] theorem finIdxOf?_toList [BEq α] {a : α} {xs : Array α} :
     xs.toList.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast (by simp)) := by
   cases xs
   simp
 
-@[simp] theorem findFinIdx?_toList {p : α → Bool} {xs : Array α} :
+@[simp, grind =] theorem findFinIdx?_toList {p : α → Bool} {xs : Array α} :
     xs.toList.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast (by simp)) := by
   cases xs
   simp
@@ -4524,10 +4529,10 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
 
 theorem toListRev_toArray {l : List α} : l.toArray.toListRev = l.reverse := by simp
 
-@[simp] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by
+@[simp, grind =] theorem take_toArray {l : List α} {i : Nat} : l.toArray.take i = (l.take i).toArray := by
   apply Array.ext <;> simp
 
-@[simp] theorem mapM_toArray [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} :
+@[simp, grind =] theorem mapM_toArray [Monad m] [LawfulMonad m] {f : α → m β} {l : List α} :
     l.toArray.mapM f = List.toArray <$> l.mapM f := by
   simp only [← mapM'_eq_mapM, mapM_eq_foldlM]
   suffices ∀ xs : Array β,
@@ -4544,12 +4549,12 @@ theorem toListRev_toArray {l : List α} : l.toArray.toListRev = l.reverse := by
 theorem uset_toArray {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray.size} :
     l.toArray.uset i a h = (l.set i.toNat a).toArray := by simp
 
-@[simp] theorem modify_toArray {f : α → α} {l : List α} {i : Nat} :
+@[simp, grind =] theorem modify_toArray {f : α → α} {l : List α} {i : Nat} :
     l.toArray.modify i f = (l.modify i f).toArray := by
   apply ext'
   simp
 
-@[simp] theorem flatten_toArray {L : List (List α)} :
+@[simp, grind =] theorem flatten_toArray {L : List (List α)} :
     (L.toArray.map List.toArray).flatten = L.flatten.toArray := by
   apply ext'
   simp [Function.comp_def]
@@ -4624,11 +4629,11 @@ end Array
 
 namespace List
 
-@[simp] theorem unzip_toArray {as : List (α × β)} :
+@[simp, grind =] theorem unzip_toArray {as : List (α × β)} :
     as.toArray.unzip = Prod.map List.toArray List.toArray as.unzip := by
   ext1 <;> simp
 
-@[simp] theorem firstM_toArray [Alternative m] {as : List α} {f : α → m β} :
+@[simp, grind =] theorem firstM_toArray [Alternative m] {as : List α} {f : α → m β} :
     as.toArray.firstM f = as.firstM f := by
   unfold Array.firstM
   suffices ∀ i, i ≤ as.length → firstM.go f as.toArray (as.length - i) = firstM f (as.drop (as.length - i)) by

src/Init/Data/Array/Lex/Lemmas.lean

@@ -16,11 +16,11 @@ namespace Array
 
 /-! ### Lexicographic ordering -/
 
-@[simp] theorem _root_.List.lt_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray < l₂.toArray ↔ l₁ < l₂ := Iff.rfl
-@[simp] theorem _root_.List.le_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂ := Iff.rfl
+@[simp, grind =] theorem _root_.List.lt_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray < l₂.toArray ↔ l₁ < l₂ := Iff.rfl
+@[simp, grind =] theorem _root_.List.le_toArray [LT α] {l₁ l₂ : List α} : l₁.toArray ≤ l₂.toArray ↔ l₁ ≤ l₂ := Iff.rfl
 
-@[simp] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
-@[simp] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
+@[simp, grind =] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
+@[simp, grind =] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
 
 protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
 protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
@@ -47,7 +47,7 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     cases a == b <;> simp
   · simp
 
-@[simp] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} :
+@[simp, grind =] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} :
     l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
   induction l₁ generalizing l₂ with
   | nil => cases l₂ <;> simp [lex, Id.run]
@@ -57,7 +57,7 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 
-@[simp] theorem lex_toList [BEq α] {lt : α → α → Bool} {xs ys : Array α} :
+@[simp, grind =] theorem lex_toList [BEq α] {lt : α → α → Bool} {xs ys : Array α} :
     xs.toList.lex ys.toList lt = xs.lex ys lt := by
   cases xs <;> cases ys <;> simp
 

src/Init/Data/Array/MapIdx.lean

@@ -111,11 +111,11 @@ end Array
 
 namespace List
 
-@[simp] theorem mapFinIdx_toArray {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
+@[simp, grind =] theorem mapFinIdx_toArray {l : List α} {f : (i : Nat) → α → (h : i < l.length) → β} :
     l.toArray.mapFinIdx f = (l.mapFinIdx f).toArray := by
   ext <;> simp
 
-@[simp] theorem mapIdx_toArray {f : Nat → α → β} {l : List α} :
+@[simp, grind =] theorem mapIdx_toArray {f : Nat → α → β} {l : List α} :
     l.toArray.mapIdx f = (l.mapIdx f).toArray := by
   ext <;> simp
 
@@ -132,7 +132,7 @@ namespace Array
 @[deprecated getElem_zipIdx (since := "2025-01-21")]
 abbrev getElem_zipWithIndex := @getElem_zipIdx
 
-@[simp] theorem zipIdx_toArray {l : List α} {k : Nat} :
+@[simp, grind =] theorem zipIdx_toArray {l : List α} {k : Nat} :
     l.toArray.zipIdx k = (l.zipIdx k).toArray := by
   ext i hi₁ hi₂ <;> simp [Nat.add_comm]
 
@@ -454,7 +454,7 @@ end Array
 
 namespace List
 
-theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
+@[grind] theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
     {f : (i : Nat) → α → (h : i < l.length) → m β} :
     l.toArray.mapFinIdxM f = toArray <$> l.mapFinIdxM f := by
   let rec go (i : Nat) (acc : Array β) (inv : i + acc.size = l.length) :
@@ -475,7 +475,7 @@ theorem mapFinIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
   simp only [Array.mapFinIdxM, mapFinIdxM]
   exact go _ #[] _
 
-theorem mapIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
+@[grind] theorem mapIdxM_toArray [Monad m] [LawfulMonad m] {l : List α}
     {f : Nat → α → m β} :
     l.toArray.mapIdxM f = toArray <$> l.mapIdxM f := by
   let rec go (bs : List α) (acc : Array β) (inv : bs.length + acc.size = l.length) :

src/Init/Data/Array/Monadic.lean

@@ -264,7 +264,7 @@ end Array
 
 namespace List
 
-theorem filterM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
+@[grind =] theorem filterM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
     l.toArray.filterM p = toArray <$> l.filterM p := by
   simp only [Array.filterM, filterM, foldlM_toArray, bind_pure_comp, Functor.map_map]
   conv => lhs; rw [← reverse_nil]
@@ -284,7 +284,7 @@ theorem filterM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bo
   subst w
   rw [filterM_toArray]
 
-theorem filterRevM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
+@[grind =] theorem filterRevM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m Bool} :
     l.toArray.filterRevM p = toArray <$> l.filterRevM p := by
   simp [Array.filterRevM, filterRevM]
   rw [← foldlM_reverse, ← foldlM_toArray, ← Array.filterM, filterM_toArray]
@@ -296,7 +296,7 @@ theorem filterRevM_toArray [Monad m] [LawfulMonad m] {l : List α} {p : α → m
   subst w
   rw [filterRevM_toArray]
 
-theorem filterMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} :
+@[grind =] theorem filterMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Option β)} :
     l.toArray.filterMapM f = toArray <$> l.filterMapM f := by
   simp [Array.filterMapM, filterMapM]
   conv => lhs; rw [← reverse_nil]
@@ -314,7 +314,7 @@ theorem filterMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m
   subst w
   rw [filterMapM_toArray]
 
-@[simp] theorem flatMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Array β)} :
+@[simp, grind =] theorem flatMapM_toArray [Monad m] [LawfulMonad m] {l : List α} {f : α → m (Array β)} :
     l.toArray.flatMapM f = toArray <$> l.flatMapM (fun a => Array.toList <$> f a) := by
   simp only [Array.flatMapM, bind_pure_comp, foldlM_toArray, flatMapM]
   conv => lhs; arg 2; change [].reverse.flatten.toArray

src/Init/Data/List/ToArray.lean

@@ -66,7 +66,7 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr
   apply ext'
   simp
 
-@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
+@[simp, grind =] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
   apply ext'
   simp
 
@@ -75,37 +75,37 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr
   funext a
   simp
 
-@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
+@[simp, grind =] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
   cases l <;> simp [Array.isEmpty]
 
 @[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = Array.singleton a := rfl
 
-@[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
+@[simp, grind =] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
   simp only [back!, size_toArray, getElem!_toArray, getLast!_eq_getElem!]
 
-@[simp] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by
+@[simp, grind =] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by
   simp [back?, List.getLast?_eq_getElem?]
 
-@[simp] theorem back_toArray (l : List α) (h) :
+@[simp, grind =] theorem back_toArray (l : List α) (h) :
     l.toArray.back = l.getLast (by simp at h; exact ne_nil_of_length_pos h) := by
   simp [back, List.getLast_eq_getElem]
 
-@[simp] theorem _root_.Array.getLast!_toList [Inhabited α] (xs : Array α) :
+@[simp, grind =] theorem _root_.Array.getLast!_toList [Inhabited α] (xs : Array α) :
     xs.toList.getLast! = xs.back! := by
   rcases xs with ⟨xs⟩
   simp
 
-@[simp] theorem _root_.Array.getLast?_toList (xs : Array α) :
+@[simp, grind =] theorem _root_.Array.getLast?_toList (xs : Array α) :
     xs.toList.getLast? = xs.back? := by
   rcases xs with ⟨xs⟩
   simp
 
-@[simp] theorem _root_.Array.getLast_toList (xs : Array α) (h) :
+@[simp, grind =] theorem _root_.Array.getLast_toList (xs : Array α) (h) :
     xs.toList.getLast h = xs.back (by simpa [ne_nil_iff_length_pos] using h) := by
   rcases xs with ⟨xs⟩
   simp
 
-@[simp] theorem set_toArray (l : List α) (i : Nat) (a : α) (h : i < l.length) :
+@[simp, grind =] theorem set_toArray (l : List α) (i : Nat) (a : α) (h : i < l.length) :
     (l.toArray.set i a) = (l.set i a).toArray := rfl
 
 @[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
@@ -126,30 +126,30 @@ theorem toArray_cons (a : α) (l : List α) : (a :: l).toArray = #[a] ++ l.toArr
     simp only [t]
     congr
 
-@[simp] theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) :
+@[simp, grind =] theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) :
     forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b) := by
   change Array.forIn' _ _ _ = List.forIn' _ _ _
   rw [Array.forIn', forIn'_loop_toArray]
   simp
 
-@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) :
+@[simp, grind =] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) :
     forIn l.toArray b f = forIn l b f := by
   simpa using forIn'_toArray l b fun a m b => f a b
 
-theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
+@[grind =] theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
     l.toArray.foldrM f init = l.foldrM f init := by
   rw [foldrM_eq_reverse_foldlM_toList]
   simp
 
-theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
+@[grind =] theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
     l.toArray.foldlM f init = l.foldlM f init := by
   rw [foldlM_toList]
 
-theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
+@[grind =] theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
     l.toArray.foldr f init = l.foldr f init := by
   rw [foldr_toList]
 
-theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
+@[grind =] theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
     l.toArray.foldl f init = l.foldl f init := by
   rw [foldl_toList]
 
@@ -176,7 +176,7 @@ theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
   simp only [size_toArray, foldlM_toArray']
   induction l <;> simp_all
 
-@[simp]
+@[simp, grind =]
 theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
     (forM l.toArray f) = l.forM f :=
   forM_toArray' l f rfl
@@ -195,15 +195,15 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
   subst h
   rw [foldl_toList]
 
-@[simp] theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum := by
+@[simp, grind =] theorem sum_toArray [Add α] [Zero α] (l : List α) : l.toArray.sum = l.sum := by
   simp [Array.sum, List.sum]
 
-@[simp] theorem append_toArray (l₁ l₂ : List α) :
+@[simp, grind =] theorem append_toArray (l₁ l₂ : List α) :
     l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
   apply ext'
   simp
 
-@[simp] theorem push_append_toArray {as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a ::bs).toArray := by
+@[simp] theorem push_append_toArray {as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a :: bs).toArray := by
   cases as
   simp
 
@@ -213,7 +213,7 @@ theorem forM_toArray [Monad m] (l : List α) (f : α → m PUnit) :
 @[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a bs => push bs a) as = as ++ l.reverse.toArray := by
   rw [foldr_eq_foldl_reverse, foldl_push]
 
-@[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
+@[simp, grind =] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
     l.toArray.findSomeM? f = l.findSomeM? f := by
   rw [Array.findSomeM?]
   simp only [bind_pure_comp, map_pure, forIn_toArray]
@@ -246,7 +246,7 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis
     l.toArray.findRevM? f = l.reverse.findM? f := by
   rw [Array.findRevM?, findSomeRevM?_toArray, findM?_eq_findSomeM?]
 
-@[simp] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
+@[simp, grind =] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
     l.toArray.findM? f = l.findM? f := by
   rw [Array.findM?]
   simp only [bind_pure_comp, map_pure, forIn_toArray]
@@ -257,11 +257,11 @@ theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : Lis
     congr
     ext1 (_|_) <;> simp [ih]
 
-@[simp] theorem findSome?_toArray (f : α → Option β) (l : List α) :
+@[simp, grind =] theorem findSome?_toArray (f : α → Option β) (l : List α) :
     l.toArray.findSome? f = l.findSome? f := by
   rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run]
 
-@[simp] theorem find?_toArray (f : α → Bool) (l : List α) :
+@[simp, grind =] theorem find?_toArray (f : α → Bool) (l : List α) :
     l.toArray.find? f = l.find? f := by
   rw [Array.find?]
   simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray]
@@ -297,12 +297,12 @@ private theorem findFinIdx?_loop_toArray (w : l' = l.drop j) :
     simp
 termination_by l.length - j
 
-@[simp] theorem findFinIdx?_toArray (p : α → Bool) (l : List α) :
+@[simp, grind =] theorem findFinIdx?_toArray (p : α → Bool) (l : List α) :
     l.toArray.findFinIdx? p = l.findFinIdx? p := by
   rw [Array.findFinIdx?, findFinIdx?, findFinIdx?_loop_toArray]
   simp
 
-@[simp] theorem findIdx?_toArray (p : α → Bool) (l : List α) :
+@[simp, grind =] theorem findIdx?_toArray (p : α → Bool) (l : List α) :
     l.toArray.findIdx? p = l.findIdx? p := by
   rw [Array.findIdx?_eq_map_findFinIdx?_val, findIdx?_eq_map_findFinIdx?_val]
   simp
@@ -334,21 +334,21 @@ private theorem idxAuxOf_toArray [BEq α] (a : α) (l : List α) (j : Nat) (w :
     simp
 termination_by l.length - j
 
-@[simp] theorem finIdxOf?_toArray [BEq α] (a : α) (l : List α) :
+@[simp, grind =] theorem finIdxOf?_toArray [BEq α] (a : α) (l : List α) :
     l.toArray.finIdxOf? a = l.finIdxOf? a := by
   rw [Array.finIdxOf?, finIdxOf?, findFinIdx?]
   simp [idxAuxOf_toArray]
 
-@[simp] theorem idxOf?_toArray [BEq α] (a : α) (l : List α) :
+@[simp, grind =] theorem idxOf?_toArray [BEq α] (a : α) (l : List α) :
     l.toArray.idxOf? a = l.idxOf? a := by
   rw [Array.idxOf?, idxOf?]
   simp [finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
 
-@[simp] theorem findIdx_toArray {as : List α} {p : α → Bool} :
+@[simp, grind =] theorem findIdx_toArray {as : List α} {p : α → Bool} :
     as.toArray.findIdx p = as.findIdx p := by
   rw [Array.findIdx, findIdx?_toArray, findIdx_eq_getD_findIdx?]
 
-@[simp] theorem idxOf_toArray [BEq α] {as : List α} {a : α} :
+@[simp, grind =] theorem idxOf_toArray [BEq α] {as : List α} {a : α} :
     as.toArray.idxOf a = as.idxOf a := by
   rw [Array.idxOf, findIdx_toArray, idxOf]
 
@@ -383,7 +383,7 @@ theorem isPrefixOfAux_toArray_zero [BEq α] (l₁ l₂ : List α) (hle : l₁.le
   | a::l₁, b::l₂ =>
     simp [isPrefixOf_cons₂, isPrefixOfAux_toArray_succ', isPrefixOfAux_toArray_zero]
 
-@[simp] theorem isPrefixOf_toArray [BEq α] (l₁ l₂ : List α) :
+@[simp, grind =] theorem isPrefixOf_toArray [BEq α] (l₁ l₂ : List α) :
     l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂ := by
   rw [Array.isPrefixOf]
   split <;> rename_i h
@@ -429,12 +429,12 @@ theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List
   | a :: as, b :: bs =>
     simp [zipWith_cons_cons, zipWithAux_toArray_succ', zipWithAux_toArray_zero, push_append_toArray]
 
-@[simp] theorem zipWith_toArray (as : List α) (bs : List β) (f : α → β → γ) :
+@[simp, grind =] theorem zipWith_toArray (as : List α) (bs : List β) (f : α → β → γ) :
     Array.zipWith f as.toArray bs.toArray = (List.zipWith f as bs).toArray := by
   rw [Array.zipWith]
   simp [zipWithAux_toArray_zero]
 
-@[simp] theorem zip_toArray (as : List α) (bs : List β) :
+@[simp, grind =] theorem zip_toArray (as : List α) (bs : List β) :
     Array.zip as.toArray bs.toArray = (List.zip as bs).toArray := by
   simp [Array.zip, zipWith_toArray, zip]
 
@@ -472,16 +472,16 @@ theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → O
   termination_by max as.length bs.length - i
   decreasing_by simp_wf; decreasing_trivial_pre_omega
 
-@[simp] theorem zipWithAll_toArray (f : Option α → Option β → γ) (as : List α) (bs : List β) :
+@[simp, grind =] theorem zipWithAll_toArray (f : Option α → Option β → γ) (as : List α) (bs : List β) :
     Array.zipWithAll f as.toArray bs.toArray = (List.zipWithAll f as bs).toArray := by
   simp [Array.zipWithAll, zipWithAll_go_toArray]
 
-@[simp] theorem toArray_appendList (l₁ l₂ : List α) :
+@[simp, grind =] theorem toArray_appendList (l₁ l₂ : List α) :
     l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray := by
   apply ext'
   simp
 
-@[simp] theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray := by
+@[simp, grind =] theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray := by
   apply ext'
   simp
 
@@ -513,7 +513,7 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
         split <;> simp_all
       · simp_all [drop_eq_nil_of_le]
 
-@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) :
+@[simp, grind =] theorem takeWhile_toArray (p : α → Bool) (l : List α) :
     l.toArray.takeWhile p = (l.takeWhile p).toArray := by
   simp [Array.takeWhile, takeWhile_go_toArray]
 
@@ -528,11 +528,11 @@ private theorem popWhile_toArray_aux (p : α → Bool) (l : List α) :
     · rfl
     · simp
 
-@[simp] theorem popWhile_toArray (p : α → Bool) (l : List α) :
+@[simp, grind =] theorem popWhile_toArray (p : α → Bool) (l : List α) :
     l.toArray.popWhile p = (l.reverse.dropWhile p).reverse.toArray := by
   simp [← popWhile_toArray_aux]
 
-@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
+@[simp, grind =] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
     l.toArray.setIfInBounds i a  = (l.set i a).toArray := by
   apply ext'
   simp only [setIfInBounds]
@@ -540,7 +540,7 @@ private theorem popWhile_toArray_aux (p : α → Bool) (l : List α) :
   · simp
   · simp_all [List.set_eq_of_length_le]
 
-@[simp] theorem toArray_replicate (n : Nat) (v : α) :
+@[simp, grind =] theorem toArray_replicate (n : Nat) (v : α) :
     (List.replicate n v).toArray = Array.replicate n v := rfl
 
 theorem _root_.Array.replicate_eq_toArray_replicate :
@@ -550,7 +550,7 @@ theorem _root_.Array.replicate_eq_toArray_replicate :
 @[deprecated _root_.Array.replicate_eq_toArray_replicate (since := "2025-03-18")]
 abbrev _root_.Array.mkArray_eq_toArray_replicate := @_root_.Array.replicate_eq_toArray_replicate
 
-@[simp] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl
+@[simp, grind =] theorem flatMap_empty {β} (f : α → Array β) : (#[] : Array α).flatMap f = #[] := rfl
 
 theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α) :
     (a :: as).toArray.flatMap f = f a ++ as.toArray.flatMap f := by
@@ -562,7 +562,7 @@ theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α)
   intro xs
   induction as generalizing xs <;> simp_all
 
-@[simp] theorem flatMap_toArray {β} (f : α → Array β) (as : List α) :
+@[simp, grind =] theorem flatMap_toArray {β} (f : α → Array β) (as : List α) :
     as.toArray.flatMap f = (as.flatMap (fun a => (f a).toList)).toArray := by
   induction as with
   | nil => simp
@@ -570,12 +570,12 @@ theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α)
     apply ext'
     simp [ih, flatMap_toArray_cons]
 
-@[simp] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
+@[simp, grind =] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
     l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by
   apply ext'
   simp
 
-@[simp] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
+@[simp, grind =] theorem eraseIdx_toArray (l : List α) (i : Nat) (h : i < l.toArray.size) :
     l.toArray.eraseIdx i h = (l.eraseIdx i).toArray := by
   rw [Array.eraseIdx]
   split <;> rename_i h'
@@ -593,19 +593,19 @@ decreasing_by
   simp
   omega
 
-@[simp] theorem eraseIdxIfInBounds_toArray (l : List α) (i : Nat) :
+@[simp, grind =] theorem eraseIdxIfInBounds_toArray (l : List α) (i : Nat) :
     l.toArray.eraseIdxIfInBounds i = (l.eraseIdx i).toArray := by
   rw [Array.eraseIdxIfInBounds]
   split
   · simp
   · simp_all [eraseIdx_eq_self.2]
 
-@[simp] theorem eraseP_toArray {as : List α} {p : α → Bool} :
+@[simp, grind =] theorem eraseP_toArray {as : List α} {p : α → Bool} :
     as.toArray.eraseP p = (as.eraseP p).toArray := by
   rw [Array.eraseP, List.eraseP_eq_eraseIdx, findFinIdx?_toArray]
   split <;> simp [*, findIdx?_eq_map_findFinIdx?_val]
 
-@[simp] theorem erase_toArray [BEq α] {as : List α} {a : α} :
+@[simp, grind =] theorem erase_toArray [BEq α] {as : List α} {a : α} :
     as.toArray.erase a = (as.erase a).toArray := by
   rw [Array.erase, finIdxOf?_toArray, List.erase_eq_eraseIdx]
   rw [idxOf?_eq_map_finIdxOf?_val]
@@ -635,7 +635,7 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j
     subst this
     simp
 
-@[simp] theorem insertIdx_toArray (l : List α) (i : Nat) (a : α) (h : i ≤ l.toArray.size):
+@[simp, grind =] theorem insertIdx_toArray (l : List α) (i : Nat) (a : α) (h : i ≤ l.toArray.size):
     l.toArray.insertIdx i a = (l.insertIdx i a).toArray := by
   rw [Array.insertIdx]
   rw [insertIdx_loop_toArray (h := h)]
@@ -658,7 +658,7 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j
         congr
         omega
 
-@[simp] theorem insertIdxIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
+@[simp, grind =] theorem insertIdxIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
     l.toArray.insertIdxIfInBounds i a = (l.insertIdx i a).toArray := by
   rw [Array.insertIdxIfInBounds]
   split <;> rename_i h'
@@ -666,7 +666,7 @@ private theorem insertIdx_loop_toArray (i : Nat) (l : List α) (j : Nat) (hj : j
   · simp only [size_toArray, Nat.not_le] at h'
     rw [List.insertIdx_of_length_lt (h := h')]
 
-@[simp]
+@[simp, grind =]
 theorem replace_toArray [BEq α] [LawfulBEq α] (l : List α) (a b : α) :
     l.toArray.replace a b = (l.replace a b).toArray := by
   rw [Array.replace]
@@ -700,11 +700,11 @@ theorem replace_toArray [BEq α] [LawfulBEq α] (l : List α) (a b : α) :
               exact ⟨i, by omega, h.1⟩
           · rfl
 
-@[simp] theorem leftpad_toArray (n : Nat) (a : α) (l : List α) :
+@[simp, grind =] theorem leftpad_toArray (n : Nat) (a : α) (l : List α) :
     Array.leftpad n a l.toArray = (leftpad n a l).toArray := by
   simp [leftpad, Array.leftpad, ← toArray_replicate]
 
-@[simp] theorem rightpad_toArray (n : Nat) (a : α) (l : List α) :
+@[simp, grind =] theorem rightpad_toArray (n : Nat) (a : α) (l : List α) :
     Array.rightpad n a l.toArray = (rightpad n a l).toArray := by
   simp [rightpad, Array.rightpad, ← toArray_replicate]
 

src/Init/Data/Option/Attach.lean

@@ -138,7 +138,7 @@ theorem toList_attach (o : Option α) :
     o.attach.toList = o.toList.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
   cases o <;> simp
 
-@[simp] theorem attach_toList (o : Option α) :
+@[simp, grind =] theorem attach_toList (o : Option α) :
     o.toList.attach = (o.attach.map fun ⟨a, h⟩ => ⟨a, by simpa using h⟩).toList := by
   cases o <;> simp
 

src/Init/Data/Vector/Basic.lean

@@ -29,7 +29,7 @@ structure Vector (α : Type u) (n : Nat) extends Array α where
   size_toArray : toArray.size = n
 deriving Repr, DecidableEq
 
-attribute [simp] Vector.size_toArray
+attribute [simp, grind] Vector.size_toArray
 
 /--
 Converts an array to a vector. The resulting vector's size is the array's size.

src/Init/Data/Vector/DecidableEq.lean

@@ -58,7 +58,7 @@ theorem beq_eq_decide [BEq α] (xs ys : Vector α n) :
     (mk xs ha == mk ys hb) = (xs == ys) := by
   simp [BEq.beq]
 
-@[simp] theorem beq_toArray [BEq α] (xs ys : Vector α n) : (xs.toArray == ys.toArray) = (xs == ys) := by
+@[simp, grind =] theorem beq_toArray [BEq α] (xs ys : Vector α n) : (xs.toArray == ys.toArray) = (xs == ys) := by
   simp [beq_eq_decide, Array.beq_eq_decide]
 
 @[simp] theorem beq_toList [BEq α] (xs ys : Vector α n) : (xs.toList == ys.toList) = (xs == ys) := by

src/Init/Data/Vector/Lemmas.lean

@@ -263,57 +263,57 @@ abbrev zipWithIndex_mk := @zipIdx_mk
 
 /-! ### toArray lemmas -/
 
-@[simp] theorem getElem_toArray {α n} {xs : Vector α n} {i : Nat} (h : i < xs.toArray.size) :
+@[simp, grind] theorem getElem_toArray {α n} {xs : Vector α n} {i : Nat} (h : i < xs.toArray.size) :
     xs.toArray[i] = xs[i]'(by simpa using h) := by
   cases xs
   simp
 
-@[simp] theorem getElem?_toArray {α n} {xs : Vector α n} {i : Nat} :
+@[simp, grind] theorem getElem?_toArray {α n} {xs : Vector α n} {i : Nat} :
     xs.toArray[i]? = xs[i]? := by
   cases xs
   simp
 
-@[simp] theorem toArray_append {xs : Vector α m} {ys : Vector α n} :
+@[simp, grind _=_] theorem toArray_append {xs : Vector α m} {ys : Vector α n} :
     (xs ++ ys).toArray = xs.toArray ++ ys.toArray := rfl
 
-@[simp] theorem toArray_drop {xs : Vector α n} {i} :
+@[simp, grind] theorem toArray_drop {xs : Vector α n} {i} :
     (xs.drop i).toArray = xs.toArray.extract i xs.size := rfl
 
-@[simp] theorem toArray_empty : (#v[] : Vector α 0).toArray = #[] := rfl
+@[simp, grind] theorem toArray_empty : (#v[] : Vector α 0).toArray = #[] := rfl
 
-@[simp] theorem toArray_emptyWithCapacity {cap} :
+@[simp, grind] theorem toArray_emptyWithCapacity {cap} :
     (Vector.emptyWithCapacity (α := α) cap).toArray = Array.emptyWithCapacity cap := rfl
 
 @[deprecated toArray_emptyWithCapacity (since := "2025-03-12")]
 abbrev toArray_mkEmpty := @toArray_emptyWithCapacity
 
-@[simp] theorem toArray_eraseIdx {xs : Vector α n} {i} (h) :
+@[simp, grind] theorem toArray_eraseIdx {xs : Vector α n} {i} (h) :
     (xs.eraseIdx i h).toArray = xs.toArray.eraseIdx i (by simp [h]) := rfl
 
-@[simp] theorem toArray_eraseIdx! {xs : Vector α n} {i} (hi : i < n) :
+@[simp, grind] theorem toArray_eraseIdx! {xs : Vector α n} {i} (hi : i < n) :
     (xs.eraseIdx! i).toArray = xs.toArray.eraseIdx! i := by
   cases xs; simp_all [Array.eraseIdx!]
 
-@[simp] theorem toArray_insertIdx {xs : Vector α n} {i x} (h) :
+@[simp, grind] theorem toArray_insertIdx {xs : Vector α n} {i x} (h) :
     (xs.insertIdx i x h).toArray = xs.toArray.insertIdx i x (by simp [h]) := rfl
 
-@[simp] theorem toArray_insertIdx! {xs : Vector α n} {i x} (hi : i ≤ n) :
+@[simp, grind] theorem toArray_insertIdx! {xs : Vector α n} {i x} (hi : i ≤ n) :
     (xs.insertIdx! i x).toArray = xs.toArray.insertIdx! i x := by
   cases xs; simp_all [Array.insertIdx!]
 
-@[simp] theorem toArray_cast {xs : Vector α n} (h : n = m) :
+@[simp, grind] theorem toArray_cast {xs : Vector α n} (h : n = m) :
     (xs.cast h).toArray = xs.toArray := rfl
 
-@[simp] theorem toArray_extract {xs : Vector α n} {start stop} :
+@[simp, grind] theorem toArray_extract {xs : Vector α n} {start stop} :
     (xs.extract start stop).toArray = xs.toArray.extract start stop := rfl
 
-@[simp] theorem toArray_map {f : α → β} {xs : Vector α n} :
+@[simp, grind] theorem toArray_map {f : α → β} {xs : Vector α n} :
     (xs.map f).toArray = xs.toArray.map f := rfl
 
-@[simp] theorem toArray_mapIdx {f : Nat → α → β} {xs : Vector α n} :
+@[simp, grind] theorem toArray_mapIdx {f : Nat → α → β} {xs : Vector α n} :
     (xs.mapIdx f).toArray = xs.toArray.mapIdx f := rfl
 
-@[simp] theorem toArray_mapFinIdx {f : (i : Nat) → α → (h : i < n) → β} {xs : Vector α n} :
+@[simp, grind] theorem toArray_mapFinIdx {f : (i : Nat) → α → (h : i < n) → β} {xs : Vector α n} :
     (xs.mapFinIdx f).toArray =
       xs.toArray.mapFinIdx (fun i a h => f i a (by simpa [xs.size_toArray] using h)) :=
   rfl
@@ -331,145 +331,145 @@ theorem toArray_mapM_go [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector
     rfl
   · simp
 
-@[simp] theorem toArray_mapM [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector α n} :
+@[simp, grind] theorem toArray_mapM [Monad m] [LawfulMonad m] {f : α → m β} {xs : Vector α n} :
     toArray <$> xs.mapM f = xs.toArray.mapM f := by
   rcases xs with ⟨xs, rfl⟩
   unfold mapM
   rw [toArray_mapM_go]
   rfl
 
-@[simp] theorem toArray_ofFn {f : Fin n → α} : (Vector.ofFn f).toArray = Array.ofFn f := rfl
+@[simp, grind] theorem toArray_ofFn {f : Fin n → α} : (Vector.ofFn f).toArray = Array.ofFn f := rfl
 
-@[simp] theorem toArray_pop {xs : Vector α n} : xs.pop.toArray = xs.toArray.pop := rfl
+@[simp, grind] theorem toArray_pop {xs : Vector α n} : xs.pop.toArray = xs.toArray.pop := rfl
 
-@[simp] theorem toArray_push {xs : Vector α n} {x} : (xs.push x).toArray = xs.toArray.push x := rfl
+@[simp, grind] theorem toArray_push {xs : Vector α n} {x} : (xs.push x).toArray = xs.toArray.push x := rfl
 
-@[simp] theorem toArray_beq_toArray [BEq α] {xs : Vector α n} {ys : Vector α n} :
+@[simp, grind] theorem toArray_beq_toArray [BEq α] {xs : Vector α n} {ys : Vector α n} :
     (xs.toArray == ys.toArray) = (xs == ys) := by
   simp [instBEq, isEqv, Array.instBEq, Array.isEqv, xs.2, ys.2]
 
-@[simp] theorem toArray_range : (Vector.range n).toArray = Array.range n := rfl
+@[simp, grind] theorem toArray_range : (Vector.range n).toArray = Array.range n := rfl
 
-@[simp] theorem toArray_reverse (xs : Vector α n) : xs.reverse.toArray = xs.toArray.reverse := rfl
+@[simp, grind] theorem toArray_reverse (xs : Vector α n) : xs.reverse.toArray = xs.toArray.reverse := rfl
 
-@[simp] theorem toArray_set {xs : Vector α n} {i x} (h) :
+@[simp, grind] theorem toArray_set {xs : Vector α n} {i x} (h) :
     (xs.set i x).toArray = xs.toArray.set i x (by simpa using h):= rfl
 
-@[simp] theorem toArray_set! {xs : Vector α n} {i x} :
+@[simp, grind] theorem toArray_set! {xs : Vector α n} {i x} :
     (xs.set! i x).toArray = xs.toArray.set! i x := rfl
 
-@[simp] theorem toArray_setIfInBounds {xs : Vector α n} {i x} :
+@[simp, grind] theorem toArray_setIfInBounds {xs : Vector α n} {i x} :
     (xs.setIfInBounds i x).toArray = xs.toArray.setIfInBounds i x := rfl
 
-@[simp] theorem toArray_singleton {x : α} : (Vector.singleton x).toArray = #[x] := rfl
+@[simp, grind] theorem toArray_singleton {x : α} : (Vector.singleton x).toArray = #[x] := rfl
 
-@[simp] theorem toArray_swap {xs : Vector α n} {i j} (hi hj) : (xs.swap i j).toArray =
+@[simp, grind] theorem toArray_swap {xs : Vector α n} {i j} (hi hj) : (xs.swap i j).toArray =
     xs.toArray.swap i j (by simp [hi, hj]) (by simp [hi, hj]) := rfl
 
-@[simp] theorem toArray_swapIfInBounds {xs : Vector α n} {i j} :
+@[simp, grind] theorem toArray_swapIfInBounds {xs : Vector α n} {i j} :
     (xs.swapIfInBounds i j).toArray = xs.toArray.swapIfInBounds i j := rfl
 
-@[simp] theorem toArray_swapAt {xs : Vector α n} {i x} (h) :
+theorem toArray_swapAt {xs : Vector α n} {i x} (h) :
     ((xs.swapAt i x).fst, (xs.swapAt i x).snd.toArray) =
       ((xs.toArray.swapAt i x (by simpa using h)).fst,
         (xs.toArray.swapAt i x (by simpa using h)).snd) := rfl
 
-@[simp] theorem toArray_swapAt! {xs : Vector α n} {i x} :
+theorem toArray_swapAt! {xs : Vector α n} {i x} :
     ((xs.swapAt! i x).fst, (xs.swapAt! i x).snd.toArray) =
       ((xs.toArray.swapAt! i x).fst, (xs.toArray.swapAt! i x).snd) := rfl
 
-@[simp] theorem toArray_take {xs : Vector α n} {i} : (xs.take i).toArray = xs.toArray.take i := rfl
+@[simp, grind] theorem toArray_take {xs : Vector α n} {i} : (xs.take i).toArray = xs.toArray.take i := rfl
 
-@[simp] theorem toArray_zipIdx {xs : Vector α n} (k : Nat := 0) :
+@[simp, grind] theorem toArray_zipIdx {xs : Vector α n} (k : Nat := 0) :
     (xs.zipIdx k).toArray = xs.toArray.zipIdx k := rfl
 
-@[simp] theorem toArray_zipWith {f : α → β → γ} {as : Vector α n} {bs : Vector β n} :
+@[simp, grind] theorem toArray_zipWith {f : α → β → γ} {as : Vector α n} {bs : Vector β n} :
     (Vector.zipWith f as bs).toArray = Array.zipWith f as.toArray bs.toArray := rfl
 
-@[simp] theorem anyM_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
+@[simp, grind] theorem anyM_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
     xs.toArray.anyM p = xs.anyM p := by
   cases xs
   simp
 
-@[simp] theorem allM_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
+@[simp, grind] theorem allM_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
     xs.toArray.allM p = xs.allM p := by
   cases xs
   simp
 
-@[simp] theorem any_toArray {p : α → Bool} {xs : Vector α n} :
+@[simp, grind] theorem any_toArray {p : α → Bool} {xs : Vector α n} :
     xs.toArray.any p = xs.any p := by
   cases xs
   simp
 
-@[simp] theorem all_toArray {p : α → Bool} {xs : Vector α n} :
+@[simp, grind] theorem all_toArray {p : α → Bool} {xs : Vector α n} :
     xs.toArray.all p = xs.all p := by
   cases xs
   simp
 
-@[simp] theorem countP_toArray {p : α → Bool} {xs : Vector α n} :
+@[simp, grind] theorem countP_toArray {p : α → Bool} {xs : Vector α n} :
     xs.toArray.countP p = xs.countP p := by
   cases xs
   simp
 
-@[simp] theorem count_toArray [BEq α] {a : α} {xs : Vector α n} :
+@[simp, grind] theorem count_toArray [BEq α] {a : α} {xs : Vector α n} :
     xs.toArray.count a = xs.count a := by
   cases xs
   simp
 
-@[simp] theorem replace_toArray [BEq α] {xs : Vector α n} {a b} :
+@[simp, grind] theorem replace_toArray [BEq α] {xs : Vector α n} {a b} :
     xs.toArray.replace a b = (xs.replace a b).toArray := rfl
 
-@[simp] theorem find?_toArray {p : α → Bool} {xs : Vector α n} :
+@[simp, grind] theorem find?_toArray {p : α → Bool} {xs : Vector α n} :
     xs.toArray.find? p = xs.find? p := by
   cases xs
   simp
 
-@[simp] theorem findSome?_toArray {f : α → Option β} {xs : Vector α n} :
+@[simp, grind] theorem findSome?_toArray {f : α → Option β} {xs : Vector α n} :
     xs.toArray.findSome? f = xs.findSome? f := by
   cases xs
   simp
 
-@[simp] theorem findRev?_toArray {p : α → Bool} {xs : Vector α n} :
+@[simp, grind] theorem findRev?_toArray {p : α → Bool} {xs : Vector α n} :
     xs.toArray.findRev? p = xs.findRev? p := by
   cases xs
   simp
 
-@[simp] theorem findSomeRev?_toArray {f : α → Option β} {xs : Vector α n} :
+@[simp, grind] theorem findSomeRev?_toArray {f : α → Option β} {xs : Vector α n} :
     xs.toArray.findSomeRev? f = xs.findSomeRev? f := by
   cases xs
   simp
 
-@[simp] theorem findM?_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
+@[simp, grind] theorem findM?_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
     xs.toArray.findM? p = xs.findM? p := by
   cases xs
   simp
 
-@[simp] theorem findSomeM?_toArray [Monad m] {f : α → m (Option β)} {xs : Vector α n} :
+@[simp, grind] theorem findSomeM?_toArray [Monad m] {f : α → m (Option β)} {xs : Vector α n} :
     xs.toArray.findSomeM? f = xs.findSomeM? f := by
   cases xs
   simp
 
-@[simp] theorem findRevM?_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
+@[simp, grind] theorem findRevM?_toArray [Monad m] {p : α → m Bool} {xs : Vector α n} :
     xs.toArray.findRevM? p = xs.findRevM? p := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem findSomeRevM?_toArray [Monad m] {f : α → m (Option β)} {xs : Vector α n} :
+@[simp, grind] theorem findSomeRevM?_toArray [Monad m] {f : α → m (Option β)} {xs : Vector α n} :
     xs.toArray.findSomeRevM? f = xs.findSomeRevM? f := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem finIdxOf?_toArray [BEq α] {a : α} {xs : Vector α n} :
+@[simp, grind] theorem finIdxOf?_toArray [BEq α] {a : α} {xs : Vector α n} :
     xs.toArray.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast xs.size_toArray.symm) := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem findFinIdx?_toArray {p : α → Bool} {xs : Vector α n} :
+@[simp, grind] theorem findFinIdx?_toArray {p : α → Bool} {xs : Vector α n} :
     xs.toArray.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast xs.size_toArray.symm) := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem toArray_replicate : (replicate n a).toArray = Array.replicate n a := rfl
+@[simp, grind] theorem toArray_replicate : (replicate n a).toArray = Array.replicate n a := rfl
 
 @[deprecated toArray_replicate (since := "2025-03-18")]
 abbrev toArray_mkVector := @toArray_replicate
@@ -3082,7 +3082,7 @@ set_option linter.indexVariables false in
 
 /-! ### swap -/
 
-theorem getElem_swap {xs : Vector α n} {i j : Nat} (hi hj) {k : Nat} (hk : k < n) :
+@[grind] theorem getElem_swap {xs : Vector α n} {i j : Nat} (hi hj) {k : Nat} (hk : k < n) :
     (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k] := by
   cases xs
   simp_all [Array.getElem_swap]
@@ -3099,6 +3099,13 @@ theorem getElem_swap {xs : Vector α n} {i j : Nat} (hi hj) {k : Nat} (hk : k <
       (hi' : k ≠ i) (hj' : k ≠ j) : (xs.swap i j hi hj)[k] = xs[k] := by
   simp_all [getElem_swap]
 
+@[grind]
+theorem getElem?_swap {xs : Vector α n} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i j hi hj)[k]? =
+    if j = k then some xs[i] else if i = k then some xs[j] else xs[k]? := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.getElem?_swap]
+
+
 @[simp] theorem swap_swap {xs : Vector α n} {i j : Nat} (hi hj) :
     (xs.swap i j hi hj).swap i j hi hj = xs := by
   cases xs

src/Init/Data/Vector/Lex.lean

@@ -18,8 +18,8 @@ namespace Vector
 
 /-! ### Lexicographic ordering -/
 
-@[simp] theorem lt_toArray [LT α] {xs ys : Vector α n} : xs.toArray < ys.toArray ↔ xs < ys := Iff.rfl
-@[simp] theorem le_toArray [LT α] {xs ys : Vector α n} : xs.toArray ≤ ys.toArray ↔ xs ≤ ys := Iff.rfl
+@[simp, grind =] theorem lt_toArray [LT α] {xs ys : Vector α n} : xs.toArray < ys.toArray ↔ xs < ys := Iff.rfl
+@[simp, grind =] theorem le_toArray [LT α] {xs ys : Vector α n} : xs.toArray ≤ ys.toArray ↔ xs ≤ ys := Iff.rfl
 
 @[simp] theorem lt_toList [LT α] {xs ys : Vector α n} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
 @[simp] theorem le_toList [LT α] {xs ys : Vector α n} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
@@ -40,7 +40,7 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys
   simp [Vector.lex, Array.lex, n₁, n₂]
   rfl
 
-@[simp] theorem lex_toArray [BEq α] {lt : α → α → Bool} {xs ys : Vector α n} :
+@[simp, grind =] theorem lex_toArray [BEq α] {lt : α → α → Bool} {xs ys : Vector α n} :
     xs.toArray.lex ys.toArray lt = xs.lex ys lt := by
   cases xs
   cases ys

tests/lean/run/grind_array.lean

@@ -0,0 +1,4 @@
+set_option grind.warning false
+
+example {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray.size} :
+    l.toArray.uset i a h = (l.set i.toNat a).toArray := by grind

tests/lean/run/grind_vector.lean

@@ -0,0 +1,5 @@
+set_option grind.warning false
+
+example [BEq α] (xs ys : Vector α n) : (xs.toList == ys.toList) = (xs == ys) := by grind
+
+example [LT α] {xs ys : Vector α n} : xs.toList < ys.toList ↔ xs < ys := by grind