diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean
index 21c62acb54..afcc411b96 100644
--- a/src/Std/Data/DHashMap/Basic.lean
+++ b/src/Std/Data/DHashMap/Basic.lean
@@ -30,6 +30,8 @@ universe u v w
 
 variable {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w} [Monad m]
 
+variable {_ : BEq α} {_ : Hashable α}
+
 namespace Std
 
 open DHashMap.Internal DHashMap.Internal.List
@@ -66,34 +68,34 @@ instance [BEq α] [Hashable α] : EmptyCollection (DHashMap α β) where
 instance [BEq α] [Hashable α] : Inhabited (DHashMap α β) where
   default := ∅
 
-@[inline, inherit_doc Raw.insert] def insert [BEq α] [Hashable α] (m : DHashMap α β) (a : α)
+@[inline, inherit_doc Raw.insert] def insert (m : DHashMap α β) (a : α)
     (b : β a) : DHashMap α β :=
   ⟨Raw₀.insert ⟨m.1, m.2.size_buckets_pos⟩ a b, .insert₀ m.2⟩
 
-@[inline, inherit_doc Raw.insertIfNew] def insertIfNew [BEq α] [Hashable α] (m : DHashMap α β)
+@[inline, inherit_doc Raw.insertIfNew] def insertIfNew (m : DHashMap α β)
     (a : α) (b : β a) : DHashMap α β :=
   ⟨Raw₀.insertIfNew ⟨m.1, m.2.size_buckets_pos⟩ a b, .insertIfNew₀ m.2⟩
 
-@[inline, inherit_doc Raw.containsThenInsert] def containsThenInsert [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.containsThenInsert] def containsThenInsert
     (m : DHashMap α β) (a : α) (b : β a) : Bool × DHashMap α β :=
   let m' := Raw₀.containsThenInsert ⟨m.1, m.2.size_buckets_pos⟩ a b
   ⟨m'.1, ⟨m'.2.1, .containsThenInsert₀ m.2⟩⟩
 
-@[inline, inherit_doc Raw.containsThenInsertIfNew] def containsThenInsertIfNew [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.containsThenInsertIfNew] def containsThenInsertIfNew
     (m : DHashMap α β) (a : α) (b : β a) : Bool × DHashMap α β :=
   let m' := Raw₀.containsThenInsertIfNew ⟨m.1, m.2.size_buckets_pos⟩ a b
   ⟨m'.1, ⟨m'.2.1, .containsThenInsertIfNew₀ m.2⟩⟩
 
-@[inline, inherit_doc Raw.getThenInsertIfNew?] def getThenInsertIfNew? [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.getThenInsertIfNew?] def getThenInsertIfNew?
     [LawfulBEq α] (m : DHashMap α β) (a : α) (b : β a) : Option (β a) × DHashMap α β :=
   let m' := Raw₀.getThenInsertIfNew? ⟨m.1, m.2.size_buckets_pos⟩ a b
   ⟨m'.1, ⟨m'.2.1, .getThenInsertIfNew?₀ m.2⟩⟩
 
-@[inline, inherit_doc Raw.get?] def get? [BEq α] [LawfulBEq α] [Hashable α] (m : DHashMap α β)
+@[inline, inherit_doc Raw.get?] def get? [LawfulBEq α] (m : DHashMap α β)
     (a : α) : Option (β a) :=
   Raw₀.get? ⟨m.1, m.2.size_buckets_pos⟩ a
 
-@[inline, inherit_doc Raw.contains] def contains [BEq α] [Hashable α] (m : DHashMap α β) (a : α) :
+@[inline, inherit_doc Raw.contains] def contains (m : DHashMap α β) (a : α) :
     Bool :=
   Raw₀.contains ⟨m.1, m.2.size_buckets_pos⟩ a
 
@@ -103,19 +105,19 @@ instance [BEq α] [Hashable α] : Membership α (DHashMap α β) where
 instance [BEq α] [Hashable α] {m : DHashMap α β} {a : α} : Decidable (a ∈ m) :=
   show Decidable (m.contains a) from inferInstance
 
-@[inline, inherit_doc Raw.get] def get [BEq α] [Hashable α] [LawfulBEq α] (m : DHashMap α β) (a : α)
+@[inline, inherit_doc Raw.get] def get [LawfulBEq α] (m : DHashMap α β) (a : α)
     (h : a ∈ m) : β a :=
   Raw₀.get ⟨m.1, m.2.size_buckets_pos⟩ a h
 
