oops, error in pattern

src/Init/Data/Array/Attach.lean

@@ -212,12 +212,13 @@ theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {xs H b} :
     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 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
+
 @[simp, grind =]
 theorem size_pmap {p : α → Prop} {f : ∀ a, p a → β} {xs H} : (pmap f xs H).size = xs.size := by
   cases xs; simp

src/Init/Data/Array/Basic.lean

@@ -111,10 +111,12 @@ theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
 @[simp, grind =] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
   simp [mem_def]
 
-@[simp, grind] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
+@[simp] theorem getElem_mem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i] ∈ xs := by
   rw [Array.mem_def, ← getElem_toList]
   apply List.getElem_mem
 
+grind_pattern getElem_mem => xs[i] ∈ xs
+
 @[simp, grind =] theorem emptyWithCapacity_eq {α n} : @emptyWithCapacity α n = #[] := rfl
 
 @[simp] theorem mkEmpty_eq {α n} : @mkEmpty α n = #[] := rfl

src/Init/Data/Array/Find.lean

@@ -396,7 +396,6 @@ 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)

src/Init/Data/List/Erase.lean

@@ -265,14 +265,18 @@ theorem eraseP_eq_iff {p} {l : List α} :
         subst p
         simp_all
 
-@[grind ←]
 theorem Pairwise.eraseP (q) : Pairwise p l → Pairwise p (l.eraseP q) :=
   Pairwise.sublist <| eraseP_sublist
 
-@[grind ←]
+grind_pattern Pairwise.eraseP => Pairwise p (l.eraseP q)
+grind_pattern Pairwise.eraseP => Pairwise p l, l.eraseP q
+
 theorem Nodup.eraseP (p) : Nodup l → Nodup (l.eraseP p) :=
   Pairwise.eraseP p
 
+grind_pattern Nodup.eraseP => Nodup (l.eraseP p)
+grind_pattern Nodup.eraseP => Nodup l, l.eraseP p
+
 @[grind =]
 theorem eraseP_comm {l : List α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) :
     (l.eraseP p).eraseP q = (l.eraseP q).eraseP p := by
@@ -508,10 +512,12 @@ 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 ←]
 theorem Nodup.erase [LawfulBEq α] (a : α) : Nodup l → Nodup (l.erase a) :=
   Pairwise.erase a
 
+grind_pattern Nodup.erase => Nodup (l.erase a)
+grind_pattern Nodup.erase => Nodup l, l.erase a
+
 theorem head_erase_mem (xs : List α) (a : α) (h) : (xs.erase a).head h ∈ xs :=
   erase_sublist.head_mem h
 
@@ -649,15 +655,18 @@ theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} :
     exact m.2
   · rw [eraseIdx_of_length_le (by simpa using h)]
 
-@[grind ←]
 theorem Pairwise.eraseIdx {l : List α} (k) : Pairwise p l → Pairwise p (l.eraseIdx k) :=
   Pairwise.sublist <| eraseIdx_sublist _ _
 
-@[grind ←]
+grind_pattern Pairwise.eraseIdx => Pairwise p (l.eraseIdx k)
+grind_pattern Pairwise.eraseIdx => Pairwise p l, l.eraseIdx k
+
 theorem Nodup.eraseIdx {l : List α} (k) : Nodup l → Nodup (l.eraseIdx k) :=
   Pairwise.eraseIdx k
 
-@[grind ←]
+grind_pattern Nodup.eraseIdx => Nodup (l.eraseIdx k)
+grind_pattern Nodup.eraseIdx => Nodup l, l.eraseIdx k
+
 protected theorem IsPrefix.eraseIdx {l l' : List α} (h : l <+: l') (k : Nat) :
     eraseIdx l k <+: eraseIdx l' k := by
   rcases h with ⟨t, rfl⟩
@@ -667,6 +676,10 @@ protected theorem IsPrefix.eraseIdx {l l' : List α} (h : l <+: l') (k : Nat) :
     rw [Nat.not_lt] at hkl
     simp [eraseIdx_append_of_length_le hkl, eraseIdx_of_length_le hkl]
 
+grind_pattern IsPrefix.eraseIdx => eraseIdx l k <+: eraseIdx l' k
+grind_pattern IsPrefix.eraseIdx => eraseIdx l k, l <+: l'
+grind_pattern IsPrefix.eraseIdx => eraseIdx l' k, l <+: l'
+
 -- See also `mem_eraseIdx_iff_getElem` and `mem_eraseIdx_iff_getElem?` in
 -- `Init/Data/List/Nat/Basic.lean`.
 
