diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index db18814426..20497e6274 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -51,10 +51,14 @@ theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a :=
 
 -- While setting up the API, often use this in the reverse direction,
 -- but prefer this direction for users.
-@[simp, grind _=_]
+@[simp, grind =]
 theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m :=
   Iff.rfl
 
+-- We need to specify the pattern for the reverse direction manually,
+-- as the default heuristic leaves the `DHashMap α β` argument as a wildcard.
+grind_pattern contains_iff_mem => @Membership.mem α (DHashMap α β) _ m a
+
 theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
     m.contains a = m.contains b :=
   Raw₀.contains_congr _ m.2 hab
diff --git a/src/Std/Data/ExtDHashMap/Lemmas.lean b/src/Std/Data/ExtDHashMap/Lemmas.lean
index 17715718d6..f82c5e285d 100644
--- a/src/Std/Data/ExtDHashMap/Lemmas.lean
+++ b/src/Std/Data/ExtDHashMap/Lemmas.lean
@@ -51,10 +51,15 @@ theorem not_insert_eq_empty [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
 theorem mem_iff_contains [EquivBEq α] [LawfulHashable α] {a : α} : a ∈ m ↔ m.contains a :=
   Iff.rfl
 
-@[simp, grind _=_]
+@[simp, grind =]
 theorem contains_iff_mem [EquivBEq α] [LawfulHashable α] {a : α} : m.contains a ↔ a ∈ m :=
   Iff.rfl
 
+-- We need to specify the pattern for the reverse direction manually,
+-- as the default heuristic leaves the `ExtDHashMap α β` argument as a wildcard.
+grind_pattern contains_iff_mem => @Membership.mem α (ExtDHashMap α β) _ m a
+
+
 theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : m.contains a = m.contains b :=
   m.inductionOn fun _ => DHashMap.contains_congr hab