From 01ed345643bd6e08ff5f06df993d9a3c8d8fe64c Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Thu, 11 Sep 2025 16:09:52 +1000
Subject: [PATCH] chore: more review of `@[grind]` annotations (#10340)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR completes the review of `@[grind]` annotations without a sigil
(e.g. `=` or `←`), replacing most of them with more specific annotations
or patterns.

---------

Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
---
 src/Init/Data/Array/Find.lean         |   3 +-
 src/Init/Data/Array/Lemmas.lean       |  10 +++
 src/Init/Data/List/Attach.lean        |   3 +-
 src/Init/Data/List/Basic.lean         |   8 +-
 src/Init/Data/List/Count.lean         |   6 +-
 src/Init/Data/List/Erase.lean         |  10 +--
 src/Init/Data/List/Find.lean          |   3 +-
 src/Init/Data/List/Lemmas.lean        | 120 +++++++++++++-------------
 src/Init/Data/List/Nat/Range.lean     |   3 +-
 src/Init/Data/List/Pairwise.lean      |  16 ++--
 src/Init/Data/List/Sublist.lean       | 101 +++++++++++++++-------
 src/Init/Data/Option/Attach.lean      |   2 +-
 src/Init/Data/Option/Lemmas.lean      |   2 +-
 src/Init/Data/Order/Ord.lean          |   2 +-
 src/Init/Data/Vector/Attach.lean      |   3 +-
 src/Init/Data/Vector/Find.lean        |   5 +-
 src/Init/Data/Vector/Lemmas.lean      |  87 +++++++++++--------
 src/Std/Data/DTreeMap/Lemmas.lean     |   4 +-
 src/Std/Data/DTreeMap/Raw/Lemmas.lean |   6 +-
 src/Std/Data/ExtDTreeMap/Lemmas.lean  |   4 +-
 src/Std/Data/ExtHashSet/Lemmas.lean   |   2 +-
 src/Std/Data/ExtTreeMap/Lemmas.lean   |   4 +-
 src/Std/Data/ExtTreeSet/Lemmas.lean   |  12 +--
 src/Std/Data/TreeMap/Lemmas.lean      |   4 +-
 src/Std/Data/TreeMap/Raw/Lemmas.lean  |   2 +-
 src/Std/Data/TreeSet/Lemmas.lean      |  12 +--
 src/Std/Data/TreeSet/Raw/Lemmas.lean  |   8 +-
 27 files changed, 255 insertions(+), 187 deletions(-)

diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean
index f1b26f1553..1565cea39b 100644
--- a/src/Init/Data/Array/Find.lean
+++ b/src/Init/Data/Array/Find.lean
@@ -228,11 +228,12 @@ theorem mem_of_find?_eq_some {xs : Array α} (h : find? p xs = some a) : a ∈ x
   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]
 
+grind_pattern get_find?_mem => (xs.find? p).get h
+
 @[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
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index f228abdd7e..f19730f92f 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -380,6 +380,12 @@ theorem not_mem_empty (a : α) : ¬ a ∈ #[] := by simp
 theorem mem_or_eq_of_mem_push {a b : α} {xs : Array α} :
     a ∈ xs.push b → a ∈ xs ∨ a = b := Array.mem_push.mp
 
+-- This pattern may be excessively general:
+-- it fires anytime we ae thinking about membership of arrays,
+-- and constructing a list via `push`, even if the elements are unrelated.
+-- Nevertheless in practice it is quite helpful!
+grind_pattern mem_or_eq_of_mem_push => xs.push b, a ∈ xs
+
 theorem mem_push_self {xs : Array α} {x : α} : x ∈ xs.push x :=
   mem_push.2 (Or.inr rfl)
 
@@ -3771,6 +3777,10 @@ theorem contains_iff_exists_mem_beq [BEq α] {xs : Array α} {a : α} :
   rcases xs with ⟨xs⟩
   simp [List.contains_iff_exists_mem_beq]
 
+-- We add this as a `grind` lemma because it is useful without `LawfulBEq α`.
+-- With `LawfulBEq α`, it would be better to use `contains_iff_mem` directly.
+grind_pattern contains_iff_exists_mem_beq => xs.contains a
+
 @[grind _=_]
 theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Array α} {a : α} :
     xs.contains a ↔ a ∈ xs := by
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index a82aee8fcd..47bddfcefd 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -192,12 +192,13 @@ theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H b} :
     b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b := by
   simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]
 
-@[grind]
 theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {l H} {a} (h : a ∈ l) :
     f a (H a h) ∈ pmap f l H := by
   rw [mem_pmap]
   exact ⟨a, h, rfl⟩
 
+grind_pattern mem_pmap_of_mem => _ ∈ pmap f l H, a ∈ l
+
 @[simp, grind =]
 theorem length_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H} : (pmap f l H).length = l.length := by
   induction l
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 2e942b0f03..a8631f9bee 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -538,7 +538,7 @@ Example:
     | some b => b :: filterMap f as
 
 @[simp, grind =] theorem filterMap_nil {f : α → Option β} : filterMap f [] = [] := rfl
-@[grind] theorem filterMap_cons {f : α → Option β} {a : α} {l : List α} :
+@[grind =] theorem filterMap_cons {f : α → Option β} {a : α} {l : List α} :
     filterMap f (a :: l) =
       match f a with
       | none => filterMap f l
