finish

src/Init/Data/Array/Find.lean

@@ -38,11 +38,22 @@ theorem findSome?_singleton {a : α} {f : α → Option β} : #[a].findSome? f =
 @[simp] theorem findSomeRev?_push_of_isNone {xs : Array α} (h : (f a).isNone) : (xs.push a).findSomeRev? f = xs.findSomeRev? f := by
   cases xs; simp_all
 
+@[grind =]
+theorem findSomeRev?_push {xs : Array α} {a : α} {f : α → Option β} :
+    (xs.push a).findSomeRev? f = (f a).or (xs.findSomeRev? f) := by
+  match h : f a with
+  | some b =>
+    rw [findSomeRev?_push_of_isSome]
+    all_goals simp_all
+  | none =>
+    rw [findSomeRev?_push_of_isNone]
+    all_goals simp_all
+
 theorem exists_of_findSome?_eq_some {f : α → Option β} {xs : Array α} (w : xs.findSome? f = some b) :
     ∃ a, a ∈ xs ∧ f a = some b := by
   cases xs; simp_all [List.exists_of_findSome?_eq_some]
 
-@[simp] theorem findSome?_eq_none_iff : findSome? p xs = none ↔ ∀ x ∈ xs, p x = none := by
+@[simp, grind =] theorem findSome?_eq_none_iff : findSome? p xs = none ↔ ∀ x ∈ xs, p x = none := by
   cases xs; simp
 
 @[simp] theorem findSome?_isSome_iff {f : α → Option β} {xs : Array α} :
@@ -59,36 +70,39 @@ theorem findSome?_eq_some_iff {f : α → Option β} {xs : Array α} {b : β} :
   · rintro ⟨xs, a, ys, h₀, h₁, h₂⟩
     exact ⟨xs.toList, a, ys.toList, by simpa using congrArg toList h₀, h₁, by simpa⟩
 
-@[simp] theorem findSome?_guard {xs : Array α} : findSome? (Option.guard fun x => p x) xs = find? p xs := by
+@[simp, grind =] theorem findSome?_guard {xs : Array α} : findSome? (Option.guard p) xs = find? p xs := by
   cases xs; simp
 
-theorem find?_eq_findSome?_guard {xs : Array α} : find? p xs = findSome? (Option.guard fun x => p x) xs :=
+theorem find?_eq_findSome?_guard {xs : Array α} : find? p xs = findSome? (Option.guard p) xs :=
   findSome?_guard.symm
 
-@[simp] theorem getElem?_zero_filterMap {f : α → Option β} {xs : Array α} : (xs.filterMap f)[0]? = xs.findSome? f := by
+@[simp, grind =] theorem getElem?_zero_filterMap {f : α → Option β} {xs : Array α} : (xs.filterMap f)[0]? = xs.findSome? f := by
   cases xs; simp [← List.head?_eq_getElem?]
 
-@[simp] theorem getElem_zero_filterMap {f : α → Option β} {xs : Array α} (h) :
+@[simp, grind =] theorem getElem_zero_filterMap {f : α → Option β} {xs : Array α} (h) :
     (xs.filterMap f)[0] = (xs.findSome? f).get (by cases xs; simpa [List.length_filterMap_eq_countP] using h) := by
   cases xs; simp [← List.head_eq_getElem, ← getElem?_zero_filterMap]
 
-@[simp] theorem back?_filterMap {f : α → Option β} {xs : Array α} : (xs.filterMap f).back? = xs.findSomeRev? f := by
+@[simp, grind =] theorem back?_filterMap {f : α → Option β} {xs : Array α} : (xs.filterMap f).back? = xs.findSomeRev? f := by
   cases xs; simp
 
-@[simp] theorem back!_filterMap [Inhabited β] {f : α → Option β} {xs : Array α} :
+@[simp, grind =] theorem back!_filterMap [Inhabited β] {f : α → Option β} {xs : Array α} :
     (xs.filterMap f).back! = (xs.findSomeRev? f).getD default := by
   cases xs; simp
 
-@[simp] theorem map_findSome? {f : α → Option β} {g : β → γ} {xs : Array α} :
+@[simp, grind _=_] theorem map_findSome? {f : α → Option β} {g : β → γ} {xs : Array α} :
     (xs.findSome? f).map g = xs.findSome? (Option.map g ∘ f) := by
   cases xs; simp
 
+@[grind _=_]
 theorem findSome?_map {f : β → γ} {xs : Array β} : findSome? p (xs.map f) = xs.findSome? (p ∘ f) := by
   cases xs; simp [List.findSome?_map]
 
+@[grind =]
 theorem findSome?_append {xs ys : Array α} : (xs ++ ys).findSome? f = (xs.findSome? f).or (ys.findSome? f) := by
   cases xs; cases ys; simp [List.findSome?_append]
 
+@[grind =]
 theorem getElem?_zero_flatten (xss : Array (Array α)) :
     (flatten xss)[0]? = xss.findSome? fun xs => xs[0]? := by
   cases xss using array₂_induction