-@[inline, inherit_doc Raw.get!] def get! [BEq α] [Hashable α] [LawfulBEq α] (m : DHashMap α β)
+@[inline, inherit_doc Raw.get!] def get! [LawfulBEq α] (m : DHashMap α β)
     (a : α) [Inhabited (β a)] : β a :=
   Raw₀.get! ⟨m.1, m.2.size_buckets_pos⟩ a
 
-@[inline, inherit_doc Raw.getD] def getD [BEq α] [Hashable α] [LawfulBEq α] (m : DHashMap α β)
+@[inline, inherit_doc Raw.getD] def getD [LawfulBEq α] (m : DHashMap α β)
     (a : α) (fallback : β a) : β a :=
   Raw₀.getD ⟨m.1, m.2.size_buckets_pos⟩ a fallback
 
-@[inline, inherit_doc Raw.erase] def erase [BEq α] [Hashable α] (m : DHashMap α β) (a : α) :
+@[inline, inherit_doc Raw.erase] def erase (m : DHashMap α β) (a : α) :
     DHashMap α β :=
   ⟨Raw₀.erase ⟨m.1, m.2.size_buckets_pos⟩ a, .erase₀ m.2⟩
 
@@ -123,57 +125,57 @@ section
 
 variable {β : Type v}
 
-@[inline, inherit_doc Raw.Const.get?] def Const.get? [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.get?] def Const.get?
     (m : DHashMap α (fun _ => β)) (a : α) : Option β :=
   Raw₀.Const.get? ⟨m.1, m.2.size_buckets_pos⟩ a
 
-@[inline, inherit_doc Raw.Const.get] def Const.get [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.get] def Const.get
     (m : DHashMap α (fun _ => β)) (a : α) (h : a ∈ m) : β :=
   Raw₀.Const.get ⟨m.1, m.2.size_buckets_pos⟩ a h
 
-@[inline, inherit_doc Raw.Const.getD] def Const.getD [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.getD] def Const.getD
     (m : DHashMap α (fun _ => β)) (a : α) (fallback : β) : β :=
   Raw₀.Const.getD ⟨m.1, m.2.size_buckets_pos⟩ a fallback
 
-@[inline, inherit_doc Raw.Const.get!] def Const.get! [BEq α] [Hashable α] [Inhabited β]
+@[inline, inherit_doc Raw.Const.get!] def Const.get! [Inhabited β]
     (m : DHashMap α (fun _ => β)) (a : α) : β :=
   Raw₀.Const.get! ⟨m.1, m.2.size_buckets_pos⟩ a
 
-@[inline, inherit_doc Raw.Const.getThenInsertIfNew?] def Const.getThenInsertIfNew? [BEq α]
-    [Hashable α] (m : DHashMap α (fun _ => β)) (a : α) (b : β) :
+@[inline, inherit_doc Raw.Const.getThenInsertIfNew?] def Const.getThenInsertIfNew?
+    (m : DHashMap α (fun _ => β)) (a : α) (b : β) :
     Option β × DHashMap α (fun _ => β) :=
   let m' := Raw₀.Const.getThenInsertIfNew? ⟨m.1, m.2.size_buckets_pos⟩ a b
   ⟨m'.1, ⟨m'.2.1, .constGetThenInsertIfNew?₀ m.2⟩⟩
 
 end
 
-@[inline, inherit_doc Raw.size] def size [BEq α] [Hashable α] (m : DHashMap α β) : Nat :=
+@[inline, inherit_doc Raw.size] def size (m : DHashMap α β) : Nat :=
   m.1.size
 
-@[inline, inherit_doc Raw.isEmpty] def isEmpty [BEq α] [Hashable α] (m : DHashMap α β) : Bool :=
+@[inline, inherit_doc Raw.isEmpty] def isEmpty (m : DHashMap α β) : Bool :=
   m.1.isEmpty
 
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
 
-@[inline, inherit_doc Raw.filter] def filter [BEq α] [Hashable α] (f : (a : α) → β a → Bool)
+@[inline, inherit_doc Raw.filter] def filter (f : (a : α) → β a → Bool)
     (m : DHashMap α β) : DHashMap α β :=
   ⟨Raw₀.filter f ⟨m.1, m.2.size_buckets_pos⟩, .filter₀ m.2⟩
 
-@[inline, inherit_doc Raw.foldM] def foldM [BEq α] [Hashable α] (f : δ → (a : α) → β a → m δ)
+@[inline, inherit_doc Raw.foldM] def foldM (f : δ → (a : α) → β a → m δ)
     (init : δ) (b : DHashMap α β) : m δ :=
   b.1.foldM f init
 
