.

src/Std/Data/DTreeMap/Lemmas.lean

@@ -1289,6 +1289,7 @@ theorem insertMany_cons {l : List ((a : α) × β a)} {k : α} {v : β k} :
     t.insertMany (⟨k, v⟩ :: l) = (t.insert k v).insertMany l :=
   ext <| Impl.insertMany_cons t.wf
 
+@[grind _=_]
 theorem insertMany_append {l₁ l₂ : List ((a : α) × β a)} :
     insertMany t (l₁ ++ l₂) = insertMany (insertMany t l₁) l₂ := by
   induction l₁ generalizing t with
@@ -1469,6 +1470,7 @@ theorem insertMany_cons {l : List (α × β)} {k : α} {v : β} :
     Const.insertMany t ((k, v) :: l) = Const.insertMany (t.insert k v) l :=
   ext <| Impl.Const.insertMany_cons t.wf
 
+@[grind _=_]
 theorem insertMany_append {l₁ l₂ : List (α × β)} :
     insertMany t (l₁ ++ l₂) = insertMany (insertMany t l₁) l₂ := by
   induction l₁ generalizing t with

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

@@ -1296,6 +1296,7 @@ theorem insertMany_cons {l : List ((a : α) × β a)} {k : α} {v : β k} :
     t.insertMany (⟨k, v⟩ :: l) = (t.insert k v).insertMany l :=
   ext <| Impl.insertMany!_cons
 
+@[grind _=_]
 theorem insertMany_append {l₁ l₂ : List ((a : α) × β a)} :
     insertMany t (l₁ ++ l₂) = insertMany (insertMany t l₁) l₂ := by
   induction l₁ generalizing t with
@@ -1476,6 +1477,7 @@ theorem insertMany_cons {l : List (α × β)} {k : α} {v : β} :
     Const.insertMany t ((k, v) :: l) = Const.insertMany (t.insert k v) l :=
   ext <| Impl.Const.insertMany!_cons
 
+@[grind _=_]
 theorem insertMany_append {l₁ l₂ : List (α × β)} :
     insertMany t (l₁ ++ l₂) = insertMany (insertMany t l₁) l₂ := by
   induction l₁ generalizing t with

src/Std/Data/ExtHashMap/Lemmas.lean

@@ -13,6 +13,8 @@ import Std.Data.ExtDHashMap.Lemmas
 This module contains lemmas about `Std.ExtHashMap`.
 -/
 
+set_option trace.grind.ematch.pattern true
+
 set_option linter.missingDocs true
 set_option autoImplicit false
 
@@ -32,7 +34,7 @@ private theorem ext {m m' : ExtHashMap α β} : m.inner = m'.inner → m = m' :=
 private theorem ext_iff {m m' : ExtHashMap α β} : m = m' ↔ m.inner = m'.inner :=
   ⟨fun h => h ▸ rfl, ext⟩
 
-@[simp]
+@[simp, grind =]
 theorem isEmpty_iff [EquivBEq α] [LawfulHashable α] : m.isEmpty ↔ m = ∅ :=
   ExtDHashMap.isEmpty_iff.trans ext_iff.symm
 
@@ -43,7 +45,7 @@ theorem isEmpty_eq_false_iff [EquivBEq α] [LawfulHashable α] : m.isEmpty = fal
 @[simp]
 theorem empty_eq : ∅ = m ↔ m = ∅ := eq_comm
 
-@[simp]
+@[simp, grind =]
 theorem emptyWithCapacity_eq [EquivBEq α] [LawfulHashable α] {c} : (emptyWithCapacity c : ExtHashMap α β) = ∅ :=
   ext ExtDHashMap.emptyWithCapacity_eq
 
@@ -67,7 +69,7 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
     a ∈ m ↔ b ∈ m :=
   ExtDHashMap.mem_congr hab
 
-@[simp] theorem contains_empty [EquivBEq α] [LawfulHashable α] {a : α} : (∅ : ExtHashMap α β).contains a = false :=
+@[simp, grind =] theorem contains_empty [EquivBEq α] [LawfulHashable α] {a : α} : (∅ : ExtHashMap α β).contains a = false :=
   ExtDHashMap.contains_empty
 
 @[simp] theorem not_mem_empty [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ (∅ : ExtHashMap α β) :=
@@ -87,12 +89,12 @@ theorem eq_empty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] : m = ∅
     Singleton.singleton p = (∅ : ExtHashMap α β).insert p.1 p.2 :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     (m.insert k v).contains a = (k == a || m.contains a) :=
   ExtDHashMap.contains_insert
 
-@[simp]
+@[simp, grind =]
 theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     a ∈ m.insert k v ↔ k == a ∨ a ∈ m :=
   ExtDHashMap.mem_insert
@@ -111,13 +113,14 @@ theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
 theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : k ∈ m.insert k v := by
   simp
 
-@[simp]
+@[simp, grind =]
 theorem size_empty [EquivBEq α] [LawfulHashable α] : (∅ : ExtHashMap α β).size = 0 :=
   ExtDHashMap.size_empty
 
 theorem eq_empty_iff_size_eq_zero [EquivBEq α] [LawfulHashable α] : m = ∅ ↔ m.size = 0 :=
   ext_iff.trans ExtDHashMap.eq_empty_iff_size_eq_zero
 
+@[grind =]
 theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     (m.insert k v).size = if k ∈ m then m.size else m.size + 1 :=
   ExtDHashMap.size_insert
@@ -130,7 +133,7 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     (m.insert k v).size ≤ m.size + 1 :=
   ExtDHashMap.size_insert_le
 
-@[simp]
+@[simp, grind =]
 theorem erase_empty [EquivBEq α] [LawfulHashable α] {a : α} : (∅ : ExtHashMap α β).erase a = ∅ :=
   ext ExtDHashMap.erase_empty
 
@@ -139,12 +142,12 @@ theorem erase_eq_empty_iff [EquivBEq α] [LawfulHashable α] {k : α} :
     m.erase k = ∅ ↔ m = ∅ ∨ m.size = 1 ∧ k ∈ m := by
   simpa only [ext_iff] using ExtDHashMap.erase_eq_empty_iff
 
-@[simp]
+@[simp, grind =]
 theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.erase k).contains a = (!(k == a) && m.contains a) :=
   ExtDHashMap.contains_erase
 
-@[simp]
+@[simp, grind =]
 theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m :=
   ExtDHashMap.mem_erase
@@ -156,7 +159,7 @@ theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α}
 theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.erase k → a ∈ m :=
   ExtDHashMap.mem_of_mem_erase
 
-theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
+@[grind =] theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
     (m.erase k).size = if k ∈ m then m.size - 1 else m.size :=
   ExtDHashMap.size_erase
 
@@ -167,34 +170,35 @@ theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
     m.size ≤ (m.erase k).size + 1 :=
   ExtDHashMap.size_le_size_erase
 
