diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean
index 0f7b29d5cf55..7e52cbee5f83 100644
--- a/src/Std/Data/DHashMap/Internal/List/Associative.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean
@@ -82,6 +82,11 @@ theorem isEmpty_eq_false_iff_exists_isSome_getEntry? [BEq α] [ReflBEq α] :
   | [] => by simp
   | (⟨k, v⟩::l) => by simpa using ⟨k, by simp⟩
 
+theorem isEmpty_iff_forall_isSome_getEntry? [BEq α] [ReflBEq α] :
+    {l : List ((a : α) × β a)} → l.isEmpty ↔ ∀ a, (getEntry? a l).isSome = false
+  | [] => by simp
+  | (⟨k, v⟩::l) => ⟨by simp, fun h => have := h k; by simp at this⟩
+
 section
 
 variable {β : Type v}
@@ -255,6 +260,10 @@ theorem isEmpty_eq_false_iff_exists_containsKey [BEq α] [ReflBEq α] {l : List
     l.isEmpty = false ↔ ∃ a, containsKey a l := by
   simp [isEmpty_eq_false_iff_exists_isSome_getEntry?, containsKey_eq_isSome_getEntry?]
 
+theorem isEmpty_iff_forall_containsKey [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} :
+    l.isEmpty ↔ ∀ a, containsKey a l = false := by
+  simp [isEmpty_iff_forall_isSome_getEntry?, containsKey_eq_isSome_getEntry?]
+
 @[simp]
 theorem getEntry?_eq_none [BEq α] {l : List ((a : α) × β a)} {a : α} :
     getEntry? a l = none ↔ containsKey a l = false := by
@@ -699,6 +708,11 @@ theorem length_eraseKey_le [BEq α] {l : List ((a : α) × β a)} {k : α} :
     (eraseKey k l).length ≤ l.length :=
   sublist_eraseKey.length_le
 
+theorem length_le_length_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
+    l.length ≤ (eraseKey k l).length + 1 := by
+  rw [length_eraseKey]
+  split <;> omega
+
 theorem isEmpty_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
     (eraseKey k l).isEmpty = (l.isEmpty || (l.length == 1 && containsKey k l)) := by
   rw [Bool.eq_iff_iff]
@@ -859,9 +873,12 @@ theorem length_insertEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v :
 theorem length_le_length_insertEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
     l.length ≤ (insertEntry k v l).length := by
   rw [length_insertEntry]
-  cases containsKey k l
-  · simpa using Nat.le_add_right ..
-  · simp
+  split <;> omega
+
+theorem length_insertEntry_le [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
+    (insertEntry k v l).length ≤ l.length + 1 := by
+  rw [length_insertEntry]
+  split <;> omega
 
 section
 
@@ -1121,9 +1138,12 @@ theorem length_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α}
 theorem length_le_length_insertEntryIfNew [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
     l.length ≤ (insertEntryIfNew k v l).length := by
   rw [length_insertEntryIfNew]
-  cases containsKey k l
-  · simpa using Nat.le_add_right ..
-  · simp
+  split <;> omega
+
+theorem length_insertEntryIfNew_le [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
+    (insertEntryIfNew k v l).length ≤ l.length + 1 := by
+  rw [length_insertEntryIfNew]
+  split <;> omega
 
 @[simp]
 theorem keys_eraseKey [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} :
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index 585326596508..0e68b2fdfc12 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -123,9 +123,12 @@ theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
 
 theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] :
     m.1.isEmpty = false ↔ ∃ a, m.contains a = true := by
-  simp only [contains_eq_containsKey (Raw.WF.out h)]
   simp_to_model using List.isEmpty_eq_false_iff_exists_containsKey
 
+theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
+    m.1.isEmpty ↔ ∀ a, m.contains a = false := by
+  simp_to_model using List.isEmpty_iff_forall_containsKey
+
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
     (m.insert k v).contains a = ((k == a) || m.contains a) := by
   simp_to_model using List.containsKey_insertEntry
@@ -152,6 +155,10 @@ theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
     m.1.size ≤ (m.insert k v).1.size := by
   simp_to_model using List.length_le_length_insertEntry
 
+theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
+    (m.insert k v).1.size ≤ m.1.size + 1 := by
+  simp_to_model using List.length_insertEntry_le
+
 @[simp]
 theorem erase_empty {k : α} {c : Nat} : (empty c : Raw₀ α β).erase k = empty c := by
   simp [erase, empty]
@@ -176,6 +183,10 @@ theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} :
     (m.erase k).1.size ≤ m.1.size := by
   simp_to_model using List.length_eraseKey_le
 
+theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
+    m.1.size ≤ (m.erase k).1.size + 1 := by
+  simp_to_model using List.length_le_length_eraseKey
+
 @[simp]
 theorem containsThenInsert_fst {k : α} {v : β k} : (m.containsThenInsert k v).1 = m.contains k := by
   rw [containsThenInsert_eq_containsₘ, contains_eq_containsₘ]
@@ -546,6 +557,10 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
     m.1.size ≤ (m.insertIfNew k v).1.size := by
   simp_to_model using List.length_le_length_insertEntryIfNew
 
+theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
+    (m.insertIfNew k v).1.size ≤ m.1.size + 1 := by
+  simp_to_model using List.length_insertEntryIfNew_le
+
 theorem get?_insertIfNew [LawfulBEq α] {k a : α} {v : β k} :
     (m.insertIfNew k v).get? a =
       if h : k == a ∧ m.contains k = false then some (cast (congrArg β (eq_of_beq h.1)) v)
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index f67c4c0e5ef3..0e18a41cc310 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -63,6 +63,30 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 @[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : DHashMap α β) :=
   not_mem_empty
 
+theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty → m.contains a = false :=
+  Raw₀.contains_of_isEmpty ⟨m.1, _⟩ m.2
+
+theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty → ¬a ∈ m := by
+  simpa [mem_iff_contains] using contains_of_isEmpty
+
+theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = false ↔ ∃ a, m.contains a = true :=
+  Raw₀.isEmpty_eq_false_iff_exists_contains_eq_true ⟨m.1, _⟩ m.2
+
+theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = false ↔ ∃ a, a ∈ m := by
+  simpa [mem_iff_contains] using isEmpty_eq_false_iff_exists_contains_eq_true
+
+theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = true ↔ ∀ a, m.contains a = false :=
+  Raw₀.isEmpty_iff_forall_contains ⟨m.1, _⟩ m.2
+
+theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = true ↔ ∀ a, ¬a ∈ m := by
+  simpa [mem_iff_contains] using isEmpty_iff_forall_contains
+
 @[simp]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β k} :
     (m.insert k v).contains a = (k == a || m.contains a) :=