-@[inline, inherit_doc Raw.fold] def fold [BEq α] [Hashable α] (f : δ → (a : α) → β a → δ)
+@[inline, inherit_doc Raw.fold] def fold (f : δ → (a : α) → β a → δ)
     (init : δ) (b : DHashMap α β) : δ :=
   b.1.fold f init
 
-@[inline, inherit_doc Raw.forM] def forM [BEq α] [Hashable α] (f : (a : α) → β a → m PUnit)
+@[inline, inherit_doc Raw.forM] def forM (f : (a : α) → β a → m PUnit)
     (b : DHashMap α β) : m PUnit :=
   b.1.forM f
 
-@[inline, inherit_doc Raw.forIn] def forIn [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.forIn] def forIn
     (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (b : DHashMap α β) : m δ :=
   b.1.forIn f init
 
@@ -183,49 +185,49 @@ instance [BEq α] [Hashable α] : ForM m (DHashMap α β) ((a : α) × β a) whe
 instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) where
   forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
-@[inline, inherit_doc Raw.toList] def toList [BEq α] [Hashable α] (m : DHashMap α β) :
+@[inline, inherit_doc Raw.toList] def toList (m : DHashMap α β) :
     List ((a : α) × β a) :=
   m.1.toList
 
-@[inline, inherit_doc Raw.toArray] def toArray [BEq α] [Hashable α] (m : DHashMap α β) :
+@[inline, inherit_doc Raw.toArray] def toArray (m : DHashMap α β) :
     Array ((a : α) × β a) :=
   m.1.toArray
 
-@[inline, inherit_doc Raw.Const.toList] def Const.toList {β : Type v} [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.toList] def Const.toList {β : Type v}
     (m : DHashMap α (fun _ => β)) : List (α × β) :=
   Raw.Const.toList m.1
 
-@[inline, inherit_doc Raw.Const.toArray] def Const.toArray {β : Type v} [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.toArray] def Const.toArray {β : Type v}
     (m : DHashMap α (fun _ => β)) : Array (α × β) :=
   Raw.Const.toArray m.1
 
-@[inline, inherit_doc Raw.keys] def keys [BEq α] [Hashable α] (m : DHashMap α β) : List α :=
+@[inline, inherit_doc Raw.keys] def keys (m : DHashMap α β) : List α :=
   m.1.keys
 
-@[inline, inherit_doc Raw.keysArray] def keysArray [BEq α] [Hashable α] (m : DHashMap α β) :
+@[inline, inherit_doc Raw.keysArray] def keysArray (m : DHashMap α β) :
     Array α :=
   m.1.keysArray
 
-@[inline, inherit_doc Raw.values] def values {β : Type v} [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.values] def values {β : Type v}
     (m : DHashMap α (fun _ => β)) : List β :=
   m.1.values
 
-@[inline, inherit_doc Raw.valuesArray] def valuesArray {β : Type v} [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.valuesArray] def valuesArray {β : Type v}
     (m : DHashMap α (fun _ => β)) : Array β :=
   m.1.valuesArray
 
-@[inline, inherit_doc Raw.insertMany] def insertMany [BEq α] [Hashable α] {ρ : Type w}
+@[inline, inherit_doc Raw.insertMany] def insertMany {ρ : Type w}
     [ForIn Id ρ ((a : α) × β a)] (m : DHashMap α β) (l : ρ) : DHashMap α β :=
   ⟨(Raw₀.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).1,
    (Raw₀.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).2 _ Raw.WF.insert₀ m.2⟩
 
-@[inline, inherit_doc Raw.Const.insertMany] def Const.insertMany {β : Type v} [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.insertMany] def Const.insertMany {β : Type v}
     {ρ : Type w} [ForIn Id ρ (α × β)] (m : DHashMap α (fun _ => β)) (l : ρ) :
     DHashMap α (fun _ => β) :=
   ⟨(Raw₀.Const.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).1,
    (Raw₀.Const.insertMany ⟨m.1, m.2.size_buckets_pos⟩ l).2 _ Raw.WF.insert₀ m.2⟩
 
