diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 3821c5a41d..4556397b13 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -255,7 +255,7 @@ theorem get?_insert_self [LawfulBEq α] {k : α} {v : β k} : (m.insert k v).get
 theorem contains_eq_isSome_get? [LawfulBEq α] {a : α} : m.contains a = (m.get? a).isSome :=
   Raw₀.contains_eq_isSome_get? ⟨m.1, _⟩ m.2
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [LawfulBEq α] {a : α} : (m.get? a).isSome = m.contains a :=
   contains_eq_isSome_get?.symm
 
@@ -314,7 +314,7 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = (get? m a).isSome :=
   Raw₀.Const.contains_eq_isSome_get? ⟨m.1, _⟩ m.2
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
     (get? m a).isSome = m.contains a :=
   contains_eq_isSome_get?.symm
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 7b4e43ff2c..9b44a10807 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -302,7 +302,7 @@ theorem contains_eq_isSome_get? [LawfulBEq α] (h : m.WF) {a : α} :
     m.contains a = (m.get? a).isSome := by
   simp_to_raw using Raw₀.contains_eq_isSome_get?
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [LawfulBEq α] (h : m.WF) {a : α} :
     (m.get? a).isSome = m.contains a :=
   (contains_eq_isSome_get? h).symm
@@ -364,7 +364,7 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a
     m.contains a = (get? m a).isSome := by
   simp_to_raw using Raw₀.Const.contains_eq_isSome_get?
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     (get? m a).isSome = m.contains a :=
   (contains_eq_isSome_get? h).symm
diff --git a/src/Std/Data/DTreeMap/Basic.lean b/src/Std/Data/DTreeMap/Basic.lean
index cd05191822..01d5f04c3e 100644
--- a/src/Std/Data/DTreeMap/Basic.lean
+++ b/src/Std/Data/DTreeMap/Basic.lean
@@ -94,7 +94,7 @@ structure Equiv (m₁ m₂ : DTreeMap α β cmp) where
 
 @[inherit_doc] scoped infix:50 " ~m " => Equiv
 
-@[simp]
+@[simp, grind =]
 theorem empty_eq_emptyc : (empty : DTreeMap α β cmp) = ∅ :=
   rfl
 
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index b2715e8892..8d5c3acc22 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -236,7 +236,7 @@ theorem contains_eq_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
     t.contains a = (t.get? a).isSome :=
   Impl.contains_eq_isSome_get? t.wf
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
     (t.get? a).isSome = t.contains a :=
   contains_eq_isSome_get?.symm
diff --git a/src/Std/Data/DTreeMap/Raw/Basic.lean b/src/Std/Data/DTreeMap/Raw/Basic.lean
index 2ad34e304e..89f2afd5eb 100644
--- a/src/Std/Data/DTreeMap/Raw/Basic.lean
+++ b/src/Std/Data/DTreeMap/Raw/Basic.lean
@@ -99,7 +99,7 @@ structure Equiv (m₁ m₂ : Raw α β cmp) where
 
 @[inherit_doc] scoped infix:50 " ~m " => Equiv
 
-@[simp]
+@[simp, grind =]
 theorem empty_eq_emptyc : (empty : Raw α β cmp) = ∅ :=
   rfl
 
diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
index 6b77c56ec0..13b02c2566 100644
--- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
@@ -237,7 +237,7 @@ theorem contains_eq_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a :
     t.contains a = (t.get? a).isSome :=
   Impl.contains_eq_isSome_get? h
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} :
     (t.get? a).isSome = t.contains a :=
   (contains_eq_isSome_get? h).symm
@@ -295,7 +295,7 @@ theorem contains_eq_isSome_get? [TransCmp cmp] (h : t.WF) {a : α} :
     t.contains a = (get? t a).isSome :=
   Impl.Const.contains_eq_isSome_get? h
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [TransCmp cmp] (h : t.WF) {a : α} :
     (get? t a).isSome = t.contains a :=
   (contains_eq_isSome_get? h).symm
diff --git a/src/Std/Data/ExtDHashMap/Lemmas.lean b/src/Std/Data/ExtDHashMap/Lemmas.lean
index 751887a027..7958303667 100644
--- a/src/Std/Data/ExtDHashMap/Lemmas.lean
+++ b/src/Std/Data/ExtDHashMap/Lemmas.lean
@@ -195,7 +195,7 @@ theorem get?_insert_self [LawfulBEq α] {k : α} {v : β k} : (m.insert k v).get
 theorem contains_eq_isSome_get? [LawfulBEq α] {a : α} : m.contains a = (m.get? a).isSome :=
   m.inductionOn fun _ => DHashMap.contains_eq_isSome_get?
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [LawfulBEq α] {a : α} : (m.get? a).isSome = m.contains a :=
   contains_eq_isSome_get?.symm
 