@@ -686,6 +699,4 @@ theorem erase_eq_eraseIdx_of_idxOf [BEq α] [LawfulBEq α]
     rw [eq_comm, eraseIdx_eq_self]
     exact Nat.le_of_eq (idxOf_eq_length h).symm
 
-
-
 end List

src/Init/Data/List/Find.lean

@@ -559,7 +559,6 @@ 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

src/Init/Data/List/Pairwise.lean

@@ -277,10 +277,12 @@ theorem pairwise_of_forall_mem_list {l : List α} {r : α → α → Prop} (h :
 
 @[grind =] theorem nodup_iff_pairwise_ne : List.Nodup l ↔ List.Pairwise (· ≠ ·) l := Iff.rfl
 
-@[simp, grind]
+@[simp]
 theorem nodup_nil : @Nodup α [] :=
   Pairwise.nil
 
+grind_pattern nodup_nil => @Nodup α []
+
 @[simp, grind =]
 theorem nodup_cons {a : α} {l : List α} : Nodup (a :: l) ↔ a ∉ l ∧ Nodup l := by
   simp only [Nodup, pairwise_cons, forall_mem_ne]

src/Init/Data/List/Sublist.lean

@@ -638,15 +638,21 @@ protected theorem Sublist.drop : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → ∀
 
 /-! ### IsPrefix / IsSuffix / IsInfix -/
 
-@[simp, grind] theorem prefix_append (l₁ l₂ : List α) : l₁ <+: l₁ ++ l₂ := ⟨l₂, rfl⟩
+@[simp] theorem prefix_append (l₁ l₂ : List α) : l₁ <+: l₁ ++ l₂ := ⟨l₂, rfl⟩
 
-@[simp, grind] theorem suffix_append (l₁ l₂ : List α) : l₂ <:+ l₁ ++ l₂ := ⟨l₁, rfl⟩
+grind_pattern prefix_append => l₁ <+: l₁ ++ l₂
+
+@[simp] theorem suffix_append (l₁ l₂ : List α) : l₂ <:+ l₁ ++ l₂ := ⟨l₁, rfl⟩
+
+grind_pattern suffix_append => l₂ <:+ l₁ ++ l₂
 
 theorem infix_append (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ l₂ ++ l₃ := ⟨l₁, l₃, rfl⟩
 
-@[simp, grind] theorem infix_append' (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ (l₂ ++ l₃) := by
+@[simp] theorem infix_append' (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ (l₂ ++ l₃) := by
   rw [← List.append_assoc]; apply infix_append
 
+grind_pattern infix_append' => l₂ <:+: l₁ ++ (l₂ ++ l₃)
+
 theorem infix_append_left : l₁ <:+: l₁ ++ l₂ := ⟨[], l₂, rfl⟩
 theorem infix_append_right : l₂ <:+: l₁ ++ l₂ := ⟨l₁, [], by simp⟩
 
@@ -673,7 +679,9 @@ theorem suffix_refl (l : List α) : l <:+ l := ⟨[], rfl⟩
 theorem infix_refl (l : List α) : l <:+: l := prefix_rfl.isInfix
 @[simp, grind] theorem infix_rfl {l : List α} : l <:+: l := infix_refl l
 
-@[simp, grind] theorem suffix_cons (a : α) : ∀ l, l <:+ a :: l := suffix_append [a]
+@[simp] theorem suffix_cons (a : α) : ∀ l, l <:+ a :: l := suffix_append [a]
+
+grind_pattern suffix_cons => _ <:+ a :: l
 
 theorem infix_cons : l₁ <:+: l₂ → l₁ <:+: a :: l₂ := fun ⟨l₁', l₂', h⟩ => ⟨a :: l₁', l₂', h ▸ rfl⟩
 

src/Init/Data/Vector/Lemmas.lean

@@ -901,10 +901,12 @@ theorem getElem?_singleton {a : α} {i : Nat} : #v[a][i]? = if i = 0 then some a
 
 /-! ### mem -/
 
-@[simp, grind] theorem getElem_mem {xs : Vector α n} {i : Nat} (h : i < n) : xs[i] ∈ xs := by
+@[simp] theorem getElem_mem {xs : Vector α n} {i : Nat} (h : i < n) : xs[i] ∈ xs := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
+grind_pattern getElem_mem => xs[i] ∈ xs
+
 theorem not_mem_empty (a : α) : ¬ a ∈ #v[] := nofun
 
 @[simp, grind =] theorem mem_push {xs : Vector α n} {x y : α} : x ∈ xs.push y ↔ x ∈ xs ∨ x = y := by

src/Init/GetElem.lean

@@ -299,10 +299,12 @@ theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) :
 theorem getElem_cons_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) :=
     rfl
 
