diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index 471fca9ed8b9..837b6c76545c 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -815,22 +815,22 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
     m.1.keys.length = m.1.size := by
   simp_to_model using List.length_keys_eq_length
 
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α] (h: m.1.WF):
+    m.1.keys.isEmpty = m.1.isEmpty:= by
+  simp_to_model using List.isEmpty_keys_eq_isEmpty
+
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
     m.1.keys.contains k = m.contains k := by
   simp_to_model using List.containsKey_eq_keys_contains.symm
 
 @[simp]
-theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h: m.1.WF):
-    m.1.keys.isEmpty = m.1.isEmpty:= by
-  simp_to_model using List.isEmpty_keys_eq_isEmpty
-
-@[simp]
-theorem mem_keys_iff_contains [LawfulBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
     k ∈ m.1.keys ↔ m.contains k := by
   simp_to_model 
   rw [List.containsKey_eq_keys_contains]
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index a1a583f21928..e6016179028c 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -944,9 +944,14 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] :
+theorem length_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.length = m.size :=
-  Raw₀.length_keys_eq_size ⟨m.1, m.2.size_buckets_pos⟩ m.2
+  Raw₀.length_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α]:
+    m.keys.isEmpty = m.isEmpty  :=
+  Raw₀.isEmpty_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
@@ -954,15 +959,10 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
   Raw₀.contains_keys ⟨m.1, _⟩ m.2
 
 @[simp]
-theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α]:
-    m.keys.isEmpty = m.isEmpty  :=
-  Raw₀.isEmpty_keys_eq_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2
-
-@[simp]
-theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] {k : α} :
     k ∈ m.keys ↔ k ∈ m := by 
   rw [mem_iff_contains]
-  exact Raw₀.mem_keys_iff_contains ⟨m.1, _⟩ m.2
+  exact Raw₀.mem_keys ⟨m.1, _⟩ m.2
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) := 
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index f890d36423c5..42d4db498753 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1023,9 +1023,14 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.length = m.size := by
-  simp_to_raw using Raw₀.length_keys_eq_size ⟨m, h.size_buckets_pos⟩ h
+  simp_to_raw using Raw₀.length_keys ⟨m, h.size_buckets_pos⟩ h
+
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.keys.isEmpty = m.isEmpty := by
+  simp_to_raw using Raw₀.isEmpty_keys ⟨m, h.size_buckets_pos⟩
 
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
@@ -1033,15 +1038,10 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
   simp_to_raw using Raw₀.contains_keys ⟨m, _⟩ h
 
 @[simp]
-theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
-    m.keys.isEmpty = m.isEmpty := by
-  simp_to_raw using Raw₀.isEmpty_keys_eq_isEmpty ⟨m, h.size_buckets_pos⟩
-
-@[simp]
-theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     k ∈ m.keys ↔ k ∈ m := by 
   rw [mem_iff_contains]
-  simp_to_raw using Raw₀.mem_keys_iff_contains ⟨m, _⟩ h
+  simp_to_raw using Raw₀.mem_keys ⟨m, _⟩ h
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.Pairwise (fun a b => (a == b) = false) := by
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 6f9fa63dcf8e..077a51c74b02 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -678,9 +678,14 @@ instance [EquivBEq α] [LawfulHashable α] : LawfulGetElem (HashMap α β) α β
     split <;> simp_all
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] :
+theorem length_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.length = m.size :=
-  DHashMap.length_keys_eq_size
+  DHashMap.length_keys
+
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α]:
+    m.keys.isEmpty = m.isEmpty :=
+  DHashMap.isEmpty_keys
 
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
@@ -688,14 +693,9 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
   DHashMap.contains_keys
 
 @[simp]
-theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α]:
-    m.keys.isEmpty = m.isEmpty :=
-  DHashMap.isEmpty_keys_eq_isEmpty
-
-@[simp]
-theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] {k : α} :
     k ∈ m.keys ↔ k ∈ m := 