@@ -104,12 +118,14 @@ theorem getElem_zero_flatten.proof {xss : Array (Array α)} (h : 0 < xss.flatten
   obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h
   exact ⟨xs, m, by simpa using h⟩
 
+@[grind =]
 theorem getElem_zero_flatten {xss : Array (Array α)} (h) :
     (flatten xss)[0] = (xss.findSome? fun xs => xs[0]?).get (getElem_zero_flatten.proof h) := by
   have t := getElem?_zero_flatten xss
   simp [getElem?_eq_getElem, h] at t
   simp [← t]
 
+@[grind =]
 theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   simp [← List.toArray_replicate, List.findSome?_replicate]
 
@@ -140,8 +156,9 @@ abbrev findSome?_mkArray_of_isNone := @findSome?_replicate_of_isNone
 
 /-! ### find? -/
 
-@[simp] theorem find?_empty : find? p #[] = none := rfl
+@[simp, grind =] theorem find?_empty : find? p #[] = none := rfl
 
+@[grind =]
 theorem find?_singleton {a : α} {p : α → Bool} :
     #[a].find? p = if p a then some a else none := by
   simp
@@ -150,11 +167,26 @@ theorem find?_singleton {a : α} {p : α → Bool} :
     findRev? p (xs.push a) = some a := by
   cases xs; simp [h]
 
-@[simp] theorem findRev?_cons_of_neg {xs : Array α} (h : ¬p a) :
+@[simp] theorem findRev?_push_of_neg {xs : Array α} (h : ¬p a) :
     findRev? p (xs.push a) = findRev? p xs := by
   cases xs; simp [h]
 
-@[simp] theorem find?_eq_none : find? p xs = none ↔ ∀ x ∈ xs, ¬ p x := by
+@[deprecated findRev?_push_of_neg (since := "2025-06-12")]
+abbrev findRev?_cons_of_neg := @findRev?_push_of_neg
+
+@[grind =]
+theorem finRev?_push {xs : Array α} :
+    findRev? p (xs.push a) = (Option.guard p a).or (xs.findRev? p) := by
+  cases h : p a
+  · rw [findRev?_push_of_neg, Option.guard_eq_none_iff.mpr h]
+    all_goals simp [h]
+  · rw [findRev?_push_of_pos, Option.guard_eq_some_iff.mpr ⟨rfl, h⟩]
+    all_goals simp [h]
+
+@[deprecated finRev?_push (since := "2025-06-12")]
+abbrev findRev?_cons := @finRev?_push
+
+@[simp, grind =] theorem find?_eq_none : find? p xs = none ↔ ∀ x ∈ xs, ¬ p x := by
   cases xs; simp
 
 theorem find?_eq_some_iff_append {xs : Array α} :
@@ -178,60 +210,63 @@ theorem find?_push_eq_some {xs : Array α} :
     (xs.push a).find? p = some b ↔ xs.find? p = some b ∨ (xs.find? p = none ∧ (p a ∧ a = b)) := by
   cases xs; simp
 
-@[simp] theorem find?_isSome {xs : Array α} {p : α → Bool} : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x := by
+@[simp, grind =] theorem find?_isSome {xs : Array α} {p : α → Bool} : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x := by
   cases xs; simp
 
+@[grind →]
 theorem find?_some {xs : Array α} (h : find? p xs = some a) : p a := by
   cases xs
   simp at h
   exact List.find?_some h
 
+@[grind →]
 theorem mem_of_find?_eq_some {xs : Array α} (h : find? p xs = some a) : a ∈ xs := by
   cases xs
   simp at h
   simpa using List.mem_of_find?_eq_some h
 
+@[grind]
 theorem get_find?_mem {xs : Array α} (h) : (xs.find? p).get h ∈ xs := by
   cases xs
   simp [List.get_find?_mem]
 
-@[simp] theorem find?_filter {xs : Array α} (p q : α → Bool) :
+@[simp, grind =] theorem find?_filter {xs : Array α} (p q : α → Bool) :
     (xs.filter p).find? q = xs.find? (fun a => p a ∧ q a) := by
   cases xs; simp
 
-@[simp] theorem getElem?_zero_filter {p : α → Bool} {xs : Array α} :
+@[simp, grind =] theorem getElem?_zero_filter {p : α → Bool} {xs : Array α} :
     (xs.filter p)[0]? = xs.find? p := by
   cases xs; simp [← List.head?_eq_getElem?]
 
-@[simp] theorem getElem_zero_filter {p : α → Bool} {xs : Array α} (h) :
+@[simp, grind =] theorem getElem_zero_filter {p : α → Bool} {xs : Array α} (h) :
     (xs.filter p)[0] =
       (xs.find? p).get (by cases xs; simpa [← List.countP_eq_length_filter] using h) := by
   cases xs
   simp [List.getElem_zero_eq_head]
 
-@[simp] theorem back?_filter {p : α → Bool} {xs : Array α} : (xs.filter p).back? = xs.findRev? p := by
+@[simp, grind =] theorem back?_filter {p : α → Bool} {xs : Array α} : (xs.filter p).back? = xs.findRev? p := by
   cases xs; simp
 
-@[simp] theorem back!_filter [Inhabited α] {p : α → Bool} {xs : Array α} :
+@[simp, grind =] theorem back!_filter [Inhabited α] {p : α → Bool} {xs : Array α} :
     (xs.filter p).back! = (xs.findRev? p).get! := by
   cases xs; simp [Option.get!_eq_getD]
 
-@[simp] theorem find?_filterMap {xs : Array α} {f : α → Option β} {p : β → Bool} :
+@[simp, grind =] theorem find?_filterMap {xs : Array α} {f : α → Option β} {p : β → Bool} :
     (xs.filterMap f).find? p = (xs.find? (fun a => (f a).any p)).bind f := by
   cases xs; simp
 
-@[simp] theorem find?_map {f : β → α} {xs : Array β} :
+@[simp, grind =] theorem find?_map {f : β → α} {xs : Array β} :
     find? p (xs.map f) = (xs.find? (p ∘ f)).map f := by
   cases xs; simp
 
-@[simp] theorem find?_append {xs ys : Array α} :
+@[simp, grind =] theorem find?_append {xs ys : Array α} :
     (xs ++ ys).find? p = (xs.find? p).or (ys.find? p) := by
   cases xs
   cases ys
   simp
 
-@[simp] theorem find?_flatten {xss : Array (Array α)} {p : α → Bool} :
-    xss.flatten.find? p = xss.findSome? (·.find? p) := by
+@[simp, grind _=_] theorem find?_flatten {xss : Array (Array α)} {p : α → Bool} :
+    xss.flatten.find? p = xss.findSome? (find? p) := by
   cases xss using array₂_induction
   simp [List.findSome?_map, Function.comp_def]
 
@@ -270,7 +305,7 @@ theorem find?_flatten_eq_some_iff {xss : Array (Array α)} {p : α → Bool} {a
 @[deprecated find?_flatten_eq_some_iff (since := "2025-02-03")]
 abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
 
-@[simp] theorem find?_flatMap {xs : Array α} {f : α → Array β} {p : β → Bool} :
+@[simp, grind =] theorem find?_flatMap {xs : Array α} {f : α → Array β} {p : β → Bool} :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   cases xs
   simp [List.find?_flatMap, Array.flatMap_toArray]
@@ -282,6 +317,7 @@ theorem find?_flatMap_eq_none_iff {xs : Array α} {f : α → Array β} {p : β
 @[deprecated find?_flatMap_eq_none_iff (since := "2025-02-03")]
 abbrev find?_flatMap_eq_none := @find?_flatMap_eq_none_iff
 
+@[grind =]
 theorem find?_replicate :
     find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   simp [← List.toArray_replicate, List.find?_replicate]
@@ -334,6 +370,7 @@ abbrev find?_mkArray_eq_some := @find?_replicate_eq_some_iff
 @[deprecated get_find?_replicate (since := "2025-03-18")]
 abbrev get_find?_mkArray := @get_find?_replicate
 
+@[grind =]
 theorem find?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Array α}
     (H : ∀ (a : α), a ∈ xs → P a) {p : β → Bool} :
     (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m) := by
@@ -347,12 +384,15 @@ theorem find?_eq_some_iff_getElem {xs : Array α} {p : α → Bool} {b : α} :
 
 /-! ### findIdx -/
 
+@[grind =]
 theorem findIdx_empty : findIdx p #[] = 0 := rfl
 
+@[grind =]
 theorem findIdx_singleton {a : α} {p : α → Bool} :
     #[a].findIdx p = if p a then 0 else 1 := by
   simp
 
+@[grind →]
 theorem findIdx_of_getElem?_eq_some {xs : Array α} (w : xs[xs.findIdx p]? = some y) : p y := by
   rcases xs with ⟨xs⟩
   exact List.findIdx_of_getElem?_eq_some (by simpa using w)
@@ -361,6 +401,8 @@ theorem findIdx_getElem {xs : Array α} {w : xs.findIdx p < xs.size} :
     p xs[xs.findIdx p] :=
   xs.findIdx_of_getElem?_eq_some (getElem?_eq_getElem w)
 
+grind_pattern findIdx_getElem => xs[xs.findIdx p]
+
 theorem findIdx_lt_size_of_exists {xs : Array α} (h : ∃ x ∈ xs, p x) :
     xs.findIdx p < xs.size := by
   rcases xs with ⟨xs⟩
@@ -387,18 +429,24 @@ theorem findIdx_le_size {p : α → Bool} {xs : Array α} : xs.findIdx p ≤ xs.
   · simp at e
     exact Nat.le_of_eq (findIdx_eq_size.mpr e)
 
+grind_pattern findIdx_le_size => xs.findIdx p, xs.size
+
 @[simp]
 theorem findIdx_lt_size {p : α → Bool} {xs : Array α} :
     xs.findIdx p < xs.size ↔ ∃ x ∈ xs, p x := by
   rcases xs with ⟨xs⟩
   simp
 
+grind_pattern findIdx_lt_size => xs.findIdx p, xs.size
+
 /-- `p` does not hold for elements with indices less than `xs.findIdx p`. -/
 theorem not_of_lt_findIdx {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.findIdx p) :
     p (xs[i]'(Nat.le_trans h findIdx_le_size)) = false := by
   rcases xs with ⟨xs⟩
   simpa using List.not_of_lt_findIdx (by simpa using h)
 
+grind_pattern not_of_lt_findIdx => xs.findIdx p, xs[i]
+
 /-- If `¬ p xs[j]` for all `j < i`, then `i ≤ xs.findIdx p`. -/
 theorem le_findIdx_of_not {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size)
     (h2 : ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false) : i ≤ xs.findIdx p := by
@@ -426,6 +474,7 @@ theorem findIdx_eq {p : α → Bool} {xs : Array α} {i : Nat} (h : i < xs.size)
   simp at h3
   simp_all [not_of_lt_findIdx h3]
 
+@[grind =]
 theorem findIdx_append {p : α → Bool} {xs ys : Array α} :
     (xs ++ ys).findIdx p =
       if xs.findIdx p < xs.size then xs.findIdx p else ys.findIdx p + xs.size := by
@@ -433,6 +482,7 @@ theorem findIdx_append {p : α → Bool} {xs ys : Array α} :
   rcases ys with ⟨ys⟩
   simp [List.findIdx_append]
 
+@[grind =]
 theorem findIdx_push {xs : Array α} {a : α} {p : α → Bool} :
     (xs.push a).findIdx p = if xs.findIdx p < xs.size then xs.findIdx p else xs.size + if p a then 0 else 1 := by
   simp only [push_eq_append, findIdx_append]
@@ -455,7 +505,7 @@ theorem false_of_mem_extract_findIdx {xs : Array α} {p : α → Bool} (h : x
   rcases xs with ⟨xs⟩
   exact List.false_of_mem_take_findIdx (by simpa using h)
 
-@[simp] theorem findIdx_extract {xs : Array α} {i : Nat} {p : α → Bool} :
+@[simp, grind =] theorem findIdx_extract {xs : Array α} {i : Nat} {p : α → Bool} :
     (xs.extract 0 i).findIdx p = min i (xs.findIdx p) := by
   cases xs
   simp
@@ -467,24 +517,24 @@ theorem false_of_mem_extract_findIdx {xs : Array α} {p : α → Bool} (h : x
 
 /-! ### findIdx? -/
 
-@[simp] theorem findIdx?_empty : (#[] : Array α).findIdx? p = none := by simp
-theorem findIdx?_singleton {a : α} {p : α → Bool} :
+@[simp, grind =] theorem findIdx?_empty : (#[] : Array α).findIdx? p = none := by simp
+@[grind =] theorem findIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findIdx? p = if p a then some 0 else none := by
   simp
 
-@[simp]
+@[simp, grind =]
 theorem findIdx?_eq_none_iff {xs : Array α} {p : α → Bool} :
     xs.findIdx? p = none ↔ ∀ x, x ∈ xs → p x = false := by
   rcases xs with ⟨xs⟩
   simp
 
-@[simp]
+@[simp, grind =]
 theorem findIdx?_isSome {xs : Array α} {p : α → Bool} :
     (xs.findIdx? p).isSome = xs.any p := by
   rcases xs with ⟨xs⟩
   simp [List.findIdx?_isSome]
 
-@[simp]
+@[simp, grind =]
 theorem findIdx?_isNone {xs : Array α} {p : α → Bool} :
     (xs.findIdx? p).isNone = xs.all (¬p ·) := by
   rcases xs with ⟨xs⟩
@@ -526,18 +576,19 @@ theorem of_findIdx?_eq_none {xs : Array α} {p : α → Bool} (w : xs.findIdx? p
   rcases xs with ⟨xs⟩
   simpa using List.of_findIdx?_eq_none (by simpa using w)
 
-@[simp] theorem findIdx?_map {f : β → α} {xs : Array β} {p : α → Bool} :
+@[simp, grind =] theorem findIdx?_map {f : β → α} {xs : Array β} {p : α → Bool} :
     findIdx? p (xs.map f) = xs.findIdx? (p ∘ f) := by
   rcases xs with ⟨xs⟩
   simp [List.findIdx?_map]
 
-@[simp] theorem findIdx?_append :
+@[simp, grind =] theorem findIdx?_append :
     (xs ++ ys : Array α).findIdx? p =
       (xs.findIdx? p).or ((ys.findIdx? p).map fun i => i + xs.size) := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   simp [List.findIdx?_append]
 
+@[grind =]
 theorem findIdx?_push {xs : Array α} {a : α} {p : α → Bool} :
     (xs.push a).findIdx? p = (xs.findIdx? p).or (if p a then some xs.size else none) := by
   simp only [push_eq_append, findIdx?_append]
@@ -553,7 +604,7 @@ theorem findIdx?_flatten {xss : Array (Array α)} {p : α → Bool} :
   cases xss using array₂_induction
   simp [List.findIdx?_flatten, Function.comp_def]
 
-@[simp] theorem findIdx?_replicate :
+@[simp, grind =] theorem findIdx?_replicate :
     (replicate n a).findIdx? p = if 0 < n ∧ p a then some 0 else none := by
   rw [← List.toArray_replicate]
   simp only [List.findIdx?_toArray]
@@ -578,6 +629,7 @@ theorem findIdx?_eq_none_of_findIdx?_eq_none {xs : Array α} {p q : α → Bool}
   rcases xs with ⟨xs⟩
   simpa using List.findIdx?_eq_none_of_findIdx?_eq_none (by simpa using w)
 
+@[grind =]
 theorem findIdx_eq_getD_findIdx? {xs : Array α} {p : α → Bool} :
     xs.findIdx p = (xs.findIdx? p).getD xs.size := by
   rcases xs with ⟨xs⟩
@@ -594,15 +646,17 @@ theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : Array α} {p q : α → Bo
   cases xs
   simp [hf]
 
-@[simp] theorem findIdx?_take {xs : Array α} {i : Nat} {p : α → Bool} :
+@[simp, grind =] theorem findIdx?_take {xs : Array α} {i : Nat} {p : α → Bool} :
     (xs.take i).findIdx? p = (xs.findIdx? p).bind (Option.guard (fun j => j < i)) := by
   cases xs
   simp
 
 /-! ### findFinIdx? -/
 
+@[grind =]
 theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p #[] = none := by simp
 
+@[grind =]
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
   simp
@@ -620,7 +674,7 @@ theorem findFinIdx?_eq_pmap_findIdx? {xs : Array α} {p : α → Bool} :
         (fun i h => h) := by
   simp [findIdx?_eq_map_findFinIdx?_val, Option.pmap_map]
 
-@[simp] theorem findFinIdx?_eq_none_iff {xs : Array α} {p : α → Bool} :
+@[simp, grind =] theorem findFinIdx?_eq_none_iff {xs : Array α} {p : α → Bool} :
     xs.findFinIdx? p = none ↔ ∀ x, x ∈ xs → ¬ p x := by
   simp [findFinIdx?_eq_pmap_findIdx?]
 
@@ -636,12 +690,14 @@ theorem findFinIdx?_eq_some_iff {xs : Array α} {p : α → Bool} {i : Fin xs.si
   · rintro ⟨h, w⟩
     exact ⟨i, ⟨i.2, h, fun j hji => w ⟨j, by omega⟩ hji⟩, rfl⟩
 
+@[grind =]
 theorem findFinIdx?_push {xs : Array α} {a : α} {p : α → Bool} :
     (xs.push a).findFinIdx? p =
       ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or (if p a then some ⟨xs.size, by simp⟩ else none) := by
   simp only [findFinIdx?_eq_pmap_findIdx?, findIdx?_push, Option.pmap_or]
   split <;> rename_i h _ <;> split <;> simp [h]
 
+@[grind =]
 theorem findFinIdx?_append {xs ys : Array α} {p : α → Bool} :
     (xs ++ ys).findFinIdx? p =
       ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or
@@ -651,13 +707,13 @@ theorem findFinIdx?_append {xs ys : Array α} {p : α → Bool} :
   · simp [h, Option.pmap_map, Option.map_pmap, Nat.add_comm]
   · simp [h]
 
-@[simp]
+@[simp, grind =]
 theorem isSome_findFinIdx? {xs : Array α} {p : α → Bool} :
     (xs.findFinIdx? p).isSome = xs.any p := by
   rcases xs with ⟨xs⟩
   simp [Array.size]
 
-@[simp]
+@[simp, grind =]
 theorem isNone_findFinIdx? {xs : Array α} {p : α → Bool} :
     (xs.findFinIdx? p).isNone = xs.all (fun x => ¬ p x) := by
   rcases xs with ⟨xs⟩
@@ -678,6 +734,7 @@ The verification API for `idxOf` is still incomplete.
 The lemmas below should be made consistent with those for `findIdx` (and proved using them).
 -/
 
+@[grind =]
 theorem idxOf_append [BEq α] [LawfulBEq α] {xs ys : Array α} {a : α} :
     (xs ++ ys).idxOf a = if a ∈ xs then xs.idxOf a else ys.idxOf a + xs.size := by
   rw [idxOf, findIdx_append]
@@ -691,10 +748,23 @@ theorem idxOf_eq_size [BEq α] [LawfulBEq α] {xs : Array α} (h : a ∉ xs) : x
   rcases xs with ⟨xs⟩
   simp [List.idxOf_eq_length (by simpa using h)]
 
-theorem idxOf_lt_length [BEq α] [LawfulBEq α] {xs : Array α} (h : a ∈ xs) : xs.idxOf a < xs.size := by
+theorem idxOf_lt_length_of_mem [BEq α] [LawfulBEq α] {xs : Array α} (h : a ∈ xs) : xs.idxOf a < xs.size := by
   rcases xs with ⟨xs⟩
-  simp [List.idxOf_lt_length (by simpa using h)]
+  simp [List.idxOf_lt_length_of_mem (by simpa using h)]
 
+theorem idxOf_le_size [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
+    xs.idxOf a ≤ xs.size := by
+  rcases xs with ⟨xs⟩
+  simp [List.idxOf_le_length]
+
+grind_pattern idxOf_le_size => xs.idxOf a, xs.size
+
+theorem idxOf_lt_size_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
+    xs.idxOf a < xs.size ↔ a ∈ xs := by
+  rcases xs with ⟨xs⟩
+  simp [List.idxOf_lt_length_iff]
+
+grind_pattern idxOf_lt_size_iff => xs.idxOf a, xs.size
 
 /-! ### idxOf?
 
@@ -702,19 +772,20 @@ The verification API for `idxOf?` is still incomplete.
 The lemmas below should be made consistent with those for `findIdx?` (and proved using them).
 -/
 
-theorem idxOf?_empty [BEq α] : (#[] : Array α).idxOf? a = none := by simp
+@[grind =] theorem idxOf?_empty [BEq α] : (#[] : Array α).idxOf? a = none := by simp
 
-@[simp] theorem idxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
+@[simp, grind =] theorem idxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = none ↔ a ∉ xs := by
   rcases xs with ⟨xs⟩
   simp [List.idxOf?_eq_none_iff]
 
-@[simp]
+@[simp, grind =]
 theorem isSome_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     (xs.idxOf? a).isSome ↔ a ∈ xs := by
   rcases xs with ⟨xs⟩
   simp
 
+@[grind =]
 theorem isNone_idxOf? [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     (xs.idxOf? a).isNone = ¬ a ∈ xs := by
   simp
@@ -729,9 +800,9 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : Array α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
   simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
 
-theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
+@[grind =] theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by simp
 
-@[simp] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
+@[simp, grind =] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.finIdxOf? a = none ↔ a ∉ xs := by
   rcases xs with ⟨xs⟩
   simp [List.finIdxOf?_eq_none_iff, Array.size]
@@ -742,13 +813,13 @@ theorem finIdxOf?_empty [BEq α] : (#[] : Array α).finIdxOf? a = none := by sim
   unfold Array.size at i ⊢
   simp [List.finIdxOf?_eq_some_iff]
 
-@[simp]
+@[simp, grind =]
 theorem isSome_finIdxOf? [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} :
     (xs.finIdxOf? a).isSome = xs.contains a := by
   rcases xs with ⟨xs⟩
   simp [Array.size]
 
-@[simp]
+@[simp, grind =]
 theorem isNone_finIdxOf? [BEq α] [PartialEquivBEq α] {xs : Array α} {a : α} :
     (xs.finIdxOf? a).isNone = !xs.contains a := by
   rcases xs with ⟨xs⟩

src/Init/Data/List/Basic.lean

@@ -1624,8 +1624,8 @@ def find? (p : α → Bool) : List α → Option α
     | true  => some a
     | false => find? p as
 
-@[simp] theorem find?_nil : ([] : List α).find? p = none := rfl
-theorem find?_cons : (a::as).find? p = match p a with | true => some a | false => as.find? p :=
+@[simp, grind =] theorem find?_nil : ([] : List α).find? p = none := rfl
+@[grind =]theorem find?_cons : (a::as).find? p = match p a with | true => some a | false => as.find? p :=
   rfl
 
 /-! ### findSome? -/
@@ -1845,8 +1845,8 @@ def lookup [BEq α] : α → List (α × β) → Option β
     | true  => some b
     | false => lookup a as
 
-@[simp] theorem lookup_nil [BEq α] : ([] : List (α × β)).lookup a = none := rfl
-theorem lookup_cons [BEq α] {k : α} :
+@[simp, grind =] theorem lookup_nil [BEq α] : ([] : List (α × β)).lookup a = none := rfl
+@[grind =] theorem lookup_cons [BEq α] {k : α} :
     ((k, b)::as).lookup a = match a == k with | true => some b | false => as.lookup a :=
   rfl
 

src/Init/Data/List/Find.lean

@@ -45,7 +45,7 @@ theorem exists_of_findSome?_eq_some {l : List α} {f : α → Option β} (w : l.
     simp_all only [findSome?_cons, mem_cons, exists_eq_or_imp]
     split at w <;> simp_all
 
-@[simp] theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
+@[simp, grind =] theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
   induction l <;> simp [findSome?_cons]; split <;> simp [*]
 
 @[simp] theorem findSome?_isSome_iff {f : α → Option β} {l : List α} :
@@ -91,7 +91,7 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
           obtain ⟨⟨rfl, rfl⟩, rfl⟩ := h₁
           exact ⟨l₁, a, l₂, rfl, h₂, fun a' w => h₃ a' (mem_cons_of_mem p w)⟩
 
-@[simp] theorem findSome?_guard {l : List α} : findSome? (Option.guard fun x => p x) l = find? p l := by
+@[simp, grind =] theorem findSome?_guard {l : List α} : findSome? (Option.guard p) l = find? p l := by
   induction l with
   | nil => simp
   | cons x xs ih =>
@@ -103,32 +103,33 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
     · simp only [Option.guard_eq_none_iff] at h
       simp [ih, h]
 
-theorem find?_eq_findSome?_guard {l : List α} : find? p l = findSome? (Option.guard fun x => p x) l :=
+theorem find?_eq_findSome?_guard {l : List α} : find? p l = findSome? (Option.guard p) l :=
   findSome?_guard.symm
 
-@[simp] theorem head?_filterMap {f : α → Option β} {l : List α} : (l.filterMap f).head? = l.findSome? f := by
+@[simp, grind =] theorem head?_filterMap {f : α → Option β} {l : List α} : (l.filterMap f).head? = l.findSome? f := by
   induction l with
   | nil => simp
   | cons x xs ih =>
     simp only [filterMap_cons, findSome?_cons]
     split <;> simp [*]
 
-@[simp] theorem head_filterMap {f : α → Option β} {l : List α} (h) :
+@[simp, grind =] theorem head_filterMap {f : α → Option β} {l : List α} (h) :
     (l.filterMap f).head h = (l.findSome? f).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [head_eq_iff_head?_eq_some]
 
-@[simp] theorem getLast?_filterMap {f : α → Option β} {l : List α} : (l.filterMap f).getLast? = l.reverse.findSome? f := by
+@[simp, grind =] theorem getLast?_filterMap {f : α → Option β} {l : List α} : (l.filterMap f).getLast? = l.reverse.findSome? f := by
   rw [getLast?_eq_head?_reverse]
   simp [← filterMap_reverse]
 
-@[simp] theorem getLast_filterMap {f : α → Option β} {l : List α} (h) :
+@[simp, grind =] theorem getLast_filterMap {f : α → Option β} {l : List α} (h) :
     (l.filterMap f).getLast h = (l.reverse.findSome? f).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [getLast_eq_iff_getLast?_eq_some]
 
-@[simp] theorem map_findSome? {f : α → Option β} {g : β → γ} {l : List α} :
+@[simp, grind _=_] theorem map_findSome? {f : α → Option β} {g : β → γ} {l : List α} :
     (l.findSome? f).map g = l.findSome? (Option.map g ∘ f) := by
   induction l <;> simp [findSome?_cons]; split <;> simp [*]
 
+@[grind _=_]
 theorem findSome?_map {f : β → γ} {l : List β} : findSome? p (l.map f) = l.findSome? (p ∘ f) := by
   induction l with
   | nil => simp
@@ -136,15 +137,18 @@ theorem findSome?_map {f : β → γ} {l : List β} : findSome? p (l.map f) = l.
     simp only [map_cons, findSome?]
     split <;> simp_all
 
+@[grind =]
 theorem head_flatten {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
-    (flatten L).head (by simpa using h) = (L.findSome? fun l => l.head?).get (by simpa using h) := by
+    (flatten L).head (by simpa using h) = (L.findSome? head?).get (by simpa using h) := by
   simp [head_eq_iff_head?_eq_some, head?_flatten]
 
+@[grind =]
 theorem getLast_flatten {L : List (List α)} (h : ∃ l, l ∈ L ∧ l ≠ []) :
     (flatten L).getLast (by simpa using h) =
-      (L.reverse.findSome? fun l => l.getLast?).get (by simpa using h) := by
+      (L.reverse.findSome? getLast?).get (by simpa using h) := by
   simp [getLast_eq_iff_getLast?_eq_some, getLast?_flatten]
 
+@[grind =]
 theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   cases n with
   | zero => simp
@@ -174,6 +178,9 @@ theorem Sublist.findSome?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
     · simp_all
     · exact ih
 
+grind_pattern Sublist.findSome?_isSome => l₁ <+ l₂, l₁.findSome? f
+grind_pattern Sublist.findSome?_isSome => l₁ <+ l₂, l₂.findSome? f
+
 theorem Sublist.findSome?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) :
     l₂.findSome? f = none → l₁.findSome? f = none := by
   simp only [List.findSome?_eq_none_iff, Bool.not_eq_true]
@@ -185,16 +192,30 @@ theorem IsPrefix.findSome?_eq_some {l₁ l₂ : List α} {f : α → Option β}
   obtain ⟨t, rfl⟩ := h
   simp +contextual [findSome?_append]
 
+grind_pattern IsPrefix.findSome?_eq_some => l₁ <+: l₂, l₁.findSome? f, some b
+grind_pattern IsPrefix.findSome?_eq_some => l₁ <+: l₂, l₂.findSome? f, some b
+
 theorem IsPrefix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <+: l₂) :
     List.findSome? f l₂ = none → List.findSome? f l₁ = none :=
   h.sublist.findSome?_eq_none
+
+grind_pattern IsPrefix.findSome?_eq_none => l₁ <+: l₂, l₂.findSome? f
+grind_pattern IsPrefix.findSome?_eq_none => l₁ <+: l₂, l₁.findSome? f
+
 theorem IsSuffix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <:+ l₂) :
     List.findSome? f l₂ = none → List.findSome? f l₁ = none :=
   h.sublist.findSome?_eq_none
+
+grind_pattern IsSuffix.findSome?_eq_none => l₁ <+: l₂, l₂.findSome? f
+grind_pattern IsSuffix.findSome?_eq_none => l₁ <+: l₂, l₁.findSome? f
+
 theorem IsInfix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <:+: l₂) :
     List.findSome? f l₂ = none → List.findSome? f l₁ = none :=
   h.sublist.findSome?_eq_none
 
+grind_pattern IsInfix.findSome?_eq_none => l₁ <+: l₂, l₂.findSome? f
+grind_pattern IsInfix.findSome?_eq_none => l₁ <+: l₂, l₁.findSome? f
+
 /-! ### find? -/
 
 @[simp] theorem find?_cons_of_pos {l} (h : p a) : find? p (a :: l) = some a := by
@@ -203,7 +224,7 @@ theorem IsInfix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (
 @[simp] theorem find?_cons_of_neg {l} (h : ¬p a) : find? p (a :: l) = find? p l := by
   simp [find?, h]
 
-@[simp] theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
+@[simp, grind =] theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
   induction l <;> simp [find?_cons]; split <;> simp [*]
 
 theorem find?_eq_some_iff_append :
@@ -248,25 +269,28 @@ theorem find?_cons_eq_some : (a :: xs).find? p = some b ↔ (p a ∧ a = b) ∨
   rw [find?_cons]
   split <;> simp_all
 
-@[simp] theorem find?_isSome {xs : List α} {p : α → Bool} : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x := by
+@[simp, grind =] theorem find?_isSome {xs : List α} {p : α → Bool} : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x := by
   induction xs with
   | nil => simp
   | cons x xs ih =>
     simp only [find?_cons, mem_cons, exists_eq_or_imp]
     split <;> simp_all
 
+@[grind →]
 theorem find?_some : ∀ {l}, find? p l = some a → p a
   | b :: l, H => by
     by_cases h : p b <;> simp [find?, h] at H
     · exact H ▸ h
     · exact find?_some H
 
+@[grind →]
 theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
   | b :: l, H => by
     by_cases h : p b <;> simp [find?, h] at H
     · exact H ▸ .head _
     · exact .tail _ (mem_of_find?_eq_some H)
 
+@[grind]
 theorem get_find?_mem {xs : List α} {p : α → Bool} (h) : (xs.find? p).get h ∈ xs := by
   induction xs with
   | nil => simp at h
@@ -278,7 +302,7 @@ theorem get_find?_mem {xs : List α} {p : α → Bool} (h) : (xs.find? p).get h
       right
       apply ih
 
-@[simp] theorem find?_filter {xs : List α} {p : α → Bool} {q : α → Bool} :
+@[simp, grind =] theorem find?_filter {xs : List α} {p : α → Bool} {q : α → Bool} :
     (xs.filter p).find? q = xs.find? (fun a => p a ∧ q a) := by
   induction xs with
   | nil => simp
@@ -288,22 +312,22 @@ theorem get_find?_mem {xs : List α} {p : α → Bool} (h) : (xs.find? p).get h
     · simp only [find?_cons]
       split <;> simp_all
 
-@[simp] theorem head?_filter {p : α → Bool} {l : List α} : (l.filter p).head? = l.find? p := by
+@[simp, grind =] theorem head?_filter {p : α → Bool} {l : List α} : (l.filter p).head? = l.find? p := by
   rw [← filterMap_eq_filter, head?_filterMap, findSome?_guard]
 
-@[simp] theorem head_filter {p : α → Bool} {l : List α} (h) :
+@[simp, grind =] theorem head_filter {p : α → Bool} {l : List α} (h) :
     (l.filter p).head h = (l.find? p).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [head_eq_iff_head?_eq_some]
 
-@[simp] theorem getLast?_filter {p : α → Bool} {l : List α} : (l.filter p).getLast? = l.reverse.find? p := by
+@[simp, grind =] theorem getLast?_filter {p : α → Bool} {l : List α} : (l.filter p).getLast? = l.reverse.find? p := by
   rw [getLast?_eq_head?_reverse]
   simp [← filter_reverse]
 
-@[simp] theorem getLast_filter {p : α → Bool} {l : List α} (h) :
+@[simp, grind =] theorem getLast_filter {p : α → Bool} {l : List α} (h) :
     (l.filter p).getLast h = (l.reverse.find? p).get (by simp_all [Option.isSome_iff_ne_none]) := by
   simp [getLast_eq_iff_getLast?_eq_some]
 
-@[simp] theorem find?_filterMap {xs : List α} {f : α → Option β} {p : β → Bool} :
+@[simp, grind =] theorem find?_filterMap {xs : List α} {f : α → Option β} {p : β → Bool} :
     (xs.filterMap f).find? p = (xs.find? (fun a => (f a).any p)).bind f := by
   induction xs with
   | nil => simp
@@ -313,15 +337,15 @@ theorem get_find?_mem {xs : List α} {p : α → Bool} (h) : (xs.find? p).get h
     · simp only [find?_cons]
       split <;> simp_all
 
-@[simp] theorem find?_map {f : β → α} {l : List β} : find? p (l.map f) = (l.find? (p ∘ f)).map f := by
+@[simp, grind =] theorem find?_map {f : β → α} {l : List β} : find? p (l.map f) = (l.find? (p ∘ f)).map f := by
   induction l with
   | nil => simp
   | cons x xs ih =>
     simp only [map_cons, find?]
     by_cases h : p (f x) <;> simp [h, ih]
 
-@[simp] theorem find?_flatten {xss : List (List α)} {p : α → Bool} :
-    xss.flatten.find? p = xss.findSome? (·.find? p) := by
+@[simp, grind _=_] theorem find?_flatten {xss : List (List α)} {p : α → Bool} :
+    xss.flatten.find? p = xss.findSome? (find? p) := by
   induction xss with
   | nil => simp
   | cons _ _ ih =>
@@ -378,7 +402,7 @@ theorem find?_flatten_eq_some_iff {xs : List (List α)} {p : α → Bool} {a :
 @[deprecated find?_flatten_eq_some_iff (since := "2025-02-03")]
 abbrev find?_flatten_eq_some := @find?_flatten_eq_some_iff
 
-@[simp] theorem find?_flatMap {xs : List α} {f : α → List β} {p : β → Bool} :
+@[simp, grind =] theorem find?_flatMap {xs : List α} {f : α → List β} {p : β → Bool} :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   simp [flatMap_def, findSome?_map]; rfl
 
@@ -386,6 +410,7 @@ theorem find?_flatMap_eq_none_iff {xs : List α} {f : α → List β} {p : β
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
+@[grind =]
 theorem find?_replicate : find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   cases n
   · simp
@@ -430,6 +455,9 @@ theorem Sublist.find?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) : (l₁.fi
     · simp
     · simpa using ih
 
+grind_pattern Sublist.find?_isSome => l₁ <+ l₂, l₁.find? p
+grind_pattern Sublist.find?_isSome => l₁ <+ l₂, l₂.find? p
+
 theorem Sublist.find?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) : l₂.find? p = none → l₁.find? p = none := by
   simp only [List.find?_eq_none, Bool.not_eq_true]
   exact fun w x m => w x (Sublist.mem m h)
@@ -440,16 +468,31 @@ theorem IsPrefix.find?_eq_some {l₁ l₂ : List α} {p : α → Bool} (h : l₁
   obtain ⟨t, rfl⟩ := h
   simp +contextual [find?_append]
 
+grind_pattern IsPrefix.find?_eq_some => l₁ <+: l₂, l₁.find? p, some b
+grind_pattern IsPrefix.find?_eq_some => l₁ <+: l₂, l₂.find? p, some b
+
 theorem IsPrefix.find?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
     List.find? p l₂ = none → List.find? p l₁ = none :=
   h.sublist.find?_eq_none
+
+grind_pattern Sublist.find?_eq_none => l₁ <+ l₂, l₂.find? p
+grind_pattern Sublist.find?_eq_none => l₁ <+ l₂, l₁.find? p
+
 theorem IsSuffix.find?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+ l₂) :
     List.find? p l₂ = none → List.find? p l₁ = none :=
   h.sublist.find?_eq_none
+
+grind_pattern IsPrefix.find?_eq_none => l₁ <+: l₂, l₂.find? p
+grind_pattern IsPrefix.find?_eq_none => l₁ <+: l₂, l₁.find? p
+
 theorem IsInfix.find?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+: l₂) :
     List.find? p l₂ = none → List.find? p l₁ = none :=
   h.sublist.find?_eq_none
 
+grind_pattern IsSuffix.find?_eq_none => l₁ <:+ l₂, l₂.find? p
+grind_pattern IsSuffix.find?_eq_none => l₁ <:+ l₂, l₁.find? p
+
+@[grind =]
 theorem find?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : List α}
     (H : ∀ (a : α), a ∈ xs → P a) {p : β → Bool} :
     (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m) := by
@@ -482,9 +525,9 @@ private theorem findIdx?_go_eq {p : α → Bool} {xs : List α} {i : Nat} :
       ext
       simp only [Nat.add_comm i, Function.comp_apply, Nat.add_assoc]
 
-@[simp] theorem findIdx?_nil : ([] : List α).findIdx? p = none := rfl
+@[simp, grind =] theorem findIdx?_nil : ([] : List α).findIdx? p = none := rfl
 
-theorem findIdx?_cons :
+@[grind =] theorem findIdx?_cons :
     (x :: xs).findIdx? p = if p x then some 0 else (xs.findIdx? p).map fun i => i + 1 := by
   simp [findIdx?, findIdx?_go_eq]
 
@@ -493,6 +536,7 @@ theorem findIdx?_cons :
 
 /-! ### findIdx -/
 
+@[grind =]
 theorem findIdx_cons {p : α → Bool} {b : α} {l : List α} :
     (b :: l).findIdx p = bif p b then 0 else (l.findIdx p) + 1 := by
   cases H : p b with
@@ -511,6 +555,7 @@ where
 @[simp] theorem findIdx_singleton {a : α} {p : α → Bool} : [a].findIdx p = if p a then 0 else 1 := by
   simp [findIdx_cons, findIdx_nil]
 
+@[grind →]
 theorem findIdx_of_getElem?_eq_some {xs : List α} (w : xs[xs.findIdx p]? = some y) : p y := by
   induction xs with
   | nil => simp_all
@@ -520,6 +565,8 @@ theorem findIdx_getElem {xs : List α} {w : xs.findIdx p < xs.length} :
     p xs[xs.findIdx p] :=
   xs.findIdx_of_getElem?_eq_some (getElem?_eq_getElem w)
 
+grind_pattern findIdx_getElem => xs[xs.findIdx p]
+
 theorem findIdx_lt_length_of_exists {xs : List α} (h : ∃ x ∈ xs, p x) :
     xs.findIdx p < xs.length := by
   induction xs with
@@ -558,6 +605,8 @@ theorem findIdx_le_length {p : α → Bool} {xs : List α} : xs.findIdx p ≤ xs
   · simp at e
     exact Nat.le_of_eq (findIdx_eq_length.mpr e)
 
+grind_pattern findIdx_le_length => xs.findIdx p, xs.length
+
 @[simp]
 theorem findIdx_lt_length {p : α → Bool} {xs : List α} :
     xs.findIdx p < xs.length ↔ ∃ x ∈ xs, p x := by
@@ -567,6 +616,8 @@ theorem findIdx_lt_length {p : α → Bool} {xs : List α} :
   rw [← this, findIdx_eq_length, not_exists]
   simp only [Bool.not_eq_true, not_and]
 
+grind_pattern findIdx_lt_length => xs.findIdx p, xs.length
+
 /-- `p` does not hold for elements with indices less than `xs.findIdx p`. -/
 theorem not_of_lt_findIdx {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.findIdx p) :
     p (xs[i]'(Nat.le_trans h findIdx_le_length)) = false := by
@@ -591,6 +642,8 @@ theorem not_of_lt_findIdx {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs
       rw [← ipm, Nat.succ_lt_succ_iff] at h
       simpa using ih h
 
+grind_pattern not_of_lt_findIdx => xs.findIdx p, xs[i]
+
 /-- If `¬ p xs[j]` for all `j < i`, then `i ≤ xs.findIdx p`. -/
 theorem le_findIdx_of_not {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length)
     (h2 : ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false) : i ≤ xs.findIdx p := by
@@ -618,6 +671,7 @@ theorem findIdx_eq {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length
   simp at h3
   simp_all [not_of_lt_findIdx h3]
 
+@[grind =]
 theorem findIdx_append {p : α → Bool} {l₁ l₂ : List α} :
     (l₁ ++ l₂).findIdx p =
       if l₁.findIdx p < l₁.length then l₁.findIdx p else l₂.findIdx p + l₁.length := by
@@ -639,6 +693,9 @@ theorem IsPrefix.findIdx_le {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+
   · exact Nat.le_refl ..
   · simp_all [findIdx_eq_length_of_false]
 
+grind_pattern IsPrefix.findIdx_le => l₁ <:+ l₂, l₁.findIdx p
+grind_pattern IsPrefix.findIdx_le => l₁ <:+ l₂, l₂.findIdx p
+
 theorem IsPrefix.findIdx_eq_of_findIdx_lt_length {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂)
     (lt : l₁.findIdx p < l₁.length) : l₂.findIdx p = l₁.findIdx p := by
   rw [IsPrefix] at h
@@ -648,6 +705,8 @@ theorem IsPrefix.findIdx_eq_of_findIdx_lt_length {l₁ l₂ : List α} {p : α
   · rfl
   · simp_all
 
+grind_pattern IsPrefix.findIdx_eq_of_findIdx_lt_length => l₁ <:+ l₂, l₁.findIdx p, l₂.findIdx p
+
 theorem findIdx_le_findIdx {l : List α} {p q : α → Bool} (h : ∀ x ∈ l, p x → q x) : l.findIdx q ≤ l.findIdx p := by
   induction l with
   | nil => simp
@@ -671,7 +730,7 @@ theorem findIdx_le_findIdx {l : List α} {p q : α → Bool} (h : ∀ x ∈ l, p
 
 /-! ### findIdx? -/
 
-@[simp]
+@[simp, grind =]
 theorem findIdx?_eq_none_iff {xs : List α} {p : α → Bool} :
     xs.findIdx? p = none ↔ ∀ x, x ∈ xs → p x = false := by
   induction xs with
@@ -680,7 +739,7 @@ theorem findIdx?_eq_none_iff {xs : List α} {p : α → Bool} :
     simp only [findIdx?_cons]
     split <;> simp_all [cond_eq_if]
 
-@[simp]
+@[simp, grind =]
 theorem findIdx?_isSome {xs : List α} {p : α → Bool} :
     (xs.findIdx? p).isSome = xs.any p := by
   induction xs with
@@ -689,7 +748,7 @@ theorem findIdx?_isSome {xs : List α} {p : α → Bool} :
     simp only [findIdx?_cons]
     split <;> simp_all
 
-@[simp]
+@[simp, grind =]
 theorem findIdx?_isNone {xs : List α} {p : α → Bool} :
     (xs.findIdx? p).isNone = xs.all (¬p ·) := by
   induction xs with
@@ -795,14 +854,14 @@ theorem of_findIdx?_eq_none {xs : List α} {p : α → Bool} (w : xs.findIdx? p
 @[deprecated of_findIdx?_eq_none (since := "2025-02-02")]
 abbrev findIdx?_of_eq_none := @of_findIdx?_eq_none
 
-@[simp] theorem findIdx?_map {f : β → α} {l : List β} : findIdx? p (l.map f) = l.findIdx? (p ∘ f) := by
+@[simp, grind _=_] theorem findIdx?_map {f : β → α} {l : List β} : findIdx? p (l.map f) = l.findIdx? (p ∘ f) := by
   induction l with
   | nil => simp
   | cons x xs ih =>
     simp only [map_cons, findIdx?_cons]
     split <;> simp_all
 
-@[simp] theorem findIdx?_append :
+@[simp, grind =] theorem findIdx?_append :
     (xs ++ ys : List α).findIdx? p =
       (xs.findIdx? p).or ((ys.findIdx? p).map fun i => i + xs.length) := by
   induction xs with simp [findIdx?_cons]
@@ -824,7 +883,7 @@ theorem findIdx?_flatten {l : List (List α)} {p : α → Bool} :
     · rw [Option.or_of_isNone (by simp_all [findIdx?_isNone])]
       simp [Function.comp_def, Nat.add_comm, Nat.add_assoc]
 
-@[simp] theorem findIdx?_replicate :
+@[simp, grind =] theorem findIdx?_replicate :
     (replicate n a).findIdx? p = if 0 < n ∧ p a then some 0 else none := by
   cases n with
   | zero => simp
@@ -878,22 +937,38 @@ theorem Sublist.findIdx?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) :
   simp only [findIdx?_eq_none_iff]
   exact fun w x m => w x (h.mem m)
 
+grind_pattern Sublist.findIdx?_eq_none => l₁ <+ l₂, l₁.findIdx? p
+grind_pattern Sublist.findIdx?_eq_none => l₁ <+ l₂, l₂.findIdx? p
+
 theorem IsPrefix.findIdx?_eq_some {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
     List.findIdx? p l₁ = some i → List.findIdx? p l₂ = some i := by
   rw [IsPrefix] at h
   obtain ⟨t, rfl⟩ := h
   intro h
   simp [findIdx?_append, h]
+
 theorem IsPrefix.findIdx?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
     List.findIdx? p l₂ = none → List.findIdx? p l₁ = none :=
   h.sublist.findIdx?_eq_none
+
+grind_pattern IsPrefix.findIdx?_eq_none => l₁ <+: l₂, l₁.findIdx? p
+grind_pattern IsPrefix.findIdx?_eq_none => l₁ <+: l₂, l₂.findIdx? p
+
 theorem IsSuffix.findIdx?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+ l₂) :
     List.findIdx? p l₂ = none → List.findIdx? p l₁ = none :=
   h.sublist.findIdx?_eq_none
+
+grind_pattern IsSuffix.findIdx?_eq_none => l₁ <:+ l₂, l₁.findIdx? p
+grind_pattern IsSuffix.findIdx?_eq_none => l₁ <:+ l₂, l₂.findIdx? p
+
 theorem IsInfix.findIdx?_eq_none {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <:+: l₂) :
     List.findIdx? p l₂ = none → List.findIdx? p l₁ = none :=
   h.sublist.findIdx?_eq_none
 
+grind_pattern IsInfix.findIdx?_eq_none => l₁ <:+: l₂, l₁.findIdx? p
+grind_pattern IsInfix.findIdx?_eq_none => l₁ <:+: l₂, l₂.findIdx? p
+
+@[grind =]
 theorem findIdx_eq_getD_findIdx? {xs : List α} {p : α → Bool} :
     xs.findIdx p = (xs.findIdx? p).getD xs.length := by
   induction xs with
@@ -914,7 +989,7 @@ theorem findIdx_eq_getD_findIdx? {xs : List α} {p : α → Bool} :
 
 /-! ### findFinIdx? -/
 
-@[simp] theorem findFinIdx?_nil {p : α → Bool} : findFinIdx? p [] = none := rfl
+@[simp, grind =] theorem findFinIdx?_nil {p : α → Bool} : findFinIdx? p [] = none := rfl
 
 theorem findIdx?_go_eq_map_findFinIdx?_go_val {xs : List α} {p : α → Bool} {i : Nat} {h} :
     List.findIdx?.go p xs i =
@@ -940,6 +1015,7 @@ theorem findFinIdx?_eq_pmap_findIdx? {xs : List α} {p : α → Bool} :
         (fun i h => h) := by
   simp [findIdx?_eq_map_findFinIdx?_val, Option.pmap_map]
 
+@[grind =]
 theorem findFinIdx?_cons {p : α → Bool} {x : α} {xs : List α} :
     findFinIdx? p (x :: xs) = if p x then some 0 else (findFinIdx? p xs).map Fin.succ := by
   rw [← Option.map_inj_right (f := Fin.val) (fun a b => Fin.eq_of_val_eq)]
@@ -950,6 +1026,7 @@ theorem findFinIdx?_cons {p : α → Bool} {x : α} {xs : List α} :
   · rw [findIdx?_eq_map_findFinIdx?_val]
     simp [Function.comp_def]
 
+@[grind =]
 theorem findFinIdx?_append {xs ys : List α} {p : α → Bool} :
     (xs ++ ys).findFinIdx? p =
       ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or
@@ -959,11 +1036,11 @@ theorem findFinIdx?_append {xs ys : List α} {p : α → Bool} :
   · simp [h, Option.pmap_map, Option.map_pmap, Nat.add_comm]
   · simp [h]
 
-@[simp] theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
+@[simp, grind =] theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     [a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
   simp [findFinIdx?_cons, findFinIdx?_nil]
 
-@[simp] theorem findFinIdx?_eq_none_iff {l : List α} {p : α → Bool} :
+@[simp, grind =] theorem findFinIdx?_eq_none_iff {l : List α} {p : α → Bool} :
     l.findFinIdx? p = none ↔ ∀ x ∈ l, ¬ p x := by
   simp [findFinIdx?_eq_pmap_findIdx?]
 
@@ -979,7 +1056,7 @@ theorem findFinIdx?_eq_some_iff {xs : List α} {p : α → Bool} {i : Fin xs.len
   · rintro ⟨h, w⟩
     exact ⟨i, ⟨i.2, h, fun j hji => w ⟨j, by omega⟩ hji⟩, rfl⟩
 
-@[simp]
+@[simp, grind =]
 theorem isSome_findFinIdx? {l : List α} {p : α → Bool} :
     (l.findFinIdx? p).isSome = l.any p := by
   induction l with
@@ -988,7 +1065,7 @@ theorem isSome_findFinIdx? {l : List α} {p : α → Bool} :
     simp only [findFinIdx?_cons]
     split <;> simp_all
 
-@[simp]
+@[simp, grind =]
 theorem isNone_findFinIdx? {l : List α} {p : α → Bool} :
     (l.findFinIdx? p).isNone = l.all (fun x => ¬ p x) := by
   induction l with
@@ -1013,6 +1090,7 @@ The verification API for `idxOf` is still incomplete.
 The lemmas below should be made consistent with those for `findIdx` (and proved using them).
 -/
 
+@[grind =]
 theorem idxOf_cons [BEq α] :
     (x :: xs : List α).idxOf y = bif x == y then 0 else xs.idxOf y + 1 := by
   dsimp [idxOf]
@@ -1027,6 +1105,7 @@ abbrev indexOf_cons := @idxOf_cons
 @[deprecated idxOf_cons_self (since := "2025-01-29")]
 abbrev indexOf_cons_self := @idxOf_cons_self
 
+@[grind =]
 theorem idxOf_append [BEq α] [LawfulBEq α] {l₁ l₂ : List α} {a : α} :
     (l₁ ++ l₂).idxOf a = if a ∈ l₁ then l₁.idxOf a else l₂.idxOf a + l₁.length := by
   rw [idxOf, findIdx_append]
@@ -1050,7 +1129,7 @@ theorem idxOf_eq_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∉ l) : l.
 @[deprecated idxOf_eq_length (since := "2025-01-29")]
 abbrev indexOf_eq_length := @idxOf_eq_length
 
-theorem idxOf_lt_length [BEq α] [EquivBEq α] {l : List α} (h : a ∈ l) : l.idxOf a < l.length := by
+theorem idxOf_lt_length_of_mem [BEq α] [EquivBEq α] {l : List α} (h : a ∈ l) : l.idxOf a < l.length := by
   induction l with
   | nil => simp at h
   | cons x xs ih =>
@@ -1063,8 +1142,23 @@ theorem idxOf_lt_length [BEq α] [EquivBEq α] {l : List α} (h : a ∈ l) : l.i
       · exact zero_lt_succ xs.length
       · exact Nat.add_lt_add_right ih 1
 
-@[deprecated idxOf_lt_length (since := "2025-01-29")]
-abbrev indexOf_lt_length := @idxOf_lt_length
+theorem idxOf_le_length [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+    l.idxOf a ≤ l.length := by
+  simpa [idxOf] using findIdx_le_length
+
+grind_pattern idxOf_le_length => l.idxOf a, l.length
+
+theorem idxOf_lt_length_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+    l.idxOf a < l.length ↔ a ∈ l := by
+  constructor
+  · intro h
+    simpa [idxOf] using h
+  · exact idxOf_lt_length_of_mem
+
+grind_pattern idxOf_lt_length_iff => l.idxOf a, l.length
+
+@[deprecated idxOf_lt_length_of_mem (since := "2025-01-29")]
+abbrev indexOf_lt_length := @idxOf_lt_length_of_mem
 
 /-! ### finIdxOf?
 
@@ -1076,14 +1170,14 @@ theorem idxOf?_eq_map_finIdxOf?_val [BEq α] {xs : List α} {a : α} :
     xs.idxOf? a = (xs.finIdxOf? a).map (·.val) := by
   simp [idxOf?, finIdxOf?, findIdx?_eq_map_findFinIdx?_val]
 
-@[simp] theorem finIdxOf?_nil [BEq α] : ([] : List α).finIdxOf? a = none := rfl
+@[simp, grind =] theorem finIdxOf?_nil [BEq α] : ([] : List α).finIdxOf? a = none := rfl
 
-theorem finIdxOf?_cons [BEq α] {a : α} {xs : List α} :
+@[grind =] theorem finIdxOf?_cons [BEq α] {a : α} {xs : List α} :
     (a :: xs).finIdxOf? b =
       if a == b then some ⟨0, by simp⟩ else (xs.finIdxOf? b).map (·.succ) := by
   simp [finIdxOf?, findFinIdx?_cons]
 
-@[simp] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+@[simp, grind =] theorem finIdxOf?_eq_none_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     l.finIdxOf? a = none ↔ a ∉ l := by
   simp only [finIdxOf?, findFinIdx?_eq_none_iff, beq_iff_eq]
   constructor
@@ -1096,7 +1190,7 @@ theorem finIdxOf?_cons [BEq α] {a : α} {xs : List α} :
     l.finIdxOf? a = some i ↔ l[i] = a ∧ ∀ j (_ : j < i), ¬l[j] = a := by
   simp only [finIdxOf?, findFinIdx?_eq_some_iff, beq_iff_eq]
 
-@[simp]
+@[simp, grind =]
 theorem isSome_finIdxOf? [BEq α] [PartialEquivBEq α] {l : List α} {a : α} :
     (l.finIdxOf? a).isSome = l.contains a := by
   induction l with
@@ -1116,16 +1210,16 @@ The verification API for `idxOf?` is still incomplete.
 The lemmas below should be made consistent with those for `findIdx?` (and proved using them).
 -/
 
-@[simp] theorem idxOf?_nil [BEq α] : ([] : List α).idxOf? a = none := rfl
+@[simp, grind =] theorem idxOf?_nil [BEq α] : ([] : List α).idxOf? a = none := rfl
 
-theorem idxOf?_cons [BEq α] {a : α} {xs : List α} {b : α} :
+@[grind =] theorem idxOf?_cons [BEq α] {a : α} {xs : List α} {b : α} :
     (a :: xs).idxOf? b = if a == b then some 0 else (xs.idxOf? b).map (· + 1) := by
   simp [idxOf?, findIdx?_cons]
 
 @[simp] theorem idxOf?_singleton [BEq α] {a b : α} : [a].idxOf? b = if a == b then some 0 else none := by
   simp [idxOf?_cons, idxOf?_nil]
 
-@[simp] theorem idxOf?_eq_none_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+@[simp, grind =] theorem idxOf?_eq_none_iff [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     l.idxOf? a = none ↔ a ∉ l := by
   simp only [idxOf?, findIdx?_eq_none_iff, beq_eq_false_iff_ne, ne_eq]
   constructor
@@ -1138,7 +1232,7 @@ theorem idxOf?_cons [BEq α] {a : α} {xs : List α} {b : α} :
 @[deprecated idxOf?_eq_none_iff (since := "2025-01-29")]
 abbrev indexOf?_eq_none_iff := @idxOf?_eq_none_iff
 
-@[simp]
+@[simp, grind =]
 theorem isSome_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     (l.idxOf? a).isSome ↔ a ∈ l := by
   induction l with
@@ -1147,6 +1241,7 @@ theorem isSome_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     simp only [idxOf?_cons]
     split <;> simp_all [@eq_comm _ x a]
 
+@[grind =]
 theorem isNone_idxOf? [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     (l.idxOf? a).isNone = ¬ a ∈ l := by
   simp
@@ -1173,7 +1268,7 @@ theorem lookup_eq_findSome? {l : List (α × β)} {k : α} :
       simp only [lookup_cons, findSome?_cons]
       split <;> simp_all
 
-@[simp] theorem lookup_eq_none_iff {l : List (α × β)} {k : α} :
+@[simp, grind =] theorem lookup_eq_none_iff {l : List (α × β)} {k : α} :
     l.lookup k = none ↔ ∀ p ∈ l, k != p.1 := by
   simp [lookup_eq_findSome?]
 
@@ -1193,10 +1288,12 @@ theorem lookup_eq_some_iff {l : List (α × β)} {k : α} {b : β} :
   · rintro ⟨l₁, l₂, rfl, h⟩
     exact ⟨l₁, (k, b), l₂, rfl, by simp, by simpa using h⟩
 
+@[grind =]
 theorem lookup_append {l₁ l₂ : List (α × β)} {k : α} :
     (l₁ ++ l₂).lookup k = (l₁.lookup k).or (l₂.lookup k) := by
   simp [lookup_eq_findSome?, findSome?_append]
 
+@[grind =]
 theorem lookup_replicate {k : α} :
     (replicate n (a,b)).lookup k = if n = 0 then none else if k == a then some b else none := by
   induction n with
@@ -1231,6 +1328,9 @@ theorem Sublist.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <+ l₂)
   simp only [lookup_eq_findSome?]
   exact h.findSome?_eq_none
 
+grind_pattern Sublist.lookup_isSome => l₁ <+ l₂, l₁.lookup k
+grind_pattern Sublist.lookup_isSome => l₁ <+ l₂, l₂.lookup k
+
 theorem IsPrefix.lookup_eq_some {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂) :
     List.lookup k l₁ = some b → List.lookup k l₂ = some b := by
   simp only [lookup_eq_findSome?]
@@ -1239,13 +1339,24 @@ theorem IsPrefix.lookup_eq_some {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂
 theorem IsPrefix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <+: l₂) :
     List.lookup k l₂ = none → List.lookup k l₁ = none :=
   h.sublist.lookup_eq_none
+
+grind_pattern IsPrefix.lookup_eq_none => l₁ <+: l₂, l₁.lookup k
+grind_pattern IsPrefix.lookup_eq_none => l₁ <+: l₂, l₂.lookup k
+
 theorem IsSuffix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <:+ l₂) :
     List.lookup k l₂ = none → List.lookup k l₁ = none :=
   h.sublist.lookup_eq_none
+
+grind_pattern IsSuffix.lookup_eq_none => l₁ <:+ l₂, l₁.lookup k
+grind_pattern IsSuffix.lookup_eq_none => l₁ <:+ l₂, l₂.lookup k
+
 theorem IsInfix.lookup_eq_none {l₁ l₂ : List (α × β)} (h : l₁ <:+: l₂) :
     List.lookup k l₂ = none → List.lookup k l₁ = none :=
   h.sublist.lookup_eq_none
 
+grind_pattern IsInfix.lookup_eq_none => l₁ <:+: l₂, l₁.lookup k
+grind_pattern IsInfix.lookup_eq_none => l₁ <:+: l₂, l₂.lookup k
+
 end lookup
 
 end List

src/Init/Data/List/Impl.lean

@@ -265,7 +265,7 @@ def findRev?TR (p : α → Bool) (l : List α) : Option α := l.reverse.find? p
   simp only [find?]
   split <;> simp_all
 
-@[simp] theorem find?_append {xs ys : List α} : (xs ++ ys).find? p = (xs.find? p).or (ys.find? p) := by
+@[simp, grind =] theorem find?_append {xs ys : List α} : (xs ++ ys).find? p = (xs.find? p).or (ys.find? p) := by
   induction xs with
   | nil => simp [find?]
   | cons x xs ih =>

src/Init/Data/Vector/Find.lean

@@ -44,12 +44,23 @@ theorem findSome?_singleton {a : α} {f : α → Option β} : #v[a].findSome? f
   rcases xs with ⟨xs, rfl⟩
   simp only [push_mk, findSomeRev?_mk, Array.findSomeRev?_push_of_isNone, h]
 
+@[grind =]
+theorem findSomeRev?_push {xs : Vector α n} {a : α} {f : α → Option β} :
+    (xs.push a).findSomeRev? f = (f a).or (xs.findSomeRev? f) := by
+  match h : f a with
+  | some b =>
+    rw [findSomeRev?_push_of_isSome]
+    all_goals simp_all
+  | none =>
+    rw [findSomeRev?_push_of_isNone]
+    all_goals simp_all
+
 theorem exists_of_findSome?_eq_some {f : α → Option β} {xs : Vector α n} (w : xs.findSome? f = some b) :
     ∃ a, a ∈ xs ∧ f a = some b := by
   rcases xs with ⟨xs, rfl⟩
   simpa using Array.exists_of_findSome?_eq_some (by simpa using w)
 
-@[simp] theorem findSome?_eq_none_iff {f : α → Option β} {xs : Vector α n} :
+@[simp, grind =] theorem findSome?_eq_none_iff {f : α → Option β} {xs : Vector α n} :
     xs.findSome? f = none ↔ ∀ x ∈ xs, f x = none := by
   rcases xs with ⟨xs, rfl⟩
   simp
@@ -72,24 +83,27 @@ theorem findSome?_eq_some_iff {f : α → Option β} {xs : Vector α n} {b : β}
   · rintro ⟨k₁, k₂, h, ys, a, zs, w, h₁, h₂⟩
     exact ⟨ys.toArray, a, zs.toArray, by simp [w], h₁, by simpa using h₂⟩
 
-@[simp] theorem findSome?_guard {xs : Vector α n} : findSome? (Option.guard fun x => p x) xs = find? p xs := by
+@[simp, grind =] theorem findSome?_guard {xs : Vector α n} : findSome? (Option.guard p) xs = find? p xs := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-theorem find?_eq_findSome?_guard {xs : Vector α n} : find? p xs = findSome? (Option.guard fun x => p x) xs :=
+theorem find?_eq_findSome?_guard {xs : Vector α n} : find? p xs = findSome? (Option.guard p) xs :=
   findSome?_guard.symm
 
-@[simp] theorem map_findSome? {f : α → Option β} {g : β → γ} {xs : Vector α n} :
+@[simp, grind =] theorem map_findSome? {f : α → Option β} {g : β → γ} {xs : Vector α n} :
     (xs.findSome? f).map g = xs.findSome? (Option.map g ∘ f) := by
   cases xs; simp
 
+@[grind _=_]
 theorem findSome?_map {f : β → γ} {xs : Vector β n} : findSome? p (xs.map f) = xs.findSome? (p ∘ f) := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.findSome?_map]
 
+@[grind =]
 theorem findSome?_append {xs : Vector α n₁} {ys : Vector α n₂} : (xs ++ ys).findSome? f = (xs.findSome? f).or (ys.findSome? f) := by
   cases xs; cases ys; simp [Array.findSome?_append]
 
+@[grind =]
 theorem getElem?_zero_flatten {xss : Vector (Vector α m) n} :
     (flatten xss)[0]? = xss.findSome? fun xs => xs[0]? := by
   cases xss using vector₂_induction
@@ -106,12 +120,14 @@ theorem getElem_zero_flatten.proof {xss : Vector (Vector α m) n} (h : 0 < n * m
       Option.isSome_some, and_true]
     exact ⟨⟨xss[0], h₂ _ (by simp)⟩, by simp⟩
 
+@[grind =]
 theorem getElem_zero_flatten {xss : Vector (Vector α m) n} (h : 0 < n * m) :
     (flatten xss)[0] = (xss.findSome? fun xs => xs[0]?).get (getElem_zero_flatten.proof h) := by
   have t := getElem?_zero_flatten (xss := xss)
   simp [getElem?_eq_getElem, h] at t
   simp [← t]
 
+@[grind =]
 theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a := by
   rw [replicate_eq_mk_replicate, findSome?_mk, Array.findSome?_replicate]
 
@@ -142,9 +158,9 @@ abbrev findSome?_mkVector_of_isNone := @findSome?_replicate_of_isNone
 
 /-! ### find? -/
 
-@[simp] theorem find?_empty : find? p #v[] = none := rfl
+@[simp, grind =] theorem find?_empty : find? p #v[] = none := rfl
 
-theorem find?_singleton {a : α} {p : α → Bool} :
+@[grind =]theorem find?_singleton {a : α} {p : α → Bool} :
     #v[a].find? p = if p a then some a else none := by
   simp
 
@@ -152,11 +168,23 @@ theorem find?_singleton {a : α} {p : α → Bool} :
     findRev? p (xs.push a) = some a := by
   cases xs; simp [h]
 
-@[simp] theorem findRev?_cons_of_neg {xs : Vector α n} (h : ¬p a) :
+@[simp] theorem findRev?_push_of_neg {xs : Vector α n} (h : ¬p a) :
     findRev? p (xs.push a) = findRev? p xs := by
   cases xs; simp [h]
 
-@[simp] theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
+@[deprecated findRev?_push_of_neg (since := "2025-06-12")]
+abbrev findRev?_cons_of_neg := @findRev?_push_of_neg
+
+@[grind =]
+theorem finRev?_push {xs : Vector α n} :
+    findRev? p (xs.push a) = (Option.guard p a).or (xs.findRev? p) := by
+  cases h : p a
+  · rw [findRev?_push_of_neg, Option.guard_eq_none_iff.mpr h]
+    all_goals simp [h]
+  · rw [findRev?_push_of_pos, Option.guard_eq_some_iff.mpr ⟨rfl, h⟩]
+    all_goals simp [h]
+
+@[simp, grind =] theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x := by
   cases l; simp
 
 theorem find?_eq_some_iff_append {xs : Vector α n} :
@@ -181,35 +209,38 @@ theorem find?_push_eq_some {xs : Vector α n} :
     (xs.push a).find? p = some b ↔ xs.find? p = some b ∨ (xs.find? p = none ∧ (p a ∧ a = b)) := by
   cases xs; simp
 
-@[simp] theorem find?_isSome {xs : Vector α n} {p : α → Bool} : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x := by
+@[simp, grind =] theorem find?_isSome {xs : Vector α n} {p : α → Bool} : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x := by
   cases xs; simp
 
+@[grind →]
 theorem find?_some {xs : Vector α n} (h : find? p xs = some a) : p a := by
   rcases xs with ⟨xs, rfl⟩
   simp at h
   exact Array.find?_some h
 
+@[grind →]
 theorem mem_of_find?_eq_some {xs : Vector α n} (h : find? p xs = some a) : a ∈ xs := by
   cases xs
   simp at h
   simpa using Array.mem_of_find?_eq_some h
 
+@[grind]
 theorem get_find?_mem {xs : Vector α n} (h) : (xs.find? p).get h ∈ xs := by
   cases xs
   simp [Array.get_find?_mem]
 
-@[simp] theorem find?_map {f : β → α} {xs : Vector β n} :
+@[simp, grind =] theorem find?_map {f : β → α} {xs : Vector β n} :
     find? p (xs.map f) = (xs.find? (p ∘ f)).map f := by
   cases xs; simp
 
-@[simp] theorem find?_append {xs : Vector α n₁} {ys : Vector α n₂} :
+@[simp, grind =] theorem find?_append {xs : Vector α n₁} {ys : Vector α n₂} :
     (xs ++ ys).find? p = (xs.find? p).or (ys.find? p) := by
   cases xs
   cases ys
   simp
 
-@[simp] theorem find?_flatten {xs : Vector (Vector α m) n} {p : α → Bool} :
-    xs.flatten.find? p = xs.findSome? (·.find? p) := by
+@[simp, grind =] theorem find?_flatten {xs : Vector (Vector α m) n} {p : α → Bool} :
+    xs.flatten.find? p = xs.findSome? (find? p) := by
   cases xs using vector₂_induction
   simp [Array.findSome?_map, Function.comp_def]
 
@@ -217,7 +248,7 @@ theorem find?_flatten_eq_none_iff {xs : Vector (Vector α m) n} {p : α → Bool
     xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by
   simp
 
-@[simp] theorem find?_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
+@[simp, grind =] theorem find?_flatMap {xs : Vector α n} {f : α → Vector β m} {p : β → Bool} :
     (xs.flatMap f).find? p = xs.findSome? (fun x => (f x).find? p) := by
   cases xs
   simp [Array.find?_flatMap, Array.flatMap_toArray]
@@ -227,6 +258,7 @@ theorem find?_flatMap_eq_none_iff {xs : Vector α n} {f : α → Vector β m} {p
     (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
   simp
 
+@[grind =]
 theorem find?_replicate :
     find? p (replicate n a) = if n = 0 then none else if p a then some a else none := by
   rw [replicate_eq_mk_replicate, find?_mk, Array.find?_replicate]
@@ -278,6 +310,7 @@ abbrev find?_mkVector_eq_some_iff := @find?_replicate_eq_some_iff
 @[deprecated get_find?_replicate (since := "2025-03-18")]
 abbrev get_find?_mkVector := @get_find?_replicate
 
+@[grind =]
 theorem find?_pmap {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n}
     (H : ∀ (a : α), a ∈ xs → P a) {p : β → Bool} :
     (xs.pmap f H).find? p = (xs.attach.find? (fun ⟨a, m⟩ => p (f a (H a m)))).map fun ⟨a, m⟩ => f a (H a m) := by
@@ -291,8 +324,10 @@ theorem find?_eq_some_iff_getElem {xs : Vector α n} {p : α → Bool} {b : α}
 
 /-! ### findFinIdx? -/
 
+@[grind =]
 theorem findFinIdx?_empty {p : α → Bool} : findFinIdx? p (#v[] : Vector α 0) = none := by simp
 
+@[grind =]
 theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
     #[a].findFinIdx? p = if p a then some ⟨0, by simp⟩ else none := by
   simp
@@ -302,6 +337,12 @@ theorem findFinIdx?_singleton {a : α} {p : α → Bool} :
   subst w
   simp
 
+@[simp, grind =] theorem findFinIdx?_eq_none_iff {xs : Vector α n} {p : α → Bool} :
+    xs.findFinIdx? p = none ↔ ∀ x, x ∈ xs → ¬ p x := by
+  rcases xs with ⟨xs, rfl⟩
+  simp [Array.findFinIdx?_eq_none_iff]
+
+@[grind =]
 theorem findFinIdx?_push {xs : Vector α n} {a : α} {p : α → Bool} :
     (xs.push a).findFinIdx? p =
       ((xs.findFinIdx? p).map Fin.castSucc).or (if p a then some ⟨n, by simp⟩ else none) := by
@@ -309,6 +350,7 @@ theorem findFinIdx?_push {xs : Vector α n} {a : α} {p : α → Bool} :
   simp [Array.findFinIdx?_push, Option.map_or, Function.comp_def]
   congr
 
+@[grind =]
 theorem findFinIdx?_append {xs : Vector α n₁} {ys : Vector α n₂} {p : α → Bool} :
     (xs ++ ys).findFinIdx? p =
       ((xs.findFinIdx? p).map (Fin.castLE (by simp))).or
@@ -317,13 +359,13 @@ theorem findFinIdx?_append {xs : Vector α n₁} {ys : Vector α n₂} {p : α
   rcases ys with ⟨ys, rfl⟩
   simp [Array.findFinIdx?_append, Option.map_or, Function.comp_def]
 
-@[simp]
+@[simp, grind =]
 theorem isSome_findFinIdx? {xs : Vector α n} {p : α → Bool} :
     (xs.findFinIdx? p).isSome = xs.any p := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[simp]
+@[simp, grind =]
 theorem isNone_findFinIdx? {xs : Vector α n} {p : α → Bool} :
     (xs.findFinIdx? p).isNone = xs.all (fun x => ¬ p x) := by
   rcases xs with ⟨xs, rfl⟩

tests/lean/run/grind_list_find.lean

@@ -0,0 +1,56 @@
+open List
+
+theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
+  induction l with grind
+
+theorem findSome?_isSome_iff {f : α → Option β} {l : List α} :
+    (l.findSome? f).isSome ↔ ∃ x, x ∈ l ∧ (f x).isSome := by
+  induction l with grind
+
+attribute [grind] Option.isSome_iff_ne_none -- Can we add this?
+
+theorem Sublist.findSome?_eq_none {l₁ l₂ : List α} (h : l₁ <+ l₂) :
+    l₂.findSome? f = none → l₁.findSome? f = none := by
+  grind
+
+theorem IsPrefix.findSome?_eq_none {l₁ l₂ : List α} {f : α → Option β} (h : l₁ <+: l₂) :
+    List.findSome? f l₂ = none → List.findSome? f l₁ = none := by
+  grind
+
+theorem find?_flatten_eq_none_iff {xs : List (List α)} {p : α → Bool} :
+    xs.flatten.find? p = none ↔ ∀ ys ∈ xs, ∀ x ∈ ys, !p x := by
+  grind
+
+theorem find?_flatMap_eq_none_iff {xs : List α} {f : α → List β} {p : β → Bool} :
+    (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y := by
+  grind
+
+theorem find?_replicate_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
+    (replicate n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b := by
+  grind
+
+macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
+
+example (xs : List Nat) (h : 3 ∈ xs) : (xs.find? (· ≤ 5)).isSome := by grind
+example (xs : List Nat) (h : 3 ∈ xs) : xs.findIdx (· ≤ 5) < xs.length := by grind
+example (xs : List Nat) (h : 3 ∈ xs) : xs[xs.findIdx (· ≤ 5)] < 7 := by grind
+example (xs : List Nat) (h : 3 ∈ xs) : xs[xs.findIdx (· ≤ 5)] < 5 + xs.length := by grind
+example (xs : List Nat) (h : 3 ∈ xs) : xs[xs.findIdx (· ≤ 5)] = 4 → 2 ≤ xs.length := by
+  grind [cases List]
+
+example (xs : List Nat) (h : ∀ x, x ∈ xs → x > 7) : xs.find? (· ≤ 5) = none := by grind
+example (xs : List Nat) (h : ∀ x, x ∈ xs → x > 7) : xs.findIdx (· ≤ 5) = xs.length := by grind
+
+/-- If `¬ p xs[j]` for all `j < i`, then `i ≤ xs.findIdx p`. -/
+theorem le_findIdx_of_not {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length)
+    (h2 : ∀ j (hji : j < i), p (xs[j]'(Nat.lt_trans hji h)) = false) : i ≤ xs.findIdx p := by
+  grind
+
+/-- If `¬ p xs[j]` for all `j ≤ i`, then `i < xs.findIdx p`. -/
+theorem lt_findIdx_of_not {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.length)
+    (h2 : ∀ j (hji : j ≤ i), ¬p (xs[j]'(Nat.lt_of_le_of_lt hji h))) : i < xs.findIdx p := by
+  grind
+
+theorem Sublist.findIdx?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
+    (l₁.findIdx? p).isSome → (l₂.findIdx? p).isSome := by
+  grind