-@[simp, grind] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
+@[simp] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
   | _ :: _, 0, _ => .head ..
   | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
 
+grind_pattern getElem_mem => l[n]'h ∈ l
+
 theorem getElem_cons_drop_succ_eq_drop {as : List α} {i : Nat} (h : i < as.length) :
     as[i] :: as.drop (i+1) = as.drop i :=
   match as, i with

src/Std/Data/DTreeMap/Lemmas.lean

@@ -3185,10 +3185,12 @@ 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} :
+theorem minKey_mem [TransCmp cmp] {he} :
     t.minKey he ∈ t :=
   Impl.minKey_mem t.wf
 
+grind_pattern minKey_mem => t.minKey he ∈ t
+
 theorem minKey_le_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
     cmp (t.minKey <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) k |>.isLE :=
   Impl.minKey_le_of_contains t.wf hc
@@ -3827,10 +3829,12 @@ 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} :
+theorem maxKey_mem [TransCmp cmp] {he} :
     t.maxKey he ∈ t :=
   Impl.maxKey_mem t.wf
 
+grind_pattern maxKey_mem => t.maxKey he ∈ t
+
 theorem le_maxKey_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
     cmp k (t.maxKey <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
   Impl.le_maxKey_of_contains t.wf hc

src/Std/Data/DTreeMap/Raw/Lemmas.lean

@@ -3243,11 +3243,12 @@ theorem contains_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpt
     t.contains t.minKey! :=
   Impl.contains_minKey! h he
 
-@[grind ←]
 theorem minKey!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
     t.minKey! ∈ t :=
   Impl.minKey!_mem h he
 
+grind_pattern contains_minKey! => t.contains t.minKey!
+
 theorem minKey!_le_of_contains [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : t.contains k) :
     cmp t.minKey! k |>.isLE :=
   Impl.minKey!_le_of_contains h hc
@@ -3393,6 +3394,8 @@ theorem minKeyD_mem [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback
     t.minKeyD fallback ∈ t :=
   Impl.minKeyD_mem h he
 
+grind_pattern minKeyD_mem => t.minKeyD fallback ∈ t
+
 theorem minKeyD_le_of_contains [TransCmp cmp] (h : t.WF) {k} (hc : t.contains k) {fallback} :
     cmp (t.minKeyD fallback) k |>.isLE :=
   Impl.minKeyD_le_of_contains h hc
@@ -3740,11 +3743,12 @@ theorem contains_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpt
     t.contains t.maxKey! :=
   Impl.contains_maxKey! h he
 
-@[grind ←]
 theorem maxKey!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
     t.maxKey! ∈ t :=
   Impl.maxKey!_mem h he
 
+grind_pattern contains_maxKey! => t.contains t.maxKey!
+
 theorem le_maxKey!_of_contains [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : t.contains k) :
     cmp k t.maxKey! |>.isLE :=
   Impl.le_maxKey!_of_contains h hc
@@ -3887,11 +3891,12 @@ theorem contains_maxKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fal
     t.contains (t.maxKeyD fallback) :=
   Impl.contains_maxKeyD h he
 
-@[grind ←]
 theorem maxKeyD_mem [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
     t.maxKeyD fallback ∈ t :=
   Impl.maxKeyD_mem h he
 
+grind_pattern maxKeyD_mem => t.maxKeyD fallback ∈ t
+
 theorem le_maxKeyD_of_contains [TransCmp cmp] (h : t.WF) {k} (hc : t.contains k) {fallback} :
     cmp k (t.maxKeyD fallback) |>.isLE :=
   Impl.le_maxKeyD_of_contains h hc

src/Std/Data/ExtDTreeMap/Lemmas.lean

@@ -3317,10 +3317,12 @@ 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} :
+theorem minKey_mem [TransCmp cmp] {he} :
     t.minKey he ∈ t :=
   t.inductionOn (fun _ _ => DTreeMap.minKey_mem) he
 
+grind_pattern minKey_mem => t.minKey he ∈ t
+
 theorem minKey_le_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
     cmp (t.minKey (ne_empty_of_mem hc)) k |>.isLE :=
   t.inductionOn (fun _ hc => DTreeMap.minKey_le_of_contains hc) hc
@@ -3952,10 +3954,12 @@ 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} :
+theorem maxKey_mem [TransCmp cmp] {he} :
     t.maxKey he ∈ t :=
   t.inductionOn (fun _ _ => DTreeMap.maxKey_mem) he
 
+grind_pattern maxKey_mem => t.maxKey he ∈ t
+
 theorem le_maxKey_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
     cmp k (t.maxKey (ne_empty_of_mem hc)) |>.isLE :=
   t.inductionOn (fun _ hc => DTreeMap.le_maxKey_of_contains hc) hc

src/Std/Data/ExtTreeMap/Lemmas.lean

@@ -2077,10 +2077,12 @@ theorem minKey_insert_le_self [TransCmp cmp] {k v} :
     t.contains (t.minKey he) :=
   ExtDTreeMap.contains_minKey
 
-@[grind ←] theorem minKey_mem [TransCmp cmp] {he} :
+theorem minKey_mem [TransCmp cmp] {he} :
     t.minKey he ∈ t :=
   ExtDTreeMap.minKey_mem
 
+grind_pattern minKey_mem => t.minKey he ∈ t
+
 theorem minKey_le_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
     cmp (t.minKey (ne_empty_of_mem hc)) k |>.isLE :=
   ExtDTreeMap.minKey_le_of_contains hc
@@ -2652,10 +2654,12 @@ theorem self_le_maxKey_insert [TransCmp cmp] {k v} :
     t.contains (t.maxKey he) :=
   ExtDTreeMap.contains_maxKey
 
-@[grind ←] theorem maxKey_mem [TransCmp cmp] {he} :
+theorem maxKey_mem [TransCmp cmp] {he} :
     t.maxKey he ∈ t :=
   ExtDTreeMap.maxKey_mem
 
+grind_pattern maxKey_mem => t.maxKey he ∈ t
+
 theorem le_maxKey_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
     cmp k (t.maxKey (ne_empty_of_mem hc)) |>.isLE :=
   ExtDTreeMap.le_maxKey_of_contains hc

src/Std/Data/ExtTreeSet/Lemmas.lean

@@ -889,10 +889,12 @@ theorem min_insert_le_self [TransCmp cmp] {k} :
     t.contains (t.min he) :=
   ExtTreeMap.contains_minKey
 
-@[grind ←] theorem min_mem [TransCmp cmp] {he} :
+theorem min_mem [TransCmp cmp] {he} :
     t.min he ∈ t :=
   ExtTreeMap.minKey_mem
 
+grind_pattern min_mem => t.min he ∈ t
+
 theorem min_le_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
     cmp (t.min (ne_empty_of_mem hc)) k |>.isLE :=
   ExtTreeMap.minKey_le_of_contains hc
@@ -986,10 +988,12 @@ 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 ≠ ∅) :
+theorem min!_mem [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
     t.min! ∈ t :=
   ExtTreeMap.minKey!_mem (mt ext he)
 
+grind_pattern min!_mem => t.min! ∈ t
+
 theorem min!_le_of_contains [TransCmp cmp] [Inhabited α] {k} (hc : t.contains k) :
     cmp t.min! k |>.isLE :=
   ExtTreeMap.minKey!_le_of_contains hc
@@ -1077,10 +1081,12 @@ 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} :
+theorem minD_mem [TransCmp cmp] (he : t ≠ ∅) {fallback} :
     t.minD fallback ∈ t :=
   ExtTreeMap.minKeyD_mem (mt ext he)
 
