Ext lemma

src/Init/Control/Lawful/Basic.lean

@@ -144,6 +144,7 @@ class LawfulMonad (m : Type u → Type v) [Monad m] : Prop extends LawfulApplica
 
 export LawfulMonad (bind_pure_comp bind_map pure_bind bind_assoc)
 attribute [simp] pure_bind bind_assoc bind_pure_comp
+attribute [grind] pure_bind
 
 @[simp] theorem bind_pure [Monad m] [LawfulMonad m] (x : m α) : x >>= pure = x := by
   show x >>= (fun a => pure (id a)) = x

src/Init/Core.lean

@@ -23,6 +23,8 @@ which applies to all applications of the function).
 
 theorem id_def {α : Sort u} (a : α) : id a = a := rfl
 
+attribute [grind] id
+
 /--
 `flip f a b` is `f b a`. It is useful for "point-free" programming,
 since it can sometimes be used to avoid introducing variables.

src/Init/Data/Array/Basic.lean

@@ -40,11 +40,11 @@ namespace Array
 
 /-! ### Preliminary theorems -/
 
-@[simp] theorem size_set {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
+@[simp, grind] theorem size_set {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
     (set xs i v h).size = xs.size :=
   List.length_set ..
 
-@[simp] theorem size_push {xs : Array α} (v : α) : (push xs v).size = xs.size + 1 :=
+@[simp, grind] theorem size_push {xs : Array α} (v : α) : (push xs v).size = xs.size + 1 :=
   List.length_concat ..
 
 theorem ext {xs ys : Array α}
@@ -110,7 +110,7 @@ theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
 @[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [mem_def]
 
-@[simp] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
+@[simp, grind] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
   rw [Array.mem_def, ← getElem_toList]
   apply List.getElem_mem
 
@@ -194,7 +194,7 @@ Examples:
 def pop (xs : Array α) : Array α where
   toList := xs.toList.dropLast
 
-@[simp] theorem size_pop {xs : Array α} : xs.pop.size = xs.size - 1 := by
+@[simp, grind] theorem size_pop {xs : Array α} : xs.pop.size = xs.size - 1 := by
   match xs with
   | ⟨[]⟩ => rfl
   | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]

src/Init/Data/Array/Bootstrap.lean

@@ -112,19 +112,19 @@ abbrev pop_toList := @Array.toList_pop
 
 @[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl
 
-@[simp] 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] 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")]
 abbrev nil_append := @empty_append
 
-@[simp] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
+@[simp, grind _=_] theorem append_assoc {xs ys zs : Array α} : xs ++ ys ++ zs = xs ++ (ys ++ zs) := by
   apply ext'; simp only [toList_append, List.append_assoc]
 
 @[simp] theorem appendList_eq_append {xs : Array α} {l : List α} : xs.appendList l = xs ++ l := rfl

src/Init/Data/Array/Find.lean

@@ -23,10 +23,11 @@ open Nat
 
 /-! ### findSome? -/
 
-@[simp] theorem findSome?_empty : (#[] : Array α).findSome? f = none := rfl
-@[simp] theorem findSome?_push {xs : Array α} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
+@[simp, grind] theorem findSome?_empty : (#[] : Array α).findSome? f = none := rfl
+@[simp, grind] theorem findSome?_push {xs : Array α} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
   cases xs; simp [List.findSome?_append]
 
+@[grind]
 theorem findSome?_singleton {a : α} {f : α → Option β} : #[a].findSome? f = f a := by
   simp
 

src/Init/Data/List/Basic.lean

@@ -75,17 +75,17 @@ namespace List
 
 /-! ### length -/
 
-@[simp] theorem length_nil : length ([] : List α) = 0 :=
+@[simp, grind] theorem length_nil : length ([] : List α) = 0 :=
   rfl
 
 @[simp] theorem length_singleton {a : α} : length [a] = 1 := rfl
 
-@[simp] theorem length_cons {a : α} {as : List α} : (cons a as).length = as.length + 1 :=
+@[simp, grind] theorem length_cons {a : α} {as : List α} : (cons a as).length = as.length + 1 :=
   rfl
 
 /-! ### set -/
 
-@[simp] theorem length_set {as : List α} {i : Nat} {a : α} : (as.set i a).length = as.length := by
+@[simp, grind] theorem length_set {as : List α} {i : Nat} {a : α} : (as.set i a).length = as.length := by
   induction as generalizing i with
   | nil => rfl
   | cons x xs ih =>
@@ -96,8 +96,8 @@ namespace List
 /-! ### foldl -/
 
 -- As `List.foldl` is defined in `Init.Prelude`, we write the basic simplification lemmas here.
-@[simp] theorem foldl_nil : [].foldl f b = b := rfl
-@[simp] theorem foldl_cons {l : List α} {f : β → α → β} {b : β} : (a :: l).foldl f b = l.foldl f (f b a) := rfl
+@[simp, grind] theorem foldl_nil : [].foldl f b = b := rfl
+@[simp, grind] theorem foldl_cons {l : List α} {f : β → α → β} {b : β} : (a :: l).foldl f b = l.foldl f (f b a) := rfl
 
 /-! ### concat -/
 
@@ -328,7 +328,7 @@ def getLast? : List α → Option α
   | []    => none
   | a::as => some (getLast (a::as) (fun h => List.noConfusion h))
 
-@[simp] theorem getLast?_nil : @getLast? α [] = none := rfl
+@[simp, grind] theorem getLast?_nil : @getLast? α [] = none := rfl
 
 /-! ### getLastD -/
 
@@ -361,7 +361,7 @@ Returns the first element of a non-empty list.
 def head : (as : List α) → as ≠ [] → α
   | a::_, _ => a
 
-@[simp] theorem head_cons {a : α} {l : List α} {h} : head (a::l) h = a := rfl
+@[simp, grind] theorem head_cons {a : α} {l : List α} {h} : head (a::l) h = a := rfl
 
 /-! ### head? -/
 
@@ -379,8 +379,8 @@ def head? : List α → Option α
   | []   => none
   | a::_ => some a
 
-@[simp] theorem head?_nil : head? ([] : List α) = none := rfl
-@[simp] theorem head?_cons {a : α} {l : List α} : head? (a::l) = some a := rfl
+@[simp, grind] theorem head?_nil : head? ([] : List α) = none := rfl
+@[simp, grind] theorem head?_cons {a : α} {l : List α} : head? (a::l) = some a := rfl
 
 /-! ### headD -/
 
@@ -416,8 +416,8 @@ def tail : List α → List α
   | []    => []
   | _::as => as
 
-@[simp] theorem tail_nil : tail ([] : List α) = [] := rfl
-@[simp] theorem tail_cons {a : α} {as : List α} : tail (a::as) = as := rfl
+@[simp, grind] theorem tail_nil : tail ([] : List α) = [] := rfl
+@[simp, grind] theorem tail_cons {a : α} {as : List α} : tail (a::as) = as := rfl
 
 /-! ### tail? -/
 
@@ -437,8 +437,8 @@ def tail? : List α → Option (List α)
   | []    => none
   | _::as => some as
 
-@[simp] theorem tail?_nil : tail? ([] : List α) = none := rfl
-@[simp] theorem tail?_cons {a : α} {l : List α} : tail? (a::l) = some l := rfl
+@[simp, grind] theorem tail?_nil : tail? ([] : List α) = none := rfl
+@[simp, grind] theorem tail?_cons {a : α} {l : List α} : tail? (a::l) = some l := rfl
 
 /-! ### tailD -/
 
@@ -486,8 +486,8 @@ Examples:
   | []    => []
   | a::as => f a :: map f as
 
-@[simp] theorem map_nil {f : α → β} : map f [] = [] := rfl
-@[simp] theorem map_cons {f : α → β} {a : α} {l : List α} : map f (a :: l) = f a :: map f l := rfl
+@[simp, grind] theorem map_nil {f : α → β} : map f [] = [] := rfl
+@[simp, grind] theorem map_cons {f : α → β} {a : α} {l : List α} : map f (a :: l) = f a :: map f l := rfl
 
 /-! ### filter -/
 
@@ -507,7 +507,7 @@ def filter (p : α → Bool) : (l : List α) → List α
     | true => a :: filter p as
     | false => filter p as
 
-@[simp] theorem filter_nil {p : α → Bool} : filter p [] = [] := rfl
+@[simp, grind] theorem filter_nil {p : α → Bool} : filter p [] = [] := rfl
 
 /-! ### filterMap -/
 
@@ -533,8 +533,8 @@ Example:
     | none   => filterMap f as
     | some b => b :: filterMap f as
 
-@[simp] theorem filterMap_nil {f : α → Option β} : filterMap f [] = [] := rfl
-theorem filterMap_cons {f : α → Option β} {a : α} {l : List α} :
+@[simp, grind] theorem filterMap_nil {f : α → Option β} : filterMap f [] = [] := rfl
+@[grind] theorem filterMap_cons {f : α → Option β} {a : α} {l : List α} :
     filterMap f (a :: l) =
       match f a with
       | none => filterMap f l
@@ -557,8 +557,8 @@ Examples:
   | []     => init
   | a :: l => f a (foldr f init l)
 
-@[simp] theorem foldr_nil : [].foldr f b = b := rfl
-@[simp] theorem foldr_cons {a} {l : List α} {f : α → β → β} {b} :
+@[simp, grind] theorem foldr_nil : [].foldr f b = b := rfl
+@[simp, grind] theorem foldr_cons {a} {l : List α} {f : α → β → β} {b} :
     (a :: l).foldr f b = f a (l.foldr f b) := rfl
 
 /-! ### reverse -/
@@ -587,7 +587,7 @@ Examples:
 def reverse (as : List α) : List α :=
   reverseAux as []
 
-@[simp] theorem reverse_nil : reverse ([] : List α) = [] := rfl
+@[simp, grind] theorem reverse_nil : reverse ([] : List α) = [] := rfl
 
 theorem reverseAux_reverseAux {as bs cs : List α} :
     reverseAux (reverseAux as bs) cs = reverseAux bs (reverseAux (reverseAux as []) cs) := by
@@ -641,10 +641,10 @@ instance : Append (List α) := ⟨List.append⟩
 
 @[simp] theorem append_eq {as bs : List α} : List.append as bs = as ++ bs := rfl
 
-@[simp] theorem nil_append (as : List α) : [] ++ as = as := rfl
-@[simp] theorem cons_append {a : α} {as bs : List α} : (a::as) ++ bs = a::(as ++ bs) := rfl
+@[simp, grind] theorem nil_append (as : List α) : [] ++ as = as := rfl
+@[simp, grind _=_] theorem cons_append {a : α} {as bs : List α} : (a::as) ++ bs = a::(as ++ bs) := rfl
 
-@[simp] theorem append_nil (as : List α) : as ++ [] = as := by
+@[simp, grind] theorem append_nil (as : List α) : as ++ [] = as := by
   induction as with
   | nil => rfl
   | cons a as ih =>
@@ -654,12 +654,12 @@ instance : Std.LawfulIdentity (α := List α) (· ++ ·) [] where
   left_id := nil_append
   right_id := append_nil
 
-@[simp] theorem length_append {as bs : List α} : (as ++ bs).length = as.length + bs.length := by
+@[simp, grind] theorem length_append {as bs : List α} : (as ++ bs).length = as.length + bs.length := by
   induction as with
   | nil => simp
   | cons _ as ih => simp [ih, Nat.succ_add]
 
-@[simp] theorem append_assoc (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs) := by
+@[simp, grind _=_] theorem append_assoc (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs) := by
   induction as with
   | nil => rfl
   | cons a as ih => simp [ih]
@@ -681,7 +681,7 @@ theorem reverseAux_eq_append {as bs : List α} : reverseAux as bs = reverseAux a
     rw [ih (bs := a :: bs), ih (bs := [a]), append_assoc]
     rfl
 
-@[simp] theorem reverse_cons {a : α} {as : List α} : reverse (a :: as) = reverse as ++ [a] := by
+@[simp, grind] theorem reverse_cons {a : α} {as : List α} : reverse (a :: as) = reverse as ++ [a] := by
   simp [reverse, reverseAux]
   rw [← reverseAux_eq_append]
 
@@ -700,8 +700,8 @@ def flatten : List (List α) → List α
   | []      => []
   | l :: L => l ++ flatten L
 
-@[simp] theorem flatten_nil : List.flatten ([] : List (List α)) = [] := rfl
-@[simp] theorem flatten_cons : (l :: L).flatten = l ++ L.flatten := rfl
+@[simp, grind] theorem flatten_nil : List.flatten ([] : List (List α)) = [] := rfl
+@[simp, grind] theorem flatten_cons : (l :: L).flatten = l ++ L.flatten := rfl
 
 @[deprecated flatten (since := "2024-10-14"), inherit_doc flatten] abbrev join := @flatten
 
@@ -732,8 +732,8 @@ Examples:
 -/
 @[inline] def flatMap {α : Type u} {β : Type v} (b : α → List β) (as : List α) : List β := flatten (map b as)
 
-@[simp] theorem flatMap_nil {f : α → List β} : List.flatMap f [] = [] := by simp [flatten, List.flatMap]
-@[simp] theorem flatMap_cons {x : α} {xs : List α} {f : α → List β} :
+@[simp, grind] theorem flatMap_nil {f : α → List β} : List.flatMap f [] = [] := by simp [flatten, List.flatMap]
+@[simp, grind] theorem flatMap_cons {x : α} {xs : List α} {f : α → List β} :
   List.flatMap f (x :: xs) = f x ++ List.flatMap f xs := by simp [flatten, List.flatMap]
 
 set_option linter.missingDocs false in
@@ -756,10 +756,10 @@ def replicate : (n : Nat) → (a : α) → List α
   | 0,   _ => []
   | n+1, a => a :: replicate n a
 
-@[simp] theorem replicate_zero {a : α} : replicate 0 a = [] := rfl
-theorem replicate_succ {a : α} {n : Nat} : replicate (n+1) a = a :: replicate n a := rfl
+@[simp, grind] theorem replicate_zero {a : α} : replicate 0 a = [] := rfl
+@[grind] theorem replicate_succ {a : α} {n : Nat} : replicate (n+1) a = a :: replicate n a := rfl
 
-@[simp] theorem length_replicate {n : Nat} {a : α} : (replicate n a).length = n := by
+@[simp, grind] theorem length_replicate {n : Nat} {a : α} : (replicate n a).length = n := by
   induction n with
   | zero => simp
   | succ n ih => simp only [ih, replicate_succ, length_cons, Nat.succ_eq_add_one]
@@ -827,8 +827,8 @@ def isEmpty : List α → Bool
   | []     => true
   | _ :: _ => false
 
-@[simp] theorem isEmpty_nil : ([] : List α).isEmpty = true := rfl
-@[simp] theorem isEmpty_cons : (x :: xs : List α).isEmpty = false := rfl
+@[simp, grind] theorem isEmpty_nil : ([] : List α).isEmpty = true := rfl
+@[simp, grind] theorem isEmpty_cons : (x :: xs : List α).isEmpty = false := rfl
 
 /-! ### elem -/
 
@@ -850,7 +850,7 @@ def elem [BEq α] (a : α) : (l : List α) → Bool
     | true  => true
     | false => elem a bs
 
-@[simp] theorem elem_nil [BEq α] : ([] : List α).elem a = false := rfl
+@[simp, grind] theorem elem_nil [BEq α] : ([] : List α).elem a = false := rfl
 theorem elem_cons [BEq α] {a : α} :
     (b::bs).elem a = match a == b with | true => true | false => bs.elem a := rfl
 
@@ -912,13 +912,13 @@ theorem elem_eq_true_of_mem [BEq α] [ReflBEq α] {a : α} {as : List α} (h : a
 instance [BEq α] [LawfulBEq α] (a : α) (as : List α) : Decidable (a ∈ as) :=
   decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
 
-theorem mem_append_left {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs := by
+@[grind] theorem mem_append_left {a : α} {as : List α} (bs : List α) : a ∈ as → a ∈ as ++ bs := by
   intro h
   induction h with
   | head => apply Mem.head
   | tail => apply Mem.tail; assumption
 
-theorem mem_append_right {b : α} (as : List α) {bs : List α} : b ∈ bs → b ∈ as ++ bs := by
+@[grind] theorem mem_append_right {b : α} (as : List α) {bs : List α} : b ∈ bs → b ∈ as ++ bs := by
   intro h
   induction as with
   | nil  => simp [h]
@@ -966,9 +966,9 @@ def take : (n : Nat) → (xs : List α) → List α
   | _+1, []    => []
   | n+1, a::as => a :: take n as
 
-@[simp] theorem take_nil {i : Nat} : ([] : List α).take i = [] := by cases i <;> rfl
-@[simp] theorem take_zero {l : List α} : l.take 0 = [] := rfl
-@[simp] theorem take_succ_cons {a : α} {as : List α} {i : Nat} : (a::as).take (i+1) = a :: as.take i := rfl
+@[simp, grind] theorem take_nil {i : Nat} : ([] : List α).take i = [] := by cases i <;> rfl
+@[simp, grind] theorem take_zero {l : List α} : l.take 0 = [] := rfl
+@[simp, grind] theorem take_succ_cons {a : α} {as : List α} {i : Nat} : (a::as).take (i+1) = a :: as.take i := rfl
 
 /-! ### drop -/
 
@@ -988,10 +988,10 @@ def drop : (n : Nat) → (xs : List α) → List α
   | _+1, []    => []
   | n+1, _::as => drop n as
 
-@[simp] theorem drop_nil : ([] : List α).drop i = [] := by
+@[simp, grind] theorem drop_nil : ([] : List α).drop i = [] := by
   cases i <;> rfl
-@[simp] theorem drop_zero {l : List α} : l.drop 0 = l := rfl
-@[simp] theorem drop_succ_cons {a : α} {l : List α} {i : Nat} : (a :: l).drop (i + 1) = l.drop i := rfl
+@[simp, grind] theorem drop_zero {l : List α} : l.drop 0 = l := rfl
+@[simp, grind] theorem drop_succ_cons {a : α} {l : List α} {i : Nat} : (a :: l).drop (i + 1) = l.drop i := rfl
 
 theorem drop_eq_nil_of_le {as : List α} {i : Nat} (h : as.length ≤ i) : as.drop i = [] := by
   match as, i with
@@ -1102,9 +1102,13 @@ def dropLast {α} : List α → List α
   | [_]   => []
   | a::as => a :: dropLast as
 
-@[simp] theorem dropLast_nil : ([] : List α).dropLast = [] := rfl
-@[simp] theorem dropLast_single : [x].dropLast = [] := rfl
-@[simp] theorem dropLast_cons₂ :
+@[simp, grind] theorem dropLast_nil : ([] : List α).dropLast = [] := rfl
+@[simp, grind] theorem dropLast_singleton : [x].dropLast = [] := rfl
+
+@[deprecated dropLast_singleton (since := "2025-04-16")]
+theorem dropLast_single : [x].dropLast = [] := dropLast_singleton
+
+@[simp, grind] theorem dropLast_cons₂ :
     (x::y::zs).dropLast = x :: (y::zs).dropLast := rfl
 
 -- Later this can be proved by `simp` via `[List.length_dropLast, List.length_cons, Nat.add_sub_cancel]`,
@@ -1443,8 +1447,8 @@ def replace [BEq α] : (l : List α) → (a : α) → (b : α) → List α
     | true  => c::as
     | false => a :: replace as b c
 
-@[simp] theorem replace_nil [BEq α] : ([] : List α).replace a b = [] := rfl
-theorem replace_cons [BEq α] {a : α} :
+@[simp, grind] theorem replace_nil [BEq α] : ([] : List α).replace a b = [] := rfl
+@[grind] theorem replace_cons [BEq α] {a : α} :
     (a::as).replace b c = match b == a with | true => c::as | false => a :: replace as b c :=
   rfl
 
@@ -1652,8 +1656,8 @@ def findSome? (f : α → Option β) : List α → Option β
     | some b => some b
     | none   => findSome? f as
 
-@[simp] theorem findSome?_nil : ([] : List α).findSome? f = none := rfl
-theorem findSome?_cons {f : α → Option β} :
+@[simp, grind] theorem findSome?_nil : ([] : List α).findSome? f = none := rfl
+@[grind] theorem findSome?_cons {f : α → Option β} :
     (a::as).findSome? f = match f a with | some b => some b | none => as.findSome? f :=
   rfl
 
@@ -1884,8 +1888,8 @@ def any : (l : List α) → (p : α → Bool) → Bool
   | [], _ => false
   | h :: t, p => p h || any t p
 
-@[simp] theorem any_nil : [].any f = false := rfl
-@[simp] theorem any_cons : (a::l).any f = (f a || l.any f) := rfl
+@[simp, grind] theorem any_nil : [].any f = false := rfl
+@[simp, grind] theorem any_cons : (a::l).any f = (f a || l.any f) := rfl
 
 /-! ### all -/
 
@@ -1903,8 +1907,8 @@ def all : List α → (α → Bool) → Bool
   | [], _ => true
   | h :: t, p => p h && all t p
 
-@[simp] theorem all_nil : [].all f = true := rfl
-@[simp] theorem all_cons : (a::l).all f = (f a && l.all f) := rfl
+@[simp, grind] theorem all_nil : [].all f = true := rfl
+@[simp, grind] theorem all_cons : (a::l).all f = (f a && l.all f) := rfl
 
 /-! ### or -/
 
@@ -2044,8 +2048,8 @@ Examples:
 def sum {α} [Add α] [Zero α] : List α → α :=
   foldr (· + ·) 0
 
-@[simp] theorem sum_nil [Add α] [Zero α] : ([] : List α).sum = 0 := rfl
-@[simp] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
+@[simp, grind] theorem sum_nil [Add α] [Zero α] : ([] : List α).sum = 0 := rfl
+@[simp, grind] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
 
 /-- Sum of a list of natural numbers. -/
 @[deprecated List.sum (since := "2024-10-17")]

src/Init/Data/List/Control.lean

@@ -238,8 +238,8 @@ def foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (f : s
     let s' ← f s a
     List.foldlM f s' as
 
-@[simp] theorem foldlM_nil [Monad m] {f : β → α → m β} {b : β} : [].foldlM f b = pure b := rfl
-@[simp] theorem foldlM_cons [Monad m] {f : β → α → m β} {b : β} {a : α} {l : List α} :
+@[simp, grind] theorem foldlM_nil [Monad m] {f : β → α → m β} {b : β} : [].foldlM f b = pure b := rfl
+@[simp, grind] theorem foldlM_cons [Monad m] {f : β → α → m β} {b : β} {a : α} {l : List α} :
     (a :: l).foldlM f b = f b a >>= l.foldlM f := by
   simp [List.foldlM]
 
@@ -262,7 +262,7 @@ example [Monad m] (f : α → β → m β) :
 def foldrM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : α → s → m s) (init : s) (l : List α) : m s :=
   l.reverse.foldlM (fun s a => f a s) init
 
-@[simp] theorem foldrM_nil [Monad m] {f : α → β → m β} {b : β} : [].foldrM f b = pure b := rfl
+@[simp, grind] theorem foldrM_nil [Monad m] {f : α → β → m β} {b : β} : [].foldrM f b = pure b := rfl
 
 /--
 Maps `f` over the list and collects the results with `<|>`. The result for the end of the list is

src/Init/Data/List/Lemmas.lean

@@ -92,7 +92,7 @@ open Nat
 
 /-! ### length -/
 
-theorem eq_nil_of_length_eq_zero (_ : length l = 0) : l = [] := match l with | [] => rfl
+@[grind →] theorem eq_nil_of_length_eq_zero (_ : length l = 0) : l = [] := match l with | [] => rfl
 
 theorem ne_nil_of_length_eq_add_one (_ : length l = n + 1) : l ≠ [] := fun _ => nomatch l
 
@@ -261,6 +261,7 @@ theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.le
     · match i, h with
       | i + 1, h => simp [getElem?_eq_some_iff, Nat.succ_lt_succ_iff]
 
+@[grind →]
 theorem getElem_of_getElem? {l : List α} : l[i]? = some a → ∃ h : i < l.length, l[i] = a :=
   getElem?_eq_some_iff.mp
 
@@ -295,6 +296,7 @@ theorem getD_getElem? {l : List α} {i : Nat} {d : α} :
   match i, h with
   | 0, _ => rfl
 
+@[grind]
 theorem getElem?_singleton {a : α} {i : Nat} : [a][i]? = if i = 0 then some a else none := by
   simp [getElem?_cons]
 
@@ -311,7 +313,7 @@ theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_po
   match l, h with
   | _ :: _, _ => rfl
 
-@[ext] theorem ext_getElem? {l₁ l₂ : List α} (h : ∀ i : Nat, l₁[i]? = l₂[i]?) : l₁ = l₂ :=
+@[ext, grind ext] theorem ext_getElem? {l₁ l₂ : List α} (h : ∀ i : Nat, l₁[i]? = l₂[i]?) : l₁ = l₂ :=
   match l₁, l₂, h with
   | [], [], _ => rfl
   | _ :: _, [], h => by simpa using h 0
@@ -374,7 +376,10 @@ theorem get!_eq_getElem! [Inhabited α] (l : List α) (i) : l.get! i = l[i]! :=
   ⟨fun h => by cases h <;> simp [Membership.mem, *],
    fun | Or.inl rfl => by constructor | Or.inr h => by constructor; assumption⟩
 
-theorem mem_cons_self {a : α} {l : List α} : a ∈ a :: l := .head ..
+@[grind] theorem eq_or_mem_of_mem_cons {a b : α} {l : List α} :
+    a ∈ b :: l → a = b ∨ a ∈ l := List.mem_cons.mp
+
+@[grind] theorem mem_cons_self {a : α} {l : List α} : a ∈ a :: l := .head ..
 
 theorem mem_concat_self {xs : List α} {a : α} : a ∈ xs ++ [a] :=
   mem_append_right xs mem_cons_self
@@ -396,7 +401,7 @@ theorem eq_append_cons_of_mem {a : α} {xs : List α} (h : a ∈ xs) :
       · obtain ⟨as, bs, rfl, h⟩ := ih h
         exact ⟨x :: as, bs, rfl, by simp_all⟩
 
-theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l := .tail _
+@[grind] theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l := .tail _
 
 -- The argument `l : List α` is intentionally explicit,
 -- as a tactic may generate `h` without determining `l`.
@@ -532,10 +537,10 @@ theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
 theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
     elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
 
-@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
+@[simp, grind] theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
     as.contains a = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
 
-@[simp] theorem contains_cons [BEq α] {a : α} {b : α} {l : List α} :
+@[simp, grind] theorem contains_cons [BEq α] {a : α} {b : α} {l : List α} :
     (a :: l).contains b = (b == a || l.contains b) := by
   simp only [contains, elem_cons]
   split <;> simp_all
@@ -545,6 +550,9 @@ theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
 @[simp] theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by
   cases l <;> simp
 
+@[grind →]
+theorem nil_of_isEmpty {l : List α} (h : l.isEmpty) : l = [] := List.isEmpty_iff.mp h
+
 @[deprecated isEmpty_iff (since := "2025-02-17")]
 abbrev isEmpty_eq_true := @isEmpty_iff
 
@@ -606,10 +614,10 @@ theorem all_bne' [BEq α] [PartialEquivBEq α] {l : List α} :
 /-! ### set -/
 
 -- As `List.set` is defined in `Init.Prelude`, we write the basic simplification lemmas here.
-@[simp] theorem set_nil {i : Nat} {a : α} : [].set i a = [] := rfl
-@[simp] theorem set_cons_zero {x : α} {xs : List α} {a : α} :
+@[simp, grind] theorem set_nil {i : Nat} {a : α} : [].set i a = [] := rfl
+@[simp, grind] theorem set_cons_zero {x : α} {xs : List α} {a : α} :
   (x :: xs).set 0 a = a :: xs := rfl
-@[simp] theorem set_cons_succ {x : α} {xs : List α} {i : Nat} {a : α} :
+@[simp, grind] theorem set_cons_succ {x : α} {xs : List α} {i : Nat} {a : α} :
   (x :: xs).set (i + 1) a = x :: xs.set i a := rfl
 
 @[simp] theorem getElem_set_self {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
@@ -652,14 +660,14 @@ theorem getElem?_set_self' {l : List α} {i : Nat} {a : α} :
     simp_all
   · rw [getElem?_eq_none (by simp_all), getElem?_eq_none (by simp_all)]
 
-theorem getElem_set {l : List α} {i j} {a} (h) :
+@[grind] theorem getElem_set {l : List α} {i j} {a} (h) :
     (set l i a)[j]'h = if i = j then a else l[j]'(length_set .. ▸ h) := by
   if h : i = j then
     subst h; simp only [getElem_set_self, ↓reduceIte]
   else
     simp [h]
 
-theorem getElem?_set {l : List α} {i j : Nat} {a : α} :
+@[grind] theorem getElem?_set {l : List α} {i j : Nat} {a : α} :
     (l.set i a)[j]? = if i = j then if i < l.length then some a else none else l[j]? := by
   if h : i = j then
     subst h
@@ -719,6 +727,7 @@ theorem mem_set {l : List α} {i : Nat} (h : i < l.length) (a : α) :
   simp only [mem_iff_getElem]
   exact ⟨i, by simpa using h, by simp⟩
 
+@[grind →]
 theorem mem_or_eq_of_mem_set : ∀ {l : List α} {i : Nat} {a b : α}, a ∈ l.set i b → a ∈ l ∨ a = b
   | _ :: _, 0, _, _, h => ((mem_cons ..).1 h).symm.imp_left (.tail _)
   | _ :: _, _+1, _, _, .head .. => .inl (.head ..)
@@ -728,10 +737,10 @@ theorem mem_or_eq_of_mem_set : ∀ {l : List α} {i : Nat} {a b : α}, a ∈ l.s
 
 /-! ### BEq -/
 
-@[simp] theorem beq_nil_eq [BEq α] {l : List α} : (l == []) = l.isEmpty := by
+@[simp, grind] theorem beq_nil_eq [BEq α] {l : List α} : (l == []) = l.isEmpty := by
   cases l <;> rfl
 
-@[simp] theorem nil_beq_eq [BEq α] {l : List α} : ([] == l) = l.isEmpty := by
+@[simp, grind] theorem nil_beq_eq [BEq α] {l : List α} : ([] == l) = l.isEmpty := by
   cases l <;> rfl
 
 @[deprecated beq_nil_eq (since := "2025-04-04")]
@@ -740,7 +749,7 @@ abbrev beq_nil_iff := @beq_nil_eq
 @[deprecated nil_beq_eq (since := "2025-04-04")]
 abbrev nil_beq_iff := @nil_beq_eq
 
-@[simp] theorem cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
+@[simp, grind] theorem cons_beq_cons [BEq α] {a b : α} {l₁ l₂ : List α} :
     (a :: l₁ == b :: l₂) = (a == b && l₁ == l₂) := rfl
 
 @[simp] theorem concat_beq_concat [BEq α] {a b : α} {l₁ l₂ : List α} :
@@ -806,6 +815,7 @@ theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l
 
 /-! ### getLast -/
 
+@[grind]
 theorem getLast_eq_getElem : ∀ {l : List α} (h : l ≠ []),
     getLast l h = l[l.length - 1]'(by
       match l with
@@ -819,7 +829,7 @@ theorem getElem_length_sub_one_eq_getLast {l : List α} (h : l.length - 1 < l.le
     l[l.length - 1] = getLast l (by cases l; simp at h; simp) := by
   rw [← getLast_eq_getElem]
 
-@[simp] theorem getLast_cons_cons {a : α} {l : List α} :
+@[simp, grind] theorem getLast_cons_cons {a : α} {l : List α} :
     getLast (a :: b :: l) (by simp) = getLast (b :: l) (by simp) := by
   rfl
 
@@ -832,10 +842,10 @@ theorem getLast_cons {a : α} {l : List α} : ∀ (h : l ≠ nil),
 theorem getLast_eq_getLastD {a l} (h) : @getLast α (a::l) h = getLastD l a := by
   cases l <;> rfl
 
-@[simp] theorem getLastD_eq_getLast? {a l} : @getLastD α l a = (getLast? l).getD a := by
+@[simp, grind] theorem getLastD_eq_getLast? {a l} : @getLastD α l a = (getLast? l).getD a := by
   cases l <;> rfl
 
-@[simp] theorem getLast_singleton {a} (h) : @getLast α [a] h = a := rfl
+@[simp, grind] theorem getLast_singleton {a} (h) : @getLast α [a] h = a := rfl
 
 theorem getLast!_cons_eq_getLastD [Inhabited α] : @getLast! α _ (a::l) = getLastD l a := by
   simp [getLast!, getLast_eq_getLastD]
@@ -868,7 +878,7 @@ theorem getLast?_eq_getLast : ∀ {l : List α} h, l.getLast? = some (l.getLast
   | [], h => nomatch h rfl
   | _ :: _, _ => rfl
 
-theorem getLast?_eq_getElem? : ∀ {l : List α}, l.getLast? = l[l.length - 1]?
+@[grind] theorem getLast?_eq_getElem? : ∀ {l : List α}, l.getLast? = l[l.length - 1]?
   | [] => rfl
   | a::l => by
     rw [getLast?_eq_getLast (l := a :: l) nofun, getLast_eq_getElem, getElem?_eq_getElem]
@@ -881,12 +891,14 @@ theorem getLast_eq_iff_getLast?_eq_some {xs : List α} (h) :
 -- `getLast?_eq_none_iff`, `getLast?_eq_some_iff`, `getLast?_isSome`, and `getLast_mem`
 -- are proved later once more `reverse` theorems are available.
 
+@[grind]
 theorem getLast?_cons {a : α} : (a::l).getLast? = some (l.getLast?.getD a) := by
   cases l <;> simp [getLast?, getLast]
 
 @[simp] theorem getLast?_cons_cons : (a :: b :: l).getLast? = (b :: l).getLast? := by
   simp [getLast?_cons]
 
+@[grind]
 theorem getLast?_concat {l : List α} {a : α} : (l ++ [a]).getLast? = some a := by
   simp [getLast?_eq_getElem?, Nat.succ_sub_succ]
 
@@ -905,6 +917,7 @@ theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := rfl
 theorem getLast!_of_getLast? [Inhabited α] : ∀ {l : List α}, getLast? l = some a → getLast! l = a
   | _ :: _, rfl => rfl
 
+@[grind]
 theorem getLast!_eq_getElem! [Inhabited α] {l : List α} : l.getLast! = l[l.length - 1]! := by
   cases l with
   | nil => simp
@@ -932,6 +945,7 @@ theorem head?_eq_getElem? : ∀ {l : List α}, l.head? = l[0]?
 
 theorem head_singleton {a : α} : head [a] (by simp) = a := by simp
 
+@[grind]
 theorem head_eq_getElem {l : List α} (h : l ≠ []) : head l h = l[0]'(length_pos_iff.mpr h) := by
   cases l with
   | nil => simp at h
@@ -967,7 +981,7 @@ abbrev head?_isSome := @isSome_head?
 theorem mem_of_head? : {l : List α} → {a : α} → l.head? = some a → a ∈ l
   | _::_, _, h => Option.some.inj h ▸ mem_cons_self
 
-theorem mem_of_mem_head? : ∀ {l : List α} {a : α}, a ∈ l.head? → a ∈ l :=
+@[grind →] theorem mem_of_mem_head? : ∀ {l : List α} {a : α}, a ∈ l.head? → a ∈ l :=
   mem_of_head?
 
 theorem head_mem_head? : ∀ {l : List α} (h : l ≠ []), head l h ∈ head? l
@@ -993,18 +1007,18 @@ theorem head_of_mem_head? {l : List α} {x} (hx : x ∈ l.head?) :
 /-! ### headD -/
 
 /-- `simp` unfolds `headD` in terms of `head?` and `Option.getD`. -/
-@[simp] theorem headD_eq_head?_getD {l : List α} : headD l a = (head? l).getD a := by
+@[simp, grind] theorem headD_eq_head?_getD {l : List α} : headD l a = (head? l).getD a := by
   cases l <;> simp [headD]
 
 /-! ### tailD -/
 
 /-- `simp` unfolds `tailD` in terms of `tail?` and `Option.getD`. -/
-@[simp] theorem tailD_eq_tail? {l l' : List α} : tailD l l' = (tail? l).getD l' := by
+@[simp, grind] theorem tailD_eq_tail? {l l' : List α} : tailD l l' = (tail? l).getD l' := by
   cases l <;> rfl
 
 /-! ### tail -/
 
-@[simp] theorem length_tail {l : List α} : l.tail.length = l.length - 1 := by cases l <;> rfl
+@[simp, grind] theorem length_tail {l : List α} : l.tail.length = l.length - 1 := by cases l <;> rfl
 
 theorem tail_eq_tailD {l : List α} : l.tail = tailD l [] := by cases l <;> rfl
 
@@ -1016,13 +1030,13 @@ theorem mem_of_mem_tail {a : α} {l : List α} (h : a ∈ tail l) : a ∈ l := b
 theorem ne_nil_of_tail_ne_nil {l : List α} : l.tail ≠ [] → l ≠ [] := by
   cases l <;> simp
 
-@[simp] theorem getElem_tail {l : List α} {i : Nat} (h : i < l.tail.length) :
+@[simp, grind] theorem getElem_tail {l : List α} {i : Nat} (h : i < l.tail.length) :
     (tail l)[i] = l[i + 1]'(add_lt_of_lt_sub (by simpa using h)) := by
   cases l with
   | nil => simp at h
   | cons _ l => simp
 
-@[simp] theorem getElem?_tail {l : List α} {i : Nat} :
+@[simp, grind] theorem getElem?_tail {l : List α} {i : Nat} :
     (tail l)[i]? = l[i + 1]? := by
   cases l <;> simp
 
@@ -1046,7 +1060,7 @@ theorem one_lt_length_of_tail_ne_nil {l : List α} (h : l.tail ≠ []) : 1 < l.l
 @[simp] theorem head?_tail {l : List α} : (tail l).head? = l[1]? := by
   simp [head?_eq_getElem?]
 
-@[simp] theorem getLast_tail {l : List α} (h : l.tail ≠ []) :
+@[simp, grind] theorem getLast_tail {l : List α} (h : l.tail ≠ []) :
     (tail l).getLast h = l.getLast (ne_nil_of_tail_ne_nil h) := by
   simp only [getLast_eq_getElem, length_tail, getElem_tail]
   congr
@@ -1066,7 +1080,7 @@ theorem getLast?_tail {l : List α} : (tail l).getLast? = if l.length = 1 then n
 
 /-! ### map -/
 
-@[simp] theorem length_map {as : List α} (f : α → β) : (as.map f).length = as.length := by
+@[simp, grind] theorem length_map {as : List α} (f : α → β) : (as.map f).length = as.length := by
   induction as with
   | nil => simp [List.map]
   | cons _ as ih => simp [List.map, ih]
@@ -1074,13 +1088,13 @@ theorem getLast?_tail {l : List α} : (tail l).getLast? = if l.length = 1 then n
 @[simp] theorem isEmpty_map {l : List α} {f : α → β} : (l.map f).isEmpty = l.isEmpty := by
   cases l <;> simp
 
-@[simp] theorem getElem?_map {f : α → β} : ∀ {l : List α} {i : Nat}, (map f l)[i]? = Option.map f l[i]?
+@[simp, grind] theorem getElem?_map {f : α → β} : ∀ {l : List α} {i : Nat}, (map f l)[i]? = Option.map f l[i]?
   | [], _ => rfl
   | _ :: _, 0 => by simp
   | _ :: l, i+1 => by simp [getElem?_map]
 
 -- The argument `f : α → β` is explicit, to facilitate rewriting from right to left.
-@[simp] theorem getElem_map (f : α → β) {l} {i : Nat} {h : i < (map f l).length} :
+@[simp, grind] theorem getElem_map (f : α → β) {l} {i : Nat} {h : i < (map f l).length} :
     (map f l)[i] = f (l[i]'(length_map f ▸ h)) :=
   Option.some.inj <| by rw [← getElem?_eq_getElem, getElem?_map, getElem?_eq_getElem]; rfl
 
@@ -1127,6 +1141,7 @@ theorem forall_mem_map {f : α → β} {l : List α} {P : β → Prop} :
 
 @[deprecated map_eq_nil_iff (since := "2024-09-05")] abbrev map_eq_nil := @map_eq_nil_iff
 
+@[grind →]
 theorem eq_nil_of_map_eq_nil {f : α → β} {l : List α} (h : map f l = []) : l = [] :=
   map_eq_nil_iff.mp h
 
@@ -1236,7 +1251,7 @@ theorem tailD_map {f : α → β} {l l' : List α} :
     simp only [← map_cons, getElem_map]
     simp
 
-@[simp] theorem getLast?_map {f : α → β} {l : List α} : (map f l).getLast? = l.getLast?.map f := by
+@[simp, grind _=_] theorem getLast?_map {f : α → β} {l : List α} : (map f l).getLast? = l.getLast?.map f := by
   cases l
   · simp
   · rw [getLast?_eq_getLast, getLast?_eq_getLast, getLast_map] <;> simp
@@ -1255,7 +1270,7 @@ theorem getLastD_map {f : α → β} {l : List α} {a : α} : (map f l).getLastD
 @[simp] theorem filter_cons_of_neg {p : α → Bool} {a : α} {l} (pa : ¬ p a) :
     filter p (a :: l) = filter p l := by rw [filter, eq_false_of_ne_true pa]
 
-theorem filter_cons :
+@[grind] theorem filter_cons :
     (x :: xs : List α).filter p = if p x then x :: (xs.filter p) else xs.filter p := by
   split <;> simp [*]
 
@@ -1271,6 +1286,8 @@ theorem length_filter_le (p : α → Bool) (l : List α) :
       exact Nat.succ_le_succ ih
     · exact Nat.le_trans ih (Nat.le_add_right _ _)
 
+grind_pattern List.length_filter_le => (l.filter p).length
+
 @[simp]
 theorem filter_eq_self {l} : filter p l = l ↔ ∀ a ∈ l, p a := by
   induction l with simp
@@ -1292,7 +1309,7 @@ theorem length_filter_eq_length_iff {l} : (filter p l).length = l.length ↔ ∀
 @[deprecated length_filter_eq_length_iff (since := "2025-04-04")]
 abbrev filter_length_eq_length := @length_filter_eq_length_iff
 
-@[simp] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
+@[simp, grind] theorem mem_filter : x ∈ filter p as ↔ x ∈ as ∧ p x := by
   induction as with
   | nil => simp
   | cons a as ih =>
@@ -1343,7 +1360,7 @@ theorem map_filter_eq_foldr {f : α → β} {p : α → Bool} {as : List α} :
     simp only [foldr]
     cases hp : p head <;> simp [filter, *]
 
-@[simp] theorem filter_append {p : α → Bool} :
+@[simp, grind] theorem filter_append {p : α → Bool} :
     ∀ (l₁ l₂ : List α), filter p (l₁ ++ l₂) = filter p l₁ ++ filter p l₂
   | [], _ => rfl
   | a :: l₁, l₂ => by simp only [cons_append, filter]; split <;> simp [filter_append l₁]
@@ -1410,7 +1427,7 @@ theorem filterMap_eq_map' {f : α → β} : filterMap (fun x => some (f x)) = ma
   erw [filterMap_eq_map]
   simp
 
-theorem filterMap_some {l : List α} : filterMap some l = l := by
+@[grind] theorem filterMap_some {l : List α} : filterMap some l = l := by
   rw [filterMap_some_fun, id]
 
 theorem map_filterMap_some_eq_filter_map_isSome {f : α → Option β} {l : List α} :
@@ -1423,6 +1440,8 @@ theorem length_filterMap_le (f : α → Option β) (l : List α) :
   rw [← length_map some, map_filterMap_some_eq_filter_map_isSome, ← length_map f]
   apply length_filter_le
 
+grind_pattern List.length_filterMap_le => (List.filterMap f l).length
+
 @[simp]
 theorem filterMap_length_eq_length {l} :
     (filterMap f l).length = l.length ↔ ∀ a ∈ l, (f a).isSome := by
@@ -1443,17 +1462,19 @@ theorem filterMap_eq_filter {p : α → Bool} :
   | nil => rfl
   | cons a l IH => by_cases pa : p a <;> simp [filterMap_cons, Option.guard, pa, ← IH]
 
+@[grind]
 theorem filterMap_filterMap {f : α → Option β} {g : β → Option γ} {l : List α} :
     filterMap g (filterMap f l) = filterMap (fun x => (f x).bind g) l := by
   induction l with
   | nil => rfl
   | cons a l IH => cases h : f a <;> simp [filterMap_cons, *]
 
+@[grind]
 theorem map_filterMap {f : α → Option β} {g : β → γ} {l : List α} :
     map g (filterMap f l) = filterMap (fun x => (f x).map g) l := by
   simp only [← filterMap_eq_map, filterMap_filterMap, Option.map_eq_bind]
 
-@[simp]
+@[simp, grind]
 theorem filterMap_map {f : α → β} {g : β → Option γ} {l : List α} :
     filterMap g (map f l) = filterMap (g ∘ f) l := by
   rw [← filterMap_eq_map, filterMap_filterMap]; rfl
@@ -1468,7 +1489,7 @@ theorem filterMap_filter {p : α → Bool} {f : α → Option β} {l : List α}
   rw [← filterMap_eq_filter, filterMap_filterMap]
   congr; funext x; by_cases h : p x <;> simp [Option.guard, h]
 
-@[simp] theorem mem_filterMap {f : α → Option β} {l : List α} {b : β} :
+@[simp, grind] theorem mem_filterMap {f : α → Option β} {l : List α} {b : β} :
     b ∈ filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b := by
   induction l <;> simp [filterMap_cons]; split <;> simp [*, eq_comm]
 
@@ -1480,7 +1501,7 @@ theorem forall_mem_filterMap {f : α → Option β} {l : List α} {P : β → Pr
   intro a
   rw [forall_comm]
 
-@[simp] theorem filterMap_append {l l' : List α} {f : α → Option β} :
+@[simp, grind] theorem filterMap_append {l l' : List α} {f : α → Option β} :
     filterMap f (l ++ l') = filterMap f l ++ filterMap f l' := by
   induction l <;> simp [filterMap_cons]; split <;> simp [*]
 
@@ -1497,6 +1518,7 @@ theorem head_filterMap_of_eq_some {f : α → Option β} {l : List α} (w : l
     simp only [head_cons] at h
     simp [filterMap_cons, h]
 
+@[grind →]
 theorem forall_none_of_filterMap_eq_nil (h : filterMap f xs = []) : ∀ x ∈ xs, f x = none := by
   intro x hx
   induction xs with
@@ -1555,7 +1577,7 @@ theorem filterMap_eq_cons_iff {l} {b} {bs} :
 @[simp] theorem cons_append_fun {a : α} {as : List α} :
     (fun bs => ((a :: as) ++ bs)) = fun bs => a :: (as ++ bs) := rfl
 
-@[simp] theorem mem_append {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
+@[simp, grind] theorem mem_append {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t := by
   induction s <;> simp_all [or_assoc]
 
 theorem not_mem_append {a : α} {s t : List α} (h₁ : a ∉ s) (h₂ : a ∉ t) : a ∉ s ++ t :=
@@ -1583,7 +1605,7 @@ theorem forall_mem_append {p : α → Prop} {l₁ l₂ : List α} :
     (∀ (x) (_ : x ∈ l₁ ++ l₂), p x) ↔ (∀ (x) (_ : x ∈ l₁), p x) ∧ (∀ (x) (_ : x ∈ l₂), p x) := by
   simp only [mem_append, or_imp, forall_and]
 
-theorem getElem_append {l₁ l₂ : List α} {i : Nat} (h : i < (l₁ ++ l₂).length) :
+@[grind] theorem getElem_append {l₁ l₂ : List α} {i : Nat} (h : i < (l₁ ++ l₂).length) :
     (l₁ ++ l₂)[i] = if h' : i < l₁.length then l₁[i] else l₂[i - l₁.length]'(by simp at h h'; exact Nat.sub_lt_left_of_lt_add h' h) := by
   split <;> rename_i h'
   · rw [getElem_append_left h']
@@ -1602,7 +1624,7 @@ theorem getElem?_append_right : ∀ {l₁ l₂ : List α} {i : Nat}, l₁.length
   rw [cons_append]
   simp [Nat.succ_sub_succ_eq_sub, getElem?_append_right (Nat.lt_succ.1 h₁)]
 
-theorem getElem?_append {l₁ l₂ : List α} {i : Nat} :
+@[grind] theorem getElem?_append {l₁ l₂ : List α} {i : Nat} :
     (l₁ ++ l₂)[i]? = if i < l₁.length then l₁[i]? else l₂[i - l₁.length]? := by
   split <;> rename_i h
   · exact getElem?_append_left h
@@ -1681,6 +1703,10 @@ theorem getLast_concat {a : α} : ∀ {l : List α}, getLast (l ++ [a]) (by simp
 @[simp] theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = [] := by
   rw [eq_comm, append_eq_nil_iff]
 
+@[grind →]
+theorem eq_nil_of_append_eq_nil {l₁ l₂ : List α} (h : l₁ ++ l₂ = []) : l₁ = [] ∧ l₂ = [] :=
+  append_eq_nil_iff.mp h
+
 theorem append_ne_nil_of_left_ne_nil {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ [] := by simp_all
 theorem append_ne_nil_of_right_ne_nil (s : List α) : t ≠ [] → s ++ t ≠ [] := by simp_all
 
@@ -1707,12 +1733,12 @@ theorem append_eq_append_iff {ws xs ys zs : List α} :
   | nil => simp_all
   | cons a as ih => cases ys <;> simp [eq_comm, and_assoc, ih, and_or_left]
 
-@[simp] theorem head_append_of_ne_nil {l : List α} {w₁} (w₂) :
+@[simp, grind] theorem head_append_of_ne_nil {l : List α} {w₁} (w₂) :
     head (l ++ l') w₁ = head l w₂ := by
   match l, w₂ with
   | a :: l, _ => rfl
 
-theorem head_append {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) :
+@[grind] theorem head_append {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) :
     head (l₁ ++ l₂) w =
       if h : l₁.isEmpty then
         head l₂ (by simp_all [isEmpty_iff])
@@ -1733,28 +1759,28 @@ theorem head_append_right {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) (h : l
     head (l₁ ++ l₂) w = head l₂ (by simp_all) := by
   rw [head_append, dif_pos (by simp_all)]
 
-@[simp] theorem head?_append {l : List α} : (l ++ l').head? = l.head?.or l'.head? := by
+@[simp, grind] theorem head?_append {l : List α} : (l ++ l').head? = l.head?.or l'.head? := by
   cases l <;> rfl
 
 -- Note:
 -- `getLast_append_of_ne_nil`, `getLast_append` and `getLast?_append`
 -- are stated and proved later in the `reverse` section.
 
-theorem tail?_append {l l' : List α} : (l ++ l').tail? = (l.tail?.map (· ++ l')).or l'.tail? := by
+@[grind] theorem tail?_append {l l' : List α} : (l ++ l').tail? = (l.tail?.map (· ++ l')).or l'.tail? := by
   cases l <;> simp
 
 theorem tail?_append_of_ne_nil {l l' : List α} (_ : l ≠ []) : (l ++ l').tail? = some (l.tail ++ l') :=
   match l with
   | _ :: _ => by simp
 
-theorem tail_append {l l' : List α} : (l ++ l').tail = if l.isEmpty then l'.tail else l.tail ++ l' := by
+@[grind] theorem tail_append {l l' : List α} : (l ++ l').tail = if l.isEmpty then l'.tail else l.tail ++ l' := by
   cases l <;> simp
 
 @[simp] theorem tail_append_of_ne_nil {xs ys : List α} (h : xs ≠ []) :
     (xs ++ ys).tail = xs.tail ++ ys := by
   simp_all [tail_append]
 
-theorem set_append {s t : List α} :
+@[grind] theorem set_append {s t : List α} :
     (s ++ t).set i x = if i < s.length then s.set i x ++ t else s ++ t.set (i - s.length) x := by
   induction s generalizing i with
   | nil => simp
@@ -1818,7 +1844,7 @@ theorem append_eq_filter_iff {p : α → Bool} :
 
 @[deprecated append_eq_filter_iff (since := "2024-09-05")] abbrev append_eq_filter := @append_eq_filter_iff
 
-@[simp] theorem map_append {f : α → β} : ∀ {l₁ l₂}, map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by
+@[simp, grind] theorem map_append {f : α → β} : ∀ {l₁ l₂}, map f (l₁ ++ l₂) = map f l₁ ++ map f l₂ := by
   intro l₁; induction l₁ <;> intros <;> simp_all
 
 theorem map_eq_append_iff {f : α → β} :
@@ -1888,7 +1914,7 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ l' b, l = concat l' b
   | cons =>
     simp [flatten, length_append, *]
 
-theorem flatten_singleton {l : List α} : [l].flatten = l := by simp
+@[grind] theorem flatten_singleton {l : List α} : [l].flatten = l := by simp
 
 @[simp] theorem mem_flatten : ∀ {L : List (List α)}, a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l
   | [] => by simp
@@ -1925,15 +1951,15 @@ theorem head?_flatten {L : List (List α)} : (flatten L).head? = L.findSome? fun
 -- `getLast?_flatten` is proved later, after the `reverse` section.
 -- `head_flatten` and `getLast_flatten` are proved in `Init.Data.List.Find`.
 
-@[simp] theorem map_flatten {f : α → β} {L : List (List α)} :
+@[simp, grind _=_] theorem map_flatten {f : α → β} {L : List (List α)} :
     (flatten L).map f = (map (map f) L).flatten := by
   induction L <;> simp_all
 
-@[simp] theorem filterMap_flatten {f : α → Option β} {L : List (List α)} :
+@[simp, grind _=_] theorem filterMap_flatten {f : α → Option β} {L : List (List α)} :
     filterMap f (flatten L) = flatten (map (filterMap f) L) := by
   induction L <;> simp [*, filterMap_append]
 
-@[simp] theorem filter_flatten {p : α → Bool} {L : List (List α)} :
+@[simp, grind _=_] theorem filter_flatten {p : α → Bool} {L : List (List α)} :
     filter p (flatten L) = flatten (map (filter p) L) := by
   induction L <;> simp [*, filter_append]
 
@@ -1949,7 +1975,7 @@ theorem flatten_filter_ne_nil [DecidablePred fun l : List α => l ≠ []] {L : L
   simp only [ne_eq, ← isEmpty_iff, Bool.not_eq_true, Bool.decide_eq_false,
     flatten_filter_not_isEmpty]
 
-@[simp] theorem flatten_append {L₁ L₂ : List (List α)} : flatten (L₁ ++ L₂) = flatten L₁ ++ flatten L₂ := by
+@[simp, grind _=_] theorem flatten_append {L₁ L₂ : List (List α)} : flatten (L₁ ++ L₂) = flatten L₁ ++ flatten L₂ := by
   induction L₁ <;> simp_all
 
 theorem flatten_concat {L : List (List α)} {l : List α} : flatten (L ++ [l]) = flatten L ++ l := by
@@ -2063,7 +2089,7 @@ theorem length_flatMap {l : List α} {f : α → List β} :
     length (l.flatMap f) = sum (map (fun a => (f a).length) l) := by
   rw [List.flatMap, length_flatten, map_map, Function.comp_def]
 
-@[simp] theorem mem_flatMap {f : α → List β} {b} {l : List α} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
+@[simp, grind] theorem mem_flatMap {f : α → List β} {b} {l : List α} : b ∈ l.flatMap f ↔ ∃ a, a ∈ l ∧ b ∈ f a := by
   simp [flatMap_def, mem_flatten]
   exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩
 
@@ -2092,7 +2118,7 @@ theorem flatMap_singleton (f : α → List β) (x : α) : [x].flatMap f = f x :=
 @[simp] theorem flatMap_singleton' (l : List α) : (l.flatMap fun x => [x]) = l := by
   induction l <;> simp [*]
 
-theorem head?_flatMap {l : List α} {f : α → List β} :
+@[grind] theorem head?_flatMap {l : List α} {f : α → List β} :
     (l.flatMap f).head? = l.findSome? fun a => (f a).head? := by
   induction l with
   | nil => rfl
@@ -2100,7 +2126,7 @@ theorem head?_flatMap {l : List α} {f : α → List β} :
     simp only [findSome?_cons]
     split <;> simp_all
 
-@[simp] theorem flatMap_append {xs ys : List α} {f : α → List β} :
+@[simp, grind _=_] theorem flatMap_append {xs ys : List α} {f : α → List β} :
     (xs ++ ys).flatMap f = xs.flatMap f ++ ys.flatMap f := by
   induction xs; {rfl}; simp_all [flatMap_cons, append_assoc]
 
@@ -2145,7 +2171,7 @@ theorem flatMap_eq_foldl {f : α → List β} {l : List α} :
 theorem replicate_succ' : replicate (n + 1) a = replicate n a ++ [a] := by
   induction n <;> simp_all [replicate_succ, ← cons_append]
 
-@[simp] theorem mem_replicate {a b : α} : ∀ {n}, b ∈ replicate n a ↔ n ≠ 0 ∧ b = a
+@[simp, grind] theorem mem_replicate {a b : α} : ∀ {n}, b ∈ replicate n a ↔ n ≠ 0 ∧ b = a
   | 0 => by simp
   | n+1 => by simp [replicate_succ, mem_replicate, Nat.succ_ne_zero]
 
@@ -2164,7 +2190,7 @@ theorem decide_mem_replicate [BEq α] [LawfulBEq α] {a b : α} :
   have : DecidableEq α := instDecidableEqOfLawfulBEq
   simp [Bool.beq_eq_decide_eq]
 
-theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
+@[grind →] theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
 
 theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
     (∀ b, b ∈ replicate n a → p b) ↔ n = 0 ∨ p a := by
@@ -2178,11 +2204,11 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
 
 @[deprecated replicate_eq_nil_iff (since := "2024-09-05")] abbrev replicate_eq_nil := @replicate_eq_nil_iff
 
-@[simp] theorem getElem_replicate {a : α} {n : Nat} {i : Nat} (h : i < (replicate n a).length) :
+@[simp, grind] theorem getElem_replicate {a : α} {n : Nat} {i : Nat} (h : i < (replicate n a).length) :
     (replicate n a)[i] = a :=
   eq_of_mem_replicate (getElem_mem _)
 
-theorem getElem?_replicate : (replicate n a)[i]? = if i < n then some a else none := by
+@[grind] theorem getElem?_replicate : (replicate n a)[i]? = if i < n then some a else none := by
   by_cases h : i < n
   · rw [getElem?_eq_getElem (by simpa), getElem_replicate, if_pos h]
   · rw [getElem?_eq_none (by simpa using h), if_neg h]
@@ -2190,7 +2216,7 @@ theorem getElem?_replicate : (replicate n a)[i]? = if i < n then some a else non
 @[simp] theorem getElem?_replicate_of_lt {n : Nat} {i : Nat} (h : i < n) : (replicate n a)[i]? = some a := by
   simp [getElem?_replicate, h]
 
-theorem head?_replicate {a : α} {n : Nat} : (replicate n a).head? = if n = 0 then none else some a := by
+@[grind] theorem head?_replicate {a : α} {n : Nat} : (replicate n a).head? = if n = 0 then none else some a := by
   cases n <;> simp [replicate_succ]
 
 @[simp] theorem head_replicate (w : replicate n a ≠ []) : (replicate n a).head w = a := by
@@ -2284,7 +2310,7 @@ theorem replicate_eq_append_iff {l₁ l₂ : List α} {a : α} :
   simp only [getElem?_map, getElem?_replicate]
   split <;> simp
 
-theorem filter_replicate : (replicate n a).filter p = if p a then replicate n a else [] := by
+@[grind] theorem filter_replicate : (replicate n a).filter p = if p a then replicate n a else [] := by
   cases n with
   | zero => simp
   | succ n =>
@@ -2387,7 +2413,7 @@ termination_by l.length
 
 /-! ### reverse -/
 
-@[simp] theorem length_reverse {as : List α} : (as.reverse).length = as.length := by
+@[simp, grind] theorem length_reverse {as : List α} : (as.reverse).length = as.length := by
   induction as with
   | nil => rfl
   | cons a as ih => simp [ih]
@@ -2396,7 +2422,7 @@ theorem mem_reverseAux {x : α} : ∀ {as bs}, x ∈ reverseAux as bs ↔ x ∈
   | [], _ => ⟨.inr, fun | .inr h => h⟩
   | a :: _, _ => by rw [reverseAux, mem_cons, or_assoc, or_left_comm, mem_reverseAux, mem_cons]
 
-@[simp] theorem mem_reverse {x : α} {as : List α} : x ∈ reverse as ↔ x ∈ as := by
+@[simp, grind] theorem mem_reverse {x : α} {as : List α} : x ∈ reverse as ↔ x ∈ as := by
   simp [reverse, mem_reverseAux]
 
 @[simp] theorem reverse_eq_nil_iff {xs : List α} : xs.reverse = [] ↔ xs = [] := by
@@ -2420,14 +2446,14 @@ theorem getElem?_reverse' : ∀ {l : List α} {i j}, i + j + 1 = length l →
     rw [getElem?_append_left, getElem?_reverse' this]
     rw [length_reverse, ← this]; apply Nat.lt_add_of_pos_right (Nat.succ_pos _)
 
-@[simp]
+@[simp, grind]
 theorem getElem?_reverse {l : List α} {i} (h : i < length l) :
     l.reverse[i]? = l[l.length - 1 - i]? :=
   getElem?_reverse' <| by
     rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h),
       Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)]
 
-@[simp]
+@[simp, grind]
 theorem getElem_reverse {l : List α} {i} (h : i < l.reverse.length) :
     l.reverse[i] = l[l.length - 1 - i]'(Nat.sub_one_sub_lt_of_lt (by simpa using h)) := by
   apply Option.some.inj
@@ -2440,7 +2466,7 @@ theorem reverseAux_reverseAux_nil {as bs : List α} : reverseAux (reverseAux as
   | cons a as ih => simp [reverseAux, ih]
 
 -- The argument `as : List α` is explicit to allow rewriting from right to left.
-@[simp] theorem reverse_reverse (as : List α) : as.reverse.reverse = as := by
+@[simp, grind] theorem reverse_reverse (as : List α) : as.reverse.reverse = as := by
   simp only [reverse]; rw [reverseAux_reverseAux_nil]; rfl
 
 theorem reverse_eq_iff {as bs : List α} : as.reverse = bs ↔ as = bs.reverse := by
@@ -2455,10 +2481,10 @@ theorem reverse_eq_iff {as bs : List α} : as.reverse = bs ↔ as = bs.reverse :
 
 @[deprecated reverse_eq_cons_iff (since := "2024-09-05")] abbrev reverse_eq_cons := @reverse_eq_cons_iff
 
-@[simp] theorem getLast?_reverse {l : List α} : l.reverse.getLast? = l.head? := by
+@[simp, grind] theorem getLast?_reverse {l : List α} : l.reverse.getLast? = l.head? := by
   cases l <;> simp [getLast?_concat]
 
-@[simp] theorem head?_reverse {l : List α} : l.reverse.head? = l.getLast? := by
+@[simp, grind] theorem head?_reverse {l : List α} : l.reverse.head? = l.getLast? := by
   rw [← getLast?_reverse, reverse_reverse]
 
 theorem getLast?_eq_head?_reverse {xs : List α} : xs.getLast? = xs.reverse.head? := by
@@ -2484,21 +2510,21 @@ theorem getLast_of_mem_getLast? {l : List α} (hx : x ∈ l.getLast?) :
 @[simp] theorem map_reverse {f : α → β} {l : List α} : l.reverse.map f = (l.map f).reverse := by
   induction l <;> simp [*]
 
-@[simp] theorem filter_reverse {p : α → Bool} {l : List α} : (l.reverse.filter p) = (l.filter p).reverse := by
+@[simp, grind _=_] theorem filter_reverse {p : α → Bool} {l : List α} : (l.reverse.filter p) = (l.filter p).reverse := by
   induction l with
   | nil => simp
   | cons a l ih =>
     simp only [reverse_cons, filter_append, filter_cons, ih]
     split <;> simp_all
 
-@[simp] theorem filterMap_reverse {f : α → Option β} {l : List α} : (l.reverse.filterMap f) = (l.filterMap f).reverse := by
+@[simp, grind _=_] theorem filterMap_reverse {f : α → Option β} {l : List α} : (l.reverse.filterMap f) = (l.filterMap f).reverse := by
   induction l with
   | nil => simp
   | cons a l ih =>
     simp only [reverse_cons, filterMap_append, filterMap_cons, ih]
     split <;> simp_all
 
-@[simp] theorem reverse_append {as bs : List α} : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
+@[simp, grind _=_] theorem reverse_append {as bs : List α} : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
   induction as <;> simp_all
 
 @[simp] theorem reverse_eq_append_iff {xs ys zs : List α} :
@@ -2507,7 +2533,7 @@ theorem getLast_of_mem_getLast? {l : List α} (hx : x ∈ l.getLast?) :
 
 @[deprecated reverse_eq_append_iff (since := "2024-09-05")] abbrev reverse_eq_append := @reverse_eq_append_iff
 
-theorem reverse_concat {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse := by
+@[grind _=_] theorem reverse_concat {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse := by
   rw [reverse_append]; rfl
 
 theorem reverse_eq_concat {xs ys : List α} {a : α} :
@@ -2524,16 +2550,16 @@ theorem flatten_reverse {L : List (List α)} :
     L.reverse.flatten = (L.map reverse).flatten.reverse := by
   induction L <;> simp_all
 
-theorem reverse_flatMap {β} {l : List α} {f : α → List β} : (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f) := by
+@[grind] theorem reverse_flatMap {β} {l : List α} {f : α → List β} : (l.flatMap f).reverse = l.reverse.flatMap (reverse ∘ f) := by
   induction l <;> simp_all
 
-theorem flatMap_reverse {β} {l : List α} {f : α → List β} : (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse := by
+@[grind] theorem flatMap_reverse {β} {l : List α} {f : α → List β} : (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse := by
   induction l <;> simp_all
 
 @[simp] theorem reverseAux_eq {as bs : List α} : reverseAux as bs = reverse as ++ bs :=
   reverseAux_eq_append ..
 
-@[simp] theorem reverse_replicate {n : Nat} {a : α} : reverse (replicate n a) = replicate n a :=
+@[simp, grind] theorem reverse_replicate {n : Nat} {a : α} : (replicate n a).reverse = replicate n a :=
   eq_replicate_iff.2
     ⟨by rw [length_reverse, length_replicate],
      fun _ h => eq_of_mem_replicate (mem_reverse.1 h)⟩
@@ -2545,7 +2571,7 @@ theorem flatMap_reverse {β} {l : List α} {f : α → List β} : (l.reverse.fla
     (l ++ l').foldlM f b = l.foldlM f b >>= l'.foldlM f := by
   induction l generalizing b <;> simp [*]
 
-@[simp] theorem foldrM_cons [Monad m] [LawfulMonad m] {a : α} {l : List α} {f : α → β → m β} {b : β} :
+@[simp, grind] theorem foldrM_cons [Monad m] [LawfulMonad m] {a : α} {l : List α} {f : α → β → m β} {b : β} :
     (a :: l).foldrM f b = l.foldrM f b >>= f a := by
   simp only [foldrM]
   induction l <;> simp_all
@@ -2581,32 +2607,32 @@ theorem foldr_eq_foldrM {f : α → β → β} {b : β} {l : List α} :
 
 /-! ### foldl and foldr -/
 
-@[simp] theorem foldr_cons_eq_append {l : List α} {f : α → β} {l' : List β} :
+@[simp, grind] theorem foldr_cons_eq_append {l : List α} {f : α → β} {l' : List β} :
     l.foldr (fun x ys => f x :: ys) l' = l.map f ++ l' := by
   induction l <;> simp [*]
 
 /-- Variant of `foldr_cons_eq_append` specalized to `f = id`. -/
-@[simp] theorem foldr_cons_eq_append' {l l' : List β} :
+@[simp, grind] theorem foldr_cons_eq_append' {l l' : List β} :
     l.foldr cons l' = l ++ l' := by
   induction l <;> simp [*]
 
-@[simp] theorem foldl_flip_cons_eq_append {l : List α} {f : α → β} {l' : List β} :
+@[simp, grind] theorem foldl_flip_cons_eq_append {l : List α} {f : α → β} {l' : List β} :
     l.foldl (fun xs y => f y :: xs) l' = (l.map f).reverse ++ l' := by
   induction l generalizing l' <;> simp [*]
 
-@[simp] theorem foldr_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
+@[simp, grind] theorem foldr_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
     l.foldr (f · ++ ·) l' = (l.map f).flatten ++ l' := by
   induction l <;> simp [*]
 
-@[simp] theorem foldl_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
+@[simp, grind] theorem foldl_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
     l.foldl (· ++ f ·) l' = l' ++ (l.map f).flatten := by
   induction l generalizing l'<;> simp [*]
 
-@[simp] theorem foldr_flip_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
+@[simp, grind] theorem foldr_flip_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
     l.foldr (fun x ys => ys ++ f x) l' = l' ++ (l.map f).reverse.flatten := by
   induction l generalizing l' <;> simp [*]
 
-@[simp] theorem foldl_flip_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
+@[simp, grind] theorem foldl_flip_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
     l.foldl (fun xs y => f y ++ xs) l' = (l.map f).reverse.flatten ++ l' := by
   induction l generalizing l' <;> simp [*]
 
@@ -2660,24 +2686,24 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
     (l ++ l').foldrM f b = l'.foldrM f b >>= l.foldrM f := by
   induction l <;> simp [*]
 
-@[simp] theorem foldl_append {β : Type _} {f : β → α → β} {b : β} {l l' : List α} :
+@[simp, grind _=_] theorem foldl_append {β : Type _} {f : β → α → β} {b : β} {l l' : List α} :
     (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM]
 
-@[simp] theorem foldr_append {f : α → β → β} {b : β} {l l' : List α} :
+@[simp, grind _=_] theorem foldr_append {f : α → β → β} {b : β} {l l' : List α} :
     (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM]
 
-theorem foldl_flatten {f : β → α → β} {b : β} {L : List (List α)} :
+@[grind] theorem foldl_flatten {f : β → α → β} {b : β} {L : List (List α)} :
     (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by
   induction L generalizing b <;> simp_all
 
-theorem foldr_flatten {f : α → β → β} {b : β} {L : List (List α)} :
+@[grind] theorem foldr_flatten {f : α → β → β} {b : β} {L : List (List α)} :
     (flatten L).foldr f b = L.foldr (fun l b => l.foldr f b) b := by
   induction L <;> simp_all
 
-@[simp] theorem foldl_reverse {l : List α} {f : β → α → β} {b : β} :
+@[simp, grind] theorem foldl_reverse {l : List α} {f : β → α → β} {b : β} :
     l.reverse.foldl f b = l.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
 
-@[simp] theorem foldr_reverse {l : List α} {f : α → β → β} {b : β} :
+@[simp, grind] theorem foldr_reverse {l : List α} {f : α → β → β} {b : β} :
     l.reverse.foldr f b = l.foldl (fun x y => f y x) b :=
   (foldl_reverse ..).symm.trans <| by simp
 
@@ -2829,7 +2855,7 @@ theorem foldr_rel {l : List α} {f g : α → β → β} {a b : β} {r : β →
 
 /-! #### Further results about `getLast` and `getLast?` -/
 
-@[simp] theorem head_reverse {l : List α} (h : l.reverse ≠ []) :
+@[simp, grind] theorem head_reverse {l : List α} (h : l.reverse ≠ []) :
     l.reverse.head h = getLast l (by simp_all) := by
   induction l with
   | nil => contradiction
@@ -2861,7 +2887,7 @@ theorem getLast?_eq_some_iff {xs : List α} {a : α} : xs.getLast? = some a ↔
 
 @[deprecated mem_of_getLast? (since := "2024-10-21")] abbrev mem_of_getLast?_eq_some := @mem_of_getLast?
 
-@[simp] theorem getLast_reverse {l : List α} (h : l.reverse ≠ []) :
+@[simp, grind] theorem getLast_reverse {l : List α} (h : l.reverse ≠ []) :
     l.reverse.getLast h = l.head (by simp_all) := by
   simp [getLast_eq_head_reverse]
 
@@ -2874,7 +2900,7 @@ theorem head_eq_getLast_reverse {l : List α} (h : l ≠ []) :
   simp only [getLast_eq_head_reverse, reverse_append]
   rw [head_append_of_ne_nil]
 
-theorem getLast_append {l : List α} (h : l ++ l' ≠ []) :
+@[grind] theorem getLast_append {l : List α} (h : l ++ l' ≠ []) :
     (l ++ l').getLast h =
       if h' : l'.isEmpty then
         l.getLast (by simp_all [isEmpty_iff])
@@ -2895,7 +2921,7 @@ theorem getLast_append_left {l : List α} (w : l ++ l' ≠ []) (h : l' = []) :
     (l ++ l').getLast w = l.getLast (by simp_all) := by
   rw [getLast_append, dif_pos (by simp_all)]
 
-@[simp] theorem getLast?_append {l l' : List α} : (l ++ l').getLast? = l'.getLast?.or l.getLast? := by
+@[simp, grind] theorem getLast?_append {l l' : List α} : (l ++ l').getLast? = l'.getLast?.or l.getLast? := by
   simp [← head?_reverse]
 
 theorem getLast_filter_of_pos {p : α → Bool} {l : List α} (w : l ≠ []) (h : p (getLast l w) = true) :
@@ -2969,7 +2995,7 @@ Because we immediately simplify `partition` into two `filter`s for verification
 we do not separately develop much theory about it.
 -/
 
-@[simp] theorem partition_eq_filter_filter {p : α → Bool} {l : List α} :
+@[simp, grind] theorem partition_eq_filter_filter {p : α → Bool} {l : List α} :
     partition p l = (filter p l, filter (not ∘ p) l) := by simp [partition, aux]
   where
     aux : ∀ l {as bs}, partition.loop p l (as, bs) =
@@ -2986,16 +3012,16 @@ theorem mem_partition : a ∈ l ↔ a ∈ (partition p l).1 ∨ a ∈ (partition
 are often used for theorems about `Array.pop`.
 -/
 
-@[simp] theorem length_dropLast : ∀ {xs : List α}, xs.dropLast.length = xs.length - 1
+@[simp, grind] theorem length_dropLast : ∀ {xs : List α}, xs.dropLast.length = xs.length - 1
   | [] => rfl
   | x::xs => by simp
 
-@[simp] theorem getElem_dropLast : ∀ {xs : List α} {i : Nat} (h : i < xs.dropLast.length),
+@[simp, grind] theorem getElem_dropLast : ∀ {xs : List α} {i : Nat} (h : i < xs.dropLast.length),
     xs.dropLast[i] = xs[i]'(Nat.lt_of_lt_of_le h (length_dropLast .. ▸ Nat.pred_le _))
   | _ :: _ :: _, 0, _ => rfl
   | _ :: _ :: _, _ + 1, h => getElem_dropLast (Nat.add_one_lt_add_one_iff.mp h)
 
-theorem getElem?_dropLast {xs : List α} {i : Nat} :
+@[grind] theorem getElem?_dropLast {xs : List α} {i : Nat} :
     xs.dropLast[i]? = if i < xs.length - 1 then xs[i]? else none := by
   split
   · rw [getElem?_eq_getElem, getElem?_eq_getElem, getElem_dropLast]
@@ -3121,6 +3147,10 @@ variable [BEq α]
 @[simp] theorem replace_cons_self [LawfulBEq α] {a : α} : (a::as).replace a b = b::as := by
   simp [replace_cons]
 
+@[simp] theorem replace_singleton {a b c : α} : [a].replace b c = [if b == a then c else a] := by
+  simp only [replace_cons]
+  split <;> simp_all
+
 @[simp] theorem replace_of_not_mem [LawfulBEq α] {l : List α} (h : a ∉ l) : l.replace a b = l := by
   induction l with
   | nil => rfl
@@ -3128,14 +3158,14 @@ variable [BEq α]
     simp only [replace_cons]
     split <;> simp_all
 
-@[simp] theorem length_replace {l : List α} : (l.replace a b).length = l.length := by
+@[simp, grind] theorem length_replace {l : List α} : (l.replace a b).length = l.length := by
   induction l with
   | nil => simp
   | cons x l ih =>
     simp only [replace_cons]
     split <;> simp_all
 
-theorem getElem?_replace [LawfulBEq α] {l : List α} {i : Nat} :
+@[grind] theorem getElem?_replace [LawfulBEq α] {l : List α} {i : Nat} :
     (l.replace a b)[i]? = if l[i]? == some a then if a ∈ l.take i then some a else some b else l[i]? := by
   induction l generalizing i with
   | nil => cases i <;> simp
@@ -3148,7 +3178,7 @@ theorem getElem?_replace_of_ne [LawfulBEq α] {l : List α} {i : Nat} (h : l[i]?
     (l.replace a b)[i]? = l[i]? := by
   simp_all [getElem?_replace]
 
-theorem getElem_replace [LawfulBEq α] {l : List α} {i : Nat} (h : i < l.length) :
+@[grind] theorem getElem_replace [LawfulBEq α] {l : List α} {i : Nat} (h : i < l.length) :
     (l.replace a b)[i]'(by simpa) = if l[i] == a then if a ∈ l.take i then a else b else l[i] := by
   apply Option.some.inj
   rw [← getElem?_eq_getElem, getElem?_replace]
@@ -3178,7 +3208,7 @@ theorem head_replace {l : List α} {a b : α} (w) :
   apply Option.some.inj
   rw [← head?_eq_head, head?_replace, head?_eq_head]
 
-theorem replace_append [LawfulBEq α] {l₁ l₂ : List α} :
+@[grind] theorem replace_append [LawfulBEq α] {l₁ l₂ : List α} :
     (l₁ ++ l₂).replace a b = if a ∈ l₁ then l₁.replace a b ++ l₂ else l₁ ++ l₂.replace a b := by
   induction l₁ with
   | nil => simp
@@ -3221,7 +3251,7 @@ end replace
 section insert
 variable [BEq α]
 
-@[simp] theorem insert_nil (a : α) : [].insert a = [a] := rfl
+@[simp, grind] theorem insert_nil (a : α) : [].insert a = [a] := rfl
 
 variable [LawfulBEq α]
 
@@ -3231,7 +3261,7 @@ variable [LawfulBEq α]
 @[simp] theorem insert_of_not_mem {l : List α} (h : a ∉ l) : l.insert a = a :: l := by
   simp [List.insert, h]
 
-@[simp] theorem mem_insert_iff {l : List α} : a ∈ l.insert b ↔ a = b ∨ a ∈ l := by
+@[simp, grind] theorem mem_insert_iff {l : List α} : a ∈ l.insert b ↔ a = b ∨ a ∈ l := by
   if h : b ∈ l then
     rw [insert_of_mem h]
     constructor; {apply Or.inr}
@@ -3255,7 +3285,7 @@ theorem eq_or_mem_of_mem_insert {l : List α} (h : a ∈ l.insert b) : a = b ∨
 @[simp] theorem length_insert_of_not_mem {l : List α} (h : a ∉ l) :
     length (l.insert a) = length l + 1 := by rw [insert_of_not_mem h]; rfl
 
-theorem length_insert {l : List α} :
+@[grind] theorem length_insert {l : List α} :
     (l.insert a).length = l.length + if a ∈ l then 0 else 1 := by
   split <;> simp_all
 
@@ -3266,7 +3296,9 @@ theorem length_le_length_insert {l : List α} {a : α} : l.length ≤ (l.insert
   · rw [length_insert_of_not_mem h]
     exact Nat.le_succ _
 
-theorem length_insert_pos {l : List α} {a : α} : 0 < (l.insert a).length := by
+grind_pattern List.length_le_length_insert => (l.insert a).length
+
+@[grind] theorem length_insert_pos {l : List α} {a : α} : 0 < (l.insert a).length := by
   by_cases h : a ∈ l
   · rw [length_insert_of_mem h]
     exact length_pos_of_mem h
@@ -3286,13 +3318,13 @@ theorem getElem?_insert_succ {l : List α} {a : α} {i : Nat} :
   simp only [insert_eq]
   split <;> simp
 
-theorem getElem?_insert {l : List α} {a : α} {i : Nat} :
+@[grind] theorem getElem?_insert {l : List α} {a : α} {i : Nat} :
     (l.insert a)[i]? = if a ∈ l then l[i]? else if i = 0 then some a else l[i-1]? := by
   cases i
   · simp [getElem?_insert_zero]
   · simp [getElem?_insert_succ]
 
-theorem getElem_insert {l : List α} {a : α} {i : Nat} (h : i < l.length) :
+@[grind] theorem getElem_insert {l : List α} {a : α} {i : Nat} (h : i < l.length) :
     (l.insert a)[i]'(Nat.lt_of_lt_of_le h length_le_length_insert) =
       if a ∈ l then l[i] else if i = 0 then a else l[i-1]'(Nat.lt_of_le_of_lt (Nat.pred_le _) h) := by
   apply Option.some.inj
@@ -3316,7 +3348,7 @@ theorem head_insert {l : List α} {a : α} (w) :
   apply Option.some.inj
   rw [← head?_eq_head, head?_insert]
 
-theorem insert_append {l₁ l₂ : List α} {a : α} :
+@[grind] theorem insert_append {l₁ l₂ : List α} {a : α} :
     (l₁ ++ l₂).insert a = if a ∈ l₂ then l₁ ++ l₂ else l₁.insert a ++ l₂ := by
   simp only [insert_eq, mem_append]
   (repeat split) <;> simp_all
@@ -3329,7 +3361,7 @@ theorem insert_append_of_not_mem_left {l₁ l₂ : List α} (h : ¬ a ∈ l₂)
     (l₁ ++ l₂).insert a = l₁.insert a ++ l₂ := by
   simp [insert_append, h]
 
-@[simp] theorem insert_replicate_self {a : α} (h : 0 < n) : (replicate n a).insert a = replicate n a := by
+@[simp, grind] theorem insert_replicate_self {a : α} (h : 0 < n) : (replicate n a).insert a = replicate n a := by
   cases n <;> simp_all
 
 @[simp] theorem insert_replicate_ne {a b : α} (h : !b == a) :
@@ -3409,38 +3441,38 @@ theorem all_eq_not_any_not {l : List α} {p : α → Bool} : l.all p = !l.any (!
     simp only [filterMap_cons]
     split <;> simp_all
 
-@[simp] theorem any_append {xs ys : List α} : (xs ++ ys).any f = (xs.any f || ys.any f) := by
+@[simp, grind _=_] theorem any_append {xs ys : List α} : (xs ++ ys).any f = (xs.any f || ys.any f) := by
   induction xs with
   | nil => rfl
   | cons h t ih => simp_all [Bool.or_assoc]
 
-@[simp] theorem all_append {xs ys : List α} : (xs ++ ys).all f = (xs.all f && ys.all f) := by
+@[simp, grind _=_] theorem all_append {xs ys : List α} : (xs ++ ys).all f = (xs.all f && ys.all f) := by
   induction xs with
   | nil => rfl
   | cons h t ih => simp_all [Bool.and_assoc]
 
-@[simp] theorem any_flatten {l : List (List α)} : l.flatten.any f = l.any (any · f) := by
+@[simp, grind] theorem any_flatten {l : List (List α)} : l.flatten.any f = l.any (any · f) := by
   induction l <;> simp_all
 
 @[deprecated any_flatten (since := "2024-10-14")] abbrev any_join := @any_flatten
 
-@[simp] theorem all_flatten {l : List (List α)} : l.flatten.all f = l.all (all · f) := by
+@[simp, grind] theorem all_flatten {l : List (List α)} : l.flatten.all f = l.all (all · f) := by
   induction l <;> simp_all
 
 @[deprecated all_flatten (since := "2024-10-14")] abbrev all_join := @all_flatten
 
-@[simp] theorem any_flatMap {l : List α} {f : α → List β} :
+@[simp, grind] theorem any_flatMap {l : List α} {f : α → List β} :
     (l.flatMap f).any p = l.any fun a => (f a).any p := by
   induction l <;> simp_all
 
-@[simp] theorem all_flatMap {l : List α} {f : α → List β} :
+@[simp, grind] theorem all_flatMap {l : List α} {f : α → List β} :
     (l.flatMap f).all p = l.all fun a => (f a).all p := by
   induction l <;> simp_all
 
-@[simp] theorem any_reverse {l : List α} : l.reverse.any f = l.any f := by
+@[simp, grind] theorem any_reverse {l : List α} : l.reverse.any f = l.any f := by
   induction l <;> simp_all [Bool.or_comm]
 
-@[simp] theorem all_reverse {l : List α} : l.reverse.all f = l.all f := by
+@[simp, grind] theorem all_reverse {l : List α} : l.reverse.all f = l.all f := by
   induction l <;> simp_all [Bool.and_comm]
 
 @[simp] theorem any_replicate {n : Nat} {a : α} :

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -13,7 +13,6 @@ import Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Simproc
 import Init.TacticsExtra
-import Init.Omega
 
 /-
 This module defines properties of the bitwise operations on Natural numbers.

src/Init/Data/Nat/Lemmas.lean

@@ -10,7 +10,6 @@ import Init.Data.Nat.MinMax
 import Init.Data.Nat.Log2
 import Init.Data.Nat.Power2
 import Init.Data.Nat.Mod
-import Init.Omega
 
 /-! # Basic theorems about natural numbers
 

src/Init/Data/Option/Basic.lean

@@ -23,8 +23,8 @@ def getM [Alternative m] : Option α → m α
   | some _ => true
   | none   => false
 
-@[simp] theorem isSome_none : @isSome α none = false := rfl
-@[simp] theorem isSome_some : isSome (some a) = true := rfl
+@[simp, grind] theorem isSome_none : @isSome α none = false := rfl
+@[simp, grind] theorem isSome_some : isSome (some a) = true := rfl
 
 /--
 Returns `true` on `none` and `false` on `some x`.
@@ -39,8 +39,8 @@ Examples:
   | some _ => false
   | none   => true
 
-@[simp] theorem isNone_none : @isNone α none = true := rfl
-@[simp] theorem isNone_some : isNone (some a) = false := rfl
+@[simp, grind] theorem isNone_none : @isNone α none = true := rfl
+@[simp, grind] theorem isNone_some : isNone (some a) = false := rfl
 
 /--
 Checks whether an optional value is both present and equal to some other value.
@@ -230,14 +230,14 @@ def merge (fn : α → α → α) : Option α → Option α → Option α
   | none  , some y => some y
   | some x, some y => some <| fn x y
 
-@[simp] theorem getD_none : getD none a = a := rfl
-@[simp] theorem getD_some : getD (some a) b = a := rfl
+@[simp, grind] theorem getD_none : getD none a = a := rfl
+@[simp, grind] theorem getD_some : getD (some a) b = a := rfl
 
-@[simp] theorem map_none (f : α → β) : none.map f = none := rfl
-@[simp] theorem map_some (a) (f : α → β) : (some a).map f = some (f a) := rfl
+@[simp, grind] theorem map_none (f : α → β) : none.map f = none := rfl
+@[simp, grind] theorem map_some (a) (f : α → β) : (some a).map f = some (f a) := rfl
 
-@[simp] theorem none_bind (f : α → Option β) : none.bind f = none := rfl
-@[simp] theorem some_bind (a) (f : α → Option β) : (some a).bind f = f a := rfl
+@[simp, grind] theorem none_bind (f : α → Option β) : none.bind f = none := rfl
+@[simp, grind] theorem some_bind (a) (f : α → Option β) : (some a).bind f = f a := rfl
 
 /--
 A case analysis function for `Option`.
@@ -400,11 +400,11 @@ instance (α) [BEq α] [LawfulBEq α] : LawfulBEq (Option α) where
     | some x, some y => rw [LawfulBEq.eq_of_beq (α := α) h]
     | none, none => rfl
 
-@[simp] theorem all_none : Option.all p none = true := rfl
-@[simp] theorem all_some : Option.all p (some x) = p x := rfl
+@[simp, grind] theorem all_none : Option.all p none = true := rfl
+@[simp, grind] theorem all_some : Option.all p (some x) = p x := rfl
 
-@[simp] theorem any_none : Option.any p none = false := rfl
-@[simp] theorem any_some : Option.any p (some x) = p x := rfl
+@[simp, grind] theorem any_none : Option.any p none = false := rfl
+@[simp, grind] theorem any_some : Option.any p (some x) = p x := rfl
 
 /--
 The minimum of two optional values, with `none` treated as the least element. This function is

src/Init/Data/Option/Lemmas.lean

@@ -17,7 +17,7 @@ namespace Option
 @[deprecated mem_def (since := "2025-04-07")]
 theorem mem_iff {a : α} {b : Option α} : a ∈ b ↔ b = some a := .rfl
 
-theorem mem_some {a b : α} : a ∈ some b ↔ b = a := by simp
+@[grind] theorem mem_some {a b : α} : a ∈ some b ↔ b = a := by simp
 
 theorem mem_some_iff {a b : α} : a ∈ some b ↔ b = a := mem_some
 
@@ -45,7 +45,7 @@ theorem get_of_mem : ∀ {o : Option α} (h : isSome o), a ∈ o → o.get h = a
 theorem get_of_eq_some : ∀ {o : Option α} (h : isSome o), o = some a → o.get h = a
   | _, _, rfl => rfl
 
-@[simp] theorem not_mem_none (a : α) : a ∉ (none : Option α) := nofun
+@[simp, grind] theorem not_mem_none (a : α) : a ∉ (none : Option α) := nofun
 
 theorem getD_of_ne_none {x : Option α} (hx : x ≠ none) (y : α) : some (x.getD y) = x := by
   cases x; {contradiction}; rw [getD_some]
@@ -53,9 +53,9 @@ theorem getD_of_ne_none {x : Option α} (hx : x ≠ none) (y : α) : some (x.get
 theorem getD_eq_iff {o : Option α} {a b} : o.getD a = b ↔ (o = some b ∨ o = none ∧ a = b) := by
   cases o <;> simp
 
-@[simp] theorem get!_none [Inhabited α] : (none : Option α).get! = default := rfl
+@[simp, grind] theorem get!_none [Inhabited α] : (none : Option α).get! = default := rfl
 
-@[simp] theorem get!_some [Inhabited α] {a : α} : (some a).get! = a := rfl
+@[simp, grind] theorem get!_some [Inhabited α] {a : α} : (some a).get! = a := rfl
 
 theorem get_eq_get! [Inhabited α] : (o : Option α) → {h : o.isSome} → o.get h = o.get!
   | some _, _ => rfl
@@ -85,6 +85,7 @@ theorem mem_unique {o : Option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a
 theorem eq_some_unique {o : Option α} {a b : α} (ha : o = some a) (hb : o = some b) : a = b :=
   some.inj <| ha ▸ hb
 
+-- This is not a good `@[grind ext]` lemma, as it results in too much case splitting.
 @[ext] theorem ext : ∀ {o₁ o₂ : Option α}, (∀ a, o₁ = some a ↔ o₂ = some a) → o₁ = o₂
   | none, none, _ => rfl
   | some _, _, H => ((H _).1 rfl).symm
@@ -118,7 +119,7 @@ theorem isSome_of_eq_some {x : Option α} {y : α} (h : x = some y) : x.isSome :
 @[simp] theorem isNone_eq_false_iff : isNone a = false ↔ a.isSome = true := by
   cases a <;> simp
 
-@[simp]
+@[simp, grind]
 theorem not_isSome (a : Option α) : (!a.isSome) = a.isNone := by
   cases a <;> simp
 
@@ -127,7 +128,7 @@ theorem not_comp_isSome : (! ·) ∘ @Option.isSome α = Option.isNone := by
   funext
   simp
 
-@[simp]
+@[simp, grind]
 theorem not_isNone (a : Option α) : (!a.isNone) = a.isSome := by
   cases a <;> simp
 
@@ -278,13 +279,13 @@ abbrev map_eq_none := @map_eq_none_iff
 @[deprecated map_eq_none_iff (since := "2025-04-10")]
 abbrev map_eq_none' := @map_eq_none_iff
 
-@[simp] theorem isSome_map {x : Option α} : (x.map f).isSome = x.isSome := by
+@[simp, grind] theorem isSome_map {x : Option α} : (x.map f).isSome = x.isSome := by
   cases x <;> simp
 
 @[deprecated isSome_map (since := "2025-04-10")]
 abbrev isSome_map' := @isSome_map
 
-@[simp] theorem isNone_map {x : Option α} : (x.map f).isNone = x.isNone := by
+@[simp, grind] theorem isNone_map {x : Option α} : (x.map f).isNone = x.isNone := by
   cases x <;> simp
 
 theorem map_eq_bind {x : Option α} : x.map f = x.bind (some ∘ f) := by
@@ -337,9 +338,9 @@ theorem map_inj_right {f : α → β} {o o' : Option α} (w : ∀ x y, f x = f y
      (if h : c then some (a h) else none).map f = if h : c then some (f (a h)) else none := by
   split <;> rfl
 
-@[simp] theorem filter_none (p : α → Bool) : none.filter p = none := rfl
+@[simp, grind] theorem filter_none (p : α → Bool) : none.filter p = none := rfl
 
-theorem filter_some : Option.filter p (some a) = if p a then some a else none := rfl
+@[grind] theorem filter_some : Option.filter p (some a) = if p a then some a else none := rfl
 
 theorem isSome_of_isSome_filter (p : α → Bool) (o : Option α) (h : (o.filter p).isSome) :
     o.isSome := by
@@ -447,9 +448,9 @@ theorem join_join {x : Option (Option (Option α))} : x.join.join = (x.map join)
 theorem mem_of_mem_join {a : α} {x : Option (Option α)} (h : a ∈ x.join) : some a ∈ x :=
   h.symm ▸ join_eq_some_iff.1 h
 
-@[simp] theorem some_orElse (a : α) (f) : (some a).orElse f = some a := rfl
+@[simp, grind] theorem some_orElse (a : α) (f) : (some a).orElse f = some a := rfl
 
-@[simp] theorem none_orElse (f : Unit → Option α) : none.orElse f = f () := rfl
+@[simp, grind] theorem none_orElse (f : Unit → Option α) : none.orElse f = f () := rfl
 
 @[simp] theorem orElse_none (x : Option α) : x.orElse (fun _ => none) = x := by cases x <;> rfl
 
@@ -525,13 +526,13 @@ theorem merge_eq_or_eq {f : α → α → α} (h : ∀ a b, f a b = a ∨ f a b
   | none, some _ => .inr rfl
   | some a, some b => by have := h a b; simp [merge] at this ⊢; exact this
 
-@[simp] theorem merge_none_left {f} {b : Option α} : merge f none b = b := by
+@[simp, grind] theorem merge_none_left {f} {b : Option α} : merge f none b = b := by
   cases b <;> rfl
 
-@[simp] theorem merge_none_right {f} {a : Option α} : merge f a none = a := by
+@[simp, grind] theorem merge_none_right {f} {a : Option α} : merge f a none = a := by
   cases a <;> rfl
 
-@[simp] theorem merge_some_some {f} {a b : α} :
+@[simp, grind] theorem merge_some_some {f} {a b : α} :
   merge f (some a) (some b) = some (f a b) := rfl
 
 @[deprecated merge_eq_or_eq (since := "2025-04-04")]
@@ -567,11 +568,11 @@ instance lawfulIdentity_merge (f : α → α → α) : Std.LawfulIdentity (merge
   left_id a := by cases a <;> simp [merge]
   right_id a := by cases a <;> simp [merge]
 
-@[simp] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
+@[simp, grind] theorem elim_none (x : β) (f : α → β) : none.elim x f = x := rfl
 
-@[simp] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
+@[simp, grind] theorem elim_some (x : β) (f : α → β) (a : α) : (some a).elim x f = f a := rfl
 
-@[simp] theorem getD_map (f : α → β) (x : α) (o : Option α) :
+@[simp, grind] theorem getD_map (f : α → β) (x : α) (o : Option α) :
   (o.map f).getD (f x) = f (getD o x) := by cases o <;> rfl
 
 section choice
@@ -600,14 +601,14 @@ abbrev choice_isSome_iff_nonempty := @isSome_choice_iff_nonempty
 
 end choice
 
-@[simp] theorem toList_some (a : α) : (some a).toList = [a] := rfl
+@[simp, grind] theorem toList_some (a : α) : (some a).toList = [a] := rfl
 
-@[simp] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl
+@[simp, grind] theorem toList_none (α : Type _) : (none : Option α).toList = [] := rfl
 
 -- See `Init.Data.Option.List` for lemmas about `toList`.
 
-@[simp] theorem some_or : (some a).or o = some a := rfl
-@[simp] theorem none_or : none.or o = o := rfl
+@[simp, grind] theorem some_or : (some a).or o = some a := rfl
+@[simp, grind] theorem none_or : none.or o = o := rfl
 
 theorem or_eq_right_of_none {o o' : Option α} (h : o = none) : o.or o' = o' := by
   cases h; simp
@@ -615,16 +616,16 @@ theorem or_eq_right_of_none {o o' : Option α} (h : o = none) : o.or o' = o' :=
 @[deprecated some_or (since := "2024-11-03")] theorem or_some : (some a).or o = some a := rfl
 
 /-- This will be renamed to `or_some` once the existing deprecated lemma is removed. -/
-@[simp] theorem or_some' {o : Option α} : o.or (some a) = some (o.getD a) := by
+@[simp, grind] theorem or_some' {o : Option α} : o.or (some a) = some (o.getD a) := by
   cases o <;> rfl
 
 theorem or_eq_bif : or o o' = bif o.isSome then o else o' := by
   cases o <;> rfl
 
-@[simp] theorem isSome_or : (or o o').isSome = (o.isSome || o'.isSome) := by
+@[simp, grind] theorem isSome_or : (or o o').isSome = (o.isSome || o'.isSome) := by
   cases o <;> rfl
 
-@[simp] theorem isNone_or : (or o o').isNone = (o.isNone && o'.isNone) := by
+@[simp, grind] theorem isNone_or : (or o o').isNone = (o.isNone && o'.isNone) := by
   cases o <;> rfl
 
 @[simp] theorem or_eq_none_iff : or o o' = none ↔ o = none ∧ o' = none := by
@@ -643,7 +644,7 @@ theorem or_assoc : or (or o₁ o₂) o₃ = or o₁ (or o₂ o₃) := by
   cases o₁ <;> cases o₂ <;> rfl
 instance : Std.Associative (or (α := α)) := ⟨@or_assoc _⟩
 
-@[simp]
+@[simp, grind]
 theorem or_none : or o none = o := by
   cases o <;> rfl
 
@@ -654,7 +655,7 @@ instance : Std.LawfulIdentity (or (α := α)) none where
   left_id := @none_or _
   right_id := @or_none _
 
-@[simp]
+@[simp, grind]
 theorem or_self : or o o = o := by
   cases o <;> rfl
 instance : Std.IdempotentOp (or (α := α)) := ⟨@or_self _⟩
@@ -662,7 +663,7 @@ instance : Std.IdempotentOp (or (α := α)) := ⟨@or_self _⟩
 theorem or_eq_orElse : or o o' = o.orElse (fun _ => o') := by
   cases o <;> rfl
 
-theorem map_or : (or o o').map f = (o.map f).or (o'.map f) := by
+@[grind _=_] theorem map_or : (or o o').map f = (o.map f).or (o'.map f) := by
   cases o <;> rfl
 
 @[deprecated map_or (since := "2025-04-10")]
@@ -815,8 +816,8 @@ theorem isSome_filter {α : Type _} {x : Option α} {f : α → Bool} :
 
 /-! ### pbind -/
 
-@[simp] theorem pbind_none : pbind none f = none := rfl
-@[simp] theorem pbind_some : pbind (some a) f = f a rfl := rfl
+@[simp, grind] theorem pbind_none : pbind none f = none := rfl
+@[simp, grind] theorem pbind_some : pbind (some a) f = f a rfl := rfl
 
 @[simp] theorem map_pbind {o : Option α} {f : (a : α) → o = some a → Option β}
     {g : β → γ} : (o.pbind f).map g = o.pbind (fun a h => (f a h).map g) := by
@@ -856,20 +857,24 @@ theorem pbind_eq_some_iff {o : Option α} {f : (a : α) → o = some a → Optio
 
 /-! ### pmap -/
 
-@[simp] theorem pmap_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
+@[simp, grind] theorem pmap_none {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
     pmap f none h = none := rfl
 
-@[simp] theorem pmap_some {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
+@[simp, grind] theorem pmap_some {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
     pmap f (some a) h = some (f a (h a rfl)) := rfl
 
 @[simp] theorem pmap_eq_none_iff {p : α → Prop} {f : ∀ (a : α), p a → β} {h} :
     pmap f o h = none ↔ o = none := by
   cases o <;> simp
 
-@[simp] theorem isSome_pmap {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
+@[simp, grind] theorem isSome_pmap {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
     (pmap f o h).isSome = o.isSome := by
   cases o <;> simp
 
+@[simp, grind] theorem isNone_pmap {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
+    (pmap f o h).isNone = o.isNone := by
+  cases o <;> simp
+
 @[deprecated isSome_pmap (since := "2025-04-01")] abbrev pmap_isSome := @isSome_pmap
 
 @[simp] theorem pmap_eq_some_iff {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
@@ -928,8 +933,8 @@ theorem pmap_congr {α : Type u} {β : Type v}
 
 /-! ### pelim -/
 
-@[simp] theorem pelim_none : pelim none b f = b := rfl
-@[simp] theorem pelim_some : pelim (some a) b f = f a rfl := rfl
+@[simp, grind] theorem pelim_none : pelim none b f = b := rfl
+@[simp, grind] theorem pelim_some : pelim (some a) b f = f a rfl := rfl
 
 @[simp] theorem pelim_eq_elim : pelim o b (fun a _ => f a) = o.elim b f := by
   cases o <;> simp
@@ -951,11 +956,11 @@ theorem pfilter_congr {α : Type u} {o o' : Option α} (ho : o = o')
   congr; funext a ha
   exact hf a ha
 
-@[simp] theorem pfilter_none {α : Type _} {p : (a : α) → none = some a → Bool} :
+@[simp, grind] theorem pfilter_none {α : Type _} {p : (a : α) → none = some a → Bool} :
     none.pfilter p = none := by
   rfl
 
-@[simp] theorem pfilter_some {α : Type _} {x : α} {p : (a : α) → some x = some a → Bool} :
+@[simp, grind] theorem pfilter_some {α : Type _} {x : α} {p : (a : α) → some x = some a → Bool} :
     (some x).pfilter p = if p x rfl then some x else none := by
   simp only [pfilter, cond_eq_if]
 

src/Init/Data/Ord.lean

@@ -10,7 +10,7 @@ prelude
 import Init.Data.String
 import Init.Data.Array.Basic
 import Init.Data.SInt.Basic
-import Init.Data.Vector
+import Init.Data.Vector.Basic
 
 /--
 The result of a comparison according to a total order.

src/Init/Data/Vector/Find.lean

@@ -26,10 +26,11 @@ open Nat
 
 /-! ### findSome? -/
 
-@[simp] theorem findSome?_empty : (#v[] : Vector α 0).findSome? f = none := rfl
-@[simp] theorem findSome?_push {xs : Vector α n} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
+@[simp, grind] theorem findSome?_empty : (#v[] : Vector α 0).findSome? f = none := rfl
+@[simp, grind] theorem findSome?_push {xs : Vector α n} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
   cases xs; simp [List.findSome?_append]
 
+@[grind]
 theorem findSome?_singleton {a : α} {f : α → Option β} : #v[a].findSome? f = f a := by
   simp
 

src/Init/Data/Vector/Lemmas.lean

@@ -483,7 +483,7 @@ abbrev toArray_mkVector := @toArray_replicate
 `Vector.ext` is an extensionality theorem.
 Vectors `a` and `b` are equal to each other if their elements are equal for each valid index.
 -/
-@[ext]
+@[ext, grind ext]
 protected theorem ext {xs ys : Vector α n} (h : (i : Nat) → (_ : i < n) → xs[i] = ys[i]) : xs = ys := by
   apply Vector.toArray_inj.1
   apply Array.ext
@@ -776,11 +776,12 @@ theorem singleton_inj : #v[a] = #v[b] ↔ a = b := by
 
 /-! ### replicate -/
 
-@[simp] theorem replicate_zero : replicate 0 a = #v[] := rfl
+@[simp, grind] theorem replicate_zero : replicate 0 a = #v[] := rfl
 
 @[deprecated replicate_zero (since := "2025-03-18")]
 abbrev replicate_mkVector := @replicate_zero
 
+@[grind]
 theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
   simp [replicate, Array.replicate_succ]
 
@@ -820,12 +821,17 @@ abbrev mkVector_eq_mk_mkArray := @replicate_eq_mk_replicate
 theorem getElem?_eq_none {xs : Vector α n} (h : n ≤ i) : xs[i]? = none := by
   simp [getElem?_eq_none_iff, h]
 
+-- This is a more aggressive pattern than for `List/Array.getElem?_eq_none`, because
+-- `length/size` won't appear.
+grind_pattern Vector.getElem?_eq_none => n ≤ i, xs[i]?
+
 @[simp] theorem getElem?_eq_getElem {xs : Vector α n} {i : Nat} (h : i < n) : xs[i]? = some xs[i] :=
   getElem?_pos ..
 
 theorem getElem?_eq_some_iff {xs : Vector α n} : xs[i]? = some b ↔ ∃ h : i < n, xs[i] = b := by
   simp [getElem?_def]
 
+@[grind →]
 theorem getElem_of_getElem? {xs : Vector α n} : xs[i]? = some a → ∃ h : i < n, xs[i] = a :=
   getElem?_eq_some_iff.mp
 
@@ -885,12 +891,13 @@ set_option linter.indexVariables false in
   match i, h with
   | 0, _ => rfl
 
+@[grind]
 theorem getElem?_singleton {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a else none := by
   simp [List.getElem?_singleton]
 
 /-! ### mem -/
 
-@[simp] theorem getElem_mem {xs : Vector α n} {i : Nat} (h : i < n) : xs[i] ∈ xs := by
+@[simp, grind] theorem getElem_mem {xs : Vector α n} {i : Nat} (h : i < n) : xs[i] ∈ xs := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
@@ -900,7 +907,10 @@ theorem getElem?_singleton {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a
   rcases xs with ⟨xs, rfl⟩
   simp
 
-theorem mem_push_self {xs : Vector α n} {x : α} : x ∈ xs.push x :=
+@[grind] theorem mem_or_eq_of_mem_push {a b : α} {xs : Vector α n} :
+    a ∈ xs.push b → a ∈ xs ∨ a = b := Vector.mem_push.mp
+
+@[grind] theorem mem_push_self {xs : Vector α n} {x : α} : x ∈ xs.push x :=
   mem_push.2 (Or.inr rfl)
 
 theorem eq_push_append_of_mem {xs : Vector α n} {x : α} (h : x ∈ xs) :
@@ -912,7 +922,7 @@ theorem eq_push_append_of_mem {xs : Vector α n} {x : α} (h : x ∈ xs) :
   obtain rfl := h
   exact ⟨_, _, as.toVector, bs.toVector, by simp, by simp, by simpa using w⟩
 
-theorem mem_push_of_mem {xs : Vector α n} {x : α} (y : α) (h : x ∈ xs) : x ∈ xs.push y :=
+@[grind] theorem mem_push_of_mem {xs : Vector α n} {x : α} (y : α) (h : x ∈ xs) : x ∈ xs.push y :=
   mem_push.2 (Or.inl h)
 
 theorem exists_mem_of_size_pos {xs : Vector α n} (h : 0 < n) : ∃ x, x ∈ xs := by
@@ -1198,7 +1208,9 @@ theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
 instance [BEq α] [LawfulBEq α] (a : α) (as : Vector α n) : Decidable (a ∈ as) :=
   decidable_of_decidable_of_iff contains_iff
 
-@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
+@[grind] theorem contains_empty [BEq α] : (#v[] : Vector α 0).contains a = false := rfl
+
+@[simp, grind] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
     as.contains a = decide (a ∈ as) := by
   rw [Bool.eq_iff_iff, contains_iff, decide_eq_true_iff]
 
@@ -1219,7 +1231,7 @@ instance [BEq α] [LawfulBEq α] (a : α) (as : Vector α n) : Decidable (a ∈
 
 /-! ### set -/
 
-theorem getElem_set {xs : Vector α n} {i : Nat} {x : α} (hi : i < n) {j : Nat} (hj : j < n) :
+@[grind] theorem getElem_set {xs : Vector α n} {i : Nat} {x : α} (hi : i < n) {j : Nat} (hj : j < n) :
     (xs.set i x hi)[j] = if i = j then x else xs[j] := by
   cases xs
   split <;> simp_all [Array.getElem_set]
@@ -1233,7 +1245,7 @@ abbrev getElem_set_eq := @getElem_set_self
 @[simp] theorem getElem_set_ne {xs : Vector α n} {x : α} (hi : i < n) (hj : j < n) (h : i ≠ j) :
     (xs.set i x hi)[j] = xs[j] := by simp [getElem_set, h]
 
-theorem getElem?_set {xs : Vector α n} {x : α} (hi : i < n) :
+@[grind] theorem getElem?_set {xs : Vector α n} {x : α} (hi : i < n) :
     (xs.set i x hi)[j]? = if i = j then some x else xs[j]? := by
   cases xs
   split <;> simp_all [getElem?_eq_getElem, getElem_set]
@@ -1250,6 +1262,12 @@ theorem getElem?_set {xs : Vector α n} {x : α} (hi : i < n) :
   cases xs
   simp
 
+theorem set_push {xs : Vector α n} {x y : α} {h} :
+    (xs.push x).set i y = if _ : i < n then (xs.set i y).push x else xs.push y := by
+  rcases xs with ⟨xs, rfl⟩
+  simp only [push_mk, set_mk, Array.set_push]
+  split <;> simp
+
 theorem set_comm (a b : α) {xs : Vector α n} {hi : i < n} {hj : j < n} (h : i ≠ j) :
     (xs.set i a hi).set j b hj = (xs.set j b hj).set i a hi := by
   cases xs
@@ -1264,13 +1282,17 @@ theorem mem_set {xs : Vector α n} {i : Nat} {a : α} (hi : i < n) : a ∈ xs.se
   simp [mem_iff_getElem]
   exact ⟨i, (by simpa using hi), by simp⟩
 
+@[grind →]
 theorem mem_or_eq_of_mem_set {xs : Vector α n} {i : Nat} {a b : α} {hi : i < n} (h : a ∈ xs.set i b) : a ∈ xs ∨ a = b := by
   cases xs
   simpa using Array.mem_or_eq_of_mem_set (by simpa using h)
 
 /-! ### setIfInBounds -/
 
-theorem getElem_setIfInBounds {xs : Vector α n} {x : α} (hj : j < n) :
+@[simp, grind] theorem setIfInBounds_empty {i : Nat} {a : α} :
+    #v[].setIfInBounds i a = #v[] := rfl
+
+@[grind] theorem getElem_setIfInBounds {xs : Vector α n} {x : α} (hj : j < n) :
     (xs.setIfInBounds i x)[j] = if i = j then x else xs[j] := by
   cases xs
   split <;> simp_all [Array.getElem_setIfInBounds]
@@ -1284,7 +1306,7 @@ abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
 @[simp] theorem getElem_setIfInBounds_ne {xs : Vector α n} {x : α} (hj : j < n) (h : i ≠ j) :
     (xs.setIfInBounds i x)[j] = xs[j] := by simp [getElem_setIfInBounds, h]
 
-theorem getElem?_setIfInBounds {xs : Vector α n} {x : α} :
+@[grind] theorem getElem?_setIfInBounds {xs : Vector α n} {x : α} :
     (xs.setIfInBounds i x)[j]? = if i = j then if i < n then some x else none else xs[j]? := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.getElem?_setIfInBounds]
@@ -1321,7 +1343,7 @@ theorem mem_setIfInBounds {xs : Vector α n} {a : α} (hi : i < n) :
 
 /-! ### BEq -/
 
-@[simp] theorem push_beq_push [BEq α] {a b : α} {n : Nat} {xs : Vector α n} {ys : Vector α n} :
+@[simp, grind] theorem push_beq_push [BEq α] {a b : α} {n : Nat} {xs : Vector α n} {ys : Vector α n} :
     (xs.push a == ys.push b) = (xs == ys && a == b) := by
   cases xs
   cases ys
@@ -1384,11 +1406,16 @@ abbrev mkVector_beq_mkVector := @replicate_beq_replicate
 
 /-! ### back -/
 
+@[grind] theorem back_singleton {a : α} : #v[a].back = a := by simp
+
+@[grind]
 theorem back_eq_getElem [NeZero n] {xs : Vector α n} : xs.back = xs[n - 1]'(by have := NeZero.ne n; omega) := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.back_eq_getElem]
 
-theorem back?_eq_getElem? {xs : Vector α n} : xs.back? = xs[n - 1]? := by
+@[grind] theorem back?_empty : (#v[] : Vector α 0).back? = none := by simp
+
+@[grind] theorem back?_eq_getElem? {xs : Vector α n} : xs.back? = xs[n - 1]? := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.back?_eq_getElem?]
 
@@ -1399,23 +1426,23 @@ theorem back?_eq_getElem? {xs : Vector α n} : xs.back? = xs[n - 1]? := by
 /-! ### map -/
 
 -- The argument `f : α → β` is explicit, to facilitate rewriting from right to left.
-@[simp] theorem getElem_map (f : α → β) {xs : Vector α n} (hi : i < n) :
+@[simp, grind] theorem getElem_map (f : α → β) {xs : Vector α n} (hi : i < n) :
     (xs.map f)[i] = f xs[i] := by
   cases xs
   simp
 
-@[simp] theorem getElem?_map {f : α → β} {xs : Vector α n} {i : Nat}:
+@[simp, grind] theorem getElem?_map {f : α → β} {xs : Vector α n} {i : Nat}:
     (xs.map f)[i]? = xs[i]?.map f := by
   cases xs
   simp
 
 /-- The empty vector maps to the empty vector. -/
-@[simp]
+@[simp, grind]
 theorem map_empty {f : α → β} : map f #v[] = #v[] := by
   rw [map, mk.injEq]
   exact Array.map_empty
 
-@[simp] theorem map_push {f : α → β} {as : Vector α n} {x : α} :
+@[simp, grind] theorem map_push {f : α → β} {as : Vector α n} {x : α} :
     (as.push x).map f = (as.map f).push (f x) := by
   cases as
   simp
@@ -1527,7 +1554,7 @@ theorem map_eq_iff {f : α → β} {as : Vector α n} {bs : Vector β n} :
   cases xs
   simp
 
-@[simp] theorem back?_map {f : α → β} {xs : Vector α n} : (xs.map f).back? = xs.back?.map f := by
+@[simp, grind _=_] theorem back?_map {f : α → β} {xs : Vector α n} : (xs.map f).back? = xs.back?.map f := by
   cases xs
   simp
 
@@ -1576,7 +1603,13 @@ theorem vector₃_induction (P : Vector (Vector (Vector α n) m) k → Prop)
 
 /-! ### append -/
 
-@[simp] theorem append_push {as : Vector α n} {bs : Vector α m} {a : α} :
+@[simp, grind _=_] theorem push_append {as : Vector α n} {bs : Vector α m} {a : α} :
+    (as ++ bs).push a = as ++ bs.push a := by
+  cases as
+  cases bs
+  simp
+
+theorem append_push {as : Vector α n} {bs : Vector α m} {a : α} :
     as ++ bs.push a = (as ++ bs).push a := by
   cases as
   cases bs
@@ -1584,16 +1617,16 @@ theorem vector₃_induction (P : Vector (Vector (Vector α n) m) k → Prop)
 
 theorem singleton_eq_toVector_singleton {a : α} : #v[a] = #[a].toVector := rfl
 
-@[simp] theorem mem_append {a : α} {xs : Vector α n} {ys : Vector α m} :
+@[simp, grind] theorem mem_append {a : α} {xs : Vector α n} {ys : Vector α m} :
     a ∈ xs ++ ys ↔ a ∈ xs ∨ a ∈ ys := by
   cases xs
   cases ys
   simp
 
-theorem mem_append_left {a : α} {xs : Vector α n} (ys : Vector α m) (h : a ∈ xs) : a ∈ xs ++ ys :=
+@[grind] theorem mem_append_left {a : α} {xs : Vector α n} (ys : Vector α m) (h : a ∈ xs) : a ∈ xs ++ ys :=
   mem_append.2 (Or.inl h)
 
-theorem mem_append_right {a : α} (xs : Vector α n) {ys : Vector α m} (h : a ∈ ys) : a ∈ xs ++ ys :=
+@[grind] theorem mem_append_right {a : α} (xs : Vector α n) {ys : Vector α m} (h : a ∈ ys) : a ∈ xs ++ ys :=
   mem_append.2 (Or.inr h)
 
 theorem not_mem_append {a : α} {xs : Vector α n} {ys : Vector α m} (h₁ : a ∉ xs) (h₂ : a ∉ ys) :
@@ -1620,13 +1653,16 @@ theorem forall_mem_append {p : α → Prop} {xs : Vector α n} {ys : Vector α m
     (∀ (x) (_ : x ∈ xs ++ ys), p x) ↔ (∀ (x) (_ : x ∈ xs), p x) ∧ (∀ (x) (_ : x ∈ ys), p x) := by
   simp only [mem_append, or_imp, forall_and]
 
+@[grind]
 theorem empty_append {xs : Vector α n} : (#v[] : Vector α 0) ++ xs = xs.cast (by omega) := by
   rcases xs with ⟨as, rfl⟩
   simp
 
+@[grind]
 theorem append_empty {xs : Vector α n} : xs ++ (#v[] : Vector α 0) = xs := by
   rw [← toArray_inj, toArray_append, Array.append_empty]
 
+@[grind]
 theorem getElem_append {xs : Vector α n} {ys : Vector α m} (hi : i < n + m) :
     (xs ++ ys)[i] = if h : i < n then xs[i] else ys[i - n] := by
   rcases xs with ⟨xs, rfl⟩
@@ -1653,6 +1689,7 @@ theorem getElem?_append_right {xs : Vector α n} {ys : Vector α m} (h : n ≤ i
   rcases ys with ⟨ys, rfl⟩
   simp [Array.getElem?_append_right, h]
 
+@[grind]
 theorem getElem?_append {xs : Vector α n} {ys : Vector α m} {i : Nat} :
     (xs ++ ys)[i]? = if i < n then xs[i]? else ys[i - n]? := by
   split <;> rename_i h
@@ -1731,7 +1768,22 @@ theorem append_eq_append_iff {ws : Vector α n} {xs : Vector α m} {ys : Vector
       right
       refine ⟨cs.toArray, ha, rfl⟩
 
-theorem set_append {xs : Vector α n} {ys : Vector α m} {i : Nat} {x : α} (h : i < n + m) :
+@[simp, grind] theorem append_assoc {xs : Vector α n} {ys : Vector α m} {zs : Vector α k} :
+    (xs ++ ys) ++ zs = (xs ++ (ys ++ zs)).cast (by omega) := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  rcases zs with ⟨zs, rfl⟩
+  simp [Array.append_assoc]
+
+-- Variant for rewriting the other direction: we can't use `append_assoc` as it has a `cast` on the right-hand side.
+@[grind] theorem append_assoc_symm {xs : Vector α n} {ys : Vector α m} {zs : Vector α k} :
+    xs ++ (ys ++ zs) = ((xs ++ ys) ++ zs).cast (by omega) := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  rcases zs with ⟨zs, rfl⟩
+  simp [Array.append_assoc]
+
+@[grind] theorem set_append {xs : Vector α n} {ys : Vector α m} {i : Nat} {x : α} (h : i < n + m) :
     (xs ++ ys).set i x =
       if h' : i < n then
         xs.set i x ++ ys
@@ -1751,7 +1803,7 @@ theorem set_append {xs : Vector α n} {ys : Vector α m} {i : Nat} {x : α} (h :
     (xs ++ ys).set i x = xs ++ ys.set (i - n) x := by
   rw [set_append, dif_neg (by omega)]
 
-theorem setIfInBounds_append {xs : Vector α n} {ys : Vector α m} {i : Nat} {x : α} :
+@[grind] theorem setIfInBounds_append {xs : Vector α n} {ys : Vector α m} {i : Nat} {x : α} :
     (xs ++ ys).setIfInBounds i x =
       if i < n then
         xs.setIfInBounds i x ++ ys
@@ -1771,7 +1823,7 @@ theorem setIfInBounds_append {xs : Vector α n} {ys : Vector α m} {i : Nat} {x
     (xs ++ ys).setIfInBounds i x = xs ++ ys.setIfInBounds (i - n) x := by
   rw [setIfInBounds_append, if_neg (by omega)]
 
-@[simp] theorem map_append {f : α → β} {xs : Vector α n} {ys : Vector α m} :
+@[simp, grind] theorem map_append {f : α → β} {xs : Vector α n} {ys : Vector α m} :
     map f (xs ++ ys) = map f xs ++ map f ys := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
@@ -1840,7 +1892,7 @@ theorem getElem?_flatten {xss : Vector (Vector β m) n} {i : Nat} :
         none := by
   simp [getElem?_def]
 
-@[simp] theorem flatten_singleton {xs : Vector α n} : #v[xs].flatten = xs.cast (by simp) := by
+@[simp, grind] theorem flatten_singleton {xs : Vector α n} : #v[xs].flatten = xs.cast (by simp) := by
   simp [flatten]
 
 set_option linter.listVariables false in
@@ -1862,18 +1914,22 @@ theorem forall_mem_flatten {p : α → Prop} {xss : Vector (Vector α n) m} :
   simp only [mem_flatten, forall_exists_index, and_imp]
   constructor <;> (intros; solve_by_elim)
 
-@[simp] theorem map_flatten {f : α → β} {xss : Vector (Vector α n) m} :
+@[simp, grind _=_] theorem map_flatten {f : α → β} {xss : Vector (Vector α n) m} :
     (flatten xss).map f = (map (map f) xss).flatten := by
   induction xss using vector₂_induction with
   | of xss h₁ h₂ => simp
 
-@[simp] theorem flatten_append {xss₁ : Vector (Vector α n) m₁} {xss₂ : Vector (Vector α n) m₂} :
+@[simp, grind] theorem flatten_append {xss₁ : Vector (Vector α n) m₁} {xss₂ : Vector (Vector α n) m₂} :
     flatten (xss₁ ++ xss₂) = (flatten xss₁ ++ flatten xss₂).cast (by simp [Nat.add_mul]) := by
   induction xss₁ using vector₂_induction
   induction xss₂ using vector₂_induction
   simp
 
-theorem flatten_push {xss : Vector (Vector α n) m} {xs : Vector α n} :
+@[grind] theorem append_flatten {xss₁ : Vector (Vector α n) m₁} {xss₂ : Vector (Vector α n) m₂} :
+    flatten xss₁ ++ flatten xss₂ = (flatten (xss₁ ++ xss₂)).cast (by simp [Nat.add_mul]) := by
+  simp
+
+@[grind] theorem flatten_push {xss : Vector (Vector α n) m} {xs : Vector α n} :
     flatten (xss.push xs) = (flatten xss ++ xs).cast (by simp [Nat.add_mul]) := by
   induction xss using vector₂_induction
   rcases xs with ⟨xs⟩
@@ -1923,6 +1979,14 @@ theorem flatMap_def {xs : Vector α n} {f : α → Vector β m} : xs.flatMap f =
   rcases xs with ⟨xs, rfl⟩
   simp [Array.flatMap_def, Function.comp_def]
 
+@[simp, grind] theorem flatMap_empty {f : α → Vector β m} :
+    (#v[] : Vector α 0).flatMap f = #v[].cast (by simp) := rfl
+
+@[simp, grind] theorem flatMap_push {xs : Vector α n} {x : α} {f : α → Vector β m} :
+    (xs.push x).flatMap f = (xs.flatMap f ++ f x).cast (by simp [Nat.add_mul]) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp
+
 @[simp] theorem getElem_flatMap {xs : Vector α n} {f : α → Vector β m} {i : Nat} (hi : i < n * m) :
     (xs.flatMap f)[i] =
       haveI : i / m < n := by rwa [Nat.div_lt_iff_lt_mul (Nat.pos_of_lt_mul_left hi)]
@@ -1944,7 +2008,7 @@ theorem getElem?_flatMap {xs : Vector α n} {f : α → Vector β m} {i : Nat} :
 
 @[simp] theorem flatMap_id' {xss : Vector (Vector α m) n} : xss.flatMap (fun xs => xs) = xss.flatten := by simp [flatMap_def]
 
-@[simp] theorem mem_flatMap {f : α → Vector β m} {b} {xs : Vector α n} : b ∈ xs.flatMap f ↔ ∃ a, a ∈ xs ∧ b ∈ f a := by
+@[simp, grind] theorem mem_flatMap {f : α → Vector β m} {b} {xs : Vector α n} : b ∈ xs.flatMap f ↔ ∃ a, a ∈ xs ∧ b ∈ f a := by
   simp [flatMap_def, mem_flatten]
   exact ⟨fun ⟨_, ⟨a, h₁, rfl⟩, h₂⟩ => ⟨a, h₁, h₂⟩, fun ⟨a, h₁, h₂⟩ => ⟨_, ⟨a, h₁, rfl⟩, h₂⟩⟩
 
@@ -2007,7 +2071,7 @@ theorem replicate_succ' : replicate (n + 1) a = (#v[a] ++ replicate n a).cast (b
 @[deprecated replicate_succ' (since := "2025-03-18")]
 abbrev mkVector_succ' := @replicate_succ'
 
-@[simp] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
+@[simp, grind] theorem mem_replicate {a b : α} {n} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a := by
   unfold replicate
   simp only [mem_mk]
   simp
@@ -2015,7 +2079,7 @@ abbrev mkVector_succ' := @replicate_succ'
 @[deprecated mem_replicate (since := "2025-03-18")]
 abbrev mem_mkVector := @mem_replicate
 
-theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
+@[grind →] theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
 
 @[deprecated eq_of_mem_replicate (since := "2025-03-18")]
 abbrev eq_of_mem_mkVector := @eq_of_mem_replicate
@@ -2027,14 +2091,14 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
 @[deprecated forall_mem_replicate (since := "2025-03-18")]
 abbrev forall_mem_mkVector := @forall_mem_replicate
 
-@[simp] theorem getElem_replicate {a : α} (h : i < n) : (replicate n a)[i] = a := by
+@[simp, grind] theorem getElem_replicate {a : α} (h : i < n) : (replicate n a)[i] = a := by
   rw [replicate_eq_mk_replicate, getElem_mk]
   simp
 
 @[deprecated getElem_replicate (since := "2025-03-18")]
 abbrev getElem_mkVector := @getElem_replicate
 
-theorem getElem?_replicate {a : α} {n i : Nat} : (replicate n a)[i]? = if i < n then some a else none := by
+@[grind]theorem getElem?_replicate {a : α} {n i : Nat} : (replicate n a)[i]? = if i < n then some a else none := by
   simp [getElem?_def]
 
 @[deprecated getElem?_replicate (since := "2025-03-18")]
@@ -2158,12 +2222,14 @@ abbrev sum_mkVector := @sum_replicate_nat
 
 /-! ### reverse -/
 
-@[simp] theorem reverse_push {as : Vector α n} {a : α} :
+theorem reverse_empty : reverse (#v[] : Vector α 0) = #v[] := rfl
+
+@[simp, grind] theorem reverse_push {as : Vector α n} {a : α} :
     (as.push a).reverse = (#v[a] ++ as.reverse).cast (by omega) := by
   rcases as with ⟨as, rfl⟩
   simp [Array.reverse_push]
 
-@[simp] theorem mem_reverse {x : α} {as : Vector α n} : x ∈ as.reverse ↔ x ∈ as := by
+@[simp, grind] theorem mem_reverse {x : α} {as : Vector α n} : x ∈ as.reverse ↔ x ∈ as := by
   cases as
   simp
 
@@ -2171,7 +2237,7 @@ abbrev sum_mkVector := @sum_replicate_nat
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem getElem_reverse {xs : Vector α n} {i : Nat} (hi : i < n) :
+@[simp, grind] theorem getElem_reverse {xs : Vector α n} {i : Nat} (hi : i < n) :
     (xs.reverse)[i] = xs[n - 1 - i] := by
   rcases xs with ⟨xs, rfl⟩
   simp
@@ -2187,14 +2253,14 @@ theorem getElem?_reverse' {xs : Vector α n} {i j : Nat} (h : i + j + 1 = n) : x
   rcases xs with ⟨xs, rfl⟩
   simpa using Array.getElem?_reverse' h
 
-@[simp]
+@[simp, grind]
 theorem getElem?_reverse {xs : Vector α n} {i} (h : i < n) :
     xs.reverse[i]? = xs[n - 1 - i]? := by
   cases xs
   simp_all
 
 -- The argument `xs : Vector α n` is explicit so we can rewrite from right to left.
-@[simp] theorem reverse_reverse (xs : Vector α n) : xs.reverse.reverse = xs := by
+@[simp, grind] theorem reverse_reverse (xs : Vector α n) : xs.reverse.reverse = xs := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.reverse_reverse]
 
@@ -2214,12 +2280,18 @@ theorem reverse_eq_iff {xs ys : Vector α n} : xs.reverse = ys ↔ xs = ys.rever
   rcases xs with ⟨xs, rfl⟩
   simp [Array.map_reverse]
 
-@[simp] theorem reverse_append {xs : Vector α n} {ys : Vector α m} :
+@[simp, grind] theorem reverse_append {xs : Vector α n} {ys : Vector α m} :
     (xs ++ ys).reverse = (ys.reverse ++ xs.reverse).cast (by omega) := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
   simp [Array.reverse_append]
 
+@[grind] theorem append_reverse {xs : Vector α n} {ys : Vector α m} :
+    ys.reverse ++ xs.reverse = (xs ++ ys).reverse.cast (by omega) := by
+  rcases xs with ⟨xs, rfl⟩
+  rcases ys with ⟨ys, rfl⟩
+  simp [Array.reverse_append]
+
 @[simp] theorem reverse_eq_append_iff {xs : Vector α (n + m)} {ys : Vector α n} {zs : Vector α m} :
     xs.reverse = ys ++ zs ↔ xs = (zs.reverse ++ ys.reverse).cast (by omega) := by
   cases xs
@@ -2249,7 +2321,7 @@ theorem flatMap_reverse {xs : Vector α n} {f : α → Vector β m} :
   rcases xs with ⟨xs, rfl⟩
   simp [Array.flatMap_reverse, Function.comp_def]
 
-@[simp] theorem reverse_replicate {n : Nat} {a : α} : reverse (replicate n a) = replicate n a := by
+@[simp, grind] theorem reverse_replicate {n : Nat} {a : α} : reverse (replicate n a) = replicate n a := by
   rw [← toArray_inj]
   simp
 
@@ -2274,7 +2346,7 @@ set_option linter.indexVariables false in
   rcases as with ⟨as, rfl⟩
   simp
 
-theorem extract_empty {start stop : Nat} :
+@[grind] theorem extract_empty {start stop : Nat} :
     (#v[] : Vector α 0).extract start stop = #v[].cast (by simp) := by
   simp
 
@@ -2290,11 +2362,11 @@ theorem extract_empty {start stop : Nat} :
     foldlM f init #v[] = return init := by
   simp [foldlM]
 
-@[simp] theorem foldrM_empty [Monad m] {f : α → β → m β} {init : β} :
+@[simp, grind] theorem foldrM_empty [Monad m] {f : α → β → m β} {init : β} :
     foldrM f init #v[] = return init := by
   simp [foldrM]
 
-@[simp] theorem foldlM_push [Monad m] [LawfulMonad m] {xs : Vector α n} {a : α} {f : β → α → m β} {b} :
+@[simp, grind] theorem foldlM_push [Monad m] [LawfulMonad m] {xs : Vector α n} {a : α} {f : β → α → m β} {b} :
     (xs.push a).foldlM f b = xs.foldlM f b >>= fun b => f b a := by
   rcases xs with ⟨xs, rfl⟩
   simp
@@ -2335,13 +2407,17 @@ theorem foldr_eq_foldrM {f : α → β → β} {b} {xs : Vector α n} :
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem foldrM_push [Monad m] {f : α → β → m β} {init : β} {xs : Vector α n} {a : α} :
+@[simp, grind] theorem foldrM_push [Monad m] {f : α → β → m β} {init : β} {xs : Vector α n} {a : α} :
     (xs.push a).foldrM f init = f a init >>= xs.foldrM f := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.foldrM_push]
 
 /-! ### foldl / foldr -/
 
+@[grind] theorem foldl_empty {f : β → α → β} {init : β} : (#v[].foldl f init) = init := rfl
+
+@[grind] theorem foldr_empty {f : α → β → β} {init : β} : (#v[].foldr f init) = init := rfl
+
 @[congr]
 theorem foldl_congr {xs ys : Vector α n} (h₀ : xs = ys) {f g : β → α → β} (h₁ : f = g)
      {a b : β} (h₂ : a = b) :
@@ -2354,7 +2430,12 @@ theorem foldr_congr {xs ys : Vector α n} (h₀ : xs = ys) {f g : α → β →
     xs.foldr f a = ys.foldr g b := by
   congr
 
-@[simp] theorem foldr_push {f : α → β → β} {init : β} {xs : Vector α n} {a : α} :
+@[simp, grind] theorem foldl_push {f : β → α → β} {init : β} {xs : Vector α n} {a : α} :
+    (xs.push a).foldl f init = f (xs.foldl f init) a := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.foldl_push]
+
+@[simp, grind] theorem foldr_push {f : α → β → β} {init : β} {xs : Vector α n} {a : α} :
     (xs.push a).foldr f init = xs.foldr f (f a init) := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.foldr_push]
@@ -2398,26 +2479,26 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
   rcases ys with ⟨ys, rfl⟩
   simp
 
-@[simp] theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs : Vector α n} {ys : Vector α k} :
+@[simp, grind _=_] theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs : Vector α n} {ys : Vector α k} :
     (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := by simp [foldl_eq_foldlM]
 
-@[simp] theorem foldr_append {f : α → β → β} {b} {xs : Vector α n} {ys : Vector α k} :
+@[simp, grind _=_] theorem foldr_append {f : α → β → β} {b} {xs : Vector α n} {ys : Vector α k} :
     (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := by simp [foldr_eq_foldrM]
 
-@[simp] theorem foldl_flatten {f : β → α → β} {b} {xss : Vector (Vector α m) n} :
+@[simp, grind] theorem foldl_flatten {f : β → α → β} {b} {xss : Vector (Vector α m) n} :
     (flatten xss).foldl f b = xss.foldl (fun b xs => xs.foldl f b) b := by
   cases xss using vector₂_induction
   simp [Array.foldl_flatten', Array.foldl_map']
 
-@[simp] theorem foldr_flatten {f : α → β → β} {b} {xss : Vector (Vector α m) n} :
+@[simp, grind] theorem foldr_flatten {f : α → β → β} {b} {xss : Vector (Vector α m) n} :
     (flatten xss).foldr f b = xss.foldr (fun xs b => xs.foldr f b) b := by
   cases xss using vector₂_induction
   simp [Array.foldr_flatten', Array.foldr_map']
 
-@[simp] theorem foldl_reverse {xs : Vector α n} {f : β → α → β} {b} :
+@[simp, grind] theorem foldl_reverse {xs : Vector α n} {f : β → α → β} {b} :
     xs.reverse.foldl f b = xs.foldr (fun x y => f y x) b := by simp [foldl_eq_foldlM, foldr_eq_foldrM]
 
-@[simp] theorem foldr_reverse {xs : Vector α n} {f : α → β → β} {b} :
+@[simp, grind] theorem foldr_reverse {xs : Vector α n} {f : α → β → β} {b} :
     xs.reverse.foldr f b = xs.foldl (fun x y => f y x) b :=
   (foldl_reverse ..).symm.trans <| by simp
 
@@ -2511,7 +2592,7 @@ theorem back?_eq_some_iff {xs : Vector α n} {a : α} :
   simp only [mk_append_mk, back_mk]
   rw [Array.back_append_of_size_pos]
 
-theorem back_append {xs : Vector α n} {ys : Vector α m} [NeZero (n + m)] :
+@[grind] theorem back_append {xs : Vector α n} {ys : Vector α m} [NeZero (n + m)] :
     (xs ++ ys).back =
       if h' : m = 0 then
         have : NeZero n := by subst h'; simp_all
@@ -2542,7 +2623,7 @@ theorem back_append_left {xs : Vector α n} {ys : Vector α 0} [NeZero n] :
   simp only [mk_append_mk, back_mk]
   rw [Array.back_append_left _ h]
 
-@[simp] theorem back?_append {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).back? = ys.back?.or xs.back? := by
+@[simp, grind] theorem back?_append {xs : Vector α n} {ys : Vector α m} : (xs ++ ys).back? = ys.back?.or xs.back? := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
   simp
@@ -2604,7 +2685,7 @@ theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Vector α n} {a : α} :
 
 @[simp] theorem pop_push {xs : Vector α n} {x : α} : (xs.push x).pop = xs := by simp [pop]
 
-@[simp] theorem getElem_pop {xs : Vector α n} {i : Nat} (h : i < n - 1) :
+@[simp, grind] theorem getElem_pop {xs : Vector α n} {i : Nat} (h : i < n - 1) :
     xs.pop[i] = xs[i] := by
   rcases xs with ⟨xs, rfl⟩
   simp
@@ -2617,7 +2698,7 @@ defeq issues in the implicit size argument.
     @getElem (Vector α n) Nat α (fun _ i => i < n) instGetElemNatLt xs.pop i h = xs[i] :=
   getElem_pop h
 
-theorem getElem?_pop {xs : Vector α n} {i : Nat} :
+@[grind] theorem getElem?_pop {xs : Vector α n} {i : Nat} :
     xs.pop[i]? = if i < n - 1 then xs[i]? else none := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.getElem?_pop]
@@ -2666,6 +2747,11 @@ variable [BEq α]
   rcases xs with ⟨xs, rfl⟩
   simp
 
+@[simp, grind] theorem replace_empty : (#v[] : Vector α 0).replace a b = #v[] := by rfl
+
+@[grind] theorem replace_singleton {a b c : α} : #v[a].replace b c = #v[if a == b then c else a] := by
+  simp
+
 -- This hypothesis could probably be dropped from some of the lemmas below,
 -- by proving them direct from the definition rather than going via `List`.
 variable [LawfulBEq α]
@@ -2674,7 +2760,7 @@ variable [LawfulBEq α]
   rcases xs with ⟨xs, rfl⟩
   simp_all
 
-theorem getElem?_replace {xs : Vector α n} {i : Nat} :
+@[grind] theorem getElem?_replace {xs : Vector α n} {i : Nat} :
     (xs.replace a b)[i]? = if xs[i]? == some a then if a ∈ xs.take i then some a else some b else xs[i]? := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.getElem?_replace, -beq_iff_eq]
@@ -2683,7 +2769,7 @@ theorem getElem?_replace_of_ne {xs : Vector α n} {i : Nat} (h : xs[i]? ≠ some
     (xs.replace a b)[i]? = xs[i]? := by
   simp_all [getElem?_replace]
 
-theorem getElem_replace {xs : Vector α n} {i : Nat} (h : i < n) :
+@[grind] theorem getElem_replace {xs : Vector α n} {i : Nat} (h : i < n) :
     (xs.replace a b)[i] = if xs[i] == a then if a ∈ xs.take i then a else b else xs[i] := by
   apply Option.some.inj
   rw [← getElem?_eq_getElem, getElem?_replace]
@@ -2694,7 +2780,7 @@ theorem getElem_replace_of_ne {xs : Vector α n} {i : Nat} {h : i < n} (h' : xs[
   rw [getElem_replace h]
   simp [h']
 
-theorem replace_append {xs : Vector α n} {ys : Vector α m} :
+@[grind] theorem replace_append {xs : Vector α n} {ys : Vector α m} :
     (xs ++ ys).replace a b = if a ∈ xs then xs.replace a b ++ ys else xs ++ ys.replace a b := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
@@ -2709,6 +2795,12 @@ theorem replace_append_right {xs : Vector α n} {ys : Vector α m} (h : ¬ a ∈
     (xs ++ ys).replace a b = xs ++ ys.replace a b := by
   simp [replace_append, h]
 
+@[grind] theorem replace_push {xs : Vector α n} {a b c : α} :
+    (xs.push a).replace b c = if b ∈ xs then (xs.replace b c).push a else xs.push (if b == a then c else a) := by
+  rcases xs with ⟨xs, rfl⟩
+  simp only [push_mk, replace_mk, Array.replace_push, mem_mk]
+  split <;> simp
+
 theorem replace_extract {xs : Vector α n} {i : Nat} :
     (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i := by
   rcases xs with ⟨xs, rfl⟩
@@ -2797,13 +2889,13 @@ theorem any_eq_not_all_not {xs : Vector α n} {p : α → Bool} : xs.any p = !xs
   simp
   rfl
 
-@[simp] theorem any_append {xs : Vector α n} {ys : Vector α m} :
+@[simp, grind _=_] theorem any_append {xs : Vector α n} {ys : Vector α m} :
     (xs ++ ys).any f = (xs.any f || ys.any f) := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
   simp
 
-@[simp] theorem all_append {xs : Vector α n} {ys : Vector α m} :
+@[simp, grind _=_] theorem all_append {xs : Vector α n} {ys : Vector α m} :
     (xs ++ ys).all f = (xs.all f && ys.all f) := by
   rcases xs with ⟨xs, rfl⟩
   rcases ys with ⟨ys, rfl⟩
@@ -2837,15 +2929,15 @@ theorem any_eq_not_all_not {xs : Vector α n} {p : α → Bool} : xs.any p = !xs
   unfold all
   apply allM_congr w h
 
-@[simp] theorem any_flatten {xss : Vector (Vector α n) m} : xss.flatten.any f = xss.any (any · f) := by
+@[simp, grind] theorem any_flatten {xss : Vector (Vector α n) m} : xss.flatten.any f = xss.any (any · f) := by
   cases xss using vector₂_induction
   simp
 
-@[simp] theorem all_flatten {xss : Vector (Vector α n) m} : xss.flatten.all f = xss.all (all · f) := by
+@[simp, grind] theorem all_flatten {xss : Vector (Vector α n) m} : xss.flatten.all f = xss.all (all · f) := by
   cases xss using vector₂_induction
   simp
 
-@[simp] theorem any_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
+@[simp, grind] theorem any_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
     (xs.flatMap f).any p = xs.any fun a => (f a).any p := by
   rcases xs with ⟨xs⟩
   simp only [flatMap_mk, any_mk, Array.size_flatMap, size_toArray, Array.any_flatMap']
@@ -2854,7 +2946,7 @@ theorem any_eq_not_all_not {xs : Vector α n} {p : α → Bool} : xs.any p = !xs
   congr
   simp [Vector.size_toArray]
 
-@[simp] theorem all_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
+@[simp, grind] theorem all_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
     (xs.flatMap f).all p = xs.all fun a => (f a).all p := by
   rcases xs with ⟨xs⟩
   simp only [flatMap_mk, all_mk, Array.size_flatMap, size_toArray, Array.all_flatMap']
@@ -2863,11 +2955,11 @@ theorem any_eq_not_all_not {xs : Vector α n} {p : α → Bool} : xs.any p = !xs
   congr
   simp [Vector.size_toArray]
 
-@[simp] theorem any_reverse {xs : Vector α n} : xs.reverse.any f  = xs.any f := by
+@[simp, grind] theorem any_reverse {xs : Vector α n} : xs.reverse.any f  = xs.any f := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp] theorem all_reverse {xs : Vector α n} : xs.reverse.all f = xs.all f := by
+@[simp, grind] theorem all_reverse {xs : Vector α n} : xs.reverse.all f = xs.all f := by
   rcases xs with ⟨xs, rfl⟩
   simp
 

src/Init/Ext.lean

@@ -81,6 +81,7 @@ end Lean
 
 attribute [ext] Prod PProd Sigma PSigma
 attribute [ext] funext propext Subtype.eq Array.ext
+attribute [grind ext] Array.ext
 
 @[ext] protected theorem PUnit.ext (x y : PUnit) : x = y := rfl
 protected theorem Unit.ext (x y : Unit) : x = y := rfl

src/Init/GetElem.lean

@@ -246,7 +246,7 @@ theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : g
 theorem getElem_cons_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
   rfl
 
-@[simp] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
+@[simp, grind] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
   | _ :: _, 0, _ => .head ..
   | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
 
@@ -309,6 +309,8 @@ instance : GetElem? (List α) Nat α fun as i => i < as.length where
 
 theorem getElem?_eq_none (h : length l ≤ i) : l[i]? = none := getElem?_eq_none_iff.mpr h
 
+grind_pattern List.getElem?_eq_none => l.length ≤ i, l[i]?
+
 instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where
   getElem?_def as i h := by
     split <;> simp_all

src/Init/Grind/Tactics.lean

@@ -64,7 +64,7 @@ structure Config where
   splitIndPred : Bool := false
   /--
   If `splitImp` is `true`, then given an implication `p → q` or `(h : p) → q h`, `grind` splits on `p`
-  it the implication is true. Otherwise, it will split only if `p` is an arithmetic predicate.
+  if the implication is true. Otherwise, it will split only if `p` is an arithmetic predicate.
   -/
   splitImp : Bool := false
   /-- By default, `grind` halts as soon as it encounters a sub-goal where no further progress can be made. -/

tests/lean/grind/countP.lean

@@ -0,0 +1,22 @@
+variable {α : Type u} {l : List α} {P Q : α → Bool}
+
+attribute [grind] List.countP_nil List.countP_cons
+
+-- It would be really nice if we didn't need to `specialize` here!
+
+theorem List.countP_le_countP (hpq : ∀ x ∈ l, P x → Q x) :
+    l.countP P ≤ l.countP Q := by
+  induction l with
+  | nil => grind
+  | cons x xs ih =>
+    specialize ih (by grind)
+    grind
+
+theorem List.countP_lt_countP (hpq : ∀ x ∈ l, P x → Q x) (y:α) (hx: y ∈ l) (hxP : P y = false) (hxQ : Q y) :
+    l.countP P < l.countP Q := by
+  induction l with
+  | nil => grind
+  | cons x xs ih =>
+    have : xs.countP P ≤ xs.countP Q := countP_le_countP (by grind)
+    specialize ih (by grind)
+    grind

tests/lean/grind/experiments/option.lean

@@ -0,0 +1,36 @@
+/-!
+This file contains WIP notes about potential further `grind` attributes for `Option`.
+
+-/
+
+attribute [grind] Option.some_get Option.get_some
+attribute [grind] Option.map_map -- `[grind _=_]`?
+attribute [grind] Option.get_map -- ??
+attribute [grind] Option.map_id_fun Option.map_id_fun'
+attribute [grind] Option.all_guard Option.any_guard
+attribute [grind] Option.bind_map Option.map_bind
+attribute [grind] Option.join_map_eq_map_join
+attribute [grind] Option.join_join -- `[grind _=_]`?
+attribute [grind] Option.map_orElse
+
+-- Look again at `Option.guard` lemmas, consider `bind_gaurd`.
+-- Fix statement of `isSome_guard`, add `isNone_guard`
+
+attribute [grind] Option.or_assoc -- unless `grind` gains native associativity support in the meantime!
+
+-- attribute [grind] Option.none_beq_none -- warning: this generates just `none` as the pattern!
+-- attribute [grind] Option.none_beq_some
+-- attribute [grind] Option.some_beq_none -- warning: this generates just `some _` as the pattern!
+-- attribute [grind] Option.some_beq_some
+
+attribute [grind] Option.isSome_filter
+attribute [grind] Option.get_filter Option.get_pfilter
+
+attribute [grind] Option.map_pbind Option.pbind_map
+attribute [grind] Option.map_pmap Option.pmap_map Option.elim_pmap
+
+-- Lemmas about inequalities?
+
+-- The `min_none_none` family of lemmas result in grind issues:
+-- failed to synthesize instance when instantiating Option.min_none_none
+--         Min α

tests/lean/grind/mvar.lean

@@ -0,0 +1,14 @@
+open List
+
+-- Failing with:
+-- [issue] unexpected metavariable during internalization
+--       ?α
+--     `grind` is not supposed to be used in goals containing metavariables.
+  -- [issue] type error constructing proof for Array.eq_empty_of_append_eq_empty
+  --     when assigning metavariable ?xs with
+  --       l₁
+  --     has type
+  --       List α : Type u_1
+  --     but is expected to have type
+  --       Array ?α : Type ?u.430
+theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by grind (gen := 6)