From aea42fb9b893479a9f4206a2a9de1dea292174eb Mon Sep 17 00:00:00 2001
From: jt0202 <johannes.tantow@gmail.com>
Date: Tue, 14 Jan 2025 19:24:06 +0100
Subject: [PATCH] =?UTF-8?q?Replace=20'm.contains=20k=20=3D=20false'=20by?=
 =?UTF-8?q?=20'=C2=AC=20k=20=E2=88=88=20m'=20in=20statements=20for=20inser?=
 =?UTF-8?q?tIfNewUnit?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Std/Data/DHashMap/Lemmas.lean    | 79 +++++++++++++++-------------
 src/Std/Data/DHashMap/RawLemmas.lean | 35 +++++++-----
 src/Std/Data/HashMap/Lemmas.lean     | 56 ++++++++++----------
 src/Std/Data/HashMap/RawLemmas.lean  | 56 ++++++++++----------
 src/Std/Data/HashSet/Lemmas.lean     | 56 ++++++++++----------
 src/Std/Data/HashSet/RawLemmas.lean  | 56 ++++++++++----------
 6 files changed, 176 insertions(+), 162 deletions(-)

diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 3b8721e6c6c9..c9e49d1c13be 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -990,7 +990,7 @@ theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α]
   simp [mem_iff_contains]
 
 theorem mem_of_mem_insertMany_list [EquivBEq α] [LawfulHashable α]
-    {l : List ((a : α) × β a)} {k : α}  (mem : k ∈ (m.insertMany l))
+    {l : List ((a : α) × β a)} {k : α}  (mem : k ∈ m.insertMany l)
     (contains_eq_false : (l.map Sigma.fst).contains k = false) :
     k ∈ m :=
   Raw₀.contains_of_contains_insertMany_list ⟨m.1, _⟩ m.2 mem contains_eq_false
@@ -1335,74 +1335,81 @@ theorem mem_of_mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α]
     k ∈ insertManyIfNewUnit m l → k ∈ m :=
   Raw₀.Const.contains_of_contains_insertManyIfNewUnit_list ⟨m.1, _⟩ m.2 contains_eq_false
 
-theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] {l : List α} {k : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
-    getKey? (insertManyIfNewUnit m l) k = none :=
-  Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    ⟨m.1, _⟩ m.2 contains_eq_false contains_eq_false'
+    (not_mem : ¬ k ∈ m) (contains_eq_false' : l.contains k = false) :
+    getKey? (insertManyIfNewUnit m l) k = none := by
+  simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
+  exact Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+    ⟨m.1, _⟩ m.2 not_mem contains_eq_false'
 
-theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k k' : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
-    getKey? (insertManyIfNewUnit m l) k' = some k :=
-  Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩
-    m.2 k_beq contains_eq_false distinct mem
+    getKey? (insertManyIfNewUnit m l) k' = some k := by
+  simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
+  exact Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩
+    m.2 k_beq not_mem distinct mem
 
 theorem getKey?_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} (h' : k ∈ m) :
     getKey? (insertManyIfNewUnit m l) k = getKey? m k :=
   Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains ⟨m.1, _⟩ m.2 h'
 
-theorem getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α}
     {k k' : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false) (distinct : l.Pairwise (fun a b => (a == b) = false))
+    (not_mem : ¬ k ∈ m) (distinct : l.Pairwise (fun a b => (a == b) = false))
     (mem : k ∈ l) {h} :
-    getKey (insertManyIfNewUnit m l) k' h = k :=
-  Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
-    contains_eq_false distinct mem
+    getKey (insertManyIfNewUnit m l) k' h = k := by
+  simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
+  exact Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
+    not_mem distinct mem
 
 theorem getKey_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} (mem : k ∈ m) {h} :
     getKey (insertManyIfNewUnit m l) k h = getKey m k mem :=
   Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains ⟨m.1, _⟩ m.2 _
 
-theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
-    getKey! (insertManyIfNewUnit m l) k = default :=
-  Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    ⟨m.1, _⟩ m.2 contains_eq_false contains_eq_false'
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
+    getKey! (insertManyIfNewUnit m l) k = default := by
+  simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
+  exact Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+    ⟨m.1, _⟩ m.2 not_mem contains_eq_false
 
-theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     [Inhabited α] {l : List α} {k k' : α} (k_beq : k == k')
-    (contains_eq_false: m.contains k = false) (distinct : l.Pairwise (fun a b => (a == b) = false))
+    (not_mem : ¬ k ∈ m) (distinct : l.Pairwise (fun a b => (a == b) = false))
     (mem : k ∈ l) :
-    getKey! (insertManyIfNewUnit m l) k' = k :=
-  Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
-    contains_eq_false distinct mem
+    getKey! (insertManyIfNewUnit m l) k' = k := by
+  simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
+  exact Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
+    not_mem distinct mem
 
 theorem getKey!_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
     [Inhabited α] {l : List α} {k : α} (mem : k ∈ m) :
     getKey! (insertManyIfNewUnit m l) k = getKey! m k :=
   Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains ⟨m.1, _⟩ m.2 mem
 
-theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
-    getKeyD (insertManyIfNewUnit m l) k fallback = fallback :=
-  Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    ⟨m.1, _⟩ m.2 contains_eq_false contains_eq_false'
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
+    getKeyD (insertManyIfNewUnit m l) k fallback = fallback := by
+  simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
+  exact Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+    ⟨m.1, _⟩ m.2 not_mem contains_eq_false
 
-theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k k' fallback : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
-    getKeyD (insertManyIfNewUnit m l) k' fallback = k :=
-  Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
-    contains_eq_false distinct mem
+    getKeyD (insertManyIfNewUnit m l) k' fallback = k := by
+  simp only [mem_iff_contains, Bool.not_eq_true] at not_mem
+  exact Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem ⟨m.1, _⟩ m.2 k_beq
+    not_mem distinct mem
 
 theorem getKeyD_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k fallback : α} (mem : k ∈ m) :
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index dd6989fde67c..4aa6d3e5774a 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1435,16 +1435,18 @@ theorem mem_of_mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h
   simp only [mem_iff_contains]
   simp_to_raw using Raw₀.Const.contains_of_contains_insertManyIfNewUnit_list
 
-theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α} :
-    m.contains k = false → l.contains k = false →
+    ¬ k ∈ m → l.contains k = false →
       getKey? (insertManyIfNewUnit m l) k = none := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
 
-theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α} {k k' : α} (k_beq : k == k') :
-    m.contains k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
+    ¬ k ∈ m → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
       getKey? (insertManyIfNewUnit m l) k' = some k := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
 
 theorem getKey?_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
@@ -1458,23 +1460,26 @@ theorem getKey_insertManyIfNewUnit_list_of_mem
     getKey (insertManyIfNewUnit m l) k h' = getKey m k mem := by
   simp_to_raw using Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains
 
-theorem getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α}
     {k k' : α} (k_beq : k == k') {h'} :
-    m.contains k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
+    ¬ k ∈ m → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
       getKey (insertManyIfNewUnit m l) k' h' = k := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
 
-theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {l : List α} {k : α} :
-    m.contains k = false → l.contains k = false → getKey! (insertManyIfNewUnit m l) k = default := by
+    ¬ k ∈ m → l.contains k = false → getKey! (insertManyIfNewUnit m l) k = default := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using
     Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
 
-theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     [Inhabited α] (h : m.WF) {l : List α} {k k' : α} (k_beq : k == k') :
-    contains m k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
+    ¬ k ∈ m → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
       getKey! (insertManyIfNewUnit m l) k' = k := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
 
 theorem getKey!_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
@@ -1483,17 +1488,19 @@ theorem getKey!_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α
   simp only [mem_iff_contains]
   simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains
 
-theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k fallback : α} :
-    m.contains k = false → l.contains k = false →
+    ¬ k ∈ m → l.contains k = false →
       getKeyD (insertManyIfNewUnit m l) k fallback = fallback := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using
     Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
 
-theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α} {k k' fallback : α} (k_beq : k == k') :
-    m.contains k = false → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
+    ¬ k ∈ m → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
       getKeyD (insertManyIfNewUnit m l) k' fallback = k := by
+  simp only [mem_iff_contains, Bool.not_eq_true]
   simp_to_raw using Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
 
 theorem getKeyD_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index e43a7635d851..19e2d073bc57 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -915,71 +915,71 @@ theorem getD_insertManyIfNewUnit_list
     getD (insertManyIfNewUnit m l) k fallback = () := by
   simp
 
-theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] {l : List α} {k : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
     getKey? (insertManyIfNewUnit m l) k = none :=
-  DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    contains_eq_false contains_eq_false'
+  DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    not_mem contains_eq_false
 
-theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
-    {l : List α} {k k' : α} (k_beq : k == k') (contains_eq_false : m.contains k = false)
+theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
+    {l : List α} {k k' : α} (k_beq : k == k') (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
     getKey? (insertManyIfNewUnit m l) k' = some k :=
-  DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    k_beq contains_eq_false distinct mem
+  DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem
+    k_beq not_mem distinct mem
 
 theorem getKey?_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} (mem : k ∈ m) :
     getKey? (insertManyIfNewUnit m l) k = getKey? m k :=
   DHashMap.Const.getKey?_insertManyIfNewUnit_list_of_mem mem
 
-theorem getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
-    {l : List α} {k k' : α} (k_beq : k == k') (contains_eq_false : m.contains k = false)
+theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
+    {l : List α} {k k' : α} (k_beq : k == k') (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) {h} :
     getKey (insertManyIfNewUnit m l) k' h = k :=
-  DHashMap.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    k_beq contains_eq_false distinct mem
+  DHashMap.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem
+    k_beq not_mem distinct mem
 
 theorem getKey_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} (mem : k ∈ m) {h} :
     getKey (insertManyIfNewUnit m l) k h = getKey m k mem :=
   DHashMap.Const.getKey_insertManyIfNewUnit_list_of_mem mem
 
-theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
     getKey! (insertManyIfNewUnit m l) k = default :=
-  DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    contains_eq_false contains_eq_false'
+  DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    not_mem contains_eq_false
 
-theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     [Inhabited α] {l : List α} {k k' : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
     getKey! (insertManyIfNewUnit m l) k' = k :=
-  DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    k_beq contains_eq_false distinct mem
+  DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem
+    k_beq not_mem distinct mem
 
 theorem getKey!_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
     [Inhabited α] {l : List α} {k : α} (mem : k ∈ m) :
     getKey! (insertManyIfNewUnit m l) k = getKey! m k :=
   DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_mem mem
 
-theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
     getKeyD (insertManyIfNewUnit m l) k fallback = fallback :=
-  DHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    contains_eq_false contains_eq_false'
+  DHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    not_mem contains_eq_false
 
-theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k k' fallback : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l ) :
     getKeyD (insertManyIfNewUnit m l) k' fallback = k :=
-  DHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    k_beq contains_eq_false distinct mem
+  DHashMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem
+    k_beq not_mem distinct mem
 
 theorem getKeyD_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k fallback : α} (mem : k ∈ m) :
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index fffeca95a0c5..bdcc2b0b857c 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -903,74 +903,74 @@ theorem mem_of_mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h
     k ∈ insertManyIfNewUnit m l → k ∈ m :=
   DHashMap.Raw.Const.mem_of_mem_insertManyIfNewUnit_list h.out contains_eq_false
 
-theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false': l.contains k = false) :
+    (not_mem : ¬ k ∈ m) (contains_eq_false: l.contains k = false) :
     getKey? (insertManyIfNewUnit m l) k = none :=
-  DHashMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    h.out contains_eq_false contains_eq_false'
+  DHashMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    h.out not_mem contains_eq_false
 
-theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α} {k k' : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
     getKey? (insertManyIfNewUnit m l) k' = some k :=
-  DHashMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    h.out k_beq contains_eq_false distinct mem
+  DHashMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem
+    h.out k_beq not_mem distinct mem
 
 theorem getKey?_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α} {k : α} (mem : k ∈ m) :
     getKey? (insertManyIfNewUnit m l) k = getKey? m k :=
   DHashMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_mem h.out mem
 
-theorem getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α}
     {k k' : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) {h'} :
     getKey (insertManyIfNewUnit m l) k' h' = k :=
-  DHashMap.Raw.Const.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    h.out k_beq contains_eq_false distinct mem
+  DHashMap.Raw.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem
+    h.out k_beq not_mem distinct mem
 
 theorem getKey_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α} {k : α} (mem: k ∈ m) {h₃} :
     getKey (insertManyIfNewUnit m l) k h₃ = getKey m k mem :=
   DHashMap.Raw.Const.getKey_insertManyIfNewUnit_list_of_mem h.out mem
 
-theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {l : List α} {k : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
     getKey! (insertManyIfNewUnit m l) k = default :=
-  DHashMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    h.out contains_eq_false contains_eq_false'
+  DHashMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    h.out not_mem contains_eq_false
 
-theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     [Inhabited α] (h : m.WF) {l : List α} {k k' : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
     getKey! (insertManyIfNewUnit m l) k' = k :=
-  DHashMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    h.out k_beq contains_eq_false distinct mem
+  DHashMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem
+    h.out k_beq not_mem distinct mem
 
 theorem getKey!_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
     [Inhabited α] (h : m.WF) {l : List α} {k : α} (mem : k ∈ m) :
     getKey! (insertManyIfNewUnit m l) k = getKey! m k :=
   DHashMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_mem h.out mem
 
-theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
+theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k fallback : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
     getKeyD (insertManyIfNewUnit m l) k fallback = fallback :=
-  DHashMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    h.out contains_eq_false contains_eq_false'
+  DHashMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    h.out not_mem contains_eq_false
 
-theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α} {k k' fallback : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
     getKeyD (insertManyIfNewUnit m l) k' fallback = k :=
-  DHashMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    h.out k_beq contains_eq_false distinct mem
+  DHashMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem
+    h.out k_beq not_mem distinct mem
 
 theorem getKeyD_insertManyIfNewUnit_list_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α} {k fallback : α} (mem : k ∈ m) :
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index c5905415a923..b943edb2fec8 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -405,74 +405,74 @@ theorem mem_of_mem_insertMany_list [EquivBEq α] [LawfulHashable α]
     k ∈ insertMany m l → k ∈ m :=
   HashMap.mem_of_mem_insertManyIfNewUnit_list contains_eq_false
 
-theorem get?_insertMany_list_of_contains_eq_false_of_contains_eq_false
+theorem get?_insertMany_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] {l : List α} {k : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
     get? (insertMany m l) k = none :=
-  HashMap.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    contains_eq_false contains_eq_false'
+  HashMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    not_mem contains_eq_false
 
-theorem get?_insertMany_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem get?_insertMany_list_of_not_mem_false_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k k' : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
     get? (insertMany m l) k' = some k :=
-  HashMap.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    k_beq contains_eq_false distinct mem
+  HashMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem
+    k_beq not_mem distinct mem
 
 theorem get?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} (mem : k ∈ m) :
     get? (insertMany m l) k = get? m k :=
   HashMap.getKey?_insertManyIfNewUnit_list_of_mem mem
 
-theorem get_insertMany_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem get_insertMany_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α}
     {k k' : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) {h} :
     get (insertMany m l) k' h = k :=
-  HashMap.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    k_beq contains_eq_false distinct mem
+  HashMap.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem
+    k_beq not_mem distinct mem
 
 theorem get_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} (mem : k ∈ m) {h} :
     get (insertMany m l) k h = get m k mem :=
   HashMap.getKey_insertManyIfNewUnit_list_of_mem mem
 
-theorem get!_insertMany_list_of_contains_eq_false_of_contains_eq_false
+theorem get!_insertMany_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
     get! (insertMany m l) k = default :=
-  HashMap.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    contains_eq_false contains_eq_false'
+  HashMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    not_mem contains_eq_false
 