+grind_pattern minD_mem => t.minD fallback ∈ t
+
 theorem minD_le_of_contains [TransCmp cmp] {k} (hc : t.contains k) {fallback} :
     cmp (t.minD fallback) k |>.isLE :=
   ExtTreeMap.minKeyD_le_of_contains hc
@@ -1290,10 +1296,12 @@ theorem self_le_max_insert [TransCmp cmp] {k} :
     t.contains (t.max he) :=
   ExtTreeMap.contains_maxKey
 
-@[grind ←] theorem max_mem [TransCmp cmp] {he} :
+theorem max_mem [TransCmp cmp] {he} :
     t.max he ∈ t :=
   ExtTreeMap.maxKey_mem
 
+grind_pattern max_mem => t.max he ∈ t
+
 theorem le_max_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
     cmp k (t.max (ne_empty_of_mem hc)) |>.isLE :=
   ExtTreeMap.le_maxKey_of_contains hc
@@ -1388,10 +1396,12 @@ 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 ≠ ∅) :
+theorem max!_mem [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) :
     t.max! ∈ t :=
   ExtTreeMap.maxKey!_mem (mt ext he)
 
+grind_pattern max!_mem => t.max! ∈ t
+
 theorem le_max!_of_contains [TransCmp cmp] [Inhabited α] {k} (hc : t.contains k) :
     cmp k t.max! |>.isLE :=
   ExtTreeMap.le_maxKey!_of_contains hc