@@ -749,7 +749,7 @@ def replicate : (n : Nat) → (a : α) → List α
   | n+1, a => a :: replicate n a
 
 @[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
+@[grind =] theorem replicate_succ {a : α} {n : Nat} : replicate (n+1) a = a :: replicate n a := rfl
 
 @[simp, grind =] theorem length_replicate {n : Nat} {a : α} : (replicate n a).length = n := by
   induction n with
@@ -1440,7 +1440,7 @@ def replace [BEq α] : (l : List α) → (a : α) → (b : α) → List α
     | false => a :: replace as b c
 
 @[simp, grind =] theorem replace_nil [BEq α] : ([] : List α).replace a b = [] := rfl
-@[grind] theorem replace_cons [BEq α] {a : α} :
+@[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
 
@@ -1649,7 +1649,7 @@ def findSome? (f : α → Option β) : List α → Option β
     | none   => findSome? f as
 
 @[simp, grind =] theorem findSome?_nil : ([] : List α).findSome? f = none := rfl
-@[grind] theorem findSome?_cons {f : α → Option β} :
+@[grind =] theorem findSome?_cons {f : α → Option β} :
     (a::as).findSome? f = match f a with | some b => some b | none => as.findSome? f :=
   rfl
 
diff --git a/src/Init/Data/List/Count.lean b/src/Init/Data/List/Count.lean
index 623f89686f..f17ba363ef 100644
--- a/src/Init/Data/List/Count.lean
+++ b/src/Init/Data/List/Count.lean
@@ -223,7 +223,7 @@ variable [BEq α]
 
 @[simp, grind =] theorem count_nil {a : α} : count a [] = 0 := rfl
 
-@[grind]
+@[grind =]
 theorem count_cons {a b : α} {l : List α} :
     count a (b :: l) = count a l + if b == a then 1 else 0 := by
   simp [count, countP_cons]
@@ -237,7 +237,7 @@ theorem count_eq_countP' {a : α} : count a = countP (· == a) := by
 theorem count_eq_length_filter {a : α} {l : List α} : count a l = (filter (· == a) l).length := by
   simp [count, countP_eq_length_filter]
 
-@[grind]
+@[grind =]
 theorem count_tail : ∀ {l : List α} {a : α},
       l.tail.count a = l.count a - if l.head? == some a then 1 else 0
   | [], a => by simp
@@ -380,7 +380,7 @@ theorem count_filterMap {α} [BEq β] {b : β} {f : α → Option β} {l : List
 theorem count_flatMap {α} [BEq β] {l : List α} {f : α → List β} {x : β} :
     count x (l.flatMap f) = sum (map (count x ∘ f) l) := countP_flatMap
 
-@[grind]
+@[grind =]
 theorem count_erase {a b : α} :
     ∀ {l : List α}, count a (l.erase b) = count a l - if b == a then 1 else 0
   | [] => by simp
diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean
index e10f36e5f1..00bea55bc5 100644
--- a/src/Init/Data/List/Erase.lean
+++ b/src/Init/Data/List/Erase.lean
@@ -508,7 +508,7 @@ theorem Nodup.not_mem_erase [LawfulBEq α] {a : α} (h : Nodup l) : a ∉ l.eras
 -- Only activate `not_mem_erase` when `l.Nodup` is already available.
 grind_pattern List.Nodup.not_mem_erase => a ∈ l.erase a, l.Nodup
 
-@[grind]
+@[grind ←]
 theorem Nodup.erase [LawfulBEq α] (a : α) : Nodup l → Nodup (l.erase a) :=
   Pairwise.erase a
 
@@ -578,21 +578,21 @@ theorem eraseIdx_ne_nil_iff {l : List α} {i : Nat} : eraseIdx l i ≠ [] ↔ 2
   | [a]
   | a::b::l => simp
 
-
-
-@[grind]
 theorem eraseIdx_sublist : ∀ (l : List α) (k : Nat), eraseIdx l k <+ l
   | [], _ => by simp
   | a::l, 0 => by simp
   | a::l, k + 1 => by simp [eraseIdx_sublist]
 
+grind_pattern eraseIdx_sublist => l.eraseIdx k, _ <+ l
+
 theorem mem_of_mem_eraseIdx {l : List α} {i : Nat} {a : α} (h : a ∈ l.eraseIdx i) : a ∈ l :=
   (eraseIdx_sublist _ _).mem h
 
-@[grind]
 theorem eraseIdx_subset {l : List α} {k : Nat} : eraseIdx l k ⊆ l :=
   (eraseIdx_sublist _ _).subset
 
+grind_pattern eraseIdx_sublist => l.eraseIdx k, _ ⊆ l
+
 @[simp]
 theorem eraseIdx_eq_self : ∀ {l : List α} {k : Nat}, eraseIdx l k = l ↔ length l ≤ k
   | [], _ => by simp
diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index 213d108be3..da9c95daa4 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -293,7 +293,6 @@ theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
     · 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
@@ -305,6 +304,8 @@ theorem get_find?_mem {xs : List α} {p : α → Bool} (h) : (xs.find? p).get h
       right
       apply ih
 
+grind_pattern get_find?_mem => (xs.find? p).get h
+
 @[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
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 5d4af7d0c8..3a33e1a81f 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -306,7 +306,7 @@ theorem getD_getElem? {l : List α} {i : Nat} {d : α} :
   match i, h with
   | 0, _ => rfl
 
-@[grind]
+@[grind =]
 theorem getElem?_singleton {a : α} {i : Nat} : [a][i]? = if i = 0 then some a else none := by
   simp [getElem?_cons]
 
@@ -382,14 +382,20 @@ theorem get!_eq_getElem! [Inhabited α] (l : List α) (i) : l.get! i = l[i]! :=
 
 @[simp] theorem not_mem_nil {a : α} : ¬ a ∈ [] := nofun
 
-@[simp] theorem mem_cons : a ∈ b :: l ↔ a = b ∨ a ∈ l :=
+@[simp, grind =] theorem mem_cons : a ∈ b :: l ↔ a = b ∨ a ∈ l :=
   ⟨fun h => by cases h <;> simp [Membership.mem, *],
    fun | Or.inl rfl => by constructor | Or.inr h => by constructor; assumption⟩
 
-@[grind] theorem eq_or_mem_of_mem_cons {a b : α} {l : List α} :
+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 ..
+-- This pattern may be excessively general:
+-- it fires anytime we ae thinking about membership of lists,
+-- and constructing a list via `cons`, even if the elements are unrelated.
+-- Nevertheless in practice it is quite helpful!
+grind_pattern eq_or_mem_of_mem_cons => b :: l, a ∈ l
+
+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
@@ -411,7 +417,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⟩
 
-@[grind] theorem mem_cons_of_mem (y : α) {a : α} {l : List α} : a ∈ l → a ∈ y :: l := .tail _
+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`.
@@ -605,7 +611,7 @@ theorem decide_forall_mem {l : List α} {p : α → Prop} [DecidablePred p] :
 @[simp] theorem all_eq_false {l : List α} : l.all p = false ↔ ∃ x, x ∈ l ∧ ¬p x := by
   simp [all_eq]
 
-@[grind] theorem any_beq [BEq α] {l : List α} {a : α} : (l.any fun x => a == x) = l.contains a := by
+theorem any_beq [BEq α] {l : List α} {a : α} : (l.any fun x => a == x) = l.contains a := by
   induction l <;> simp_all [contains_cons]
 
 /-- Variant of `any_beq` with `==` reversed. -/
@@ -613,7 +619,7 @@ theorem any_beq' [BEq α] [PartialEquivBEq α] {l : List α} :
     (l.any fun x => x == a) = l.contains a := by
   simp only [BEq.comm, any_beq]
 
-@[grind] theorem all_bne [BEq α] {l : List α} : (l.all fun x => a != x) = !l.contains a := by
+theorem all_bne [BEq α] {l : List α} : (l.all fun x => a != x) = !l.contains a := by
   induction l <;> simp_all [bne]
 
 /-- Variant of `all_bne` with `!=` reversed. -/
@@ -670,14 +676,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)]
 
-@[grind] 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]
 
-@[grind] 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
@@ -825,7 +831,7 @@ theorem length_eq_of_beq [BEq α] {l₁ l₂ : List α} (h : l₁ == l₂) : l
 
 /-! ### getLast -/
 
-@[grind]
+@[grind =]
 theorem getLast_eq_getElem : ∀ {l : List α} (h : l ≠ []),
     getLast l h = l[l.length - 1]'(by
       match l with
@@ -888,7 +894,7 @@ theorem getLast?_eq_getLast : ∀ {l : List α} h, l.getLast? = some (l.getLast
   | [], h => nomatch h rfl
   | _ :: _, _ => rfl
 
-@[grind] 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]
@@ -901,14 +907,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]
+@[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]
+@[grind =]
 theorem getLast?_concat {l : List α} {a : α} : (l ++ [a]).getLast? = some a := by
   simp [getLast?_eq_getElem?, Nat.succ_sub_succ]
 
@@ -927,7 +933,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]
+@[grind =]
 theorem getLast!_eq_getElem! [Inhabited α] {l : List α} : l.getLast! = l[l.length - 1]! := by
   cases l with
   | nil => simp
@@ -955,7 +961,7 @@ theorem head?_eq_getElem? : ∀ {l : List α}, l.head? = l[0]?
 
 theorem head_singleton {a : α} : head [a] (by simp) = a := by simp
 
-@[grind]
+@[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
@@ -1276,7 +1282,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]
 
-@[grind] 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 [*]
 
@@ -1330,10 +1336,12 @@ theorem forall_mem_filter {l : List α} {p : α → Bool} {P : α → Prop} :
     (∀ (i) (_ : i ∈ l.filter p), P i) ↔ ∀ (j) (_ : j ∈ l), p j → P j := by
   simp
 
-@[grind] theorem getElem_filter {xs : List α} {p : α → Bool} {i : Nat} (h : i < (xs.filter p).length) :
+theorem getElem_filter {xs : List α} {p : α → Bool} {i : Nat} (h : i < (xs.filter p).length) :
     p (xs.filter p)[i] :=
   (mem_filter.mp (getElem_mem h)).2
 
+grind_pattern getElem_filter => (xs.filter p)[i]
+
 theorem getElem?_filter {xs : List α} {p : α → Bool} {i : Nat} (h : i < (xs.filter p).length)
     (w : (xs.filter p)[i]? = some a) : p a := by
   rw [getElem?_eq_getElem] at w
@@ -1477,14 +1485,14 @@ theorem filterMap_eq_filter {p : α → Bool} :
   | nil => rfl
   | cons a l IH => by_cases pa : p a <;> simp [Option.guard, pa, ← IH]
 
-@[grind]
+@[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]
+@[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]
@@ -1611,7 +1619,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]
 
-@[grind] 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']
@@ -1630,7 +1638,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₁)]
 
-@[grind] 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
@@ -1743,7 +1751,7 @@ theorem append_eq_append_iff {ws xs ys zs : List α} :
   match l, w₂ with
   | a :: l, _ => rfl
 
-@[grind] 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])
@@ -1771,21 +1779,21 @@ theorem head_append_right {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) (h : l
 -- `getLast_append_of_ne_nil`, `getLast_append` and `getLast?_append`
 -- are stated and proved later in the `reverse` section.
 
-@[grind] 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
 
-@[grind] 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]
 
-@[grind] 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
@@ -1916,7 +1924,7 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ l' b, l = concat l' b
   | cons =>
     simp [flatten, length_append, *]
 
-@[grind] 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
@@ -2118,7 +2126,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 [*]
 
-@[grind] 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
@@ -2200,7 +2208,7 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
     (replicate n a)[i] = a :=
   eq_of_mem_replicate (getElem_mem _)
 
-@[grind] 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]
@@ -2208,7 +2216,7 @@ theorem forall_mem_replicate {p : α → Prop} {a : α} {n} :
 @[simp] theorem getElem?_replicate_of_lt {n : Nat} {i : Nat} (h : i < n) : (replicate n a)[i]? = some a := by
   simp [h]
 
-@[grind] 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
@@ -2297,7 +2305,7 @@ theorem replicate_eq_append_iff {l₁ l₂ : List α} {a : α} :
   simp only [getElem?_map, getElem?_replicate]
   split <;> simp
 
-@[grind] 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 =>
@@ -2533,10 +2541,10 @@ theorem flatten_reverse {L : List (List α)} :
     L.reverse.flatten = (L.map reverse).flatten.reverse := by
   induction L <;> simp_all
 
-@[grind] 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
 
-@[grind] 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 :=
@@ -2598,9 +2606,7 @@ theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
 
 /-! ### foldl and foldr -/
 
--- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
--- foldr_cons_eq_append: [@foldr #4 (List #3) _ #0 #2, @map _ _ #1 #2]
-@[simp, grind] theorem foldr_cons_eq_append {l : List α} {f : α → β} {l' : List β} :
+@[simp] 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 [*]
 
@@ -2609,34 +2615,28 @@ theorem id_run_foldrM {f : α → β → Id β} {b : β} {l : List α} :
     l.foldr cons l' = l ++ l' := by
   induction l <;> simp [*]
 
--- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
--- foldl_flip_cons_eq_append: [@foldl (List #3) #4 _ #0 #2, @map _ _ #1 #2]
-@[simp, grind] theorem foldl_flip_cons_eq_append {l : List α} {f : α → β} {l' : List β} :
+@[simp] 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 [*]
 
 /-- Variant of `foldl_flip_cons_eq_append` specalized to `f = id`. -/
-@[grind] theorem foldl_flip_cons_eq_append' {l l' : List α} :
+theorem foldl_flip_cons_eq_append' {l l' : List α} :
     l.foldl (fun xs y => y :: xs) l' = l.reverse ++ l' := by
   simp
 
--- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem foldr_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
+@[simp] theorem foldr_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
     l.foldr (f · ++ ·) l' = (l.map f).flatten ++ l' := by
   induction l <;> simp [*]
 
--- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem foldl_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
+@[simp] 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 [*]
 
--- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem foldr_flip_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
+@[simp] 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 [*]
 
--- TODO: a multi-pattern is being selected there because E-matching does not go inside lambdas.
-@[simp, grind] theorem foldl_flip_append_eq_append {l : List α} {f : α → List β} {l' : List β} :
+@[simp] 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 [*]
 
@@ -2690,11 +2690,11 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
 @[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, -foldrM_pure]
 
-@[grind] 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
 
-@[grind] 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
 
@@ -2899,7 +2899,7 @@ theorem head_eq_getLast_reverse {l : List α} (h : l ≠ []) :
   simp only [getLast_eq_head_reverse, reverse_append]
   rw [head_append_of_ne_nil]
 
-@[grind] 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])
@@ -2985,6 +2985,10 @@ theorem contains_iff_exists_mem_beq [BEq α] {l : List α} {a : α} :
     l.contains a ↔ ∃ a' ∈ l, a == a' := by
   induction l <;> simp_all
 
+-- We add this as a `grind` lemma because it is useful without `LawfulBEq α`.
+-- With `LawfulBEq α`, it would be better to use `contains_iff_mem` directly.
+grind_pattern contains_iff_exists_mem_beq => l.contains a
+
 @[grind _=_]
 theorem contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     l.contains a ↔ a ∈ l := by
@@ -3078,7 +3082,7 @@ are often used for theorems about `Array.pop`.
   | _ :: _ :: _, 0, _ => rfl
   | _ :: _ :: _, _ + 1, h => getElem_dropLast (Nat.add_one_lt_add_one_iff.mp h)
 
-@[grind] 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]
@@ -3350,7 +3354,7 @@ variable [BEq α]
     simp only [replace_cons]
     split <;> simp_all
 
-@[grind] 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
@@ -3363,7 +3367,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]
 
-@[grind] 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]
@@ -3393,7 +3397,7 @@ theorem head_replace {l : List α} {a b : α} (w) :
   apply Option.some.inj
   rw [← head?_eq_head, head?_replace, head?_eq_head]
 
-@[grind] 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
@@ -3480,7 +3484,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
 
-@[grind] 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
 
@@ -3515,13 +3519,13 @@ theorem getElem?_insert_succ {l : List α} {a : α} {i : Nat} :
   simp only [insert_eq]
   split <;> simp
 
-@[grind] 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]
 
-@[grind] 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
@@ -3545,7 +3549,7 @@ theorem head_insert {l : List α} {a : α} (w) :
   apply Option.some.inj
   rw [← head?_eq_head, head?_insert]
 
-@[grind] 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
diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean
index 22cc521575..3a38a61943 100644
--- a/src/Init/Data/List/Nat/Range.lean
+++ b/src/Init/Data/List/Nat/Range.lean
@@ -248,11 +248,10 @@ theorem pairwise_le_range {n : Nat} : Pairwise (· ≤ ·) (range n) :=
 theorem nodup_range {n : Nat} : Nodup (range n) := by
   simp +decide only [range_eq_range', nodup_range']
 
-@[simp, grind =] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
+@[simp] theorem find?_range_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
     (range n).find? p = some i ↔ p i ∧ i ∈ range n ∧ ∀ j, j < i → !p j := by
   simp [range_eq_range']
 
-@[grind]
 theorem find?_range_eq_none {n : Nat} {p : Nat → Bool} :
     (range n).find? p = none ↔ ∀ i, i < n → !p i := by
   simp
diff --git a/src/Init/Data/List/Pairwise.lean b/src/Init/Data/List/Pairwise.lean
index b03e318b1e..b8a5e31373 100644
--- a/src/Init/Data/List/Pairwise.lean
+++ b/src/Init/Data/List/Pairwise.lean
@@ -43,7 +43,7 @@ theorem rel_of_pairwise_cons (p : (a :: l).Pairwise R) : ∀ {a'}, a' ∈ l →
   (pairwise_cons.1 p).2
 
 set_option linter.unusedVariables false in
-@[grind] theorem Pairwise.tail : ∀ {l : List α} (h : Pairwise R l), Pairwise R l.tail
+@[grind ←] theorem Pairwise.tail : ∀ {l : List α} (h : Pairwise R l), Pairwise R l.tail
   | [], h => h
   | _ :: _, h => h.of_cons
 
@@ -103,7 +103,7 @@ theorem Pairwise.forall_of_forall_of_flip (h₁ : ∀ x ∈ l, R x x) (h₂ : Pa
     · exact h₃.1 _ hx
     · exact ih (fun x hx => h₁ _ <| mem_cons_of_mem _ hx) h₂.2 h₃.2 hx hy
 
-@[grind] theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by simp
+@[grind ←] theorem pairwise_singleton (R) (a : α) : Pairwise R [a] := by simp
 
 @[grind =] theorem pairwise_pair {a b : α} : Pairwise R [a, b] ↔ R a b := by simp
 
@@ -117,7 +117,7 @@ theorem Pairwise.of_map {S : β → β → Prop} (f : α → β) (H : ∀ a b :
     (p : Pairwise S (map f l)) : Pairwise R l :=
   (pairwise_map.1 p).imp (H _ _)
 
-@[grind] theorem Pairwise.map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b))
+@[grind <=] theorem Pairwise.map {S : β → β → Prop} (f : α → β) (H : ∀ a b : α, R a b → S (f a) (f b))
     (p : Pairwise R l) : Pairwise S (map f l) :=
   pairwise_map.2 <| p.imp (H _ _)
 
@@ -136,7 +136,7 @@ theorem Pairwise.of_map {S : β → β → Prop} (f : α → β) (H : ∀ a b :
     simpa [IH, e] using fun _ =>
       ⟨fun h a ha b hab => h _ _ ha hab, fun h a b ha hab => h _ ha _ hab⟩
 
-@[grind] theorem Pairwise.filterMap {S : β → β → Prop} (f : α → Option β)
+@[grind <=] theorem Pairwise.filterMap {S : β → β → Prop} (f : α → Option β)
     (H : ∀ a a' : α, R a a' → ∀ b, f a = some b → ∀ b', f a' = some b' → S b b') {l : List α} (p : Pairwise R l) :
     Pairwise S (filterMap f l) :=
   pairwise_filterMap.2 <| p.imp (H _ _)
@@ -146,7 +146,7 @@ theorem Pairwise.of_map {S : β → β → Prop} (f : α → β) (H : ∀ a b :
   rw [← filterMap_eq_filter, pairwise_filterMap]
   simp
 
-@[grind] theorem Pairwise.filter (p : α → Bool) : Pairwise R l → Pairwise R (filter p l) :=
+@[grind ←] theorem Pairwise.filter (p : α → Bool) : Pairwise R l → Pairwise R (filter p l) :=
   Pairwise.sublist filter_sublist
 
 @[grind =] theorem pairwise_append {l₁ l₂ : List α} :
@@ -207,10 +207,10 @@ theorem pairwise_append_comm {R : α → α → Prop} (s : ∀ {x y}, R x y →
         simp
       · exact ⟨fun _ => h, Or.inr h⟩
 
-@[grind] theorem Pairwise.drop {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.drop i) :=
+@[grind ←] theorem Pairwise.drop {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.drop i) :=
   h.sublist (drop_sublist _ _)
 
-@[grind] theorem Pairwise.take {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take i) :=
+@[grind ←] theorem Pairwise.take {l : List α} {i : Nat} (h : List.Pairwise R l) : List.Pairwise R (l.take i) :=
   h.sublist (take_sublist _ _)
 
 -- This theorem is not annotated with `grind` because it leads to a loop of instantiations with `Pairwise.sublist`.
@@ -266,7 +266,7 @@ theorem pairwise_of_forall_mem_list {l : List α} {r : α → α → Prop} (h :
     rintro H _ b hb rfl
     exact H b hb _ _
 
-@[grind] theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α → Prop} {f : ∀ a, p a → β}
+@[grind <=] theorem Pairwise.pmap {l : List α} (hl : Pairwise R l) {p : α → Prop} {f : ∀ a, p a → β}
     (h : ∀ x ∈ l, p x) {S : β → β → Prop}
     (hS : ∀ ⦃x⦄ (hx : p x) ⦃y⦄ (hy : p y), R x y → S (f x hx) (f y hy)) :
     Pairwise S (l.pmap f h) := by
diff --git a/src/Init/Data/List/Sublist.lean b/src/Init/Data/List/Sublist.lean
index 55a4e27a64..949e2ab1d9 100644
--- a/src/Init/Data/List/Sublist.lean
+++ b/src/Init/Data/List/Sublist.lean
@@ -202,12 +202,18 @@ theorem sublist_or_mem_of_sublist (h : l <+ l₁ ++ a :: l₂) : l <+ l₁ ++ l
 protected theorem Sublist.mem (hx : a ∈ l₁) (hl : l₁ <+ l₂) : a ∈ l₂ :=
   hl.subset hx
 
-@[grind] theorem Sublist.head_mem (s : ys <+ xs) (h) : ys.head h ∈ xs :=
+theorem Sublist.head_mem (s : ys <+ xs) (h) : ys.head h ∈ xs :=
   s.mem (List.head_mem h)
 
-@[grind] theorem Sublist.getLast_mem (s : ys <+ xs) (h) : ys.getLast h ∈ xs :=
+grind_pattern Sublist.head_mem => ys <+ xs, ys.head h
+grind_pattern Sublist.head_mem => ys.head h ∈ xs -- This is somewhat aggressive, as it initiates sublist based reasoning.
+
+theorem Sublist.getLast_mem (s : ys <+ xs) (h) : ys.getLast h ∈ xs :=
   s.mem (List.getLast_mem h)
 
+grind_pattern Sublist.getLast_mem => ys <+ xs, ys.getLast h
+grind_pattern Sublist.getLast_mem => ys.getLast h ∈ xs -- This is somewhat aggressive, as it initiates sublist based reasoning.
+
 instance : Trans (@Sublist α) Subset Subset :=
   ⟨fun h₁ h₂ => trans h₁.subset h₂⟩
 
@@ -248,12 +254,13 @@ theorem Sublist.eq_of_length_le (s : l₁ <+ l₂) (h : length l₂ ≤ length l
 theorem Sublist.length_eq (s : l₁ <+ l₂) : length l₁ = length l₂ ↔ l₁ = l₂ :=
   ⟨s.eq_of_length, congrArg _⟩
 
-@[grind]
 theorem tail_sublist : ∀ l : List α, tail l <+ l
   | [] => .slnil
   | a::l => sublist_cons_self a l
 
-@[grind]
+grind_pattern tail_sublist => tail l <+ _
+
+@[grind ←]
 protected theorem Sublist.tail : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → tail l₁ <+ tail l₂
   | _, _, slnil => .slnil
   | _, _, Sublist.cons _ h => (tail_sublist _).trans h
@@ -263,7 +270,7 @@ protected theorem Sublist.tail : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → tai
 theorem Sublist.of_cons_cons {l₁ l₂ : List α} {a b : α} (h : a :: l₁ <+ b :: l₂) : l₁ <+ l₂ :=
   h.tail
 
-@[grind]
+@[grind ←]
 protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : map f l₁ <+ map f l₂ := by
   induction s with
   | slnil => simp
@@ -275,7 +282,7 @@ protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : m
 grind_pattern Sublist.map => l₁ <+ l₂, map f l₁
 grind_pattern Sublist.map => l₁ <+ l₂, map f l₂
 
-@[grind]
+@[grind ←]
 protected theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) :
     filterMap f l₁ <+ filterMap f l₂ := by
   induction s <;> simp [filterMap_cons] <;> split <;> simp [*, cons]
@@ -283,7 +290,7 @@ protected theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) :
 grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₁
 grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₂
 
-@[grind]
+@[grind ←]
 protected theorem Sublist.filter (p : α → Bool) {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂ := by
   rw [← filterMap_eq_filter]; apply s.filterMap
 
@@ -481,7 +488,7 @@ theorem Sublist.of_sublist_append_right (w : ∀ a, a ∈ l → a ∉ l₁) (h :
     exact fun x m => w x (mem_append_left l₂' m) (h₁.mem m)
   simp_all
 
-@[grind]
+@[grind ←]
 theorem Sublist.middle {l : List α} (h : l <+ l₁ ++ l₂) (a : α) : l <+ l₁ ++ a :: l₂ := by
   rw [sublist_append_iff] at h
   obtain ⟨l₁', l₂', rfl, h₁, h₂⟩ := h
@@ -624,7 +631,7 @@ theorem flatten_sublist_iff {L : List (List α)} {l} :
 instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂) :=
   decidable_of_iff (l₁.isSublist l₂) isSublist_iff_sublist
 
-@[grind]
+@[grind ←]
 protected theorem Sublist.drop : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ∀ i, l₁.drop i <+ l₂.drop i
   | _, _, h, 0 => h
   | _, _, h, i + 1 => by rw [← drop_tail, ← drop_tail]; exact h.tail.drop i
@@ -1108,24 +1115,36 @@ theorem infix_of_mem_flatten : ∀ {L : List (List α)}, l ∈ L → l <:+: flat
 theorem prefix_cons_inj (a) : a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂ :=
   prefix_append_right_inj [a]
 
-@[grind] theorem take_prefix (i) (l : List α) : take i l <+: l :=
+theorem take_prefix (i) (l : List α) : take i l <+: l :=
   ⟨_, take_append_drop _ _⟩
 
-@[grind] theorem drop_suffix (i) (l : List α) : drop i l <:+ l :=
+grind_pattern take_prefix => take i l <+: _
+
+theorem drop_suffix (i) (l : List α) : drop i l <:+ l :=
   ⟨_, take_append_drop _ _⟩
 
-@[grind] theorem take_sublist (i) (l : List α) : take i l <+ l :=
+grind_pattern drop_suffix => drop i l <+: _
+
+theorem take_sublist (i) (l : List α) : take i l <+ l :=
   (take_prefix i l).sublist
 
-@[grind] theorem drop_sublist (i) (l : List α) : drop i l <+ l :=
+grind_pattern take_sublist => take i l <+ l
+
+theorem drop_sublist (i) (l : List α) : drop i l <+ l :=
   (drop_suffix i l).sublist
 
+grind_pattern drop_sublist => drop i l <+ l
+
 theorem take_subset (i) (l : List α) : take i l ⊆ l :=
   (take_sublist i l).subset
 
+grind_pattern take_subset => take i l ⊆ l
+
 theorem drop_subset (i) (l : List α) : drop i l ⊆ l :=
   (drop_sublist i l).subset
 
+grind_pattern drop_subset => drop i l ⊆ l
+
 theorem mem_of_mem_take {l : List α} (h : a ∈ l.take i) : a ∈ l :=
   take_subset _ _ h
 
@@ -1138,64 +1157,84 @@ theorem drop_suffix_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : drop j l
 
 -- See `Init.Data.List.Nat.TakeDrop` for `take_prefix_take_left`.
 
-@[grind] theorem drop_sublist_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : drop j l <+ drop i l :=
+@[grind ←] theorem drop_sublist_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : drop j l <+ drop i l :=
   (drop_suffix_drop_left l h).sublist
 
-@[grind] theorem drop_subset_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : drop j l ⊆ drop i l :=
+@[grind ←] theorem drop_subset_drop_left (l : List α) {i j : Nat} (h : i ≤ j) : drop j l ⊆ drop i l :=
   (drop_sublist_drop_left l h).subset
 
-@[grind] theorem takeWhile_prefix (p : α → Bool) : l.takeWhile p <+: l :=
+theorem takeWhile_prefix (p : α → Bool) : l.takeWhile p <+: l :=
   ⟨l.dropWhile p, takeWhile_append_dropWhile⟩
 
-@[grind] theorem dropWhile_suffix (p : α → Bool) : l.dropWhile p <:+ l :=
+grind_pattern takeWhile_prefix => l.takeWhile p <+: _
+
+theorem dropWhile_suffix (p : α → Bool) : l.dropWhile p <:+ l :=
   ⟨l.takeWhile p, takeWhile_append_dropWhile⟩
 
-@[grind] theorem takeWhile_sublist (p : α → Bool) : l.takeWhile p <+ l :=
+grind_pattern dropWhile_suffix => l.dropWhile p <+: _
+
+theorem takeWhile_sublist (p : α → Bool) : l.takeWhile p <+ l :=
   (takeWhile_prefix p).sublist
 
-@[grind] theorem dropWhile_sublist (p : α → Bool) : l.dropWhile p <+ l :=
+grind_pattern takeWhile_sublist => l.takeWhile p <+ _
+
+theorem dropWhile_sublist (p : α → Bool) : l.dropWhile p <+ l :=
   (dropWhile_suffix p).sublist
 
+grind_pattern dropWhile_sublist => l.dropWhile p <+ _
+
 theorem takeWhile_subset {l : List α} (p : α → Bool) : l.takeWhile p ⊆ l :=
   (takeWhile_sublist p).subset
 
+grind_pattern takeWhile_subset => l.takeWhile p ⊆ _
+
 theorem dropWhile_subset {l : List α} (p : α → Bool) : l.dropWhile p ⊆ l :=
   (dropWhile_sublist p).subset
 
-@[grind] theorem dropLast_prefix : ∀ l : List α, l.dropLast <+: l
+grind_pattern dropWhile_subset => l.dropWhile p ⊆ _
+
+theorem dropLast_prefix : ∀ l : List α, l.dropLast <+: l
   | [] => ⟨nil, by rw [dropLast, List.append_nil]⟩
   | a :: l => ⟨_, dropLast_concat_getLast (cons_ne_nil a l)⟩
 
-@[grind] theorem dropLast_sublist (l : List α) : l.dropLast <+ l :=
+grind_pattern dropLast_prefix => l.dropLast <+: _
+
+theorem dropLast_sublist (l : List α) : l.dropLast <+ l :=
   (dropLast_prefix l).sublist
 
+grind_pattern dropLast_sublist => l.dropLast <+ _
+
 theorem dropLast_subset (l : List α) : l.dropLast ⊆ l :=
   (dropLast_sublist l).subset
 
-@[grind] theorem tail_suffix (l : List α) : tail l <:+ l := by rw [← drop_one]; apply drop_suffix
+grind_pattern dropLast_subset => l.dropLast ⊆ _
 
-@[grind] theorem IsPrefix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : l₁.map f <+: l₂.map f := by
+theorem tail_suffix (l : List α) : tail l <:+ l := by rw [← drop_one]; apply drop_suffix
+
+grind_pattern tail_suffix => tail l <+: _
+
+@[grind ←] theorem IsPrefix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) : l₁.map f <+: l₂.map f := by
   obtain ⟨r, rfl⟩ := h
   rw [map_append]; apply prefix_append
 
 grind_pattern IsPrefix.map => l₁ <+: l₂, l₁.map f
 grind_pattern IsPrefix.map => l₁ <+: l₂, l₂.map f
 
-@[grind] theorem IsSuffix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) : l₁.map f <:+ l₂.map f := by
+@[grind ←] theorem IsSuffix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) : l₁.map f <:+ l₂.map f := by
   obtain ⟨r, rfl⟩ := h
   rw [map_append]; apply suffix_append
 
 grind_pattern IsSuffix.map => l₁ <:+ l₂, l₁.map f
 grind_pattern IsSuffix.map => l₁ <:+ l₂, l₂.map f
 
-@[grind] theorem IsInfix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : l₁.map f <:+: l₂.map f := by
+@[grind ←] theorem IsInfix.map {β} (f : α → β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) : l₁.map f <:+: l₂.map f := by
   obtain ⟨r₁, r₂, rfl⟩ := h
   rw [map_append, map_append]; apply infix_append
 
 grind_pattern IsInfix.map => l₁ <:+: l₂, l₁.map f
 grind_pattern IsInfix.map => l₁ <:+: l₂, l₂.map f
 
-@[grind] theorem IsPrefix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
+@[grind ←] theorem IsPrefix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
     l₁.filter p <+: l₂.filter p := by
   obtain ⟨xs, rfl⟩ := h
   rw [filter_append]; apply prefix_append
@@ -1203,7 +1242,7 @@ grind_pattern IsInfix.map => l₁ <:+: l₂, l₂.map f
 grind_pattern IsPrefix.filter => l₁ <+: l₂, l₁.filter p
 grind_pattern IsPrefix.filter => l₁ <+: l₂, l₂.filter p
 
-@[grind] theorem IsSuffix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
+@[grind ←] theorem IsSuffix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
     l₁.filter p <:+ l₂.filter p := by
   obtain ⟨xs, rfl⟩ := h
   rw [filter_append]; apply suffix_append
@@ -1211,7 +1250,7 @@ grind_pattern IsPrefix.filter => l₁ <+: l₂, l₂.filter p
 grind_pattern IsSuffix.filter => l₁ <:+ l₂, l₁.filter p
 grind_pattern IsSuffix.filter => l₁ <:+ l₂, l₂.filter p
 
-@[grind] theorem IsInfix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
+@[grind ←] theorem IsInfix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
     l₁.filter p <:+: l₂.filter p := by
   obtain ⟨xs, ys, rfl⟩ := h
   rw [filter_append, filter_append]; apply infix_append _
@@ -1219,7 +1258,7 @@ grind_pattern IsSuffix.filter => l₁ <:+ l₂, l₂.filter p
 grind_pattern IsInfix.filter => l₁ <:+: l₂, l₁.filter p
 grind_pattern IsInfix.filter => l₁ <:+: l₂, l₂.filter p
 
-@[grind] theorem IsPrefix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
+@[grind ←] theorem IsPrefix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
     filterMap f l₁ <+: filterMap f l₂ := by
   obtain ⟨xs, rfl⟩ := h
   rw [filterMap_append]; apply prefix_append
@@ -1227,7 +1266,7 @@ grind_pattern IsInfix.filter => l₁ <:+: l₂, l₂.filter p
 grind_pattern IsPrefix.filterMap => l₁ <+: l₂, filterMap f l₁
 grind_pattern IsPrefix.filterMap => l₁ <+: l₂, filterMap f l₂
 
-@[grind] theorem IsSuffix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
+@[grind ←] theorem IsSuffix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
     filterMap f l₁ <:+ filterMap f l₂ := by
   obtain ⟨xs, rfl⟩ := h
   rw [filterMap_append]; apply suffix_append
@@ -1235,7 +1274,7 @@ grind_pattern IsPrefix.filterMap => l₁ <+: l₂, filterMap f l₂
 grind_pattern IsSuffix.filterMap => l₁ <:+ l₂, filterMap f l₁
 grind_pattern IsSuffix.filterMap => l₁ <:+ l₂, filterMap f l₂
 
-@[grind] theorem IsInfix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
+@[grind ←] theorem IsInfix.filterMap {β} (f : α → Option β) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
     filterMap f l₁ <:+: filterMap f l₂ := by
   obtain ⟨xs, ys, rfl⟩ := h
   rw [filterMap_append, filterMap_append]; apply infix_append
diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean
index 6f6d1f4bfd..1aa6f49a8b 100644
--- a/src/Init/Data/Option/Attach.lean
+++ b/src/Init/Data/Option/Attach.lean
@@ -97,7 +97,7 @@ theorem attach_eq_some : ∀ (o : Option α) (x : {x // o = some x}), o.attach =
   | none, ⟨x, h⟩ => by simp at h
   | some a, ⟨x, h⟩ => by simpa using h
 
-@[grind]
+@[grind ←]
 theorem mem_attach : ∀ (o : Option α) (x : {x // o = some x}), x ∈ o.attach :=
   attach_eq_some
 
diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index ef45f9d83a..0de47f797f 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -24,7 +24,7 @@ namespace Option
 @[deprecated mem_def (since := "2025-04-07")]
 theorem mem_iff {a : α} {b : Option α} : a ∈ b ↔ b = some a := .rfl
 
-@[grind] 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
 
diff --git a/src/Init/Data/Order/Ord.lean b/src/Init/Data/Order/Ord.lean
index 26a48e876d..cb56c4b742 100644
--- a/src/Init/Data/Order/Ord.lean
+++ b/src/Init/Data/Order/Ord.lean
@@ -355,7 +355,7 @@ theorem LawfulEqOrd.compare_eq_iff_eq [Ord α] [LawfulEqOrd α] {a b : α} :
   LawfulEqCmp.compare_eq_iff_eq
 
 /-- The corresponding lemma for `LawfulEqCmp` is `LawfulEqCmp.compare_beq_iff_eq` -/
-@[grind]
+@[grind =]
 theorem LawfulEqOrd.compare_beq_iff_eq [Ord α] [LawfulEqOrd α] {a b : α} :
     compare a b == .eq ↔ a = b :=
   LawfulEqCmp.compare_beq_iff_eq
diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean
index 570be2b693..288be09f1d 100644
--- a/src/Init/Data/Vector/Attach.lean
+++ b/src/Init/Data/Vector/Attach.lean
@@ -211,12 +211,13 @@ theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {xs : Vector α n} {H
     b ∈ pmap f xs H ↔ ∃ (a : _) (h : a ∈ xs), f a (H a h) = b := by
   simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]
 
-@[grind]
 theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {xs : Vector α n} {H} {a} (h : a ∈ xs) :
     f a (H a h) ∈ pmap f xs H := by
   rw [mem_pmap]
   exact ⟨a, h, rfl⟩
 
+grind_pattern mem_pmap_of_mem => _ ∈ pmap f xs H, a ∈ xs
+
 theorem pmap_eq_self {xs : Vector α n} {p : α → Prop} {hp : ∀ (a : α), a ∈ xs → p a}
     {f : (a : α) → p a → α} : xs.pmap f hp = xs ↔ ∀ a (h : a ∈ xs), f a (hp a h) = a := by
   rcases xs with ⟨xs, rfl⟩
diff --git a/src/Init/Data/Vector/Find.lean b/src/Init/Data/Vector/Find.lean
index 44d2170040..6da0fbe109 100644
--- a/src/Init/Data/Vector/Find.lean
+++ b/src/Init/Data/Vector/Find.lean
@@ -36,7 +36,7 @@ open Nat
 @[simp, grind =] theorem findSome?_push {xs : Vector α n} : (xs.push a).findSome? f = (xs.findSome? f).or (f a) := by
   cases xs; simp
 
-@[grind]
+@[grind =]
 theorem findSome?_singleton {a : α} {f : α → Option β} : #v[a].findSome? f = f a := by
   simp
 
@@ -228,11 +228,12 @@ theorem mem_of_find?_eq_some {xs : Vector α n} (h : find? p xs = some a) : a 
   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]
 
+grind_pattern get_find?_mem => (xs.find? p).get h
+
 @[simp, grind =] theorem find?_map {f : β → α} {xs : Vector β n} :
     find? p (xs.map f) = (xs.find? (p ∘ f)).map f := by
   cases xs; simp
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index 230a6e945d..d22cf6485d 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -789,7 +789,7 @@ theorem singleton_inj : #v[a] = #v[b] ↔ a = b := by
 @[deprecated replicate_zero (since := "2025-03-18")]
 abbrev replicate_mkVector := @replicate_zero
 
-@[grind]
+@[grind =]
 theorem replicate_succ : replicate (n + 1) a = (replicate n a).push a := by
   simp [replicate, Array.replicate_succ]
 
@@ -895,7 +895,7 @@ theorem getElem?_push_size {xs : Vector α n} {x : α} : (xs.push x)[n]? = some
 theorem getElem_singleton {a : α} (h : i < 1) : #v[a][i] = a := by
   simp
 
-@[grind]
+@[grind =]
 theorem getElem?_singleton {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a else none := by
   simp [List.getElem?_singleton]
 
@@ -907,14 +907,21 @@ theorem getElem?_singleton {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a
 
 theorem not_mem_empty (a : α) : ¬ a ∈ #v[] := nofun
 
-@[simp] theorem mem_push {xs : Vector α n} {x y : α} : x ∈ xs.push y ↔ x ∈ xs ∨ x = y := by
+@[simp, grind =] theorem mem_push {xs : Vector α n} {x y : α} : x ∈ xs.push y ↔ x ∈ xs ∨ x = y := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
-@[grind] theorem mem_or_eq_of_mem_push {a b : α} {xs : Vector α n} :
+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 :=
+-- This pattern may be excessively general:
+-- it fires anytime we ae thinking about membership of vectors,
+-- and constructing a list via `push`, even if the elements are unrelated.
+-- Nevertheless in practice it is quite helpful!
+grind_pattern mem_or_eq_of_mem_push => xs.push b, a ∈ xs
+
+
+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) :
@@ -926,7 +933,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⟩
 
-@[grind] theorem mem_push_of_mem {xs : Vector α n} {x : α} (y : α) (h : x ∈ xs) : x ∈ xs.push y :=
+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
@@ -1213,7 +1220,7 @@ 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
 
-@[grind] theorem contains_empty [BEq α] : (#v[] : Vector α 0).contains a = false := by simp
+@[grind =] theorem contains_empty [BEq α] : (#v[] : Vector α 0).contains a = false := by simp
 
 @[simp, grind =] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {as : Vector α n} :
     as.contains a = decide (a ∈ as) := by
@@ -1236,7 +1243,7 @@ instance [BEq α] [LawfulBEq α] (a : α) (as : Vector α n) : Decidable (a ∈
 
 /-! ### set -/
 
-@[grind] 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
@@ -1249,7 +1256,7 @@ instance [BEq α] [LawfulBEq α] (a : α) (as : Vector α n) : Decidable (a ∈
 @[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]
 
-@[grind] 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
@@ -1297,7 +1304,7 @@ grind_pattern mem_or_eq_of_mem_set => a ∈ xs.set i b
 @[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) :
+@[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
@@ -1310,7 +1317,7 @@ grind_pattern mem_or_eq_of_mem_set => a ∈ xs.set i b
 @[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]
 
-@[grind] 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]
@@ -1410,16 +1417,16 @@ abbrev mkVector_beq_mkVector := @replicate_beq_replicate
 
 /-! ### back -/
 
-@[grind] theorem back_singleton {a : α} : #v[a].back = a := by simp
+@[grind =] theorem back_singleton {a : α} : #v[a].back = a := by simp
 
-@[grind]
+@[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]
 
-@[grind] theorem back?_empty : (#v[] : Vector α 0).back? = none := by simp
+@[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
+@[grind =] theorem back?_eq_getElem? {xs : Vector α n} : xs.back? = xs[n - 1]? := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.back?_eq_getElem?]
 
@@ -1441,7 +1448,7 @@ theorem back_eq_getElem [NeZero n] {xs : Vector α n} : xs.back = xs[n - 1]'(by
   simp
 
 /-- The empty vector maps to the empty vector. -/
-@[grind]
+@[grind =]
 theorem map_empty {f : α → β} : map f #v[] = #v[] := by
   simp
 
@@ -1665,7 +1672,7 @@ theorem empty_append {xs : Vector α n} : (#v[] : Vector α 0) ++ xs = xs.cast (
 theorem append_empty {xs : Vector α n} : xs ++ (#v[] : Vector α 0) = xs := by
   rw [← toArray_inj, toArray_append, Array.append_empty]
 
-@[grind]
+@[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⟩
@@ -1692,7 +1699,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]
+@[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
@@ -1779,14 +1786,14 @@ theorem append_eq_append_iff {ws : Vector α n} {xs : Vector α m} {ys : Vector
   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} :
+@[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) :
+@[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
@@ -1806,7 +1813,7 @@ theorem append_eq_append_iff {ws : Vector α n} {xs : Vector α m} {ys : Vector
     (xs ++ ys).set i x = xs ++ ys.set (i - n) x := by
   rw [set_append, dif_neg (by omega)]
 
-@[grind] 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
@@ -1928,11 +1935,11 @@ theorem forall_mem_flatten {p : α → Prop} {xss : Vector (Vector α n) m} :
   induction xss₂ using vector₂_induction
   simp
 
-@[grind] theorem append_flatten {xss₁ : Vector (Vector α n) m₁} {xss₂ : Vector (Vector α n) m₂} :
+@[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} :
+@[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⟩
@@ -2101,7 +2108,7 @@ abbrev forall_mem_mkVector := @forall_mem_replicate
 @[deprecated getElem_replicate (since := "2025-03-18")]
 abbrev getElem_mkVector := @getElem_replicate
 
-@[grind] 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")]
@@ -2285,7 +2292,7 @@ theorem reverse_eq_iff {xs ys : Vector α n} : xs.reverse = ys ↔ xs = ys.rever
   rcases ys with ⟨ys, rfl⟩
   simp [Array.reverse_append]
 
-@[grind] theorem append_reverse {xs : Vector α n} {ys : Vector α m} :
+@[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⟩
@@ -2345,7 +2352,7 @@ set_option linter.indexVariables false in
   rcases as with ⟨as, rfl⟩
   simp
 
-@[grind] 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
 
@@ -2361,7 +2368,7 @@ theorem foldlM_empty [Monad m] {f : β → α → m β} {init : β} :
     foldlM f init #v[] = return init := by
   simp
 
-@[grind] theorem foldrM_empty [Monad m] {f : α → β → m β} {init : β} :
+@[grind =] theorem foldrM_empty [Monad m] {f : α → β → m β} {init : β} :
     foldrM f init #v[] = return init := by
   simp
 
@@ -2417,9 +2424,9 @@ theorem id_run_foldrM {f : α → β → Id β} {b} {xs : Vector α n} :
 
 /-! ### foldl / foldr -/
 
-@[grind] theorem foldl_empty {f : β → α → β} {init : β} : (#v[].foldl f init) = init := rfl
+@[grind =] theorem foldl_empty {f : β → α → β} {init : β} : (#v[].foldl f init) = init := rfl
 
-@[grind] theorem foldr_empty {f : α → β → β} {init : β} : (#v[].foldr 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)
@@ -2598,7 +2605,7 @@ theorem back?_eq_some_iff {xs : Vector α n} {a : α} :
   simp only [mk_append_mk, back_mk]
   rw [Array.back_append_of_size_pos]
 
-@[grind] 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
@@ -2681,6 +2688,10 @@ theorem contains_iff_exists_mem_beq [BEq α] {xs : Vector α n} {a : α} :
   rcases xs with ⟨xs, rfl⟩
   simp [Array.contains_iff_exists_mem_beq]
 
+-- We add this as a `grind` lemma because it is useful without `LawfulBEq α`.
+-- With `LawfulBEq α`, it would be better to use `contains_iff_mem` directly.
+grind_pattern contains_iff_exists_mem_beq => xs.contains a
+
 @[grind _=_]
 theorem contains_iff_mem [BEq α] [LawfulBEq α] {xs : Vector α n} {a : α} :
     xs.contains a ↔ a ∈ xs := by
@@ -2760,7 +2771,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
 
-@[grind] 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]
@@ -2976,7 +2987,7 @@ variable [BEq α]
 
 @[simp, grind =] theorem replace_empty : (#v[] : Vector α 0).replace a b = #v[] := by simp
 
-@[grind] theorem replace_singleton {a b c : α} : #v[a].replace b c = #v[if a == b then c else a] := by
+@[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,
@@ -2987,7 +2998,7 @@ variable [LawfulBEq α]
   rcases xs with ⟨xs, rfl⟩
   simp_all
 
-@[grind] 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]
@@ -2996,7 +3007,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]
 
-@[grind] 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]
@@ -3007,7 +3018,7 @@ theorem getElem_replace_of_ne {xs : Vector α n} {i : Nat} {h : i < n} (h' : xs[
   rw [getElem_replace h]
   simp [h']
 
-@[grind] 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⟩
@@ -3022,7 +3033,7 @@ 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 : α} :
+@[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]
@@ -3091,7 +3102,7 @@ theorem take_size {as : Vector α n} : as.take n = as.cast (by simp) := by
 
 /-! ### swap -/
 
-@[grind] theorem getElem_swap {xs : Vector α n} {i j : Nat} (hi hj) {k : Nat} (hk : k < n) :
+@[grind =] theorem getElem_swap {xs : Vector α n} {i j : Nat} (hi hj) {k : Nat} (hk : k < n) :
     (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k] := by
   cases xs
   simp_all [Array.getElem_swap]
@@ -3108,7 +3119,7 @@ theorem take_size {as : Vector α n} : as.take n = as.cast (by simp) := by
       (hi' : k ≠ i) (hj' : k ≠ j) : (xs.swap i j hi hj)[k] = xs[k] := by
   simp_all [getElem_swap]
 
-@[grind]
+@[grind =]
 theorem getElem?_swap {xs : Vector α n} {i j : Nat} (hi hj) {k : Nat} : (xs.swap i j hi hj)[k]? =
     if j = k then some xs[i] else if i = k then some xs[j] else xs[k]? := by
   rcases xs with ⟨xs, rfl⟩
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index d283c52195..30669bfa0d 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -3185,7 +3185,7 @@ theorem minKey_insert_le_self [TransCmp cmp] {k v} :
     t.contains (t.minKey he) :=
   Impl.contains_minKey t.wf
 
-@[grind] theorem minKey_mem [TransCmp cmp] {he} :
+@[grind ←] theorem minKey_mem [TransCmp cmp] {he} :
     t.minKey he ∈ t :=
   Impl.minKey_mem t.wf
 
@@ -3827,7 +3827,7 @@ theorem self_le_maxKey_insert [TransCmp cmp] {k v} :
     t.contains (t.maxKey he) :=
   Impl.contains_maxKey t.wf
 
-@[grind] theorem maxKey_mem [TransCmp cmp] {he} :
+@[grind ←] theorem maxKey_mem [TransCmp cmp] {he} :
     t.maxKey he ∈ t :=
   Impl.maxKey_mem t.wf
 
diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
index 8793e4fc86..5a9d8e9a81 100644
--- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
@@ -3243,7 +3243,7 @@ theorem contains_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpt
     t.contains t.minKey! :=
   Impl.contains_minKey! h he
 
-@[grind]
+@[grind ←]
 theorem minKey!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
     t.minKey! ∈ t :=
   Impl.minKey!_mem h he
@@ -3740,7 +3740,7 @@ theorem contains_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpt
     t.contains t.maxKey! :=
   Impl.contains_maxKey! h he
 
-@[grind]
+@[grind ←]
 theorem maxKey!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
     t.maxKey! ∈ t :=
   Impl.maxKey!_mem h he
@@ -3887,7 +3887,7 @@ theorem contains_maxKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fal
     t.contains (t.maxKeyD fallback) :=
   Impl.contains_maxKeyD h he
 
-@[grind]
+@[grind ←]
 theorem maxKeyD_mem [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
     t.maxKeyD fallback ∈ t :=
   Impl.maxKeyD_mem h he
diff --git a/src/Std/Data/ExtDTreeMap/Lemmas.lean b/src/Std/Data/ExtDTreeMap/Lemmas.lean
index 0ef6e0e105..fdf48772bb 100644
--- a/src/Std/Data/ExtDTreeMap/Lemmas.lean
+++ b/src/Std/Data/ExtDTreeMap/Lemmas.lean
@@ -3317,7 +3317,7 @@ theorem minKey_insert_le_self [TransCmp cmp] {k v} :
     t.contains (t.minKey he) :=
   t.inductionOn (fun _ _ => DTreeMap.contains_minKey) he
 
-@[grind] theorem minKey_mem [TransCmp cmp] {he} :
+@[grind ←] theorem minKey_mem [TransCmp cmp] {he} :
     t.minKey he ∈ t :=
   t.inductionOn (fun _ _ => DTreeMap.minKey_mem) he
 
@@ -3952,7 +3952,7 @@ theorem self_le_maxKey_insert [TransCmp cmp] {k v} :
     t.contains (t.maxKey he) :=
   t.inductionOn (fun _ _ => DTreeMap.contains_maxKey) he
 
-@[grind] theorem maxKey_mem [TransCmp cmp] {he} :
+@[grind ←] theorem maxKey_mem [TransCmp cmp] {he} :
     t.maxKey he ∈ t :=
   t.inductionOn (fun _ _ => DTreeMap.maxKey_mem) he
 
diff --git a/src/Std/Data/ExtHashSet/Lemmas.lean b/src/Std/Data/ExtHashSet/Lemmas.lean
index 93670d1ffb..938500599d 100644
--- a/src/Std/Data/ExtHashSet/Lemmas.lean
+++ b/src/Std/Data/ExtHashSet/Lemmas.lean
@@ -339,7 +339,7 @@ theorem getD_empty [EquivBEq α] [LawfulHashable α] {a fallback : α} :
     (∅ : ExtHashSet α).getD a fallback = fallback :=
   ExtHashMap.getKeyD_empty
 
-@[grind] theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
+@[grind =] theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
     (m.insert k).getD a fallback = if k == a ∧ ¬k ∈ m then k else m.getD a fallback :=
   ExtHashMap.getKeyD_insertIfNew
 
diff --git a/src/Std/Data/ExtTreeMap/Lemmas.lean b/src/Std/Data/ExtTreeMap/Lemmas.lean
index 5430683905..1c746e26a2 100644
--- a/src/Std/Data/ExtTreeMap/Lemmas.lean
+++ b/src/Std/Data/ExtTreeMap/Lemmas.lean
@@ -2077,7 +2077,7 @@ theorem minKey_insert_le_self [TransCmp cmp] {k v} :
     t.contains (t.minKey he) :=
   ExtDTreeMap.contains_minKey
 
-@[grind] theorem minKey_mem [TransCmp cmp] {he} :
+@[grind ←] theorem minKey_mem [TransCmp cmp] {he} :
     t.minKey he ∈ t :=
   ExtDTreeMap.minKey_mem
 
@@ -2652,7 +2652,7 @@ theorem self_le_maxKey_insert [TransCmp cmp] {k v} :
     t.contains (t.maxKey he) :=
   ExtDTreeMap.contains_maxKey
 
-@[grind] theorem maxKey_mem [TransCmp cmp] {he} :
+@[grind ←] theorem maxKey_mem [TransCmp cmp] {he} :
     t.maxKey he ∈ t :=
   ExtDTreeMap.maxKey_mem
 
diff --git a/src/Std/Data/ExtTreeSet/Lemmas.lean b/src/Std/Data/ExtTreeSet/Lemmas.lean
index a380c452b4..cfc66a74e8 100644
--- a/src/Std/Data/ExtTreeSet/Lemmas.lean
+++ b/src/Std/Data/ExtTreeSet/Lemmas.lean
@@ -889,7 +889,7 @@ theorem min_insert_le_self [TransCmp cmp] {k} :
     t.contains (t.min he) :=
   ExtTreeMap.contains_minKey
 
-@[grind] theorem min_mem [TransCmp cmp] {he} :
+@[grind ←] theorem min_mem [TransCmp cmp] {he} :
     t.min he ∈ t :=
   ExtTreeMap.minKey_mem
 
@@ -986,7 +986,7 @@ theorem min!_insert_le_self [TransCmp cmp] [Inhabited α] {k} :
     t.contains t.min! :=
   ExtTreeMap.contains_minKey! (mt ext he)
 
-@[grind] theorem min!_mem [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
+@[grind ←] theorem min!_mem [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
     t.min! ∈ t :=
   ExtTreeMap.minKey!_mem (mt ext he)
 
@@ -1077,7 +1077,7 @@ theorem minD_insert_le_self [TransCmp cmp] {k fallback} :
     t.contains (t.minD fallback) :=
   ExtTreeMap.contains_minKeyD (mt ext he)
 
-@[grind] theorem minD_mem [TransCmp cmp] (he : t ≠ ∅) {fallback} :
+@[grind ←] theorem minD_mem [TransCmp cmp] (he : t ≠ ∅) {fallback} :
     t.minD fallback ∈ t :=
   ExtTreeMap.minKeyD_mem (mt ext he)
 
@@ -1290,7 +1290,7 @@ theorem self_le_max_insert [TransCmp cmp] {k} :
     t.contains (t.max he) :=
   ExtTreeMap.contains_maxKey
 
-@[grind] theorem max_mem [TransCmp cmp] {he} :
+@[grind ←] theorem max_mem [TransCmp cmp] {he} :
     t.max he ∈ t :=
   ExtTreeMap.maxKey_mem
 
@@ -1388,7 +1388,7 @@ theorem self_le_max!_insert [TransCmp cmp] [Inhabited α] {k} :
     t.contains t.max! :=
   ExtTreeMap.contains_maxKey! (mt ext he)
 
-@[grind] theorem max!_mem [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
+@[grind ←] theorem max!_mem [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
     t.max! ∈ t :=
   ExtTreeMap.maxKey!_mem (mt ext he)
 
@@ -1480,7 +1480,7 @@ theorem self_le_maxD_insert [TransCmp cmp] {k fallback} :
     t.contains (t.maxD fallback) :=
   ExtTreeMap.contains_maxKeyD (mt ext he)
 
-@[grind] theorem maxD_mem [TransCmp cmp] (he : t ≠ ∅) {fallback} :
+@[grind ←] theorem maxD_mem [TransCmp cmp] (he : t ≠ ∅) {fallback} :
     t.maxD fallback ∈ t :=
   ExtTreeMap.maxKeyD_mem (mt ext he)
 
diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
index d57a750bc5..094b0a3bc3 100644
--- a/src/Std/Data/TreeMap/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Lemmas.lean
@@ -2093,7 +2093,7 @@ theorem minKey_insert_le_self [TransCmp cmp] {k v} :
     t.contains (t.minKey he) :=
   DTreeMap.contains_minKey
 
-@[grind] theorem minKey_mem [TransCmp cmp] {he} :
+@[grind ←] theorem minKey_mem [TransCmp cmp] {he} :
     t.minKey he ∈ t :=
   DTreeMap.minKey_mem
 
@@ -2672,7 +2672,7 @@ theorem self_le_maxKey_insert [TransCmp cmp] {k v} :
     t.contains (t.maxKey he) :=
   DTreeMap.contains_maxKey
 
-@[grind] theorem maxKey_mem [TransCmp cmp] {he} :
+@[grind ←] theorem maxKey_mem [TransCmp cmp] {he} :
     t.maxKey he ∈ t :=
   DTreeMap.maxKey_mem
 
diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean
index b8083602c9..ef11e7e33c 100644
--- a/src/Std/Data/TreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean
@@ -1795,7 +1795,7 @@ theorem getElem?_modify_self [TransCmp cmp] (h : t.WF) {k : α} {f : β → β}
     (modify t k f)[k]? = t[k]?.map f :=
   DTreeMap.Raw.Const.get?_modify_self h
 
-@[grind]
+@[grind =]
 theorem getElem_modify [TransCmp cmp] (h : t.WF) {k k' : α} {f : β → β} {hc : k' ∈ modify t k f} :
     (modify t k f)[k']'hc =
       if heq : cmp k k' = .eq then
diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean
index ab59f5e773..4f5691fde8 100644
--- a/src/Std/Data/TreeSet/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Lemmas.lean
@@ -906,7 +906,7 @@ theorem min_insert_le_self [TransCmp cmp] {k} :
     t.contains (t.min he) :=
   TreeMap.contains_minKey
 
-@[grind] theorem min_mem [TransCmp cmp] {he} :
+@[grind ←] theorem min_mem [TransCmp cmp] {he} :
     t.min he ∈ t :=
   TreeMap.minKey_mem
 
@@ -1003,7 +1003,7 @@ theorem min!_insert_le_self [TransCmp cmp] [Inhabited α] {k} :
     t.contains t.min! :=
   TreeMap.contains_minKey! he
 
-@[grind] theorem min!_mem [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
+@[grind ←] theorem min!_mem [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
     t.min! ∈ t :=
   TreeMap.minKey!_mem he
 
@@ -1094,7 +1094,7 @@ theorem minD_insert_le_self [TransCmp cmp] {k fallback} :
     t.contains (t.minD fallback) :=
   TreeMap.contains_minKeyD he
 
-@[grind] theorem minD_mem [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
+@[grind ←] theorem minD_mem [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
     t.minD fallback ∈ t :=
   TreeMap.minKeyD_mem he
 
@@ -1308,7 +1308,7 @@ theorem self_le_max_insert [TransCmp cmp] {k} :
     t.contains (t.max he) :=
   TreeMap.contains_maxKey
 
-@[grind] theorem max_mem [TransCmp cmp] {he} :
+@[grind ←] theorem max_mem [TransCmp cmp] {he} :
     t.max he ∈ t :=
   TreeMap.maxKey_mem
 
@@ -1406,7 +1406,7 @@ theorem self_le_max!_insert [TransCmp cmp] [Inhabited α] {k} :
     t.contains t.max! :=
   TreeMap.contains_maxKey! he
 
-@[grind] theorem max!_mem [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
+@[grind ←] theorem max!_mem [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
     t.max! ∈ t :=
   TreeMap.maxKey!_mem he
 
@@ -1498,7 +1498,7 @@ theorem self_le_maxD_insert [TransCmp cmp] {k fallback} :
     t.contains (t.maxD fallback) :=
   TreeMap.contains_maxKeyD he
 
-@[grind] theorem maxD_mem [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
+@[grind ←] theorem maxD_mem [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
     t.maxD fallback ∈ t :=
   TreeMap.maxKeyD_mem he
 
diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean
index 9d7a192b2e..8c1bfb4cb0 100644
--- a/src/Std/Data/TreeSet/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean
@@ -906,7 +906,7 @@ theorem min!_insert_le_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k} :
     t.contains t.min! :=
   TreeMap.Raw.contains_minKey! h he
 
-@[grind] theorem min!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
+@[grind ←] theorem min!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
     t.min! ∈ t :=
   TreeMap.Raw.minKey!_mem h he
 
@@ -993,7 +993,7 @@ theorem minD_insert_le_self [TransCmp cmp] (h : t.WF) {k fallback} :
     t.contains (t.minD fallback) :=
   TreeMap.Raw.contains_minKeyD h he
 
-@[grind] theorem minD_mem [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
+@[grind ←] theorem minD_mem [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
     t.minD fallback ∈ t :=
   TreeMap.Raw.minKeyD_mem h he
 
@@ -1216,7 +1216,7 @@ theorem self_le_max!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k} :
     t.contains t.max! :=
   TreeMap.Raw.contains_maxKey! h he
 
-@[grind] theorem max!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
+@[grind ←] theorem max!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
     t.max! ∈ t :=
   TreeMap.Raw.maxKey!_mem h he
 
@@ -1303,7 +1303,7 @@ theorem self_le_maxD_insert [TransCmp cmp] (h : t.WF) {k fallback} :
     t.contains (t.maxD fallback) :=
   TreeMap.Raw.contains_maxKeyD h he
 
-@[grind] theorem maxD_mem [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
+@[grind ←] theorem maxD_mem [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
     t.maxD fallback ∈ t :=
   TreeMap.Raw.maxKeyD_mem h he