-theorem get!_insertMany_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem get!_insertMany_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     [Inhabited α] {l : List α} {k k' : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
     get! (insertMany m l) k' = k :=
-  HashMap.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    k_beq contains_eq_false distinct mem
+  HashMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem
+    k_beq not_mem distinct mem
 
 theorem get!_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
     [Inhabited α] {l : List α} {k : α} (mem : k ∈ m) :
     get! (insertMany m l) k = get! m k :=
   HashMap.getKey!_insertManyIfNewUnit_list_of_mem mem
 
-theorem getD_insertMany_list_of_contains_eq_false_of_contains_eq_false
+theorem getD_insertMany_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
     getD (insertMany m l) k fallback = fallback :=
-  HashMap.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    contains_eq_false contains_eq_false'
+  HashMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    not_mem contains_eq_false
 
-theorem getD_insertMany_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getD_insertMany_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k k' fallback : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l)  :
     getD (insertMany m l) k' fallback = k :=
-  HashMap.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    k_beq contains_eq_false distinct mem
+  HashMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem
+    k_beq not_mem distinct mem
 
 theorem getD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
     {l : List α} {k fallback : α} (mem : k ∈ m) :
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index 6ddd2fd99907..b527824e97c9 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -421,74 +421,74 @@ theorem mem_of_mem_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
     k ∈ insertMany m l → k ∈ m :=
   HashMap.Raw.mem_of_mem_insertManyIfNewUnit_list h.1 contains_eq_false
 
-theorem get?_insertMany_list_of_contains_eq_false_of_contains_eq_false
+theorem get?_insertMany_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
     get? (insertMany m l) k = none :=
-  HashMap.Raw.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    h.1 contains_eq_false contains_eq_false'
+  HashMap.Raw.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    h.1 not_mem contains_eq_false
 
-theorem get?_insertMany_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem get?_insertMany_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α} {k k' : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
     get? (insertMany m l) k' = some k :=
-  HashMap.Raw.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    h.1 k_beq contains_eq_false distinct mem
+  HashMap.Raw.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem
+    h.1 k_beq not_mem distinct mem
 
 theorem get?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α} {k : α} (mem : k ∈ m) :
     get? (insertMany m l) k = get? m k :=
   HashMap.Raw.getKey?_insertManyIfNewUnit_list_of_mem h.1 mem
 
-theorem get_insertMany_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem get_insertMany_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α}
     {k k' : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) {h'} :
     get (insertMany m l) k' h' = k :=
-  HashMap.Raw.getKey_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    h.1 k_beq contains_eq_false distinct mem
+  HashMap.Raw.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem
+    h.1 k_beq not_mem distinct mem
 
 theorem get_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α} {k : α} (mem : k ∈ m) {h₃} :
     get (insertMany m l) k h₃ = get m k mem :=
   HashMap.Raw.getKey_insertManyIfNewUnit_list_of_mem h.1 mem
 
-theorem get!_insertMany_list_of_contains_eq_false_of_contains_eq_false
+theorem get!_insertMany_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.WF) {l : List α} {k : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
     get! (insertMany m l) k = default :=
-  HashMap.Raw.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    h.1 contains_eq_false contains_eq_false'
+  HashMap.Raw.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    h.1 not_mem contains_eq_false
 
-theorem get!_insertMany_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem get!_insertMany_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     [Inhabited α] (h : m.WF) {l : List α} {k k' : α} (k_beq : k == k')
-    (contains_eq_false : contains m k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
     get! (insertMany m l) k' = k :=
-  HashMap.Raw.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    h.1 k_beq contains_eq_false distinct mem
+  HashMap.Raw.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem
+    h.1 k_beq not_mem distinct mem
 
 theorem get!_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
     [Inhabited α] (h : m.WF) {l : List α} {k : α} (mem : k ∈ m) :
     get! (insertMany m l) k = get! m k :=
   HashMap.Raw.getKey!_insertManyIfNewUnit_list_of_mem h.1 mem
 
-theorem getD_insertMany_list_of_contains_eq_false_of_contains_eq_false
+theorem getD_insertMany_list_of_not_mem_of_contains_eq_false
     [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k fallback : α}
-    (contains_eq_false : m.contains k = false) (contains_eq_false' : l.contains k = false) :
+    (not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
     getD (insertMany m l) k fallback = fallback :=
-  HashMap.Raw.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
-    h.1 contains_eq_false contains_eq_false'
+  HashMap.Raw.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
+    h.1 not_mem contains_eq_false
 
-theorem getD_insertMany_list_of_contains_eq_false_of_mem [EquivBEq α] [LawfulHashable α]
+theorem getD_insertMany_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α} {k k' fallback : α} (k_beq : k == k')
-    (contains_eq_false : m.contains k = false)
+    (not_mem : ¬ k ∈ m)
     (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
     getD (insertMany m l) k' fallback = k :=
-  HashMap.Raw.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem
-    h.1 k_beq contains_eq_false distinct mem
+  HashMap.Raw.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem
+    h.1 k_beq not_mem distinct mem
 
 theorem getD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List α} {k fallback : α} (mem : k ∈ m) :