@@ -109,6 +133,10 @@ theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
     m.size ≤ (m.insert k v).size :=
   Raw₀.size_le_size_insert ⟨m.1, _⟩ m.2
 
+theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
+    (m.insert k v).size ≤ m.size + 1 :=
+  Raw₀.size_insert_le ⟨m.1, _⟩ m.2
+
 @[simp]
 theorem erase_empty {k : α} {c : Nat} : (empty c : DHashMap α β).erase k = empty c :=
   Subtype.eq (congrArg Subtype.val (Raw₀.erase_empty (k := k)) :) -- Lean code is happy
@@ -146,6 +174,10 @@ theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
   Raw₀.size_erase_le _ m.2
 
+theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
+    m.size ≤ (m.erase k).size + 1 :=
+  Raw₀.size_le_size_erase ⟨m.1, _⟩ m.2
+
 @[simp]
 theorem containsThenInsert_fst {k : α} {v : β k} : (m.containsThenInsert k v).1 = m.contains k :=
   Raw₀.containsThenInsert_fst _
@@ -618,6 +650,10 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
     m.size ≤ (m.insertIfNew k v).size :=
   Raw₀.size_le_size_insertIfNew ⟨m.1, _⟩ m.2
 
+theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
+    (m.insertIfNew k v).size ≤ m.size + 1 :=
+  Raw₀.size_insertIfNew_le _ m.2
+
 theorem get?_insertIfNew [LawfulBEq α] {k a : α} {v : β k} : (m.insertIfNew k v).get? a =
     if h : k == a ∧ ¬k ∈ m then some (cast (congrArg β (eq_of_beq h.1)) v) else m.get? a := by
   simp only [mem_iff_contains, Bool.not_eq_true]
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 9487f4749c6f..ba99e8ffcc3f 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -111,6 +111,30 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 @[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : Raw α β) :=
   not_mem_empty
 
+theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty → m.contains a = false := by
+  simp_to_raw using Raw₀.contains_of_isEmpty ⟨m, _⟩
+
+theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty → ¬a ∈ m := by
+  simpa [mem_iff_contains] using contains_of_isEmpty h
+
+theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = false ↔ ∃ a, m.contains a = true := by
+  simp_to_raw using Raw₀.isEmpty_eq_false_iff_exists_contains_eq_true ⟨m, _⟩
+
+theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = false ↔ ∃ a, a ∈ m := by
+  simpa [mem_iff_contains] using isEmpty_eq_false_iff_exists_contains_eq_true h
+
+theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = true ↔ ∀ a, m.contains a = false := by
+  simp_to_raw using Raw₀.isEmpty_iff_forall_contains ⟨m, _⟩
+
+theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = true ↔ ∀ a, ¬a ∈ m := by
+  simpa [mem_iff_contains] using isEmpty_iff_forall_contains h
+
 @[simp]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {a k : α} {v : β k} :
     (m.insert k v).contains a = (k == a || m.contains a) := by
@@ -158,6 +182,10 @@ theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k
     m.size ≤ (m.insert k v).size := by
   simp_to_raw using Raw₀.size_le_size_insert ⟨m, _⟩ h
 
+theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
+    (m.insert k v).size ≤ m.size + 1 := by
+  simp_to_raw using Raw₀.size_insert_le ⟨m, _⟩ h
+
 @[simp]
 theorem erase_empty {k : α} {c : Nat} : (empty c : Raw α β).erase k = empty c := by
   rw [erase_eq (by wf_trivial)]
@@ -197,6 +225,10 @@ theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size := by
   simp_to_raw using Raw₀.size_erase_le
 
+theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
+    m.size ≤ (m.erase k).size + 1 := by
+  simp_to_raw using Raw₀.size_le_size_erase ⟨m, _⟩
+
 @[simp]
 theorem containsThenInsert_fst {k : α} {v : β k} : (m.containsThenInsert k v).1 = m.contains k := by
   simp_to_raw using Raw₀.containsThenInsert_fst
@@ -668,6 +700,10 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
     m.size ≤ (m.insertIfNew k v).size := by
   simp_to_raw using Raw₀.size_le_size_insertIfNew ⟨m, _⟩
 
+theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
+    (m.insertIfNew k v).size ≤ m.size + 1 := by
+  simp_to_raw using Raw₀.size_insertIfNew_le
+
 theorem get?_insertIfNew [LawfulBEq α] {k a : α} {v : β k} :
     (m.insertIfNew k v).get? a =
       if h : k == a ∧ ¬k ∈ m then some (cast (congrArg β (eq_of_beq h.1)) v)
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 88bd978a199f..9def7f0d7cc0 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -71,6 +71,30 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 @[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : HashMap α β) :=
   DHashMap.not_mem_emptyc
 
+theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty → m.contains a = false :=
+  DHashMap.contains_of_isEmpty
+
+theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty → ¬a ∈ m :=
+  DHashMap.not_mem_of_isEmpty
+
+theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = false ↔ ∃ a, m.contains a = true :=
+  DHashMap.isEmpty_eq_false_iff_exists_contains_eq_true
+
+theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = false ↔ ∃ a, a ∈ m :=
+  DHashMap.isEmpty_eq_false_iff_exists_mem
+
+theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = true ↔ ∀ a, m.contains a = false :=
+  DHashMap.isEmpty_iff_forall_contains
+
+theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = true ↔ ∀ a, ¬a ∈ m :=
+  DHashMap.isEmpty_iff_forall_not_mem
+
 @[simp]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     (m.insert k v).contains a = (k == a || m.contains a) :=
@@ -117,6 +141,10 @@ theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
     m.size ≤ (m.insert k v).size :=
   DHashMap.size_le_size_insert
 
+theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+    (m.insert k v).size ≤ m.size + 1 :=
+  DHashMap.size_insert_le
+
 @[simp]
 theorem erase_empty {a : α} {c : Nat} : (empty c : HashMap α β).erase a = empty c :=
   ext DHashMap.erase_empty
@@ -154,6 +182,10 @@ theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
   DHashMap.size_erase_le
 
+theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
+    m.size ≤ (m.erase k).size + 1 :=
+  DHashMap.size_le_size_erase
+
 @[simp]
 theorem containsThenInsert_fst {k : α} {v : β} : (m.containsThenInsert k v).1 = m.contains k :=
   DHashMap.containsThenInsert_fst
@@ -410,6 +442,10 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
     m.size ≤ (m.insertIfNew k v).size :=
   DHashMap.size_le_size_insertIfNew
 
+theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+    (m.insertIfNew k v).size ≤ m.size + 1 :=
+  DHashMap.size_insertIfNew_le
+
 theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     (m.insertIfNew k v)[a]? = if k == a ∧ ¬k ∈ m then some v else m[a]? :=
   DHashMap.Const.get?_insertIfNew
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index 76a7adabd2cf..dd34fc46f9ad 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -70,6 +70,30 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 @[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : Raw α β) :=
   DHashMap.Raw.not_mem_emptyc
 
+theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty → m.contains a = false :=
+  DHashMap.Raw.contains_of_isEmpty h.out
+
+theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty → ¬a ∈ m :=
+  DHashMap.Raw.not_mem_of_isEmpty h.out
+
+theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = false ↔ ∃ a, m.contains a = true :=
+  DHashMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true h.out
+
+theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = false ↔ ∃ a, a ∈ m :=
+  DHashMap.Raw.isEmpty_eq_false_iff_exists_mem h.out
+
+theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = true ↔ ∀ a, m.contains a = false :=
+  DHashMap.Raw.isEmpty_iff_forall_contains h.out
+
+theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = true ↔ ∀ a, ¬a ∈ m :=
+  DHashMap.Raw.isEmpty_iff_forall_not_mem h.out
+
 @[simp]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     (m.insert k v).contains a = (k == a || m.contains a) :=
@@ -116,6 +140,10 @@ theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β}
     m.size ≤ (m.insert k v).size :=
   DHashMap.Raw.size_le_size_insert h.out
 
+theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+    (m.insert k v).size ≤ m.size + 1 :=
+  DHashMap.Raw.size_insert_le h.out
+
 @[simp]
 theorem erase_empty {k : α} {c : Nat} : (empty c : Raw α β).erase k = empty c :=
   ext DHashMap.Raw.erase_empty
@@ -153,6 +181,10 @@ theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
   DHashMap.Raw.size_erase_le h.out
 
+theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
+    m.size ≤ (m.erase k).size + 1 :=
+  DHashMap.Raw.size_le_size_erase h.out
+
 @[simp]
 theorem containsThenInsert_fst {k : α} {v : β} : (m.containsThenInsert k v).1 = m.contains k :=
   DHashMap.Raw.containsThenInsert_fst h.out
@@ -408,6 +440,10 @@ theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] {k : α} {v :
     m.size ≤ (m.insertIfNew k v).size :=
   DHashMap.Raw.size_le_size_insertIfNew h.out
 
+theorem size_insertIfNew_le [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+    (m.insertIfNew k v).size ≤ m.size + 1 :=
+  DHashMap.Raw.size_insertIfNew_le h.out
+
 theorem getElem?_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} :
     (m.insertIfNew k v)[a]? = if k == a ∧ ¬k ∈ m then some v else m[a]? :=
   DHashMap.Raw.Const.get?_insertIfNew h.out
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index bee599c20d2d..91758622b3f9 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -65,6 +65,30 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 @[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : HashSet α) :=
   HashMap.not_mem_emptyc
 
+theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty → m.contains a = false :=
+  HashMap.contains_of_isEmpty
+
+theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty → ¬a ∈ m :=
+  HashMap.not_mem_of_isEmpty
+
+theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = false ↔ ∃ a, m.contains a = true :=
+  HashMap.isEmpty_eq_false_iff_exists_contains_eq_true
+
+theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = false ↔ ∃ a, a ∈ m :=
+  HashMap.isEmpty_eq_false_iff_exists_mem
+
+theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = true ↔ ∀ a, m.contains a = false :=
+  HashMap.isEmpty_iff_forall_contains
+
+theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = true ↔ ∀ a, ¬a ∈ m :=
+  HashMap.isEmpty_iff_forall_not_mem
+
 @[simp]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.insert k).contains a = (k == a || m.contains a) :=