-@[inline, inherit_doc Raw.Const.insertManyUnit] def Const.insertManyUnit [BEq α] [Hashable α]
+@[inline, inherit_doc Raw.Const.insertManyUnit] def Const.insertManyUnit
     {ρ : Type w} [ForIn Id ρ α] (m : DHashMap α (fun _ => Unit)) (l : ρ) :
     DHashMap α (fun _ => Unit) :=
   ⟨(Raw₀.Const.insertManyUnit ⟨m.1, m.2.size_buckets_pos⟩ l).1,
@@ -243,7 +245,7 @@ instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) wh
     DHashMap α (fun _ => Unit) :=
   Const.insertManyUnit ∅ l
 
-@[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets [BEq α] [Hashable α]
+@[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets
     (m : DHashMap α β) : Nat :=
   Raw.Internal.numBuckets m.1
 
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 5d2d9dc15f..cf7661d8a0 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -22,7 +22,7 @@ set_option autoImplicit false
 
 universe u v
 
-variable {α : Type u} {β : α → Type v} [BEq α] [Hashable α]
+variable {α : Type u} {β : α → Type v} {_ : BEq α} {_ : Hashable α}
 
 namespace Std.DHashMap
 
diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean
index a605c0ff1b..7cb3c0ab9b 100644
--- a/src/Std/Data/HashMap/Basic.lean
+++ b/src/Std/Data/HashMap/Basic.lean
@@ -27,7 +27,7 @@ nested inductive types.
 
 universe u v w
 
-variable {α : Type u} {β : Type v}
+variable {α : Type u} {β : Type v} {_ : BEq α} {_ : Hashable α}
 
 namespace Std
 
@@ -69,21 +69,21 @@ instance [BEq α] [Hashable α] : EmptyCollection (HashMap α β) where
 instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where
   default := ∅
 
-@[inline, inherit_doc DHashMap.insert] def insert [BEq α] [Hashable α] (m : HashMap α β) (a : α)
+@[inline, inherit_doc DHashMap.insert] def insert (m : HashMap α β) (a : α)
     (b : β) : HashMap α β :=
   ⟨m.inner.insert a b⟩
 
-@[inline, inherit_doc DHashMap.insertIfNew] def insertIfNew [BEq α] [Hashable α] (m : HashMap α β)
+@[inline, inherit_doc DHashMap.insertIfNew] def insertIfNew (m : HashMap α β)
     (a : α) (b : β) : HashMap α β :=
   ⟨m.inner.insertIfNew a b⟩
 
-@[inline, inherit_doc DHashMap.containsThenInsert] def containsThenInsert [BEq α] [Hashable α]
+@[inline, inherit_doc DHashMap.containsThenInsert] def containsThenInsert
     (m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
   let ⟨replaced, r⟩ := m.inner.containsThenInsert a b
   ⟨replaced, ⟨r⟩⟩
 
-@[inline, inherit_doc DHashMap.containsThenInsertIfNew] def containsThenInsertIfNew [BEq α]
-    [Hashable α] (m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
+@[inline, inherit_doc DHashMap.containsThenInsertIfNew] def containsThenInsertIfNew
+    (m : HashMap α β) (a : α) (b : β) : Bool × HashMap α β :=
   let ⟨replaced, r⟩ := m.inner.containsThenInsertIfNew a b
   ⟨replaced, ⟨r⟩⟩
 
@@ -96,7 +96,7 @@ returned map has a new value inserted.
 
 Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.
 -/
-@[inline] def getThenInsertIfNew? [BEq α] [Hashable α] (m : HashMap α β) (a : α) (b : β) :
+@[inline] def getThenInsertIfNew? (m : HashMap α β) (a : α) (b : β) :
     Option β × HashMap α β :=
   let ⟨previous, r⟩ := DHashMap.Const.getThenInsertIfNew? m.inner a b
   ⟨previous, ⟨r⟩⟩
@@ -106,10 +106,10 @@ The notation `m[a]?` is preferred over calling this function directly.
 
 Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.
 -/
-@[inline] def get? [BEq α] [Hashable α] (m : HashMap α β) (a : α) : Option β :=
+@[inline] def get? (m : HashMap α β) (a : α) : Option β :=
   DHashMap.Const.get? m.inner a
 
-@[inline, inherit_doc DHashMap.contains] def contains [BEq α] [Hashable α] (m : HashMap α β)
+@[inline, inherit_doc DHashMap.contains] def contains (m : HashMap α β)
     (a : α) : Bool :=
   m.inner.contains a
 
@@ -125,10 +125,10 @@ The notation `m[a]` or `m[a]'h` is preferred over calling this function directly
 Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof of
 `a ∈ m`.
 -/
-@[inline] def get [BEq α] [Hashable α] (m : HashMap α β) (a : α) (h : a ∈ m) : β :=
+@[inline] def get (m : HashMap α β) (a : α) (h : a ∈ m) : β :=
   DHashMap.Const.get m.inner a h
 
-@[inline, inherit_doc DHashMap.Const.getD] def getD [BEq α] [Hashable α] (m : HashMap α β) (a : α)
+@[inline, inherit_doc DHashMap.Const.getD] def getD (m : HashMap α β) (a : α)
     (fallback : β) : β :=
   DHashMap.Const.getD m.inner a fallback
 
@@ -137,7 +137,7 @@ The notation `m[a]!` is preferred over calling this function directly.
 
 Tries to retrieve the mapping for the given key, panicking if no such mapping is present.
 -/
-@[inline] def get! [BEq α] [Hashable α] [Inhabited β] (m : HashMap α β) (a : α) : β :=
+@[inline] def get! [Inhabited β] (m : HashMap α β) (a : α) : β :=
   DHashMap.Const.get! m.inner a
 
 instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a ∈ m) where
@@ -145,37 +145,37 @@ instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a 
   getElem? m a := m.get? a
   getElem! m a := m.get! a
 
-@[inline, inherit_doc DHashMap.erase] def erase [BEq α] [Hashable α] (m : HashMap α β) (a : α) :
+@[inline, inherit_doc DHashMap.erase] def erase (m : HashMap α β) (a : α) :
     HashMap α β :=
   ⟨m.inner.erase a⟩
 
-@[inline, inherit_doc DHashMap.size] def size [BEq α] [Hashable α] (m : HashMap α β) : Nat :=
+@[inline, inherit_doc DHashMap.size] def size (m : HashMap α β) : Nat :=
   m.inner.size
 
-@[inline, inherit_doc DHashMap.isEmpty] def isEmpty [BEq α] [Hashable α] (m : HashMap α β) : Bool :=
+@[inline, inherit_doc DHashMap.isEmpty] def isEmpty (m : HashMap α β) : Bool :=
   m.inner.isEmpty
 
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
 
-@[inline, inherit_doc DHashMap.filter] def filter [BEq α] [Hashable α] (f : α → β → Bool)
+@[inline, inherit_doc DHashMap.filter] def filter (f : α → β → Bool)
     (m : HashMap α β) : HashMap α β :=
   ⟨m.inner.filter f⟩
 
-@[inline, inherit_doc DHashMap.foldM] def foldM [BEq α] [Hashable α] {m : Type w → Type w}
+@[inline, inherit_doc DHashMap.foldM] def foldM {m : Type w → Type w}
     [Monad m] {γ : Type w} (f : γ → α → β → m γ) (init : γ) (b : HashMap α β) : m γ :=
   b.inner.foldM f init
 
-@[inline, inherit_doc DHashMap.fold] def fold [BEq α] [Hashable α] {γ : Type w}
+@[inline, inherit_doc DHashMap.fold] def fold {γ : Type w}
     (f : γ → α → β → γ) (init : γ) (b : HashMap α β) : γ :=
   b.inner.fold f init
 
-@[inline, inherit_doc DHashMap.forM] def forM [BEq α] [Hashable α] {m : Type w → Type w} [Monad m]
+@[inline, inherit_doc DHashMap.forM] def forM {m : Type w → Type w} [Monad m]
     (f : (a : α) → β → m PUnit) (b : HashMap α β) : m PUnit :=
   b.inner.forM f
 
-@[inline, inherit_doc DHashMap.forIn] def forIn [BEq α] [Hashable α] {m : Type w → Type w} [Monad m]
+@[inline, inherit_doc DHashMap.forIn] def forIn {m : Type w → Type w} [Monad m]
     {γ : Type w} (f : (a : α) → β → γ → m (ForInStep γ)) (init : γ) (b : HashMap α β) : m γ :=
   b.inner.forIn f init
 
@@ -185,33 +185,33 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForM m (HashMap α β)
 instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β) (α × β) where
   forIn m init f := m.forIn (fun a b acc => f (a, b) acc) init
 
-@[inline, inherit_doc DHashMap.Const.toList] def toList [BEq α] [Hashable α] (m : HashMap α β) :
+@[inline, inherit_doc DHashMap.Const.toList] def toList (m : HashMap α β) :
     List (α × β) :=
   DHashMap.Const.toList m.inner
 
-@[inline, inherit_doc DHashMap.Const.toArray] def toArray [BEq α] [Hashable α] (m : HashMap α β) :
+@[inline, inherit_doc DHashMap.Const.toArray] def toArray (m : HashMap α β) :
     Array (α × β) :=
   DHashMap.Const.toArray m.inner
 
-@[inline, inherit_doc DHashMap.keys] def keys [BEq α] [Hashable α] (m : HashMap α β) : List α :=
+@[inline, inherit_doc DHashMap.keys] def keys (m : HashMap α β) : List α :=
   m.inner.keys
 
-@[inline, inherit_doc DHashMap.keysArray] def keysArray [BEq α] [Hashable α] (m : HashMap α β) :
+@[inline, inherit_doc DHashMap.keysArray] def keysArray (m : HashMap α β) :
     Array α :=
   m.inner.keysArray
 
-@[inline, inherit_doc DHashMap.values] def values [BEq α] [Hashable α] (m : HashMap α β) : List β :=
+@[inline, inherit_doc DHashMap.values] def values (m : HashMap α β) : List β :=
   m.inner.values
 
-@[inline, inherit_doc DHashMap.valuesArray] def valuesArray [BEq α] [Hashable α] (m : HashMap α β) :
+@[inline, inherit_doc DHashMap.valuesArray] def valuesArray (m : HashMap α β) :
     Array β :=
   m.inner.valuesArray
 
-@[inline, inherit_doc DHashMap.Const.insertMany] def insertMany [BEq α] [Hashable α] {ρ : Type w}
+@[inline, inherit_doc DHashMap.Const.insertMany] def insertMany {ρ : Type w}
     [ForIn Id ρ (α × β)] (m : HashMap α β) (l : ρ) : HashMap α β :=
   ⟨DHashMap.Const.insertMany m.inner l⟩
 
-@[inline, inherit_doc DHashMap.Const.insertManyUnit] def insertManyUnit [BEq α] [Hashable α]
+@[inline, inherit_doc DHashMap.Const.insertManyUnit] def insertManyUnit
     {ρ : Type w} [ForIn Id ρ α] (m : HashMap α Unit) (l : ρ) : HashMap α Unit :=
   ⟨DHashMap.Const.insertManyUnit m.inner l⟩
 
@@ -223,7 +223,7 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
     HashMap α Unit :=
   ⟨DHashMap.Const.unitOfList l⟩
 
-@[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets [BEq α] [Hashable α]
+@[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets
     (m : HashMap α β) : Nat :=
   DHashMap.Internal.numBuckets m.inner
 
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 1bf2c00ff2..b271c79263 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -20,7 +20,7 @@ set_option autoImplicit false
 
 universe u v
 
-variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
+variable {α : Type u} {β : Type v} {_ : BEq α} {_ : Hashable α}
 
 namespace Std.HashMap
 
diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean
index f8eb5f1c62..bc0584b312 100644
--- a/src/Std/Data/HashSet/Basic.lean
+++ b/src/Std/Data/HashSet/Basic.lean
@@ -23,7 +23,7 @@ set_option autoImplicit false
 
 universe u v
 
-variable {α : Type u}
+variable {α : Type u} {_ : BEq α} {_ : Hashable α}
 
 namespace Std
 
@@ -71,7 +71,7 @@ instance [BEq α] [Hashable α] : Inhabited (HashSet α) where
 Inserts the given element into the set. If the hash set already contains an element that is
 equal (with regard to `==`) to the given element, then the hash set is returned unchanged.
 -/
-@[inline] def insert [BEq α] [Hashable α] (m : HashSet α) (a : α) : HashSet α :=
+@[inline] def insert (m : HashSet α) (a : α) : HashSet α :=
   ⟨m.inner.insertIfNew a ()⟩
 
 /--
@@ -81,7 +81,7 @@ element, then the hash set is returned unchanged.
 
 Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
-@[inline] def containsThenInsert [BEq α] [Hashable α] (m : HashSet α) (a : α) : Bool × HashSet α :=
+@[inline] def containsThenInsert (m : HashSet α) (a : α) : Bool × HashSet α :=
   let ⟨replaced, r⟩ := m.inner.containsThenInsertIfNew a ()
   ⟨replaced, ⟨r⟩⟩
 
@@ -92,7 +92,7 @@ this: `a ∈ m` is equivalent to `m.contains a = true`.
 Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` use
 `==` for comparisons, while for hash sets, both use `==`.
 -/
-@[inline] def contains [BEq α] [Hashable α] (m : HashSet α) (a : α) : Bool :=
+@[inline] def contains (m : HashSet α) (a : α) : Bool :=
   m.inner.contains a
 
 instance [BEq α] [Hashable α] : Membership α (HashSet α) where
@@ -102,11 +102,11 @@ instance [BEq α] [Hashable α] {m : HashSet α} {a : α} : Decidable (a ∈ m)
   inferInstanceAs (Decidable (a ∈ m.inner))
 
 /-- Removes the element if it exists. -/
-@[inline] def erase [BEq α] [Hashable α] (m : HashSet α) (a : α) : HashSet α :=
+@[inline] def erase (m : HashSet α) (a : α) : HashSet α :=
   ⟨m.inner.erase a⟩
 
 /-- The number of elements present in the set -/
-@[inline] def size [BEq α] [Hashable α] (m : HashSet α) : Nat :=
+@[inline] def size (m : HashSet α) : Nat :=
   m.inner.size
 
 /--
@@ -116,7 +116,7 @@ Note that if your `BEq` instance is not reflexive or your `Hashable` instance is
 lawful, then it is possible that this function returns `false` even though `m.contains a = false`
 for all `a`.
 -/
-@[inline] def isEmpty [BEq α] [Hashable α] (m : HashSet α) : Bool :=
+@[inline] def isEmpty (m : HashSet α) : Bool :=
   m.inner.isEmpty
 
 section Unverified
@@ -124,29 +124,29 @@ section Unverified
 /-! We currently do not provide lemmas for the functions below. -/
 
 /-- Removes all elements from the hash set for which the given function returns `false`. -/
-@[inline] def filter [BEq α] [Hashable α] (f : α → Bool) (m : HashSet α) : HashSet α :=
+@[inline] def filter (f : α → Bool) (m : HashSet α) : HashSet α :=
   ⟨m.inner.filter fun a _ => f a⟩
 
 /--
 Monadically computes a value by folding the given function over the elements in the hash set in some
 order.
 -/
-@[inline] def foldM [BEq α] [Hashable α] {m : Type v → Type v} [Monad m] {β : Type v}
+@[inline] def foldM {m : Type v → Type v} [Monad m] {β : Type v}
     (f : β → α → m β) (init : β) (b : HashSet α) : m β :=
   b.inner.foldM (fun b a _ => f b a) init
 
 /-- Folds the given function over the elements of the hash set in some order. -/
-@[inline] def fold [BEq α] [Hashable α] {β : Type v} (f : β → α → β) (init : β) (m : HashSet α) :
+@[inline] def fold {β : Type v} (f : β → α → β) (init : β) (m : HashSet α) :
     β :=
   m.inner.fold (fun b a _ => f b a) init
 
 /-- Carries out a monadic action on each element in the hash set in some order. -/
-@[inline] def forM [BEq α] [Hashable α] {m : Type v → Type v} [Monad m] (f : α → m PUnit)
+@[inline] def forM {m : Type v → Type v} [Monad m] (f : α → m PUnit)
     (b : HashSet α) : m PUnit :=
   b.inner.forM (fun a _ => f a)
 
 /-- Support for the `for` loop construct in `do` blocks. -/
-@[inline] def forIn [BEq α] [Hashable α] {m : Type v → Type v} [Monad m] {β : Type v}
+@[inline] def forIn {m : Type v → Type v} [Monad m] {β : Type v}
     (f : α → β → m (ForInStep β)) (init : β) (b : HashSet α) : m β :=
   b.inner.forIn (fun a _ acc => f a acc) init
 
@@ -157,11 +157,11 @@ instance [BEq α] [Hashable α] {m : Type v → Type v} : ForIn m (HashSet α) 
   forIn m init f := m.forIn f init
 
 /-- Transforms the hash set into a list of elements in some order. -/
-@[inline] def toList [BEq α] [Hashable α] (m : HashSet α) : List α :=
+@[inline] def toList (m : HashSet α) : List α :=
   m.inner.keys
 
 /-- Transforms the hash set into an array of elements in some order. -/
-@[inline] def toArray [BEq α] [Hashable α] (m : HashSet α) : Array α :=
+@[inline] def toArray (m : HashSet α) : Array α :=
   m.inner.keysArray
 
 /--
@@ -169,7 +169,7 @@ Inserts multiple elements into the hash set. Note that unlike repeatedly calling
 collection contains multiple elements that are equal (with regard to `==`), then the last element
 in the collection will be present in the returned hash set.
 -/
-@[inline] def insertMany [BEq α] [Hashable α] {ρ : Type v} [ForIn Id ρ α] (m : HashSet α) (l : ρ) :
+@[inline] def insertMany {ρ : Type v} [ForIn Id ρ α] (m : HashSet α) (l : ρ) :
     HashSet α :=
   ⟨m.inner.insertManyUnit l⟩
 
@@ -186,7 +186,7 @@ Returns the number of buckets in the internal representation of the hash set. Th
 be useful for things like monitoring system health, but it should be considered an internal
 implementation detail.
 -/
-def Internal.numBuckets [BEq α] [Hashable α] (m : HashSet α) : Nat :=
+def Internal.numBuckets (m : HashSet α) : Nat :=
   HashMap.Internal.numBuckets m.inner
 
 instance [BEq α] [Hashable α] [Repr α] : Repr (HashSet α) where
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index 8944dca09e..01f8356e2a 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -20,7 +20,7 @@ set_option autoImplicit false
 
 universe u v
 
-variable {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
+variable {α : Type u} {_ : BEq α} {_ : Hashable α} [EquivBEq α] [LawfulHashable α]
 
 namespace Std.HashSet
 
diff --git a/tests/lean/run/hashmap-implicits.lean b/tests/lean/run/hashmap-implicits.lean
new file mode 100644
index 0000000000..c0e1b8efe8
--- /dev/null
+++ b/tests/lean/run/hashmap-implicits.lean
@@ -0,0 +1,71 @@
+import Std.Data.HashMap
+import Std.Data.HashSet
+import Std.Data.DHashMap
+
+open Std (DHashMap HashMap HashSet)
+
+/-! (Non-exhaustive) tests that `BEq` and `Hashable` arguments to query operations and lemmas are
+correctly solved by unification. -/
+
+namespace DHashMap
+
+structure A (α) extends BEq α, Hashable α where
+  foo : DHashMap α (fun _ => Nat)
+
+def A.add (xs : A α) (x : α) : A α :=
+  {xs with foo := xs.foo.insert x 5}
+
+example (xs : A α) (x : α) : ¬x ∈ @DHashMap.empty _ (fun _ => Nat) xs.toBEq xs.toHashable 5 :=
+  DHashMap.not_mem_empty
+
+example (xs : A α) (x : α) : (@DHashMap.empty _ (fun _ => Nat) xs.toBEq xs.toHashable 5).contains x = false := by
+  rw [DHashMap.contains_empty]
+
+example (xs : A α) (x : α) : DHashMap.Const.get? (@DHashMap.empty _ (fun _ => Nat) xs.toBEq xs.toHashable 5) x = none := by
+  rw [DHashMap.Const.get?_empty]
+
+example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x 5).size :=
+  DHashMap.size_le_size_insert
+
+end DHashMap
+
+namespace HashMap
+
+structure A (α) extends BEq α, Hashable α where
+  foo : HashMap α Nat
+
+def A.add (xs : A α) (x : α) : A α :=
+  {xs with foo := xs.foo.insert x 5}
+
+example (xs : A α) (x : α) : ¬x ∈ @HashMap.empty _ Nat xs.toBEq xs.toHashable 5 :=
+  HashMap.not_mem_empty
+
+example (xs : A α) (x : α) : (@HashMap.empty _ Nat xs.toBEq xs.toHashable 5).contains x = false := by
+  rw [HashMap.contains_empty]
+
+example (xs : A α) (x : α) : (@HashMap.empty _ Nat xs.toBEq xs.toHashable 5)[x]? = none := by
+  rw [HashMap.getElem?_empty]
+
+example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x 5).size :=
+  HashMap.size_le_size_insert
+
+end HashMap
+
+namespace HashSet
+
+structure A (α) extends BEq α, Hashable α where
+  foo : HashSet α
+
+def A.add (xs : A α) (x : α) : A α :=
+  {xs with foo := xs.foo.insert x}
+
+example (xs : A α) (x : α) : ¬x ∈ @HashSet.empty _ xs.toBEq xs.toHashable 5 :=
+  DHashMap.not_mem_empty
+
+example (xs : A α) (x : α) : (@HashSet.empty _ xs.toBEq xs.toHashable 5).contains x = false := by
+  rw [HashSet.contains_empty]
+
+example (xs : A α) (x : α) [@LawfulBEq α xs.toBEq] : xs.foo.size ≤ (xs.foo.insert x).size :=
+  HashSet.size_le_size_insert
+
+end HashSet