-@[simp]
+@[simp, grind =]
 theorem containsThenInsert_fst [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     (m.containsThenInsert k v).1 = m.contains k :=
   ExtDHashMap.containsThenInsert_fst
 
-@[simp]
+@[simp, grind =]
 theorem containsThenInsert_snd [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     (m.containsThenInsert k v).2 = m.insert k v :=
   ext (ExtDHashMap.containsThenInsert_snd)
 
-@[simp]
+@[simp, grind =]
 theorem containsThenInsertIfNew_fst [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     (m.containsThenInsertIfNew k v).1 = m.contains k :=
   ExtDHashMap.containsThenInsertIfNew_fst
 
-@[simp]
+@[simp, grind =]
 theorem containsThenInsertIfNew_snd [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v :=
   ext ExtDHashMap.containsThenInsertIfNew_snd
 
-@[simp] theorem get_eq_getElem [EquivBEq α] [LawfulHashable α] {a : α} {h} : get m a h = m[a]'h := rfl
-@[simp] theorem get?_eq_getElem? [EquivBEq α] [LawfulHashable α] {a : α} : get? m a = m[a]? := rfl
-@[simp] theorem get!_eq_getElem! [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : get! m a = m[a]! := rfl
+@[simp, grind =] theorem get_eq_getElem [EquivBEq α] [LawfulHashable α] {a : α} {h} : get m a h = m[a]'h := rfl
+@[simp, grind =] theorem get?_eq_getElem? [EquivBEq α] [LawfulHashable α] {a : α} : get? m a = m[a]? := rfl
+@[simp, grind =] theorem get!_eq_getElem! [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} : get! m a = m[a]! := rfl
 
-@[simp]
+@[simp, grind =]
 theorem getElem?_empty [EquivBEq α] [LawfulHashable α] {a : α} : (∅ : ExtHashMap α β)[a]? = none :=
   ExtDHashMap.Const.get?_empty
 
+@[grind =]
 theorem getElem?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     (m.insert k v)[a]? = if k == a then some v else m[a]? :=
   ExtDHashMap.Const.get?_insert
@@ -229,7 +233,7 @@ theorem getElem?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
 theorem getElem?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m[a]? = none :=
   ExtDHashMap.Const.get?_eq_none
 
-theorem getElem?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
+@[grind =] theorem getElem?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.erase k)[a]? = if k == a then none else m[a]? :=
   ExtDHashMap.Const.get?_erase
 
@@ -240,7 +244,7 @@ theorem getElem?_erase_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.eras
 theorem getElem?_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : m[a]? = m[b]? :=
   ExtDHashMap.Const.get?_congr hab
 
-theorem getElem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
+@[grind =] theorem getElem_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     (m.insert k v)[a]'h₁ =
       if h₂ : k == a then v else m[a]'(mem_of_mem_insert h₁ (Bool.eq_false_iff.2 h₂)) :=
   ExtDHashMap.Const.get_insert (h₁ := h₁)
@@ -250,7 +254,7 @@ theorem getElem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
     (m.insert k v)[k]'mem_insert_self = v :=
   ExtDHashMap.Const.get_insert_self
 
-@[simp]
+@[simp, grind =]
 theorem getElem_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
     (m.erase k)[a]'h' = m[a]'(mem_of_mem_erase h') :=
   ExtDHashMap.Const.get_erase (h' := h')
@@ -263,7 +267,7 @@ theorem getElem_eq_get_getElem? [EquivBEq α] [LawfulHashable α] {a : α} {h} :
     m[a]'h = m[a]?.get (mem_iff_isSome_getElem?.mp h) :=
   ExtDHashMap.Const.get_eq_get_get? (h := h)
 
-theorem get_getElem? [EquivBEq α] [LawfulHashable α] {a : α} {h} :
+@[grind =] theorem get_getElem? [EquivBEq α] [LawfulHashable α] {a : α} {h} :
     m[a]?.get h = m[a]'(mem_iff_isSome_getElem?.mpr h) :=
   ExtDHashMap.Const.get_get?
 
@@ -271,12 +275,12 @@ theorem getElem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b
     m[a]'h' = m[b]'((mem_congr hab).1 h') :=
   ExtDHashMap.Const.get_congr hab (h' := h')
 
-@[simp]
+@[simp, grind =]
 theorem getElem!_empty [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
     (∅ : ExtHashMap α β)[a]! = default :=
   ExtDHashMap.Const.get!_empty
 
-theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
+@[grind =] theorem getElem!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
     (m.insert k v)[a]! = if k == a then v else m[a]! :=
   ExtDHashMap.Const.get!_insert
 
@@ -293,7 +297,7 @@ theorem getElem!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a
     ¬a ∈ m → m[a]! = default :=
   ExtDHashMap.Const.get!_eq_default
 
-theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
+@[grind =] theorem getElem!_erase [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} :
     (m.erase k)[a]! = if k == a then default else m[a]! :=
   ExtDHashMap.Const.get!_erase
 
@@ -322,12 +326,12 @@ theorem getElem!_congr [EquivBEq α] [LawfulHashable α] [Inhabited β] {a b :
     m[a]! = m[b]! :=
   ExtDHashMap.Const.get!_congr hab
 
-@[simp]
+@[simp, grind =]
 theorem getD_empty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
     (∅ : ExtHashMap α β).getD a fallback = fallback :=
   ExtDHashMap.Const.getD_empty
 
-theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
+@[grind =] theorem getD_insert [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
     (m.insert k v).getD a fallback = if k == a then v else m.getD a fallback :=
   ExtDHashMap.Const.getD_insert
 
@@ -344,7 +348,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback :
     ¬a ∈ m → m.getD a fallback = fallback :=
   ExtDHashMap.Const.getD_eq_fallback
 
-theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
+@[grind =] theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : β} :
     (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
   ExtDHashMap.Const.getD_erase
 
@@ -377,12 +381,12 @@ theorem getD_congr [EquivBEq α] [LawfulHashable α] {a b : α} {fallback : β}
     m.getD a fallback = m.getD b fallback :=
   ExtDHashMap.Const.getD_congr hab
 
-@[simp]
+@[simp, grind =]
 theorem getKey?_empty [EquivBEq α] [LawfulHashable α] {a : α} :
     (∅ : ExtHashMap α β).getKey? a = none :=
   ExtDHashMap.getKey?_empty
 
-theorem getKey?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
+@[grind =] theorem getKey?_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     (m.insert k v).getKey? a = if k == a then some k else m.getKey? a :=
   ExtDHashMap.getKey?_insert
 
@@ -420,7 +424,7 @@ theorem getKey?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {
 theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m.getKey? a = none :=
   ExtDHashMap.getKey?_eq_none
 
-theorem getKey?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
+@[grind =] theorem getKey?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.erase k).getKey? a = if k == a then none else m.getKey? a :=
   ExtDHashMap.getKey?_erase
 
@@ -442,7 +446,7 @@ theorem getKey?_eq_some_of_contains [LawfulBEq α] {k : α} (h : m.contains k) :
 theorem getKey?_eq_some [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey? k = some k := by
   simpa only [mem_iff_contains] using getKey?_eq_some_of_contains h
 
-theorem getKey_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
+@[grind =] theorem getKey_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     (m.insert k v).getKey a h₁ =
       if h₂ : k == a then k else m.getKey a ((mem_of_mem_insert h₁ (by simpa using h₂))) :=
   ExtDHashMap.getKey_insert (h₁ := h₁)
@@ -452,7 +456,7 @@ theorem getKey_insert_self [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     (m.insert k v).getKey k mem_insert_self = k :=
   ExtDHashMap.getKey_insert_self
 
-@[simp]
+@[simp, grind =]
 theorem getKey_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
     (m.erase k).getKey a h' = m.getKey a (mem_of_mem_erase h') :=
   ExtDHashMap.getKey_erase (h' := h')
@@ -465,7 +469,7 @@ theorem getKey_eq_get_getKey? [EquivBEq α] [LawfulHashable α] {a : α} {h} :
     m.getKey a h = (m.getKey? a).get (mem_iff_isSome_getKey?.mp h) :=
   ExtDHashMap.getKey_eq_get_getKey?
 
-@[simp]
+@[simp, grind =]
 theorem get_getKey? [EquivBEq α] [LawfulHashable α] {a : α} {h} :
     (m.getKey? a).get h = m.getKey a (mem_iff_isSome_getKey?.mpr h) :=
   ExtDHashMap.get_getKey?
@@ -477,16 +481,16 @@ theorem getKey_congr [EquivBEq α] [LawfulHashable α] {k₁ k₂ : α} (h : k
     (h₁ : k₁ ∈ m) : m.getKey k₁ h₁ = m.getKey k₂ ((mem_congr h).mp h₁) :=
   ExtDHashMap.getKey_congr h h₁
 
-@[simp]
+@[simp, grind =]
 theorem getKey_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.getKey k h = k :=
   ExtDHashMap.getKey_eq h
 
-@[simp]
+@[simp, grind =]
 theorem getKey!_empty [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
     (∅ : ExtHashMap α β).getKey! a = default :=
   ExtDHashMap.getKey!_empty
 
-theorem getKey!_insert [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β} :
+@[grind =] theorem getKey!_insert [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β} :
     (m.insert k v).getKey! a = if k == a then k else m.getKey! a :=
   ExtDHashMap.getKey!_insert
 
@@ -503,7 +507,7 @@ theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a :
     ¬a ∈ m → m.getKey! a = default :=
   ExtDHashMap.getKey!_eq_default
 
-theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} :
+@[grind =] theorem getKey!_erase [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} :
     (m.erase k).getKey! a = if k == a then default else m.getKey! a :=
   ExtDHashMap.getKey!_erase
 
@@ -539,12 +543,12 @@ theorem getKey!_eq_of_contains [LawfulBEq α] [Inhabited α] {k : α} (h : m.con
 theorem getKey!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : m.getKey! k = k :=
   ExtDHashMap.getKey!_eq_of_mem h
 
-@[simp]
+@[simp, grind =]
 theorem getKeyD_empty [EquivBEq α] [LawfulHashable α] {a : α} {fallback : α} :
     (∅ : ExtHashMap α β).getKeyD a fallback = fallback :=
   ExtDHashMap.getKeyD_empty
 
-theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β} :
+@[grind =] theorem getKeyD_insert [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β} :
     (m.insert k v).getKeyD a fallback = if k == a then k else m.getKeyD a fallback :=
   ExtDHashMap.getKeyD_insert
 
@@ -561,7 +565,7 @@ theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] {a : α} {fallback
     ¬a ∈ m → m.getKeyD a fallback = fallback :=
   ExtDHashMap.getKeyD_eq_fallback
 
-theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : α} :
+@[grind =] theorem getKeyD_erase [EquivBEq α] [LawfulHashable α] {k a : α} {fallback : α} :
     (m.erase k).getKeyD a fallback = if k == a then fallback else m.getKeyD a fallback :=
   ExtDHashMap.getKeyD_erase
 
@@ -607,12 +611,12 @@ theorem not_insertIfNew_eq_empty [EquivBEq α] [LawfulHashable α] {k : α} {v :
     ¬m.insertIfNew k v = ∅ :=
   (not_congr ext_iff).mpr ExtDHashMap.not_insertIfNew_eq_empty
 
-@[simp]
+@[simp, grind =]
 theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     (m.insertIfNew k v).contains a = (k == a || m.contains a) :=
   ExtDHashMap.contains_insertIfNew
 
-@[simp]
+@[simp, grind =]
 theorem mem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     a ∈ m.insertIfNew k v ↔ k == a ∨ a ∈ m :=
   ExtDHashMap.mem_insertIfNew
@@ -645,7 +649,7 @@ theorem mem_of_mem_insertIfNew' [EquivBEq α] [LawfulHashable α] {k a : α} {v
     a ∈ m.insertIfNew k v → ¬((k == a) ∧ ¬k ∈ m) → a ∈ m :=
   ExtDHashMap.mem_of_mem_insertIfNew'
 
-theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+@[grind =] theorem size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1 :=
   ExtDHashMap.size_insertIfNew
 
@@ -657,47 +661,47 @@ theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
     (m.insertIfNew k v).size ≤ m.size + 1 :=
   ExtDHashMap.size_insertIfNew_le
 
-theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
+@[grind =] theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     (m.insertIfNew k v)[a]? = if k == a ∧ ¬k ∈ m then some v else m[a]? :=
   ExtDHashMap.Const.get?_insertIfNew
 
-theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
+@[grind =] theorem getElem_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     (m.insertIfNew k v)[a]'h₁ =
       if h₂ : k == a ∧ ¬k ∈ m then v else m[a]'(mem_of_mem_insertIfNew' h₁ h₂) :=
   ExtDHashMap.Const.get_insertIfNew (h₁ := h₁)
 
-theorem getElem!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
+@[grind =] theorem getElem!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited β] {k a : α} {v : β} :
     (m.insertIfNew k v)[a]! = if k == a ∧ ¬k ∈ m then v else m[a]! :=
   ExtDHashMap.Const.get!_insertIfNew
 
-theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
+@[grind =] theorem getD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {fallback v : β} :
     (m.insertIfNew k v).getD a fallback =
       if k == a ∧ ¬k ∈ m then v else m.getD a fallback :=
   ExtDHashMap.Const.getD_insertIfNew
 
-theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
+@[grind =] theorem getKey?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     getKey? (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then some k else getKey? m a :=
   ExtDHashMap.getKey?_insertIfNew
 
-theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
+@[grind =] theorem getKey_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
     getKey (m.insertIfNew k v) a h₁ =
       if h₂ : k == a ∧ ¬k ∈ m then k else getKey m a (mem_of_mem_insertIfNew' h₁ h₂) :=
   ExtDHashMap.getKey_insertIfNew
 
-theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β} :
+@[grind =] theorem getKey!_insertIfNew [EquivBEq α] [LawfulHashable α] [Inhabited α] {k a : α} {v : β} :
     getKey! (m.insertIfNew k v) a = if k == a ∧ ¬k ∈ m then k else getKey! m a :=
   ExtDHashMap.getKey!_insertIfNew
 
-theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β} :
+@[grind =] theorem getKeyD_insertIfNew [EquivBEq α] [LawfulHashable α] {k a fallback : α} {v : β} :
     getKeyD (m.insertIfNew k v) a fallback = if k == a ∧ ¬k ∈ m then k else getKeyD m a fallback :=
   ExtDHashMap.getKeyD_insertIfNew
 
-@[simp]
+@[simp, grind =]
 theorem getThenInsertIfNew?_fst [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     (getThenInsertIfNew? m k v).1 = get? m k :=
   ExtDHashMap.Const.getThenInsertIfNew?_fst
 
-@[simp]
+@[simp, grind =]
 theorem getThenInsertIfNew?_snd [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     (getThenInsertIfNew? m k v).2 = m.insertIfNew k v :=
   ext (ExtDHashMap.Const.getThenInsertIfNew?_snd)
@@ -713,20 +717,22 @@ instance [EquivBEq α] [LawfulHashable α] : LawfulGetElem (ExtHashMap α β) α
 
 variable {ρ : Type w} [ForIn Id ρ (α × β)]
 
-@[simp]
+@[simp, grind =]
 theorem insertMany_nil [EquivBEq α] [LawfulHashable α] :
     insertMany m [] = m :=
   ext ExtDHashMap.Const.insertMany_nil
 
-@[simp]
+@[simp, grind =]
 theorem insertMany_list_singleton [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     insertMany m [⟨k, v⟩] = m.insert k v :=
   ext ExtDHashMap.Const.insertMany_list_singleton
 
+@[grind =]
 theorem insertMany_cons [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} {v : β} :
     insertMany m (⟨k, v⟩ :: l) = insertMany (m.insert k v) l :=
   ext ExtDHashMap.Const.insertMany_cons
 
+@[grind _=_]
 theorem insertMany_append [EquivBEq α] [LawfulHashable α] {l₁ l₂ : List (α × β)} :
     insertMany m (l₁ ++ l₂) = insertMany (insertMany m l₁) l₂ := by
   induction l₁ generalizing m with
@@ -742,13 +748,13 @@ theorem insertMany_ind [EquivBEq α] [LawfulHashable α]
   show motive ⟨ExtDHashMap.Const.insertMany m.1 l⟩ from
     ExtDHashMap.Const.insertMany_ind m.inner l init fun m => insert ⟨m⟩
 
-@[simp]
+@[simp, grind =]
 theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :
     (insertMany m l).contains k = (m.contains k || (l.map Prod.fst).contains k) :=
   ExtDHashMap.Const.contains_insertMany_list
 
-@[simp]
+@[simp, grind =]
 theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :
     k ∈ insertMany m l ↔ k ∈ m ∨ (l.map Prod.fst).contains k :=
@@ -776,7 +782,7 @@ theorem getElem?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
     (insertMany m l)[k']? = some v :=
   ExtDHashMap.Const.get?_insertMany_list_of_mem k_beq distinct mem
 
-theorem getElem?_insertMany_list [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem getElem?_insertMany_list [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :
     (insertMany m l)[k]? = (l.findSomeRev? (fun ⟨a, b⟩ => if a == k then some b else none)).or m[k]? :=
   ExtDHashMap.Const.get?_insertMany_list
@@ -893,11 +899,15 @@ theorem size_le_size_insertMany [EquivBEq α] [LawfulHashable α]
     {l : ρ} : m.size ≤ (insertMany m l).size :=
   ExtDHashMap.Const.size_le_size_insertMany
 
+grind_pattern size_le_size_insertMany => (insertMany m l).size
+
 theorem size_insertMany_list_le [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} :
     (insertMany m l).size ≤ m.size + l.length :=
   ExtDHashMap.Const.size_insertMany_list_le
 
+grind_pattern size_insertMany_list_le => (insertMany m l).size
+
 @[simp]
 theorem insertMany_list_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
     m.insertMany l = ∅ ↔ m = ∅ ∧ l = [] := by
@@ -1079,16 +1089,17 @@ end
 
 section
 
-@[simp]
+@[simp, grind =]
 theorem ofList_nil [EquivBEq α] [LawfulHashable α] :
     ofList ([] : List (α × β)) = ∅ :=
   ext ExtDHashMap.Const.ofList_nil
 
-@[simp]
+@[simp, grind =]
 theorem ofList_singleton [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
     ofList [⟨k, v⟩] = (∅ : ExtHashMap α β).insert k v :=
   ext ExtDHashMap.Const.ofList_singleton
 
+@[grind _=_]
 theorem ofList_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : ExtHashMap α β).insert k v) tl :=
   ext ExtDHashMap.Const.ofList_cons
@@ -1097,13 +1108,13 @@ theorem ofList_eq_insertMany_empty [EquivBEq α] [LawfulHashable α] {l : List (
     ofList l = insertMany (∅ : ExtHashMap α β) l :=
   ext ExtDHashMap.Const.ofList_eq_insertMany_empty
 
-@[simp]
+@[simp, grind =]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :
     (ofList l).contains k = (l.map Prod.fst).contains k :=
   ExtDHashMap.Const.contains_ofList
 
-@[simp]
+@[simp, grind =]
 theorem mem_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :
     k ∈ ofList l ↔ (l.map Prod.fst).contains k :=
@@ -1217,6 +1228,8 @@ theorem size_ofList_le [EquivBEq α] [LawfulHashable α]
     (ofList l).size ≤ l.length :=
   ExtDHashMap.Const.size_ofList_le
 
+grind_pattern size_ofList => (ofList l).size
+
 @[simp]
 theorem ofList_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
     ofList l = ∅ ↔ l = [] :=
@@ -1350,11 +1363,11 @@ theorem alter_eq_empty_iff [EquivBEq α] [LawfulHashable α] {k : α} {f : Optio
     alter m k f = ∅ ↔ (m = ∅ ∨ (m.size = 1 ∧ k ∈ m)) ∧ f m[k]? = none := by
   simpa only [ext_iff] using ExtDHashMap.Const.alter_eq_empty_iff
 
-theorem contains_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} :
+@[grind =] theorem contains_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} :
     (alter m k f).contains k' = if k == k' then (f m[k]?).isSome else m.contains k' :=
   ExtDHashMap.Const.contains_alter
 
-theorem mem_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} :
+@[grind =] theorem mem_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} :
     k' ∈ alter m k f ↔ if k == k' then (f m[k]?).isSome = true else k' ∈ m :=
   ExtDHashMap.Const.mem_alter
 
@@ -1381,7 +1394,7 @@ theorem mem_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α}
     {f : Option β → Option β} (h : (k == k') = false) : k' ∈ alter m k f ↔ k' ∈ m :=
   ExtDHashMap.Const.mem_alter_of_beq_eq_false h
 
-theorem size_alter [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
+@[grind =] theorem size_alter [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} :
     (m.alter k f).size =
       if k ∈ m ∧ (f m[k]?).isNone then
         m.size - 1
@@ -1419,7 +1432,7 @@ theorem size_le_size_alter [EquivBEq α] [LawfulHashable α] {k : α} {f : Optio
     m.size - 1 ≤ (alter m k f).size :=
   ExtDHashMap.Const.size_le_size_alter
 
-theorem getElem?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
+@[grind =] theorem getElem?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
     (alter m k f)[k']? =
       if k == k' then
         f m[k]?
@@ -1446,7 +1459,7 @@ theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option
     get? (alter m k f) k = f (get? m k) :=
   ExtDHashMap.Const.get?_alter_self
 
-theorem getElem_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
+@[grind =] theorem getElem_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
     {h : k' ∈ alter m k f} :
     (alter m k f)[k'] =
       if heq : k == k' then
@@ -1483,7 +1496,7 @@ theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β
     get (alter m k f) k h = (f (get? m k)).get h' :=
   ExtDHashMap.Const.get_alter_self
 
-theorem getElem!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β]
+@[grind =] theorem getElem!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β]
     {f : Option β → Option β} : (alter m k f)[k']! =
       if k == k' then
         f m[k]? |>.get!
@@ -1510,7 +1523,7 @@ theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β
     {f : Option β → Option β} : get! (alter m k f) k = (f (get? m k)).get! :=
   ExtDHashMap.Const.get!_alter_self
 
-theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β}
+@[grind =] theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β}
     {f : Option β → Option β} :
     getD (alter m k f) k' fallback =
       if k == k' then
@@ -1525,7 +1538,7 @@ theorem getD_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback :
     getD (alter m k f) k fallback = (f m[k]?).getD fallback :=
   ExtDHashMap.Const.getD_alter_self
 
-theorem getKey?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
+@[grind =] theorem getKey?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} :
     (alter m k f).getKey? k' =
       if k == k' then
         if (f m[k]?).isSome then some k else none
@@ -1537,7 +1550,7 @@ theorem getKey?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Optio
     (alter m k f).getKey? k = if (f m[k]?).isSome then some k else none :=
   ExtDHashMap.Const.getKey?_alter_self
 
-theorem getKey!_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
+@[grind =] theorem getKey!_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
     {f : Option β → Option β} : (alter m k f).getKey! k' =
       if k == k' then
         if (f m[k]?).isSome then k else default
@@ -1550,7 +1563,7 @@ theorem getKey!_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k :
     (alter m k f).getKey! k = if (f m[k]?).isSome then k else default :=
   ExtDHashMap.Const.getKey!_alter_self
 
-theorem getKey_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
+@[grind =] theorem getKey_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α}
     {f : Option β → Option β} {h : k' ∈ alter m k f} :
     (alter m k f).getKey k' h =
       if heq : k == k' then
@@ -1566,7 +1579,7 @@ theorem getKey_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k :
     (alter m k f).getKey k h = k :=
   ExtDHashMap.Const.getKey_alter_self
 
-theorem getKeyD_alter [EquivBEq α] [LawfulHashable α] {k k' fallback : α}
+@[grind =] theorem getKeyD_alter [EquivBEq α] [LawfulHashable α] {k k' fallback : α}
     {f : Option β → Option β} :
     (alter m k f).getKeyD k' fallback =
       if k == k' then
@@ -1591,22 +1604,22 @@ theorem modify_eq_empty_iff [EquivBEq α] [LawfulHashable α] {k : α} {f : β
     modify m k f = ∅ ↔ m = ∅ := by
   simpa only [ext_iff] using ExtDHashMap.Const.modify_eq_empty_iff
 
-@[simp]
+@[simp, grind =]
 theorem contains_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} :
     (modify m k f).contains k' = m.contains k' :=
   ExtDHashMap.Const.contains_modify
 
-@[simp]
+@[simp, grind =]
 theorem mem_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} :
     k' ∈ modify m k f ↔ k' ∈ m :=
   ExtDHashMap.Const.mem_modify
 
-@[simp]
+@[simp, grind =]
 theorem size_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} :
     (modify m k f).size = m.size :=
   ExtDHashMap.Const.size_modify
 
-theorem getElem?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
+@[grind =] theorem getElem?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
     (modify m k f)[k']? =
       if k == k' then
         m[k]?.map f
@@ -1633,7 +1646,7 @@ theorem get?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β →
     get? (modify m k f) k = (get? m k).map f :=
   ExtDHashMap.Const.get?_modify_self
 
-theorem getElem_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β}
+@[grind =] theorem getElem_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β}
     {h : k' ∈ modify m k f} :
     (modify m k f)[k'] =
       if heq : k == k' then
@@ -1670,7 +1683,7 @@ theorem get_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β →
     get (modify m k f) k h = f (get m k h') :=
   ExtDHashMap.Const.get_modify_self
 
-theorem getElem!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} :
+@[grind =] theorem getElem!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} :
     (modify m k f)[k']! =
       if k == k' then
         m[k]?.map f |>.get!
@@ -1697,7 +1710,7 @@ theorem get!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited
     get! (modify m k f) k = ((get? m k).map f).get! :=
   ExtDHashMap.Const.get!_modify_self
 
-theorem getD_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} :
+@[grind =] theorem getD_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} :
     getD (modify m k f) k' fallback =
       if k == k' then
         m[k]?.map f |>.getD fallback
@@ -1710,7 +1723,7 @@ theorem getD_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback :
     getD (modify m k f) k fallback = (m[k]?.map f).getD fallback :=
   ExtDHashMap.Const.getD_modify_self
 
-theorem getKey?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
+@[grind =] theorem getKey?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} :
     (modify m k f).getKey? k' =
       if k == k' then
         if k ∈ m then some k else none
@@ -1722,7 +1735,7 @@ theorem getKey?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β
     (modify m k f).getKey? k = if k ∈ m then some k else none :=
   ExtDHashMap.Const.getKey?_modify_self
 
-theorem getKey!_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} :
+@[grind =] theorem getKey!_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} :
     (modify m k f).getKey! k' =
       if k == k' then
         if k ∈ m then k else default
@@ -1734,7 +1747,7 @@ theorem getKey!_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k
     (modify m k f).getKey! k = if k ∈ m then k else default :=
   ExtDHashMap.Const.getKey!_modify_self
 
-theorem getKey_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β}
+@[grind =] theorem getKey_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β}
     {h : k' ∈ modify m k f} :
     (modify m k f).getKey k' h =
       if k == k' then
@@ -1749,7 +1762,7 @@ theorem getKey_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k :
     {h : k ∈ modify m k f} : (modify m k f).getKey k h = k :=
   ExtDHashMap.Const.getKey_modify_self
 
-theorem getKeyD_modify [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} :
+@[grind =] theorem getKeyD_modify [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} :
     (modify m k f).getKeyD k' fallback =
       if k == k' then
         if k ∈ m then k else fallback
@@ -1801,7 +1814,7 @@ theorem filterMap_eq_empty_iff [EquivBEq α] [LawfulHashable α] {f : α → β
     m.filterMap f = ∅ ↔ ∀ k h, f (m.getKey k h) (m[k]'h) = none :=
   ext_iff.trans ExtDHashMap.Const.filterMap_eq_empty_iff
 
-theorem mem_filterMap [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem mem_filterMap [EquivBEq α] [LawfulHashable α]
     {f : α → β → Option γ} {k : α} :
     k ∈ m.filterMap f ↔ ∃ h, (f (m.getKey k h) m[k]).isSome :=
   ExtDHashMap.Const.mem_filterMap
@@ -1821,12 +1834,14 @@ theorem size_filterMap_le_size [EquivBEq α] [LawfulHashable α]
     (m.filterMap f).size ≤ m.size :=
   ExtDHashMap.size_filterMap_le_size
 
+grind_pattern size_filterMap_le_size => (m.filterMap f).size
+
 theorem size_filterMap_eq_size_iff [EquivBEq α] [LawfulHashable α]
     {f : α → β → Option γ} :
     (m.filterMap f).size = m.size ↔ ∀ k h, (f (m.getKey k h) m[k]).isSome :=
   ExtDHashMap.Const.size_filterMap_eq_size_iff
 
-theorem getElem?_filterMap [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem getElem?_filterMap [EquivBEq α] [LawfulHashable α]
     {f : α → β → Option γ} {k : α} :
     (m.filterMap f)[k]? = m[k]?.pbind (fun x h' =>
       f (m.getKey k (mem_iff_isSome_getElem?.mpr (Option.isSome_of_eq_some h'))) x) :=
@@ -1844,8 +1859,7 @@ theorem isSome_apply_of_mem_filterMap [EquivBEq α] [LawfulHashable α]
         (m[k]'(mem_of_mem_filterMap h))).isSome :=
   ExtDHashMap.Const.isSome_apply_of_mem_filterMap
 
-@[simp]
-theorem getElem_filterMap [EquivBEq α] [LawfulHashable α]
+@[simp, grind =] theorem getElem_filterMap [EquivBEq α] [LawfulHashable α]
     {f : α → β → Option γ} {k : α} {h} :
     (m.filterMap f)[k]'h =
       (f (m.getKey k (mem_of_mem_filterMap h))
@@ -1853,7 +1867,7 @@ theorem getElem_filterMap [EquivBEq α] [LawfulHashable α]
           (isSome_apply_of_mem_filterMap h) :=
   ExtDHashMap.Const.get_filterMap (h := h)
 
-theorem getElem!_filterMap [EquivBEq α] [LawfulHashable α] [Inhabited γ]
+@[grind =] theorem getElem!_filterMap [EquivBEq α] [LawfulHashable α] [Inhabited γ]
     {f : α → β → Option γ} {k : α} :
     (m.filterMap f)[k]! =
       (m[k]?.pbind (fun x h' =>
@@ -1865,7 +1879,7 @@ theorem getElem!_filterMap_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α]
     (m.filterMap f)[k]! = (m[k]?.bind (f k')).get! :=
   ExtDHashMap.Const.get!_filterMap_of_getKey?_eq_some h
 
-theorem getD_filterMap [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem getD_filterMap [EquivBEq α] [LawfulHashable α]
     {f : α → β → Option γ} {k : α} {fallback : γ} :
     (m.filterMap f).getD k fallback =
       (m[k]?.pbind (fun x h' =>
@@ -1877,27 +1891,27 @@ theorem getD_filterMap_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α]
     (m.filterMap f).getD k fallback = (m[k]?.bind (f k')).getD fallback :=
   ExtDHashMap.Const.getD_filterMap_of_getKey?_eq_some h
 
-theorem getKey?_filterMap [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem getKey?_filterMap [EquivBEq α] [LawfulHashable α]
     {f : α → β → Option γ} {k : α} :
     (m.filterMap f).getKey? k =
     (m.getKey? k).pfilter (fun x h' =>
       (f x (m[x]'(mem_of_getKey?_eq_some h'))).isSome) :=
   ExtDHashMap.Const.getKey?_filterMap
 
-@[simp]
+@[simp, grind =]
 theorem getKey_filterMap [EquivBEq α] [LawfulHashable α]
     {f : α → β → Option γ} {k : α} {h'} :
     (m.filterMap f).getKey k h' = m.getKey k (mem_of_mem_filterMap h') :=
   ExtDHashMap.getKey_filterMap
 
-theorem getKey!_filterMap [EquivBEq α] [LawfulHashable α] [Inhabited α]
+@[grind =] theorem getKey!_filterMap [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {f : α → β → Option γ} {k : α} :
     (m.filterMap f).getKey! k =
     ((m.getKey? k).pfilter (fun x h' =>
       (f x (m[x]'(mem_of_getKey?_eq_some h'))).isSome)).get! :=
   ExtDHashMap.Const.getKey!_filterMap
 
-theorem getKeyD_filterMap [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem getKeyD_filterMap [EquivBEq α] [LawfulHashable α]
     {f : α → β → Option γ} {k fallback : α} :
     (m.filterMap f).getKeyD k fallback =
     ((m.getKey? k).pfilter (fun x h' =>
@@ -1918,7 +1932,7 @@ theorem filter_eq_empty_iff [EquivBEq α] [LawfulHashable α] {f : α → β →
     m.filter f = ∅ ↔ ∀ k h, f (m.getKey k h) (m[k]'h) = false :=
   ext_iff.trans ExtDHashMap.Const.filter_eq_empty_iff
 
-theorem mem_filter [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem mem_filter [EquivBEq α] [LawfulHashable α]
     {f : α → β → Bool} {k : α} :
     k ∈ m.filter f ↔ ∃ (h' : k ∈ m), f (m.getKey k h') m[k] :=
   ExtDHashMap.Const.mem_filter
@@ -1938,6 +1952,8 @@ theorem size_filter_le_size [EquivBEq α] [LawfulHashable α]
     (m.filter f).size ≤ m.size :=
   ExtDHashMap.size_filter_le_size
 
+grind_pattern size_filter_le_size => (m.filter f).size
+
 theorem size_filter_eq_size_iff [EquivBEq α] [LawfulHashable α]
     {f : α → β → Bool} :
     (m.filter f).size = m.size ↔ ∀ k h, f (m.getKey k h) (m.get k h) :=
@@ -1948,7 +1964,7 @@ theorem filter_eq_self_iff [EquivBEq α] [LawfulHashable α]
     m.filter f = m ↔ ∀ k h, f (m.getKey k h) (m.get k h) :=
   ext_iff.trans ExtDHashMap.Const.filter_eq_self_iff
 
-theorem getElem?_filter [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem getElem?_filter [EquivBEq α] [LawfulHashable α]
     {f : α → β → Bool} {k : α} :
     (m.filter f)[k]? = m[k]?.pfilter (fun x h' =>
       f (m.getKey k (mem_iff_isSome_getElem?.mpr (Option.isSome_of_eq_some h'))) x) :=
@@ -1960,13 +1976,12 @@ theorem getElem?_filter_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α]
       (m.filter f)[k]? = m[k]?.filter (fun x => f k' x) :=
   ExtDHashMap.Const.get?_filter_of_getKey?_eq_some
 
-@[simp]
-theorem getElem_filter [EquivBEq α] [LawfulHashable α]
+@[simp, grind =] theorem getElem_filter [EquivBEq α] [LawfulHashable α]
     {f : α → β → Bool} {k : α} {h'} :
     (m.filter f)[k]'(h') = m[k]'(mem_of_mem_filter h') :=
   ExtDHashMap.Const.get_filter (h' := h')
 
-theorem getElem!_filter [EquivBEq α] [LawfulHashable α] [Inhabited β]
+@[grind =] theorem getElem!_filter [EquivBEq α] [LawfulHashable α] [Inhabited β]
     {f : α → β → Bool} {k : α} :
     (m.filter f)[k]! =
       (m[k]?.pfilter (fun x h' =>
@@ -1979,7 +1994,7 @@ theorem getElem!_filter_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] [In
       (m.filter f)[k]! = (m[k]?.filter (f k')).get! :=
   ExtDHashMap.Const.get!_filter_of_getKey?_eq_some
 
-theorem getD_filter [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem getD_filter [EquivBEq α] [LawfulHashable α]
     {f : α → β → Bool} {k : α} {fallback : β} :
     (m.filter f).getD k fallback = (m[k]?.pfilter (fun x h' =>
       f (m.getKey k (mem_iff_isSome_getElem?.mpr (Option.isSome_of_eq_some h'))) x)).getD fallback :=
@@ -1992,7 +2007,7 @@ theorem getD_filter_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α]
         (m[k]?.filter (fun x => f k' x)).getD fallback :=
   ExtDHashMap.Const.getD_filter_of_getKey?_eq_some
 
-theorem getKey?_filter [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem getKey?_filter [EquivBEq α] [LawfulHashable α]
     {f : α → β → Bool} {k : α} :
     (m.filter f).getKey? k =
     (m.getKey? k).pfilter (fun x h' =>
@@ -2004,13 +2019,13 @@ theorem getKey?_filter_key [EquivBEq α] [LawfulHashable α]
     (m.filter fun k _ => f k).getKey? k = (m.getKey? k).filter f :=
   ExtDHashMap.getKey?_filter_key
 
-@[simp]
+@[simp, grind =]
 theorem getKey_filter [EquivBEq α] [LawfulHashable α]
     {f : α → β → Bool} {k : α} {h'} :
     (m.filter f).getKey k h' = m.getKey k (mem_of_mem_filter h') :=
   ExtDHashMap.getKey_filter
 
-theorem getKey!_filter [EquivBEq α] [LawfulHashable α] [Inhabited α]
+@[grind =] theorem getKey!_filter [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {f : α → β → Bool} {k : α} :
     (m.filter f).getKey! k =
     ((m.getKey? k).pfilter (fun x h' =>
@@ -2022,7 +2037,7 @@ theorem getKey!_filter_key [EquivBEq α] [LawfulHashable α] [Inhabited α]
     (m.filter fun k _ => f k).getKey! k = ((m.getKey? k).filter f).get! :=
   ExtDHashMap.getKey!_filter_key
 
-theorem getKeyD_filter [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem getKeyD_filter [EquivBEq α] [LawfulHashable α]
     {f : α → β → Bool} {k fallback : α} :
     (m.filter f).getKeyD k fallback =
     ((m.getKey? k).pfilter (fun x h' =>
@@ -2059,7 +2074,7 @@ theorem map_eq_empty_iff [EquivBEq α] [LawfulHashable α] {f : α → β → γ
     m.map f = ∅ ↔ m = ∅ := by
   simpa only [ext_iff] using ExtDHashMap.map_eq_empty_iff
 
-@[simp]
+@[simp, grind =]
 theorem contains_map [EquivBEq α] [LawfulHashable α]
     {f : α → β → γ} {k : α} :
     (m.map f).contains k = m.contains k :=
@@ -2070,7 +2085,7 @@ theorem contains_of_contains_map [EquivBEq α] [LawfulHashable α]
     (m.map f).contains k = true → m.contains k = true :=
   ExtDHashMap.contains_of_contains_map
 
-@[simp]
+@[simp, grind =]
 theorem mem_map [EquivBEq α] [LawfulHashable α]
     {f : α → β → γ} {k : α} :
     k ∈ m.map f ↔ k ∈ m := by
@@ -2081,13 +2096,13 @@ theorem mem_of_mem_map [EquivBEq α] [LawfulHashable α]
     k ∈ m.map f → k ∈ m :=
   ExtDHashMap.contains_of_contains_map
 
-@[simp]
+@[simp, grind =]
 theorem size_map [EquivBEq α] [LawfulHashable α]
     {f : α → β → γ} :
     (m.map f).size = m.size :=
   ExtDHashMap.size_map
 
-@[simp]
+@[simp, grind =]
 theorem getElem?_map [LawfulBEq α] [LawfulHashable α]
     {f : α → β → γ} {k : α} :
     (m.map f)[k]? = m[k]?.map (f k) :=
@@ -2106,7 +2121,7 @@ theorem getElem?_map_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α]
     (m.map f)[k]? = m[k]?.map (f k') :=
   ExtDHashMap.Const.get?_map_of_getKey?_eq_some h
 
-@[simp]
+@[simp, grind =]
 theorem getElem_map [LawfulBEq α] [LawfulHashable α]
     {f : α → β → γ} {k : α} {h'} :
     (m.map f)[k]' h' =
@@ -2121,7 +2136,7 @@ theorem getElem_map' [EquivBEq α] [LawfulHashable α]
       f (m.getKey k (mem_of_mem_map h')) (m[k]'(mem_of_mem_map h')) :=
   ExtDHashMap.Const.get_map' (h' := h')
 
-theorem getElem!_map [LawfulBEq α] [LawfulHashable α] [Inhabited γ]
+@[grind =] theorem getElem!_map [LawfulBEq α] [LawfulHashable α] [Inhabited γ]
     {f : α → β → γ} {k : α} :
     (m.map f)[k]! =
       (m[k]?.map (f k)).get! :=
@@ -2140,7 +2155,7 @@ theorem getElem!_map_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] [Inhab
     (m.map f)[k]! = (m[k]?.map (f k')).get! :=
   ExtDHashMap.Const.get!_map_of_getKey?_eq_some h
 
-theorem getD_map [LawfulBEq α] [LawfulHashable α]
+@[grind =] theorem getD_map [LawfulBEq α] [LawfulHashable α]
     {f : α → β → γ} {k : α} {fallback : γ} :
     (m.map f).getD k fallback =
       (m[k]?.map (f k)).getD fallback :=
@@ -2159,25 +2174,25 @@ theorem getD_map_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] [Inhabited
     (m.map f).getD k fallback = (m[k]?.map (f k')).getD fallback :=
   ExtDHashMap.Const.getD_map_of_getKey?_eq_some h
 
-@[simp]
+@[simp, grind =]
 theorem getKey?_map [EquivBEq α] [LawfulHashable α]
     {f : α → β → γ} {k : α} :
     (m.map f).getKey? k = m.getKey? k :=
   ExtDHashMap.getKey?_map
 
-@[simp]
+@[simp, grind =]
 theorem getKey_map [EquivBEq α] [LawfulHashable α]
     {f : α → β → γ} {k : α} {h'} :
     (m.map f).getKey k h' = m.getKey k (mem_of_mem_map h') :=
   ExtDHashMap.getKey_map
 
-@[simp]
+@[simp, grind =]
 theorem getKey!_map [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {f : α → β → γ} {k : α} :
     (m.map f).getKey! k = m.getKey! k :=
   ExtDHashMap.getKey!_map
 
-@[simp]
+@[simp, grind =]
 theorem getKeyD_map [EquivBEq α] [LawfulHashable α]
     {f : α → β → γ} {k fallback : α} :
     (m.map f).getKeyD k fallback = m.getKeyD k fallback :=

src/Std/Data/ExtHashSet/Lemmas.lean

@@ -13,6 +13,8 @@ import Std.Data.ExtHashSet.Basic
 This module contains lemmas about `Std.ExtHashSet`.
 -/
 
+set_option trace.grind.ematch.pattern true
+
 set_option linter.missingDocs true
 set_option autoImplicit false
 
@@ -32,7 +34,7 @@ private theorem ext {m m' : ExtHashSet α} : m.inner = m'.inner → m = m' := by
 private theorem ext_iff {m m' : ExtHashSet α} : m = m' ↔ m.inner = m'.inner :=
   ⟨fun h => h ▸ rfl, ext⟩
 
-@[simp]
+@[simp, grind =]
 theorem isEmpty_iff [EquivBEq α] [LawfulHashable α] : m.isEmpty ↔ m = ∅ :=
   ExtHashMap.isEmpty_iff.trans ext_iff.symm
 
@@ -43,7 +45,7 @@ theorem isEmpty_eq_false_iff [EquivBEq α] [LawfulHashable α] : m.isEmpty = fal
 @[simp]
 theorem empty_eq : ∅ = m ↔ m = ∅ := eq_comm
 
-@[simp]
+@[simp, grind =]
 theorem emptyWithCapacity_eq [EquivBEq α] [LawfulHashable α] {c} : (emptyWithCapacity c : ExtHashSet α) = ∅ :=
   ext ExtHashMap.emptyWithCapacity_eq
 
@@ -66,7 +68,7 @@ theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a ==
 theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m :=
   ExtHashMap.mem_congr hab
 
-@[simp] theorem contains_empty [EquivBEq α] [LawfulHashable α] {a : α} :
+@[simp, grind =] theorem contains_empty [EquivBEq α] [LawfulHashable α] {a : α} :
     (∅ : ExtHashSet α).contains a = false :=
   ExtHashMap.contains_empty
 
@@ -87,12 +89,12 @@ theorem eq_empty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] : m = ∅
     Singleton.singleton a = (∅ : ExtHashSet α).insert a :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.insert k).contains a = (k == a || m.contains a) :=
   ExtHashMap.contains_insertIfNew
 
-@[simp]
+@[simp, grind =]
 theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.insert k ↔ k == a ∨ a ∈ m :=
   ExtHashMap.mem_insertIfNew
 
@@ -121,13 +123,14 @@ theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.ins
 
 theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m.insert k := by simp
 
-@[simp]
+@[simp, grind =]
 theorem size_empty [EquivBEq α] [LawfulHashable α] : (∅ : ExtHashSet α).size = 0 :=
   ExtHashMap.size_empty
 
 theorem eq_empty_iff_size_eq_zero [EquivBEq α] [LawfulHashable α] : m = ∅ ↔ m.size = 0 :=
   ext_iff.trans ExtHashMap.eq_empty_iff_size_eq_zero
 
+@[grind =]
 theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} :
     (m.insert k).size = if k ∈ m then m.size else m.size + 1 :=
   ExtHashMap.size_insertIfNew
@@ -139,7 +142,7 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} :
     (m.insert k).size ≤ m.size + 1 :=
   ExtHashMap.size_insertIfNew_le
 
-@[simp]
+@[simp, grind =]
 theorem erase_empty [EquivBEq α] [LawfulHashable α] {a : α} : (∅ : ExtHashSet α).erase a = ∅ :=
   ext ExtHashMap.erase_empty
 
@@ -148,12 +151,12 @@ theorem erase_eq_empty_iff [EquivBEq α] [LawfulHashable α] {k : α} :
     m.erase k = ∅ ↔ m = ∅ ∨ m.size = 1 ∧ k ∈ m := by
   simpa only [ext_iff] using ExtHashMap.erase_eq_empty_iff
 
-@[simp]
+@[simp, grind =]
 theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.erase k).contains a = (!(k == a) && m.contains a) :=
   ExtHashMap.contains_erase
 
-@[simp]
+@[simp, grind =]
 theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m :=
   ExtHashMap.mem_erase
@@ -165,6 +168,7 @@ theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α}
 theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.erase k → a ∈ m :=
   ExtHashMap.mem_of_mem_erase
 
+@[grind =]
 theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
     (m.erase k).size = if k ∈ m then m.size - 1 else m.size :=
   ExtHashMap.size_erase
@@ -176,10 +180,11 @@ theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
     m.size ≤ (m.erase k).size + 1 :=
   ExtHashMap.size_le_size_erase
 
-@[simp]
+@[simp, grind =]
 theorem get?_empty [EquivBEq α] [LawfulHashable α] {a : α} : (∅ : ExtHashSet α).get? a = none :=
   ExtHashMap.getKey?_empty
 
+@[grind =]
 theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.insert k).get? a = if k == a ∧ ¬k ∈ m then some k else m.get? a :=
   ExtHashMap.getKey?_insertIfNew
@@ -209,6 +214,7 @@ theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a :
 theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m.get? a = none :=
   ExtHashMap.getKey?_eq_none
 
+@[grind =]
 theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.erase k).get? a = if k == a then none else m.get? a :=
   ExtHashMap.getKey?_erase
@@ -230,12 +236,13 @@ theorem get?_eq_some_of_contains [LawfulBEq α] {k : α} (h : m.contains k) : m.
 theorem get?_eq_some [LawfulBEq α] {k : α} (h : k ∈ m) : m.get? k = some k :=
   ExtHashMap.getKey?_eq_some h
 
+@[grind =]
 theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {h₁} :
     (m.insert k).get a h₁ =
       if h₂ : k == a ∧ ¬k ∈ m then k else m.get a (mem_of_mem_insert' h₁ h₂) :=
   ExtHashMap.getKey_insertIfNew (h₁ := h₁)
 
-@[simp]
+@[simp, grind =]
 theorem get_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
     (m.erase k).get a h' = m.get a (mem_of_mem_erase h') :=
   ExtHashMap.getKey_erase (h' := h')
@@ -248,7 +255,7 @@ theorem get_eq_get_get? [EquivBEq α] [LawfulHashable α] {k : α} {h} :
     m.get k h = (m.get? k).get (mem_iff_isSome_get?.mp h) :=
   ExtHashMap.getKey_eq_get_getKey?
 
-theorem get_get? [EquivBEq α] [LawfulHashable α] {k : α} {h} :
+@[grind =] theorem get_get? [EquivBEq α] [LawfulHashable α] {k : α} {h} :
     (m.get? k).get h = m.get k (mem_iff_isSome_get?.mpr h) :=
   ExtHashMap.get_getKey?
 
@@ -259,15 +266,16 @@ theorem get_congr [EquivBEq α] [LawfulHashable α] {k₁ k₂ : α} (h : k₁ =
     (h₁ : k₁ ∈ m) : m.get k₁ h₁ = m.get k₂ ((mem_congr h).mp h₁) :=
   ExtHashMap.getKey_congr h h₁
 
-@[simp]
+@[simp, grind =]
 theorem get_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.get k h = k :=
   ExtHashMap.getKey_eq h
 
-@[simp]
+@[simp, grind =]
 theorem get!_empty [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
     (∅ : ExtHashSet α).get! a = default :=
   ExtHashMap.getKey!_empty
 
+@[grind =]
 theorem get!_insert [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.insert k).get! a = if k == a ∧ ¬k ∈ m then k else m.get! a :=
   ExtHashMap.getKey!_insertIfNew
@@ -280,6 +288,7 @@ theorem get!_eq_default [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α
     ¬a ∈ m → m.get! a = default :=
   ExtHashMap.getKey!_eq_default
 
+@[grind =]
 theorem get!_erase [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.erase k).get! a = if k == a then default else m.get! a :=
   ExtHashMap.getKey!_erase
@@ -315,12 +324,12 @@ theorem get!_eq_of_contains [LawfulBEq α] [Inhabited α] {k : α} (h : m.contai
 theorem get!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : m.get! k = k :=
   ExtHashMap.getKey!_eq_of_mem h
 
-@[simp]
+@[simp, grind =]
 theorem getD_empty [EquivBEq α] [LawfulHashable α] {a fallback : α} :
     (∅ : ExtHashSet α).getD a fallback = fallback :=
   ExtHashMap.getKeyD_empty
 
-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
 
@@ -333,7 +342,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a fallback : α} :
     ¬a ∈ m → m.getD a fallback = fallback :=
   ExtHashMap.getKeyD_eq_fallback
 
-theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
+@[grind =] theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
     (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
   ExtHashMap.getKeyD_erase
 
@@ -373,32 +382,34 @@ theorem getD_eq_of_contains [LawfulBEq α] {k fallback : α} (h : m.contains k)
 theorem getD_eq_of_mem [LawfulBEq α] {k fallback : α} (h : k ∈ m) : m.getD k fallback = k :=
   ExtHashMap.getKeyD_eq_of_mem h
 
-@[simp]
+@[simp, grind =]
 theorem containsThenInsert_fst [EquivBEq α] [LawfulHashable α] {k : α} :
     (m.containsThenInsert k).1 = m.contains k :=
   ExtHashMap.containsThenInsertIfNew_fst
 
-@[simp]
+@[simp, grind =]
 theorem containsThenInsert_snd [EquivBEq α] [LawfulHashable α] {k : α} :
     (m.containsThenInsert k).2 = m.insert k :=
   ext ExtHashMap.containsThenInsertIfNew_snd
 
 variable {ρ : Type v} [ForIn Id ρ α]
 
-@[simp]
+@[simp, grind =]
 theorem insertMany_nil [EquivBEq α] [LawfulHashable α] :
     insertMany m [] = m :=
   ext ExtHashMap.insertManyIfNewUnit_nil
 
-@[simp]
+@[simp, grind =]
 theorem insertMany_list_singleton [EquivBEq α] [LawfulHashable α] {k : α} :
     insertMany m [k] = m.insert k :=
   ext ExtHashMap.insertManyIfNewUnit_list_singleton
 
+@[grind _=_]
 theorem insertMany_cons [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} :
     insertMany m (k :: l) = insertMany (m.insert k) l :=
   ext ExtHashMap.insertManyIfNewUnit_cons
 
+@[grind _=_]
 theorem insertMany_append [EquivBEq α] [LawfulHashable α] {l₁ l₂ : List α} :
     insertMany m (l₁ ++ l₂) = insertMany (insertMany m l₁) l₂ := by
   induction l₁ generalizing m with
@@ -414,13 +425,13 @@ theorem insertMany_ind [EquivBEq α] [LawfulHashable α]
   show motive ⟨m.1.insertManyIfNewUnit l⟩ from
     ExtHashMap.insertManyIfNewUnit_ind m.inner l init fun m => insert ⟨m⟩
 
-@[simp]
+@[simp, grind =]
 theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     (insertMany m l).contains k = (m.contains k || l.contains k) :=
   ExtHashMap.contains_insertManyIfNewUnit_list
 
-@[simp]
+@[simp, grind =]
 theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     k ∈ insertMany m l ↔ k ∈ m ∨ l.contains k :=
@@ -525,11 +536,15 @@ theorem size_le_size_insertMany [EquivBEq α] [LawfulHashable α]
     {l : ρ} : m.size ≤ (insertMany m l).size :=
   ExtHashMap.size_le_size_insertManyIfNewUnit
 
+grind_pattern size_le_size_insertMany => (insertMany m l).size
+
 theorem size_insertMany_list_le [EquivBEq α] [LawfulHashable α]
     {l : List α} :
     (insertMany m l).size ≤ m.size + l.length :=
   ExtHashMap.size_insertManyIfNewUnit_list_le
 
+grind_pattern size_insertMany_list_le => (insertMany m l).size
+
 @[simp]
 theorem insertMany_list_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List α} :
     m.insertMany l = ∅ ↔ m = ∅ ∧ l = [] := by
@@ -543,16 +558,17 @@ end
 
 section
 
-@[simp]
+@[simp, grind =]
 theorem ofList_nil [EquivBEq α] [LawfulHashable α] :
     ofList ([] : List α) = ∅ :=
   ext ExtHashMap.unitOfList_nil
 
-@[simp]
+@[simp, grind =]
 theorem ofList_singleton [EquivBEq α] [LawfulHashable α] {k : α} :
     ofList [k] = (∅ : ExtHashSet α).insert k :=
   ext ExtHashMap.unitOfList_singleton
 
+@[grind _=_]
 theorem ofList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List α} :
     ofList (hd :: tl) =
       insertMany ((∅ : ExtHashSet α).insert hd) tl :=
@@ -564,13 +580,13 @@ theorem ofList_eq_insertMany_empty [EquivBEq α] [LawfulHashable α] {l : List
   | [] => by simp
   | hd :: tl => by simp [ofList_cons, insertMany_cons]
 
-@[simp]
+@[simp, grind =]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     (ofList l).contains k = l.contains k :=
   ExtHashMap.contains_unitOfList
 
-@[simp]
+@[simp, grind =]
 theorem mem_ofList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     k ∈ ofList l ↔ l.contains k :=
@@ -632,6 +648,8 @@ theorem size_ofList_le [EquivBEq α] [LawfulHashable α]
     (ofList l).size ≤ l.length :=
   ExtHashMap.size_unitOfList_le
 
+grind_pattern size_ofList_le => (ofList l).size
+
 @[simp]
 theorem ofList_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List α} :
     ofList l = ∅ ↔ l = [] :=
@@ -664,7 +682,7 @@ theorem filter_eq_empty_iff [EquivBEq α] [LawfulHashable α] {f : α → Bool}
     m.filter f = ∅ ↔ ∀ k h, f (m.get k h) = false :=
   ext_iff.trans ExtHashMap.filter_eq_empty_iff
 
-@[simp]
+@[simp, grind =]
 theorem mem_filter [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} {k : α} :
     k ∈ m.filter f ↔ ∃ h, f (m.get k h) :=
@@ -685,6 +703,8 @@ theorem size_filter_le_size [EquivBEq α] [LawfulHashable α]
     (m.filter f).size ≤ m.size :=
   ExtHashMap.size_filter_le_size
 
+grind_pattern size_filter_le_size => (m.filter f).size
+
 theorem size_filter_eq_size_iff [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} :
     (m.filter f).size = m.size ↔ ∀ k h, f (m.get k h) :=
@@ -695,23 +715,25 @@ theorem filter_eq_self_iff [EquivBEq α] [LawfulHashable α]
     m.filter f = m ↔ ∀ k h, f (m.get k h) :=
   ext_iff.trans ExtHashMap.filter_eq_self_iff
 
-@[simp]
+@[simp, grind =]
 theorem get?_filter [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} {k : α} :
     (m.filter f).get? k = (m.get? k).filter f :=
   ExtHashMap.getKey?_filter_key
 
-@[simp]
+@[simp, grind =]
 theorem get_filter [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} {k : α} {h} :
     (m.filter f).get k h = m.get k (mem_of_mem_filter h) :=
   ExtHashMap.getKey_filter
 
+@[grind =]
 theorem get!_filter [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {f : α → Bool} {k : α} :
     (m.filter f).get! k = ((m.get? k).filter f).get! :=
   ExtHashMap.getKey!_filter_key
 
+@[grind =]
 theorem getD_filter [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} {k fallback : α} :
     (m.filter f).getD k fallback = ((m.get? k).filter f).getD fallback :=

src/Std/Data/HashSet/Lemmas.lean

@@ -15,6 +15,8 @@ This module contains lemmas about `Std.Data.HashSet`. Most of the lemmas require
 is to provide an instance of `LawfulBEq α`.
 -/
 
+set_option trace.grind.ematch.pattern true
+
 set_option linter.missingDocs true
 set_option autoImplicit false
 
@@ -31,11 +33,11 @@ variable {m : HashSet α}
 private theorem ext {m m' : HashSet α} : m.inner = m'.inner → m = m' := by
   cases m; cases m'; rintro rfl; rfl
 
-@[simp]
+@[simp, grind =]
 theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : HashSet α).isEmpty :=
   HashMap.isEmpty_emptyWithCapacity
 
-@[simp]
+@[simp, grind =]
 theorem isEmpty_empty : (∅ : HashSet α).isEmpty :=
   HashMap.isEmpty_empty
 
@@ -43,7 +45,7 @@ set_option linter.missingDocs false in
 @[deprecated isEmpty_empty (since := "2025-03-12")]
 abbrev isEmpty_emptyc := @isEmpty_empty
 
-@[simp]
+@[simp, grind =]
 theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] {a : α} : (m.insert a).isEmpty = false :=
   HashMap.isEmpty_insertIfNew
 
@@ -61,14 +63,14 @@ theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a ==
 theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : a ∈ m ↔ b ∈ m :=
   HashMap.mem_congr hab
 
-@[simp]
+@[simp, grind =]
 theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashSet α).contains a = false :=
   HashMap.contains_emptyWithCapacity
 
-@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : HashSet α) :=
+@[simp, grind] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : HashSet α) :=
   HashMap.not_mem_emptyWithCapacity
 
-@[simp] theorem contains_empty {a : α} : (∅ : HashSet α).contains a = false :=
+@[simp, grind =] theorem contains_empty {a : α} : (∅ : HashSet α).contains a = false :=
   HashMap.contains_empty
 
 set_option linter.missingDocs false in
@@ -110,12 +112,12 @@ theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] :
 
 @[simp] theorem singleton_eq_insert {a : α} : Singleton.singleton a = (∅ : HashSet α).insert a := rfl
 
-@[simp]
+@[simp, grind =]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.insert k).contains a = (k == a || m.contains a) :=
   HashMap.contains_insertIfNew
 
-@[simp]
+@[simp, grind =]
 theorem mem_insert [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.insert k ↔ k == a ∨ a ∈ m :=
   HashMap.mem_insertIfNew
 
@@ -144,11 +146,11 @@ theorem contains_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : (m.ins
 
 theorem mem_insert_self [EquivBEq α] [LawfulHashable α] {k : α} : k ∈ m.insert k := by simp
 
-@[simp]
+@[simp, grind =]
 theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : HashSet α).size = 0 :=
   HashMap.size_emptyWithCapacity
 
-@[simp]
+@[simp, grind =]
 theorem size_empty : (∅ : HashSet α).size = 0 :=
   HashMap.size_empty
 
@@ -159,7 +161,7 @@ abbrev size_emptyc := @size_empty
 theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
   HashMap.isEmpty_eq_size_eq_zero
 
-theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} :
+@[grind =] theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} :
     (m.insert k).size = if k ∈ m then m.size else m.size + 1 :=
   HashMap.size_insertIfNew
 
@@ -170,11 +172,11 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} :
     (m.insert k).size ≤ m.size + 1 :=
   HashMap.size_insertIfNew_le
 
-@[simp]
+@[simp, grind =]
 theorem erase_emptyWithCapacity {a : α} {c : Nat} : (emptyWithCapacity c : HashSet α).erase a = emptyWithCapacity c :=
   ext HashMap.erase_emptyWithCapacity
 
-@[simp]
+@[simp, grind =]
 theorem erase_empty {a : α} : (∅ : HashSet α).erase a = ∅ :=
   ext HashMap.erase_empty
 
@@ -182,17 +184,17 @@ set_option linter.missingDocs false in
 @[deprecated erase_empty (since := "2025-03-12")]
 abbrev erase_emptyc := @erase_empty
 
-@[simp]
+@[simp, grind =]
 theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} :
     (m.erase k).isEmpty = (m.isEmpty || (m.size == 1 && m.contains k)) :=
   HashMap.isEmpty_erase
 
-@[simp]
+@[simp, grind =]
 theorem contains_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.erase k).contains a = (!(k == a) && m.contains a) :=
   HashMap.contains_erase
 
-@[simp]
+@[simp, grind =]
 theorem mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m :=
   HashMap.mem_erase
@@ -204,7 +206,7 @@ theorem contains_of_contains_erase [EquivBEq α] [LawfulHashable α] {k a : α}
 theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] {k a : α} : a ∈ m.erase k → a ∈ m :=
   HashMap.mem_of_mem_erase
 
-theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
+@[grind =] theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
     (m.erase k).size = if k ∈ m then m.size - 1 else m.size :=
   HashMap.size_erase
 
@@ -215,11 +217,11 @@ theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
     m.size ≤ (m.erase k).size + 1 :=
   HashMap.size_le_size_erase
 
-@[simp]
+@[simp, grind =]
 theorem get?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : HashSet α).get? a = none :=
   HashMap.getKey?_emptyWithCapacity
 
-@[simp]
+@[simp, grind =]
 theorem get?_empty {a : α} : (∅ : HashSet α).get? a = none :=
   HashMap.getKey?_empty
 
@@ -231,7 +233,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
     m.isEmpty = true → m.get? a = none :=
   HashMap.getKey?_of_isEmpty
 
-theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
+@[grind =] theorem get?_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.insert k).get? a = if k == a ∧ ¬k ∈ m then some k else m.get? a :=
   HashMap.getKey?_insertIfNew
 
@@ -260,7 +262,7 @@ theorem get?_eq_none_of_contains_eq_false [EquivBEq α] [LawfulHashable α] {a :
 theorem get?_eq_none [EquivBEq α] [LawfulHashable α] {a : α} : ¬a ∈ m → m.get? a = none :=
   HashMap.getKey?_eq_none
 
-theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
+@[grind =] theorem get?_erase [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.erase k).get? a = if k == a then none else m.get? a :=
   HashMap.getKey?_erase
 
@@ -281,12 +283,12 @@ theorem get?_eq_some_of_contains [LawfulBEq α] {k : α} (h : m.contains k) : m.
 theorem get?_eq_some [LawfulBEq α] {k : α} (h : k ∈ m) : m.get? k = some k :=
   HashMap.getKey?_eq_some h
 
-theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {h₁} :
+@[grind =] theorem get_insert [EquivBEq α] [LawfulHashable α] {k a : α} {h₁} :
     (m.insert k).get a h₁ =
       if h₂ : k == a ∧ ¬k ∈ m then k else m.get a (mem_of_mem_insert' h₁ h₂) :=
   HashMap.getKey_insertIfNew (h₁ := h₁)
 
-@[simp]
+@[simp, grind =]
 theorem get_erase [EquivBEq α] [LawfulHashable α] {k a : α} {h'} :
     (m.erase k).get a h' = m.get a (mem_of_mem_erase h') :=
   HashMap.getKey_erase (h' := h')
@@ -299,7 +301,7 @@ theorem get_eq_get_get? [EquivBEq α] [LawfulHashable α] {k : α} {h} :
     m.get k h = (m.get? k).get (mem_iff_isSome_get?.mp h) :=
   HashMap.getKey_eq_get_getKey?
 
-theorem get_get? [EquivBEq α] [LawfulHashable α] {k : α} {h} :
+@[grind =] theorem get_get? [EquivBEq α] [LawfulHashable α] {k : α} {h} :
     (m.get? k).get h = m.get k (mem_iff_isSome_get?.mpr h) :=
   HashMap.get_getKey?
 
@@ -310,15 +312,15 @@ theorem get_congr [EquivBEq α] [LawfulHashable α] {k₁ k₂ : α} (h : k₁ =
     (h₁ : k₁ ∈ m) : m.get k₁ h₁ = m.get k₂ ((mem_congr h).mp h₁) :=
   HashMap.getKey_congr h h₁
 
-@[simp]
+@[simp, grind =]
 theorem get_eq [LawfulBEq α] {k : α} (h : k ∈ m) : m.get k h = k :=
   HashMap.getKey_eq h
 
-@[simp]
+@[simp, grind =]
 theorem get!_emptyWithCapacity [Inhabited α] {a : α} {c} : (emptyWithCapacity c : HashSet α).get! a = default :=
   HashMap.getKey!_emptyWithCapacity
 
-@[simp]
+@[simp, grind =]
 theorem get!_empty [Inhabited α] {a : α} : (∅ : HashSet α).get! a = default :=
   HashMap.getKey!_empty
 
@@ -330,7 +332,7 @@ theorem get!_of_isEmpty [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α
     m.isEmpty = true → m.get! a = default :=
   HashMap.getKey!_of_isEmpty
 
-theorem get!_insert [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} :
+@[grind =] theorem get!_insert [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.insert k).get! a = if k == a ∧ ¬k ∈ m then k else m.get! a :=
   HashMap.getKey!_insertIfNew
 
@@ -342,7 +344,7 @@ theorem get!_eq_default [Inhabited α] [EquivBEq α] [LawfulHashable α] {a : α
     ¬a ∈ m → m.get! a = default :=
   HashMap.getKey!_eq_default
 
-theorem get!_erase [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} :
+@[grind =] theorem get!_erase [Inhabited α] [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.erase k).get! a = if k == a then default else m.get! a :=
   HashMap.getKey!_erase
 
@@ -377,11 +379,11 @@ theorem get!_eq_of_contains [LawfulBEq α] [Inhabited α] {k : α} (h : m.contai
 theorem get!_eq_of_mem [LawfulBEq α] [Inhabited α] {k : α} (h : k ∈ m) : m.get! k = k :=
   HashMap.getKey!_eq_of_mem h
 
-@[simp]
+@[simp, grind =]
 theorem getD_emptyWithCapacity {a fallback : α} {c} : (emptyWithCapacity c : HashSet α).getD a fallback = fallback :=
   HashMap.getKeyD_emptyWithCapacity
 
-@[simp]
+@[simp, grind =]
 theorem getD_empty {a fallback : α} : (∅ : HashSet α).getD a fallback = fallback :=
   HashMap.getKeyD_empty
 
@@ -393,7 +395,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] {a fallback : α} :
     m.isEmpty = true → m.getD a fallback = fallback :=
   HashMap.getKeyD_of_isEmpty
 
-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 :=
   HashMap.getKeyD_insertIfNew
 
@@ -406,7 +408,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] {a fallback : α} :
     ¬a ∈ m → m.getD a fallback = fallback :=
   HashMap.getKeyD_eq_fallback
 
-theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
+@[grind =] theorem getD_erase [EquivBEq α] [LawfulHashable α] {k a fallback : α} :
     (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
   HashMap.getKeyD_erase
 
@@ -446,30 +448,30 @@ theorem getD_eq_of_contains [LawfulBEq α] {k fallback : α} (h : m.contains k)
 theorem getD_eq_of_mem [LawfulBEq α] {k fallback : α} (h : k ∈ m) : m.getD k fallback = k :=
   HashMap.getKeyD_eq_of_mem h
 
-@[simp]
+@[simp, grind =]
 theorem containsThenInsert_fst {k : α} : (m.containsThenInsert k).1 = m.contains k :=
   HashMap.containsThenInsertIfNew_fst
 
-@[simp]
+@[simp, grind =]
 theorem containsThenInsert_snd {k : α} : (m.containsThenInsert k).2 = m.insert k :=
   ext HashMap.containsThenInsertIfNew_snd
 
-@[simp]
+@[simp, grind =]
 theorem length_toList [EquivBEq α] [LawfulHashable α] :
     m.toList.length = m.size :=
   HashMap.length_keys
 
-@[simp]
+@[simp, grind =]
 theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] :
     m.toList.isEmpty = m.isEmpty :=
   HashMap.isEmpty_keys
 
-@[simp]
+@[simp, grind =]
 theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α} :
     m.toList.contains k = m.contains k :=
   HashMap.contains_keys
 
-@[simp]
+@[simp, grind =]
 theorem mem_toList [LawfulBEq α] [LawfulHashable α] {k : α} :
     k ∈ m.toList ↔ k ∈ m :=
   HashMap.mem_keys
@@ -491,7 +493,7 @@ theorem fold_eq_foldl_toList {f : δ → α → δ} {init : δ} :
     m.fold f init = m.toList.foldl f init :=
   HashMap.fold_eq_foldl_keys
 
-@[simp]
+@[simp, grind =]
 theorem forM_eq_forM [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
     m.forM f = ForM.forM m f := rfl
 
@@ -499,7 +501,7 @@ theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
     ForM.forM m f = ForM.forM m.toList f :=
   HashMap.forM_eq_forM_keys
 
-@[simp]
+@[simp, grind =]
 theorem forIn_eq_forIn [Monad m'] [LawfulMonad m']
     {f : α → δ → m' (ForInStep δ)} {init : δ} :
     ForIn.forIn m init f = ForIn.forIn m init f := rfl
@@ -513,20 +515,21 @@ end monadic
 
 variable {ρ : Type v} [ForIn Id ρ α]
 
-@[simp]
+@[simp, grind =]
 theorem insertMany_nil :
     insertMany m [] = m :=
   ext HashMap.insertManyIfNewUnit_nil
 
-@[simp]
+@[simp, grind =]
 theorem insertMany_list_singleton {k : α} :
     insertMany m [k] = m.insert k :=
   ext HashMap.insertManyIfNewUnit_list_singleton
 
-theorem insertMany_cons {l : List α} {k : α} :
+@[grind _=_] theorem insertMany_cons {l : List α} {k : α} :
     insertMany m (k :: l) = insertMany (m.insert k) l :=
   ext HashMap.insertManyIfNewUnit_cons
 
+@[grind _=_]
 theorem insertMany_append {l₁ l₂ : List α} :
     insertMany m (l₁ ++ l₂) = insertMany (insertMany m l₁) l₂ := by
   induction l₁ generalizing m with
@@ -541,13 +544,13 @@ theorem insertMany_ind {motive : HashSet α → Prop} (m : HashSet α) {l : ρ}
   show motive ⟨m.1.insertManyIfNewUnit l⟩ from
     HashMap.insertManyIfNewUnit_ind m.inner l init fun m => insert ⟨m⟩
 
-@[simp]
+@[simp, grind =]
 theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     (insertMany m l).contains k = (m.contains k || l.contains k) :=
   HashMap.contains_insertManyIfNewUnit_list
 
-@[simp]
+@[simp, grind =]
 theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     k ∈ insertMany m l ↔ k ∈ m ∨ l.contains k :=
@@ -652,12 +655,16 @@ theorem size_le_size_insertMany [EquivBEq α] [LawfulHashable α]
     {l : ρ} : m.size ≤ (insertMany m l).size :=
   HashMap.size_le_size_insertManyIfNewUnit
 
+grind_pattern size_le_size_insertMany => (insertMany m l).size
+
 theorem size_insertMany_list_le [EquivBEq α] [LawfulHashable α]
     {l : List α} :
     (insertMany m l).size ≤ m.size + l.length :=
   HashMap.size_insertManyIfNewUnit_list_le
 
-@[simp]
+grind_pattern size_insertMany_list_le => (insertMany m l).size
+
+@[simp, grind =]
 theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α]
     {l : List α} :
     (insertMany m l).isEmpty = (m.isEmpty && l.isEmpty) :=
@@ -671,17 +678,17 @@ end
 
 section
 
-@[simp]
+@[simp, grind =]
 theorem ofList_nil :
     ofList ([] : List α) = ∅ :=
   ext HashMap.unitOfList_nil
 
-@[simp]
+@[simp, grind =]
 theorem ofList_singleton {k : α} :
     ofList [k] = (∅ : HashSet α).insert k :=
   ext HashMap.unitOfList_singleton
 
-theorem ofList_cons {hd : α} {tl : List α} :
+@[grind _=_] theorem ofList_cons {hd : α} {tl : List α} :
     ofList (hd :: tl) =
       insertMany ((∅ : HashSet α).insert hd) tl :=
   ext HashMap.unitOfList_cons
@@ -692,13 +699,13 @@ theorem ofList_eq_insertMany_empty {l : List α} :
   | [] => by simp
   | hd :: tl => by simp [ofList_cons, insertMany_cons]
 
-@[simp]
+@[simp, grind =]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     (ofList l).contains k = l.contains k :=
   HashMap.contains_unitOfList
 
-@[simp]
+@[simp, grind =]
 theorem mem_ofList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     k ∈ ofList l ↔ l.contains k :=
@@ -760,7 +767,9 @@ theorem size_ofList_le [EquivBEq α] [LawfulHashable α]
     (ofList l).size ≤ l.length :=
   HashMap.size_unitOfList_le
 
-@[simp]
+grind_pattern size_ofList_le => (ofList l).size
+
+@[simp, grind =]
 theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
     {l : List α} :
     (ofList l).isEmpty = l.isEmpty :=
@@ -893,7 +902,7 @@ theorem toList_filter {f : α → Bool} :
     (m.filter f).toList.Perm (m.toList.filter f) :=
   HashMap.keys_filter_key
 
-theorem isEmpty_filter_iff [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem isEmpty_filter_iff [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} :
     (m.filter f).isEmpty ↔ ∀ k h, f (m.get k h) = false :=
   HashMap.isEmpty_filter_iff
@@ -903,7 +912,9 @@ theorem isEmpty_filter_eq_false_iff [EquivBEq α] [LawfulHashable α]
     (m.filter f).isEmpty = false ↔ ∃ k h, f (m.get k h) :=
   HashMap.isEmpty_filter_eq_false_iff
 
-@[simp]
+-- TODO: `contains_filter` is missing.
+
+@[simp, grind =]
 theorem mem_filter [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} {k : α} :
     k ∈ m.filter f ↔ ∃ h, f (m.get k h) :=
@@ -924,6 +935,8 @@ theorem size_filter_le_size [EquivBEq α] [LawfulHashable α]
     (m.filter f).size ≤ m.size :=
   HashMap.size_filter_le_size
 
+grind_pattern size_filter_le_size => (m.filter f).size
+
 theorem size_filter_eq_size_iff [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} :
     (m.filter f).size = m.size ↔ ∀ k h, f (m.get k h) :=
@@ -935,23 +948,25 @@ theorem filter_equiv_self_iff [EquivBEq α] [LawfulHashable α]
   ⟨fun h => HashMap.filter_equiv_self_iff.mp h.1,
     fun h => ⟨HashMap.filter_equiv_self_iff.mpr h⟩⟩
 
-@[simp]
+@[simp, grind =]
 theorem get?_filter [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} {k : α} :
     (m.filter f).get? k = (m.get? k).filter f :=
   HashMap.getKey?_filter_key
 
-@[simp]
+@[simp, grind =]
 theorem get_filter [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} {k : α} {h} :
     (m.filter f).get k h = m.get k (mem_of_mem_filter h) :=
   HashMap.getKey_filter
 
+@[grind =]
 theorem get!_filter [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {f : α → Bool} {k : α} :
     (m.filter f).get! k = ((m.get? k).filter f).get! :=
   HashMap.getKey!_filter_key
 
+@[grind =]
 theorem getD_filter [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} {k fallback : α} :
     (m.filter f).getD k fallback = ((m.get? k).filter f).getD fallback :=

src/Std/Data/HashSet/RawLemmas.lean

@@ -15,6 +15,8 @@ This module contains lemmas about `Std.Data.HashSet.Raw`. Most of the lemmas req
 is to provide an instance of `LawfulBEq α`.
 -/
 
+set_option trace.grind.ematch.pattern true
+
 set_option linter.missingDocs true
 set_option autoImplicit false
 
@@ -31,11 +33,11 @@ variable {m : Raw α}
 private theorem ext {m m' : Raw α} : m.inner = m'.inner → m = m' := by
   cases m; cases m'; rintro rfl; rfl
 
-@[simp]
+@[simp, grind =]
 theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α).size = 0 :=
   HashMap.Raw.size_emptyWithCapacity
 
-@[simp]
+@[simp, grind =]
 theorem size_empty : (∅ : Raw α).size = 0 :=
   HashMap.Raw.size_empty
 
@@ -48,11 +50,11 @@ theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) :=
 
 variable [BEq α] [Hashable α]
 
-@[simp]
+@[simp, grind =]
 theorem isEmpty_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α).isEmpty :=
   HashMap.Raw.isEmpty_emptyWithCapacity
 
-@[simp]
+@[simp, grind =]
 theorem isEmpty_empty : (∅ : Raw α).isEmpty :=
   HashMap.Raw.isEmpty_empty
 
@@ -60,7 +62,7 @@ set_option linter.missingDocs false in
 @[deprecated isEmpty_empty (since := "2025-03-12")]
 abbrev isEmpty_emptyc := @isEmpty_empty
 
-@[simp]
+@[simp, grind =]
 theorem isEmpty_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     (m.insert a).isEmpty = false :=
   HashMap.Raw.isEmpty_insertIfNew h.out
@@ -80,13 +82,13 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab :
     a ∈ m ↔ b ∈ m :=
   HashMap.Raw.mem_congr h.out hab
 
-@[simp] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α).contains a = false :=
+@[simp, grind =] theorem contains_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α).contains a = false :=
   HashMap.Raw.contains_emptyWithCapacity
 
-@[simp] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α) :=
+@[simp, grind] theorem not_mem_emptyWithCapacity {a : α} {c} : ¬a ∈ (emptyWithCapacity c : Raw α) :=
   HashMap.Raw.not_mem_emptyWithCapacity
 
-@[simp] theorem contains_empty {a : α} : (∅ : Raw α).contains a = false :=
+@[simp, grind =] theorem contains_empty {a : α} : (∅ : Raw α).contains a = false :=
   HashMap.Raw.contains_empty
 
 set_option linter.missingDocs false in
@@ -128,12 +130,12 @@ theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
 
 @[simp] theorem singleton_eq_insert {a : α} : Singleton.singleton a = (∅ : Raw α).insert a := rfl
 
-@[simp]
+@[simp, grind =]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     (m.insert k).contains a = (k == a || m.contains a) :=
   HashMap.Raw.contains_insertIfNew h.out
 
-@[simp]
+@[simp, grind =]
 theorem mem_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     a ∈ m.insert k ↔ k == a ∨ a ∈ m :=
   HashMap.Raw.mem_insertIfNew h.out
@@ -167,7 +169,7 @@ theorem contains_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k :
 theorem mem_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} : k ∈ m.insert k :=
   HashMap.Raw.mem_insertIfNew_self h.out
 
-theorem size_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+@[grind =]theorem size_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     (m.insert k).size = if k ∈ m then m.size else m.size + 1 :=
   HashMap.Raw.size_insertIfNew h.out
 
@@ -179,11 +181,11 @@ theorem size_insert_le [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     (m.insert k).size ≤ m.size + 1 :=
   HashMap.Raw.size_insertIfNew_le h.out
 
-@[simp]
+@[simp, grind =]
 theorem erase_emptyWithCapacity {k : α} {c : Nat} : (emptyWithCapacity c : Raw α).erase k = emptyWithCapacity c :=
   ext HashMap.Raw.erase_emptyWithCapacity
 
-@[simp]
+@[simp, grind =]
 theorem erase_empty {k : α} : (∅ : Raw α).erase k = ∅ :=
   ext HashMap.Raw.erase_empty
 
@@ -191,17 +193,17 @@ set_option linter.missingDocs false in
 @[deprecated erase_empty (since := "2025-03-12")]
 abbrev erase_emptyc := @erase_empty
 
-@[simp]
+@[simp, grind =]
 theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     (m.erase k).isEmpty = (m.isEmpty || (m.size == 1 && m.contains k)) :=
   HashMap.Raw.isEmpty_erase h.out
 
-@[simp]
+@[simp, grind =]
 theorem contains_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     (m.erase k).contains a = (!(k == a) && m.contains a) :=
   HashMap.Raw.contains_erase h.out
 
-@[simp]
+@[simp, grind =]
 theorem mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m :=
   HashMap.Raw.mem_erase h.out
@@ -214,6 +216,7 @@ theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α}
     a ∈ m.erase k → a ∈ m :=
   HashMap.Raw.mem_of_mem_erase h.out
 
+@[grind =]
 theorem size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     (m.erase k).size = if k ∈ m then m.size - 1 else m.size :=
   HashMap.Raw.size_erase h.out
@@ -226,11 +229,11 @@ theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
     m.size ≤ (m.erase k).size + 1 :=
   HashMap.Raw.size_le_size_erase h.out
 
-@[simp]
+@[simp, grind =]
 theorem get?_emptyWithCapacity {a : α} {c} : (emptyWithCapacity c : Raw α).get? a = none :=
   HashMap.Raw.getKey?_emptyWithCapacity
 
-@[simp]
+@[simp, grind =]
 theorem get?_empty {a : α} : (∅ : Raw α).get? a = none :=
   HashMap.Raw.getKey?_empty
 
@@ -242,7 +245,7 @@ theorem get?_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     m.isEmpty = true → m.get? a = none :=
   HashMap.Raw.getKey?_of_isEmpty h.out
 
-theorem get?_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
+@[grind =] theorem get?_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     (m.insert k).get? a = if k == a ∧ ¬k ∈ m then some k else m.get? a :=
   HashMap.Raw.getKey?_insertIfNew h.out
 
@@ -272,7 +275,7 @@ theorem get?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     ¬a ∈ m → m.get? a = none :=
   HashMap.Raw.getKey?_eq_none h.out
 
-theorem get?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
+@[grind =] theorem get?_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     (m.erase k).get? a = if k == a then none else m.get? a :=
   HashMap.Raw.getKey?_erase h.out
 
@@ -292,12 +295,12 @@ theorem get?_eq_some [LawfulBEq α] (h : m.WF) {k : α} (h' : k ∈ m) :
     m.get? k = some k :=
   HashMap.Raw.getKey?_eq_some h.out h'
 
-theorem get_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h₁} :
+@[grind =] theorem get_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h₁} :
     (m.insert k).get a h₁ =
       if h₂ : k == a ∧ ¬k ∈ m then k else m.get a (mem_of_mem_insert' h h₁ h₂) :=
   HashMap.Raw.getKey_insertIfNew (h₁ := h₁) h.out
 
-@[simp]
+@[simp, grind =]
 theorem get_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} {h'} :
     (m.erase k).get a h' = m.get a (mem_of_mem_erase h h') :=
   HashMap.Raw.getKey_erase (h' := h') h.out
@@ -310,7 +313,7 @@ theorem get_eq_get_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {h
     m.get k h' = (m.get? k).get ((mem_iff_isSome_get? h).mp h') :=
   HashMap.Raw.getKey_eq_get_getKey? h.out
 
-theorem get_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {h'} :
+@[grind =] theorem get_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {h'} :
     (m.get? k).get h' = m.get k ((mem_iff_isSome_get? h).mpr h') :=
   HashMap.Raw.get_getKey? h.out
 
@@ -328,16 +331,16 @@ theorem get_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {k₁ k₂ : α}
     m.get k₁ h₁ = m.get k₂ (((mem_congr h h').mp h₁)) :=
   HashMap.Raw.getKey_congr h.out h' h₁
 
-@[simp]
+@[simp, grind =]
 theorem get_eq [LawfulBEq α] (h : m.WF) {k : α} (h' : m.contains k) :
     m.get k h' = k :=
   HashMap.Raw.getKey_eq h.out h'
 
-@[simp]
+@[simp, grind =]
 theorem get!_emptyWithCapacity [Inhabited α] {a : α} {c} : (emptyWithCapacity c : Raw α).get! a = default :=
   HashMap.Raw.getKey!_emptyWithCapacity
 
-@[simp]
+@[simp, grind =]
 theorem get!_empty [Inhabited α] {a : α} : (∅ : Raw α).get! a = default :=
   HashMap.Raw.getKey!_empty
 
@@ -349,7 +352,7 @@ theorem get!_of_isEmpty [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.
     m.isEmpty = true → m.get! a = default :=
   HashMap.Raw.getKey!_of_isEmpty h.out
 
-theorem get!_insert [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
+@[grind =] theorem get!_insert [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     (m.insert k).get! a = if k == a ∧ ¬k ∈ m then k else m.get! a :=
   HashMap.Raw.getKey!_insertIfNew h.out
 
@@ -362,7 +365,7 @@ theorem get!_eq_default [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.
     ¬a ∈ m → m.get! a = default :=
   HashMap.Raw.getKey!_eq_default h.out
 
-theorem get!_erase [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
+@[grind =] theorem get!_erase [Inhabited α] [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
     (m.erase k).get! a = if k == a then default else m.get! a :=
   HashMap.Raw.getKey!_erase h.out
 
@@ -398,11 +401,11 @@ theorem get!_eq_of_contains [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h
 theorem get!_eq_of_mem [LawfulBEq α] [Inhabited α] (h : m.WF) {k : α} (h' : k ∈ m) : m.get! k = k :=
   HashMap.Raw.getKey!_eq_of_mem h.out h'
 
-@[simp]
+@[simp, grind =]
 theorem getD_emptyWithCapacity {a fallback : α} {c} : (emptyWithCapacity c : Raw α).getD a fallback = fallback :=
   HashMap.Raw.getKeyD_emptyWithCapacity
 
-@[simp]
+@[simp, grind =]
 theorem getD_empty {a fallback : α} : (∅ : Raw α).getD a fallback = fallback :=
   HashMap.Raw.getKeyD_empty
 
@@ -414,7 +417,7 @@ theorem getD_of_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback
     m.isEmpty = true → m.getD a fallback = fallback :=
   HashMap.Raw.getKeyD_of_isEmpty h.out
 
-theorem getD_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :
+@[grind =] theorem getD_insert [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :
     (m.insert k).getD a fallback = if k == a ∧ ¬k ∈ m then k else m.getD a fallback :=
   HashMap.Raw.getKeyD_insertIfNew h.out
 
@@ -427,7 +430,7 @@ theorem getD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallbac
     ¬a ∈ m → m.getD a fallback = fallback :=
   HashMap.Raw.getKeyD_eq_fallback h.out
 
-theorem getD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :
+@[grind =] theorem getD_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a fallback : α} :
     (m.erase k).getD a fallback = if k == a then fallback else m.getD a fallback :=
   HashMap.Raw.getKeyD_erase h.out
 
@@ -469,30 +472,30 @@ theorem getD_eq_of_mem [LawfulBEq α] (h : m.WF) {k fallback : α} (h' : k ∈ m
     m.getD k fallback = k :=
   HashMap.Raw.getKeyD_eq_of_mem h.out h'
 
-@[simp]
+@[simp, grind =]
 theorem containsThenInsert_fst (h : m.WF) {k : α} : (m.containsThenInsert k).1 = m.contains k :=
   HashMap.Raw.containsThenInsertIfNew_fst h.out
 
-@[simp]
+@[simp, grind =]
 theorem containsThenInsert_snd (h : m.WF) {k : α} : (m.containsThenInsert k).2 = m.insert k :=
   ext (HashMap.Raw.containsThenInsertIfNew_snd h.out)
 
-@[simp]
+@[simp, grind =]
 theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.length = m.size :=
   HashMap.Raw.length_keys h.1
 
-@[simp]
+@[simp, grind =]
 theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.isEmpty = m.isEmpty :=
   HashMap.Raw.isEmpty_keys h.1
 
-@[simp]
+@[simp, grind =]
 theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α} (h : m.WF) :
     m.toList.contains k = m.contains k :=
   HashMap.Raw.contains_keys h.1
 
-@[simp]
+@[simp, grind =]
 theorem mem_toList [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     k ∈ m.toList ↔ k ∈ m :=
   HashMap.Raw.mem_keys h.1
@@ -515,7 +518,7 @@ theorem fold_eq_foldl_toList (h : m.WF) {f : δ → α → δ} {init : δ} :
   HashMap.Raw.fold_eq_foldl_keys h.out
 
 omit [BEq α] [Hashable α] in
-@[simp]
+@[simp, grind =]
 theorem forM_eq_forM [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
     m.forM f = ForM.forM m f := rfl
 
@@ -524,7 +527,7 @@ theorem forM_eq_forM_toList [Monad m'] [LawfulMonad m'] (h : m.WF) {f : α → m
   HashMap.Raw.forM_eq_forM_keys h.out
 
 omit [BEq α] [Hashable α] in
-@[simp]
+@[simp, grind =]
 theorem forIn_eq_forIn [Monad m'] [LawfulMonad m']
     {f : α → δ → m' (ForInStep δ)} {init : δ} :
     m.forIn f init = ForIn.forIn m init f := rfl
@@ -538,20 +541,22 @@ end monadic
 
 variable {ρ : Type v} [ForIn Id ρ α]
 
-@[simp]
+@[simp, grind =]
 theorem insertMany_nil (h : m.WF) :
     insertMany m [] = m :=
   ext (HashMap.Raw.insertManyIfNewUnit_nil h.1)
 
-@[simp]
+@[simp, grind =]
 theorem insertMany_list_singleton (h : m.WF) {k : α} :
     insertMany m [k] = m.insert k :=
   ext (HashMap.Raw.insertManyIfNewUnit_list_singleton h.1)
 
+@[grind _=_]
 theorem insertMany_cons (h : m.WF) {l : List α} {k : α} :
     insertMany m (k :: l) = insertMany (m.insert k) l :=
   ext (HashMap.Raw.insertManyIfNewUnit_cons h.1)
 
+@[grind _=_]
 theorem insertMany_append (h : m.WF) {l₁ l₂ : List α} :
     insertMany m (l₁ ++ l₂) = insertMany (insertMany m l₁) l₂ := by
   induction l₁ generalizing m with
@@ -566,13 +571,13 @@ theorem insertMany_ind {motive : Raw α → Prop} (m : Raw α) (l : ρ)
   show motive ⟨m.1.insertManyIfNewUnit l⟩ from
     HashMap.Raw.insertManyIfNewUnit_ind m.inner l init fun m => insert ⟨m⟩
 
-@[simp]
+@[simp, grind =]
 theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
     {l : List α} {k : α} :
     (insertMany m l).contains k = (m.contains k || l.contains k) :=
   HashMap.Raw.contains_insertManyIfNewUnit_list h.1
 
-@[simp]
+@[simp, grind =]
 theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
     {l : List α} {k : α} :
     k ∈ insertMany m l ↔ k ∈ m ∨ l.contains k :=
@@ -677,12 +682,16 @@ theorem size_le_size_insertMany [EquivBEq α] [LawfulHashable α] (h : m.WF)
     {l : ρ} : m.size ≤ (insertMany m l).size :=
   HashMap.Raw.size_le_size_insertManyIfNewUnit h.out
 
+grind_pattern size_le_size_insertMany => (insertMany m l).size
+
 theorem size_insertMany_list_le [EquivBEq α] [LawfulHashable α] (h : m.WF)
     {l : List α} :
     (insertMany m l).size ≤ m.size + l.length :=
   HashMap.Raw.size_insertManyIfNewUnit_list_le h.1
 
-@[simp]
+grind_pattern size_insertMany_list_le => (insertMany m l).size
+
+@[simp, grind =]
 theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
     {l : List α} :
     (insertMany m l).isEmpty = (m.isEmpty && l.isEmpty) :=
@@ -692,27 +701,28 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] (h : m.W
     {l : ρ} : (insertMany m l).isEmpty → m.isEmpty :=
   HashMap.Raw.isEmpty_of_isEmpty_insertManyIfNewUnit h.out
 
-@[simp]
+@[simp, grind =]
 theorem ofList_nil :
     ofList ([] : List α) = ∅ :=
   ext HashMap.Raw.unitOfList_nil
 
-@[simp]
+@[simp, grind =]
 theorem ofList_singleton {k : α} :
     ofList [k] = (∅ : Raw α).insert k :=
   ext HashMap.Raw.unitOfList_singleton
 
+@[grind _=_]
 theorem ofList_cons {hd : α} {tl : List α} :
     ofList (hd :: tl) = insertMany ((∅ : Raw α).insert hd) tl :=
   ext HashMap.Raw.unitOfList_cons
 
-@[simp]
+@[simp, grind =]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     (ofList l).contains k = l.contains k :=
   HashMap.Raw.contains_unitOfList
 
-@[simp]
+@[simp, grind =]
 theorem mem_ofList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
     k ∈ ofList l ↔ l.contains k :=
@@ -774,7 +784,9 @@ theorem size_ofList_le [EquivBEq α] [LawfulHashable α]
     (ofList l).size ≤ l.length :=
   HashMap.Raw.size_unitOfList_le
 
-@[simp]
+grind_pattern size_ofList_le => (ofList l).size
+
+@[simp, grind =]
 theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
     {l : List α} :
     (ofList l).isEmpty = l.isEmpty :=
@@ -896,7 +908,7 @@ theorem toList_filter {f : α → Bool} (h : m.WF) :
     (m.filter f).toList.Perm (m.toList.filter f) :=
   HashMap.Raw.keys_filter_key h.1
 
-theorem isEmpty_filter_iff [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem isEmpty_filter_iff [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} (h : m.WF) :
     (m.filter f).isEmpty ↔
       ∀ (k : α) (h : k ∈ m), f (m.get k h) = false :=
@@ -908,7 +920,9 @@ theorem isEmpty_filter_eq_false_iff [EquivBEq α] [LawfulHashable α]
       ∃ (k : α) (h : k ∈ m), f (m.get k h) :=
   HashMap.Raw.isEmpty_filter_eq_false_iff h.out
 
-@[simp]
+-- TODO: `contains_filter` is missing.
+
+@[simp, grind =]
 theorem mem_filter [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} {k : α} (h : m.WF) :
     (k ∈ m.filter f) ↔ ∃ (h' : k ∈ m), f (m.get k h') :=
@@ -924,6 +938,8 @@ theorem size_filter_le_size [EquivBEq α] [LawfulHashable α]
     (m.filter f).size ≤ m.size :=
   HashMap.Raw.size_filter_le_size h.out
 
+grind_pattern size_filter_le_size => (m.filter f).size
+
 theorem size_filter_eq_size_iff [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} (h : m.WF) :
     (m.filter f).size = m.size ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) :=
@@ -935,24 +951,24 @@ theorem filter_equiv_self_iff [EquivBEq α] [LawfulHashable α]
   ⟨fun h' => (HashMap.Raw.filter_equiv_self_iff h.out).mp h'.1,
     fun h' => ⟨(HashMap.Raw.filter_equiv_self_iff h.out).mpr h'⟩⟩
 
-@[simp]
+@[simp, grind =]
 theorem get?_filter [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} {k : α} (h : m.WF) :
     (m.filter f).get? k = (m.get? k).filter f :=
   HashMap.Raw.getKey?_filter_key h.out
 
-@[simp]
+@[simp, grind =]
 theorem get_filter [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} {k : α} {h'} (h : m.WF) :
     (m.filter f).get k h' = (m.get k (mem_of_mem_filter h h')) :=
   HashMap.Raw.getKey_filter h.out
 
-theorem get!_filter [EquivBEq α] [LawfulHashable α] [Inhabited α]
+@[grind =] theorem get!_filter [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {f : α → Bool} {k : α} (h : m.WF) :
     (m.filter f).get! k = ((m.get? k).filter f).get! :=
   HashMap.Raw.getKey!_filter_key h.out
 
-theorem getD_filter [EquivBEq α] [LawfulHashable α]
+@[grind =] theorem getD_filter [EquivBEq α] [LawfulHashable α]
     {f : α → Bool} {k fallback : α} (h : m.WF) :
     (m.filter f).getD k fallback = ((m.get? k).filter f).getD fallback :=
   HashMap.Raw.getKeyD_filter_key h.out

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

@@ -920,6 +920,7 @@ theorem insertMany_cons {l : List (α × β)} {k : α} {v : β} :
     t.insertMany (⟨k, v⟩ :: l) = (t.insert k v).insertMany l :=
   ext <| DTreeMap.Raw.Const.insertMany_cons
 
+@[grind _=_]
 theorem insertMany_append {l₁ l₂ : List (α × β)} :
     insertMany t (l₁ ++ l₂) = insertMany (insertMany t l₁) l₂ := by
   induction l₁ generalizing t with

src/Std/Data/TreeSet/Lemmas.lean

@@ -490,6 +490,7 @@ theorem insertMany_cons {l : List α} {k : α} :
     t.insertMany (k :: l) = (t.insert k).insertMany l :=
   ext TreeMap.insertManyIfNewUnit_cons
 
+@[grind _=_]
 theorem insertMany_append {l₁ l₂ : List α} :
     insertMany t (l₁ ++ l₂) = insertMany (insertMany t l₁) l₂ := by
   induction l₁ generalizing t with

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

@@ -488,6 +488,7 @@ theorem insertMany_cons {l : List α} {k : α} :
     t.insertMany (k :: l) = (t.insert k).insertMany l :=
   ext TreeMap.Raw.insertManyIfNewUnit_cons
 
+@[grind _=_]
 theorem insertMany_append {l₁ l₂ : List α} :
     insertMany t (l₁ ++ l₂) = insertMany (insertMany t l₁) l₂ := by
   induction l₁ generalizing t with

tests/lean/grind/experiments/map.lean

@@ -0,0 +1,26 @@
+import Std.Data.HashMap
+import Std.Data.DHashMap
+import Std.Data.ExtHashMap
+set_option grind.warning false
+
+open Std
+
+-- Do we want this?
+example (m : HashMap Nat Nat) (h : m.isEmpty) : m[3]? = none := by grind [HashMap.getElem?_of_isEmpty]
+
+-- Don't just use `@[grind]`, instead add two patterns!
+-- Do this for List etc?
+-- attribute [grind] HashMap.getElem?_eq_some_getElem -- Do we do this for list?
+grind_pattern HashMap.getElem?_eq_some_getElem => a ∈ m, m[a]?
+
+example (m : HashMap Nat Nat) : ((m.alter 5 id).erase 7).size ≥ m.size - 1 := by grind
+
+example (m : ExtHashMap Nat Nat) :
+    (m.insert 1 2).filter (fun k v => k > 1000) = (m.insert 1 3).filter fun k v => k > 1000 := by
+  ext1 k
+  grind
+
+example (m : ExtHashMap Nat Nat) :
+    (((m.insert 1 2).insert 3 4).insert 5 6).filter (fun k v => k > 6) = m.filter fun k v => k > 6 := by
+  ext1 k
+  grind

tests/lean/run/grind_map.lean

@@ -0,0 +1,34 @@
+import Std.Data.HashMap
+import Std.Data.DHashMap
+import Std.Data.ExtHashMap
+import Std.Data.HashSet
+set_option grind.warning false
+
+open Std
+
+section
+
+variable [BEq α] [LawfulBEq α] [Hashable α] [LawfulHashable α ]
+
+example : (∅ : DHashMap α β).isEmpty := by grind
+example (m : DHashMap α β) (h : m = ∅) : m.isEmpty := by grind
+
+example : (((∅ : HashMap Nat Nat).insert 3 6).insert 4 7).contains 3 := by grind
+
+example : (((∅ : HashMap Nat Nat).insert 3 6).insert 4 7).contains 9 == false := by grind
+
+example (m : HashMap Nat Nat) (h : m.contains 3) : (m.erase 2).contains 3 := by grind
+example (m : HashMap Nat Nat) (h : (m.erase 2).contains 3) : m.contains 3 := by grind
+example (m : HashMap Nat Nat) : (m.erase 3).contains 3 = false := by grind
+example (m : HashMap Nat Nat) (h : m.contains 3 = false) : (m.erase 2).contains 3 = false := by grind
+
+-- Insert twice
+example (m : HashMap Nat Nat) : m.size ≤ ((m.insert 1 2).insert 3 4).size := by grind
+example (m : HashMap Nat Nat) : ((m.insert 1 2).insert 3 4).size ≤ m.size + 2 := by grind
+-- Insert the same key twice
+example (m : HashMap Nat Nat) : m.size ≤ ((m.insert 1 2).insert 1 4).size := by grind
+example (m : HashMap Nat Nat) : ((m.insert 1 2).insert 1 4).size ≤ m.size + 1 := by grind
+
+example : (((∅ : HashMap Nat Nat).insert 3 6).erase 4)[3]? = some 6 := by grind
+
+end

tests/lean/run/grind_map_uniform.lean

@@ -0,0 +1,12 @@
+import Lean.Meta.Tactic.Grind
+import Std.Data.DHashMap
+import Std.Data.HashMap
+import Std.Data.HashSet
+import Std.Data.TreeMap
+import Std.Data.TreeSet
+
+#eval Lean.Meta.Grind.isEMatchTheorem `Std.DHashMap.isEmpty_emptyWithCapacity
+#eval Lean.Meta.Grind.isEMatchTheorem `Std.HashMap.isEmpty_emptyWithCapacity
+#eval Lean.Meta.Grind.isEMatchTheorem `Std.HashSet.isEmpty_emptyWithCapacity
+#eval Lean.Meta.Grind.isEMatchTheorem `Std.TreeMap.isEmpty_emptyWithCapacity
+#eval Lean.Meta.Grind.isEMatchTheorem `Std.TreeSet.isEmpty_emptyWithCapacity