@@ -108,6 +132,10 @@ theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} :
 theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} : m.size ≤ (m.insert k).size :=
   HashMap.size_le_size_insertIfNew
 
+theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} :
+    (m.insert k).size ≤ m.size + 1 :=
+  HashMap.size_insertIfNew_le
+
 @[simp]
 theorem erase_empty {a : α} {c : Nat} : (empty c : HashSet α).erase a = empty c :=
   ext HashMap.erase_empty
@@ -145,6 +173,10 @@ theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
   HashMap.size_erase_le
 
+theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
+    m.size ≤ (m.erase k).size + 1 :=
+  HashMap.size_le_size_erase
+
 @[simp]
 theorem containsThenInsert_fst {k : α} : (m.containsThenInsert k).1 = m.contains k :=
   HashMap.containsThenInsertIfNew_fst
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index 40e3315c380b..f9a381a45860 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -65,6 +65,30 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) :
 @[simp] theorem not_mem_emptyc {a : α} : ¬a ∈ (∅ : Raw α) :=
   HashMap.Raw.not_mem_emptyc
 
+theorem contains_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty → m.contains a = false :=
+  HashMap.Raw.contains_of_isEmpty h.out
+
+theorem not_mem_of_isEmpty [EquivBEq α] [LawfulHashable α] {a : α} :
+    m.isEmpty → ¬a ∈ m :=
+  HashMap.Raw.not_mem_of_isEmpty h.out
+
+theorem isEmpty_eq_false_iff_exists_contains_eq_true [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = false ↔ ∃ a, m.contains a = true :=
+  HashMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true h.out
+
+theorem isEmpty_eq_false_iff_exists_mem [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = false ↔ ∃ a, a ∈ m :=
+  HashMap.Raw.isEmpty_eq_false_iff_exists_mem h.out
+
+theorem isEmpty_iff_forall_contains [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = true ↔ ∀ a, m.contains a = false :=
+  HashMap.Raw.isEmpty_iff_forall_contains h.out
+
+theorem isEmpty_iff_forall_not_mem [EquivBEq α] [LawfulHashable α] :
+    m.isEmpty = true ↔ ∀ a, ¬a ∈ m :=
+  HashMap.Raw.isEmpty_iff_forall_not_mem h.out
+
 @[simp]
 theorem contains_insert [EquivBEq α] [LawfulHashable α] {k a : α} :
     (m.insert k).contains a = (k == a || m.contains a) :=
@@ -108,6 +132,9 @@ theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} :
 theorem size_le_size_insert [EquivBEq α] [LawfulHashable α] {k : α} : m.size ≤ (m.insert k).size :=
   HashMap.Raw.size_le_size_insertIfNew h.out
 
+theorem size_insert_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).size ≤ m.size + 1 :=
+  HashMap.Raw.size_insertIfNew_le h.out
+
 @[simp]
 theorem erase_empty {k : α} {c : Nat} : (empty c : Raw α).erase k = empty c :=
   ext HashMap.Raw.erase_empty
@@ -145,6 +172,10 @@ theorem size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
 theorem size_erase_le [EquivBEq α] [LawfulHashable α] {k : α} : (m.erase k).size ≤ m.size :=
   HashMap.Raw.size_erase_le h.out
 
+theorem size_le_size_erase [EquivBEq α] [LawfulHashable α] {k : α} :
+    m.size ≤ (m.erase k).size + 1 :=
+  HashMap.Raw.size_le_size_erase h.out
+
 @[simp]
 theorem containsThenInsert_fst {k : α} : (m.containsThenInsert k).1 = m.contains k :=
   HashMap.Raw.containsThenInsertIfNew_fst h.out