@@ -242,7 +242,7 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = (get? m a).isSome :=
   m.inductionOn fun _ => DHashMap.Const.contains_eq_isSome_get?
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
     (get? m a).isSome = m.contains a :=
   contains_eq_isSome_get?.symm
diff --git a/src/Std/Data/ExtDTreeMap/Basic.lean b/src/Std/Data/ExtDTreeMap/Basic.lean
index fd6564cfdc..c6fc344ad1 100644
--- a/src/Std/Data/ExtDTreeMap/Basic.lean
+++ b/src/Std/Data/ExtDTreeMap/Basic.lean
@@ -124,7 +124,7 @@ instance : EmptyCollection (ExtDTreeMap α β cmp) where
 instance : Inhabited (ExtDTreeMap α β cmp) where
   default := ∅
 
-@[simp]
+@[simp, grind =]
 theorem empty_eq_emptyc : (empty : ExtDTreeMap α β cmp) = ∅ :=
   rfl
 
diff --git a/src/Std/Data/ExtDTreeMap/Lemmas.lean b/src/Std/Data/ExtDTreeMap/Lemmas.lean
index ef41412202..9e073a9bcb 100644
--- a/src/Std/Data/ExtDTreeMap/Lemmas.lean
+++ b/src/Std/Data/ExtDTreeMap/Lemmas.lean
@@ -43,11 +43,6 @@ theorem mem_iff_contains [TransCmp cmp] {k : α} : k ∈ t ↔ t.contains k :=
 theorem contains_iff_mem [TransCmp cmp] {k : α} : t.contains k ↔ k ∈ t :=
   Iff.rfl
 
--- We need to specify the pattern for the reverse direction manually,
--- as the default heuristic leaves the `ExtDTreeMap α β` argument as a wildcard.
-grind_pattern contains_iff_mem => @Membership.mem α (ExtDTreeMap α β cmp) _ t k
-
-
 theorem contains_congr [TransCmp cmp] {k k' : α} (hab : cmp k k' = .eq) :
     t.contains k = t.contains k' :=
   t.inductionOn (fun _ hab => DTreeMap.contains_congr hab) hab
@@ -221,7 +216,7 @@ theorem contains_eq_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
     t.contains a = (t.get? a).isSome :=
   t.inductionOn fun _ => DTreeMap.contains_eq_isSome_get?
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
     (t.get? a).isSome = t.contains a :=
   t.inductionOn fun _ => DTreeMap.isSome_get?_eq_contains
diff --git a/src/Std/Data/ExtHashSet/Lemmas.lean b/src/Std/Data/ExtHashSet/Lemmas.lean
index 71832a75d0..f64187aad6 100644
--- a/src/Std/Data/ExtHashSet/Lemmas.lean
+++ b/src/Std/Data/ExtHashSet/Lemmas.lean
@@ -191,7 +191,7 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = (m.get? a).isSome :=
   ExtHashMap.contains_eq_isSome_getKey?
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
     (m.get? a).isSome = m.contains a :=
   contains_eq_isSome_get?.symm
diff --git a/src/Std/Data/ExtTreeMap/Basic.lean b/src/Std/Data/ExtTreeMap/Basic.lean
index b5b7b45650..f2016dcade 100644
--- a/src/Std/Data/ExtTreeMap/Basic.lean
+++ b/src/Std/Data/ExtTreeMap/Basic.lean
@@ -79,7 +79,7 @@ instance : EmptyCollection (ExtTreeMap α β cmp) where
 
 instance : Inhabited (ExtTreeMap α β cmp) := ⟨∅⟩
 
-@[simp]
+@[simp, grind =]
 theorem empty_eq_emptyc : (empty : ExtTreeMap α β cmp) = ∅ :=
   rfl
 
diff --git a/src/Std/Data/ExtTreeSet/Basic.lean b/src/Std/Data/ExtTreeSet/Basic.lean
index 5547031428..99e098860e 100644
--- a/src/Std/Data/ExtTreeSet/Basic.lean
+++ b/src/Std/Data/ExtTreeSet/Basic.lean
@@ -84,7 +84,7 @@ instance : EmptyCollection (ExtTreeSet α cmp) where
 instance : Inhabited (ExtTreeSet α cmp) where
   default := ∅
 
-@[simp]
+@[simp, grind =]
 theorem empty_eq_emptyc : (empty : ExtTreeSet α cmp) = ∅ :=
   rfl
 
