diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean
index 99660540ba4b..06043cca696f 100644
--- a/src/Lean/Data/HashMap.lean
+++ b/src/Lean/Data/HashMap.lean
@@ -64,18 +64,21 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
 
 def findEntry? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
   match m with
+  | ⟨0, _⟩ => none
   | ⟨_, buckets⟩ =>
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
     buckets.val[i].findEntry? a
 
 def find? [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
   match m with
+  | ⟨0, _⟩ => none
   | ⟨_, buckets⟩ =>
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
     buckets.val[i].find? a
 
 def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
   match m with
+  | ⟨0, _⟩ => false
   | ⟨_, buckets⟩ =>
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
     buckets.val[i].contains a
diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean
index 43f77c721f58..fb1731af1188 100644
--- a/src/Lean/Data/HashSet.lean
+++ b/src/Lean/Data/HashSet.lean
@@ -60,12 +60,14 @@ private def mkIdx {sz : Nat} (hash : UInt64) (h : sz.isPowerOfTwo) : { u : USize
 
 def find? [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
   match m with
+  | ⟨0, _⟩ => none
   | ⟨_, buckets⟩ =>
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
     buckets.val[i].find? (fun a' => a == a')
 
 def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
   match m with
+  | ⟨0, _⟩ => false
   | ⟨_, buckets⟩ =>
     let ⟨i, h⟩ := mkIdx (hash a) buckets.property
     buckets.val[i].contains a