-  DHashMap.mem_keys_iff_mem
+  DHashMap.mem_keys
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) := 
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index b13932fb51c7..cc0816a966c7 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -683,9 +683,14 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
   ext (DHashMap.Raw.Const.getThenInsertIfNew?_snd h.out)
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.length = m.size :=
-  DHashMap.Raw.length_keys_eq_size h.out
+  DHashMap.Raw.length_keys h.out
+
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.keys.isEmpty = m.isEmpty :=
+  DHashMap.Raw.isEmpty_keys h.out
 
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
@@ -693,14 +698,9 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
   DHashMap.Raw.contains_keys h.out
 
 @[simp]
-theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
-    m.keys.isEmpty = m.isEmpty :=
-  DHashMap.Raw.isEmpty_keys_eq_isEmpty h.out
-
-@[simp]
-theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     k ∈ m.keys ↔ k ∈ m := 
-  DHashMap.Raw.mem_keys_iff_mem h.out
+  DHashMap.Raw.mem_keys h.out
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.Pairwise (fun a b => (a == b) = false) := 
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index 4aa626725aef..b0318c0f47ce 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -354,8 +354,14 @@ theorem containsThenInsert_snd {k : α} : (m.containsThenInsert k).2 = m.insert
   ext HashMap.containsThenInsertIfNew_snd
 
 @[simp]
-theorem toList_length_eq_size [EquivBEq α] [LawfulHashable α] : m.toList.length = m.size :=
-  HashMap.length_keys_eq_size
+theorem length_toList [EquivBEq α] [LawfulHashable α] : 
+    m.toList.length = m.size :=
+  HashMap.length_keys
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.isEmpty = m.isEmpty :=
+  HashMap.isEmpty_keys
 
 @[simp]
 theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α}:
@@ -363,14 +369,9 @@ theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α}:
   HashMap.contains_keys
 
 @[simp]
-theorem isEmpty_toList_eq_isEmpty [EquivBEq α] [LawfulHashable α] :
-    m.toList.isEmpty = m.isEmpty :=
-  HashMap.isEmpty_keys_eq_isEmpty
-
-@[simp]
-theorem mem_toList_iff_mem [LawfulBEq α] [LawfulHashable α]  {k : α}:
+theorem mem_toList [LawfulBEq α] [LawfulHashable α]  {k : α}:
     k ∈ m.toList ↔ k ∈ m :=
-  HashMap.mem_keys_iff_mem
+  HashMap.mem_keys
 
 theorem distinct_toList [EquivBEq α] [LawfulHashable α]:
     m.toList.Pairwise (fun a b => (a == b) = false) :=
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index f652c3a081fe..77dcaa5bcfd8 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -367,8 +367,14 @@ theorem containsThenInsert_snd (h : m.WF) {k : α} : (m.containsThenInsert k).2
   ext (HashMap.Raw.containsThenInsertIfNew_snd h.out)
 
 @[simp]
-theorem toList_length_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF): m.toList.length = m.size :=
-  HashMap.Raw.length_keys_eq_size h.1
+theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF): 
+    m.toList.length = m.size :=
+  HashMap.Raw.length_keys h.1
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.toList.isEmpty = m.isEmpty :=
+  HashMap.Raw.isEmpty_keys h.1
 
 @[simp]
 theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α} (h : m.WF):
@@ -376,14 +382,9 @@ theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α} (h : m.WF):
   HashMap.Raw.contains_keys h.1
 
 @[simp]
-theorem isEmpty_toList_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
-    m.toList.isEmpty = m.isEmpty :=
-  HashMap.Raw.isEmpty_keys_eq_isEmpty h.1
-
-@[simp]
-theorem mem_toList_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α}:
+theorem mem_toList [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α}:
     k ∈ m.toList ↔ k ∈ m :=
-  HashMap.Raw.mem_keys_iff_mem h.1
+  HashMap.Raw.mem_keys h.1
 
 theorem distinct_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.Pairwise (fun a b => (a == b) = false) :=