@@ -1480,10 +1490,12 @@ 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} :
+theorem maxD_mem [TransCmp cmp] (he : t ≠ ∅) {fallback} :
     t.maxD fallback ∈ t :=
   ExtTreeMap.maxKeyD_mem (mt ext he)
 
+grind_pattern maxD_mem => t.maxD fallback ∈ t
+
 theorem le_maxD_of_contains [TransCmp cmp] {k} (hc : t.contains k) {fallback} :
     cmp k (t.maxD fallback) |>.isLE :=
   ExtTreeMap.le_maxKeyD_of_contains hc

src/Std/Data/TreeMap/Lemmas.lean

@@ -2093,10 +2093,12 @@ theorem minKey_insert_le_self [TransCmp cmp] {k v} :
     t.contains (t.minKey he) :=
   DTreeMap.contains_minKey
 
-@[grind ←] theorem minKey_mem [TransCmp cmp] {he} :
+theorem minKey_mem [TransCmp cmp] {he} :
     t.minKey he ∈ t :=
   DTreeMap.minKey_mem
 
+grind_pattern minKey_mem => t.minKey he ∈ t
+
 theorem minKey_le_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
     cmp (t.minKey <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) k |>.isLE :=
   DTreeMap.minKey_le_of_contains hc
@@ -2672,10 +2674,12 @@ theorem self_le_maxKey_insert [TransCmp cmp] {k v} :
     t.contains (t.maxKey he) :=
   DTreeMap.contains_maxKey
 
-@[grind ←] theorem maxKey_mem [TransCmp cmp] {he} :
+theorem maxKey_mem [TransCmp cmp] {he} :
     t.maxKey he ∈ t :=
   DTreeMap.maxKey_mem
 