diff --git a/src/Std/Data/ExtTreeSet/Lemmas.lean b/src/Std/Data/ExtTreeSet/Lemmas.lean
index 49562f4cad..6245d0b9b4 100644
--- a/src/Std/Data/ExtTreeSet/Lemmas.lean
+++ b/src/Std/Data/ExtTreeSet/Lemmas.lean
@@ -203,7 +203,7 @@ theorem contains_eq_isSome_get? [TransCmp cmp] {a : α} :
     t.contains a = (t.get? a).isSome :=
   ExtTreeMap.contains_eq_isSome_getKey?
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [TransCmp cmp] {a : α} :
     (t.get? a).isSome = t.contains a :=
   contains_eq_isSome_get?.symm
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index e80bc2d883..7db8fd49f3 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -239,7 +239,7 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] {a : α} :
     m.contains a = (m.get? a).isSome :=
   HashMap.contains_eq_isSome_getKey?
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] {a : α} :
     (m.get? a).isSome = m.contains a :=
   contains_eq_isSome_get?.symm
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index 23b71762d6..9458ae39f5 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -251,7 +251,7 @@ theorem contains_eq_isSome_get? [EquivBEq α] [LawfulHashable α] (h : m.WF) {a
     m.contains a = (m.get? a).isSome :=
   HashMap.Raw.contains_eq_isSome_getKey? h.out
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [EquivBEq α] [LawfulHashable α] (h : m.WF) {a : α} :
     (m.get? a).isSome = m.contains a :=
   (contains_eq_isSome_get? h).symm
diff --git a/src/Std/Data/TreeMap/Basic.lean b/src/Std/Data/TreeMap/Basic.lean
index a5b62426dc..79c18a24a5 100644
--- a/src/Std/Data/TreeMap/Basic.lean
+++ b/src/Std/Data/TreeMap/Basic.lean
@@ -82,7 +82,7 @@ structure Equiv (m₁ m₂ : TreeMap α β cmp) where
 
 @[inherit_doc] scoped infix:50 " ~m " => Equiv
 
-@[simp]
+@[simp, grind =]
 theorem empty_eq_emptyc : (empty : TreeMap α β cmp) = ∅ :=
   rfl
 
diff --git a/src/Std/Data/TreeMap/Raw/Basic.lean b/src/Std/Data/TreeMap/Raw/Basic.lean
index 64779ec893..2006e50256 100644
--- a/src/Std/Data/TreeMap/Raw/Basic.lean
+++ b/src/Std/Data/TreeMap/Raw/Basic.lean
@@ -95,7 +95,7 @@ structure Equiv (m₁ m₂ : Raw α β cmp) where
 
 @[inherit_doc] scoped infix:50 " ~m " => Equiv
 
-@[simp]
+@[simp, grind =]
 theorem empty_eq_emptyc : (empty : Raw α β cmp) = ∅ :=
   rfl
 
diff --git a/src/Std/Data/TreeSet/Basic.lean b/src/Std/Data/TreeSet/Basic.lean
index 2fc05da8b6..b1a90c18cd 100644
--- a/src/Std/Data/TreeSet/Basic.lean
+++ b/src/Std/Data/TreeSet/Basic.lean
@@ -87,7 +87,7 @@ structure Equiv (m₁ m₂ : TreeSet α cmp) where
 
 @[inherit_doc] scoped infix:50 " ~m " => Equiv
 
-@[simp]
+@[simp, grind =]
 theorem empty_eq_emptyc : (empty : TreeSet α cmp) = ∅ :=
   rfl
 
diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean
index 68947c986d..fe6e20a038 100644
--- a/src/Std/Data/TreeSet/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Lemmas.lean
@@ -215,7 +215,7 @@ theorem contains_eq_isSome_get? [TransCmp cmp] {a : α} :
     t.contains a = (t.get? a).isSome :=
   TreeMap.contains_eq_isSome_getKey?
 
-@[simp]
+@[simp, grind =]
 theorem isSome_get?_eq_contains [TransCmp cmp] {a : α} :
     (t.get? a).isSome = t.contains a :=
   contains_eq_isSome_get?.symm
diff --git a/src/Std/Data/TreeSet/Raw/Basic.lean b/src/Std/Data/TreeSet/Raw/Basic.lean
index 238b6d854a..a442c96fbd 100644
--- a/src/Std/Data/TreeSet/Raw/Basic.lean
+++ b/src/Std/Data/TreeSet/Raw/Basic.lean
@@ -95,7 +95,7 @@ structure Equiv (m₁ m₂ : Raw α cmp) where
 
 @[inherit_doc] scoped infix:50 " ~m " => Equiv
 
-@[simp]
+@[simp, grind =]
 theorem empty_eq_emptyc : (empty : Raw α cmp) = ∅ :=
   rfl