+grind_pattern maxKey_mem => t.maxKey he ∈ t
+
 theorem le_maxKey_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
     cmp k (t.maxKey <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
   DTreeMap.le_maxKey_of_contains hc

src/Std/Data/TreeSet/Lemmas.lean

@@ -906,10 +906,12 @@ theorem min_insert_le_self [TransCmp cmp] {k} :
     t.contains (t.min he) :=
   TreeMap.contains_minKey
 
-@[grind ←] theorem min_mem [TransCmp cmp] {he} :
+theorem min_mem [TransCmp cmp] {he} :
     t.min he ∈ t :=
   TreeMap.minKey_mem
 
+grind_pattern min_mem => t.min he ∈ t
+
 theorem min_le_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
     cmp (t.min <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) k |>.isLE :=
   TreeMap.minKey_le_of_contains hc
@@ -1003,10 +1005,12 @@ 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) :
+theorem min!_mem [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
     t.min! ∈ t :=
   TreeMap.minKey!_mem he
 
+grind_pattern min!_mem => t.min! ∈ t
+
 theorem min!_le_of_contains [TransCmp cmp] [Inhabited α] {k} (hc : t.contains k) :
     cmp t.min! k |>.isLE :=
   TreeMap.minKey!_le_of_contains hc
@@ -1094,10 +1098,12 @@ 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} :
+theorem minD_mem [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
     t.minD fallback ∈ t :=
   TreeMap.minKeyD_mem he
 
+grind_pattern minD_mem => t.minD fallback ∈ t
+
 theorem minD_le_of_contains [TransCmp cmp] {k} (hc : t.contains k) {fallback} :
     cmp (t.minD fallback) k |>.isLE :=
   TreeMap.minKeyD_le_of_contains hc
@@ -1308,10 +1314,12 @@ theorem self_le_max_insert [TransCmp cmp] {k} :
     t.contains (t.max he) :=
   TreeMap.contains_maxKey
 
-@[grind ←] theorem max_mem [TransCmp cmp] {he} :
+theorem max_mem [TransCmp cmp] {he} :
     t.max he ∈ t :=
   TreeMap.maxKey_mem
 
+grind_pattern max_mem => t.max he ∈ t
+
 theorem le_max_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
     cmp k (t.max <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
   TreeMap.le_maxKey_of_contains hc
@@ -1406,10 +1414,12 @@ 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) :
+theorem max!_mem [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
     t.max! ∈ t :=
   TreeMap.maxKey!_mem he
 
+grind_pattern max!_mem => t.max! ∈ t
+
 theorem le_max!_of_contains [TransCmp cmp] [Inhabited α] {k} (hc : t.contains k) :
     cmp k t.max! |>.isLE :=
   TreeMap.le_maxKey!_of_contains hc
@@ -1498,10 +1508,12 @@ 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} :
+theorem maxD_mem [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
     t.maxD fallback ∈ t :=
   TreeMap.maxKeyD_mem he
 
+grind_pattern maxD_mem => t.maxD fallback ∈ t
+
 theorem le_maxD_of_contains [TransCmp cmp] {k} (hc : t.contains k) {fallback} :
     cmp k (t.maxD fallback) |>.isLE :=
   TreeMap.le_maxKeyD_of_contains hc

src/Std/Data/TreeSet/Raw/Lemmas.lean

@@ -906,10 +906,12 @@ 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) :
+theorem min!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
     t.min! ∈ t :=
   TreeMap.Raw.minKey!_mem h he
 
+grind_pattern min!_mem => t.min! ∈ t
+
 theorem min!_le_of_contains [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : t.contains k) :
     cmp t.min! k |>.isLE :=
   TreeMap.Raw.minKey!_le_of_contains h hc
@@ -993,10 +995,12 @@ 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} :
+theorem minD_mem [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
     t.minD fallback ∈ t :=
   TreeMap.Raw.minKeyD_mem h he
 
+grind_pattern minD_mem => t.minD fallback ∈ t
+
 theorem minD_le_of_contains [TransCmp cmp] (h : t.WF) {k} (hc : t.contains k) {fallback} :
     cmp (t.minD fallback) k |>.isLE :=
   TreeMap.Raw.minKeyD_le_of_contains h hc
@@ -1216,10 +1220,12 @@ 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) :
+theorem max!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
     t.max! ∈ t :=
   TreeMap.Raw.maxKey!_mem h he
 
+grind_pattern max!_mem => t.max! ∈ t
+
 theorem le_max!_of_contains [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : t.contains k) :
     cmp k t.max! |>.isLE :=
   TreeMap.Raw.le_maxKey!_of_contains h hc
@@ -1303,10 +1309,12 @@ 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} :
+theorem maxD_mem [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
     t.maxD fallback ∈ t :=
   TreeMap.Raw.maxKeyD_mem h he
 
+grind_pattern maxD_mem => t.maxD fallback ∈ t
+
 theorem le_maxD_of_contains [TransCmp cmp] (h : t.WF) {k} (hc : t.contains k) {fallback} :
     cmp k (t.maxD fallback) |>.isLE :=
   TreeMap.Raw.le_maxKeyD_of_contains h hc

src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean

@@ -59,7 +59,9 @@ class Clause (α : outParam (Type u)) (β : Type v) where
 
 namespace Clause
 
-attribute [grind] empty_eq unit_eq isUnit_iff negate_eq delete_iff contains_iff
+grind_pattern empty_eq => toList (empty : β)
+grind_pattern unit_eq => @toList _ _ self (unit l)
+attribute [grind] isUnit_iff negate_eq delete_iff contains_iff
 
 instance : Entails α (Literal α) where
   eval := fun p l => p l.1 = l.2

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Class.lean

@@ -62,8 +62,12 @@ class Formula (α : outParam (Type u)) (β : outParam (Type v)) [Clause α β] (
 
 open Formula
 
-attribute [grind] insert_iff readyForRupAdd_insert readyForRatAdd_insert
-  delete_subset readyForRupAdd_delete readyForRatAdd_delete
+attribute [grind] insert_iff delete_subset
+
+grind_pattern readyForRupAdd_insert => ReadyForRupAdd (insert f c)
+grind_pattern readyForRupAdd_delete => ReadyForRupAdd (delete f arr)
+grind_pattern readyForRatAdd_insert => ReadyForRatAdd (insert f c)
+grind_pattern readyForRatAdd_delete => ReadyForRatAdd (delete f arr)
 
 attribute [grind →]
   rupAdd_result rupAdd_sound ratAdd_result ratAdd_sound