diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean
index ec21672c5387..a428a23fd2da 100644
--- a/src/Std/Data/DHashMap/Internal/List/Associative.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean
@@ -2169,12 +2169,12 @@ theorem getKey!_insertList_of_mem [BEq α] [EquivBEq α] [Inhabited α]
 
 theorem getKeyD_insertList_of_contains_eq_false [BEq α] [EquivBEq α]
     {l toInsert : List ((a : α) × β a)} {k fallback : α}
-    (h : (toInsert.map Sigma.fst).contains k = false) :
+    (not_contains : (toInsert.map Sigma.fst).contains k = false) :
     getKeyD k (insertList l toInsert) fallback = getKeyD k l fallback := by
   rw [getKeyD_eq_getKey?]
   rw [getKey?_insertList_of_contains_eq_false]
   . rw [getKeyD_eq_getKey?]
-  . exact h
+  . exact not_contains
 
 theorem getKeyD_insertList_of_mem [BEq α] [EquivBEq α]
     {l toInsert : List ((a : α) × β a)}
@@ -2230,103 +2230,6 @@ theorem isEmpty_insertList [BEq α]
 section
 variable {β : Type v}
 
-theorem getValue?_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α]
-    {l toInsert : List ((_ : α) × β)} {k : α}
-    (not_contains : (toInsert.map Sigma.fst).contains k = false) :
-    getValue? k (insertList l toInsert) = getValue? k l := by
-  rw [← containsKey_eq_contains_map_fst] at not_contains
-  rw [getValue?_eq_getEntry?, getValue?_eq_getEntry?]
-  rw [getEntry?_insertList_of_contains_eq_false not_contains]
-
-theorem getValue?_insertList_of_mem [BEq α] [EquivBEq α]
-    {l toInsert : List ((_ : α) × β )}
-    {k k' : α} (k_beq : k == k') {v : β}
-    (distinct_l : DistinctKeys l)
-    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
-    (mem : ⟨k, v⟩ ∈ toInsert) :
-    getValue? k' (insertList l toInsert) = v := by
-  rw [getValue?_eq_getEntry?]
-  have : getEntry? k' (insertList l toInsert) = getEntry? k' toInsert := by
-    apply getEntry?_insertList_of_contains_eq_true distinct_l distinct_toInsert
-    apply containsKey_of_beq _ k_beq
-    exact containsKey_of_mem mem
-  rw [← DistinctKeys.def] at distinct_toInsert
-  rw [getEntry?_of_mem distinct_toInsert k_beq mem] at this
-  rw [this]
-  simp
-
-theorem getValue_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α]
-    {l toInsert : List ((_ : α) × β)} {k : α}
-    (h' : (toInsert.map Sigma.fst).contains k = false)
-    {h} :
-    getValue k (insertList l toInsert) h =
-    getValue k l (containsKey_of_containsKey_insertList h h') := by
-  rw [← Option.some_inj]
-  rw [← getValue?_eq_some_getValue]
-  rw [← getValue?_eq_some_getValue]
-  rw [getValue?_insertList_of_contains_eq_false]
-  exact h'
-
-theorem getValue_insertList_of_mem [BEq α] [EquivBEq α]
-    {l toInsert : List ((_ : α) × β)}
-    {k k' : α} (k_beq : k == k') {v : β}
-    (distinct_l : DistinctKeys l)
-    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
-    (mem : ⟨k, v⟩ ∈ toInsert)
-    {h} :
-    getValue k' (insertList l toInsert) h = v := by
-  rw [← Option.some_inj]
-  rw [← getValue?_eq_some_getValue]
-  rw [getValue?_insertList_of_mem]
-  . exact k_beq
-  . exact distinct_l
-  . exact distinct_toInsert
-  . exact mem
-
-theorem getValue!_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α] [Inhabited β]
-    {l toInsert : List ((_ : α) × β)} {k : α}
-    (h : (toInsert.map Sigma.fst).contains k = false) :
-    getValue! k (insertList l toInsert) = getValue! k l := by
-  simp only [getValue!_eq_getValue?]
-  rw [getValue?_insertList_of_contains_eq_false]
-  exact h
-
-theorem getValue!_insertList_of_mem [BEq α] [EquivBEq α] [Inhabited β]
-    {l toInsert : List ((_ : α) × β)} {k k' : α} {v: β} (k_beq : k == k')
-    (distinct_l : DistinctKeys l)
-    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
-    (mem : ⟨k, v⟩ ∈ toInsert):
-    getValue! k' (insertList l toInsert) = v := by
-  simp only [getValue!_eq_getValue?]
-  rw [getValue?_insertList_of_mem]
-  · rw [Option.get!_some]
-  · exact k_beq
-  · exact distinct_l
-  . exact distinct_toInsert
-  . exact mem
-
-theorem getValueD_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α]
-    {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β}
-    (h : (toInsert.map Sigma.fst).contains k = false) :
-    getValueD k (insertList l toInsert) fallback = getValueD k l fallback := by
-  simp only [getValueD_eq_getValue?]
-  rw [getValue?_insertList_of_contains_eq_false]
-  exact h
-
-theorem getValueD_insertList_of_mem [BEq α] [EquivBEq α]
-    {l toInsert : List ((_ : α) × β)} {k k' : α} {v fallback: β} (k_beq : k == k')
-    (distinct_l : DistinctKeys l)
-    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
-    (mem : ⟨k, v⟩ ∈ toInsert):
-    getValueD k' (insertList l toInsert) fallback= v := by
-  simp only [getValueD_eq_getValue?]
-  rw [getValue?_insertList_of_mem]
-  · rw [Option.getD_some]
-  · exact k_beq
-  · exact distinct_l
-  . exact distinct_toInsert
-  . exact mem
-
 -- TODO: this should be unified with Mathlib...
 /-- Internal implementation detail of the hash map -/
 def Prod.toSigma_HashMapInternal (p : α × β) : ((_ : α) × β) := ⟨p.fst, p.snd⟩
@@ -2360,7 +2263,7 @@ theorem containsKey_of_containsKey_insertListConst [BEq α] [PartialEquivBEq α]
 
 theorem getKey?_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
-    (h : (toInsert.map Prod.fst).contains k = false) :
+    (not_contains : (toInsert.map Prod.fst).contains k = false) :
     getKey? k (insertListConst l toInsert) = getKey? k l := by
   unfold insertListConst
   apply getKey?_insertList_of_contains_eq_false
@@ -2383,15 +2286,15 @@ theorem getKey?_insertListConst_of_mem [BEq α] [EquivBEq α]
 
 theorem getKey_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
-    (h' : (toInsert.map Prod.fst).contains k = false)
+    (not_contains : (toInsert.map Prod.fst).contains k = false)
     {h} :
     getKey k (insertListConst l toInsert) h =
-      getKey k l (containsKey_of_containsKey_insertListConst h h') := by
+      getKey k l (containsKey_of_containsKey_insertListConst h not_contains) := by
     rw [← Option.some_inj]
     rw [← getKey?_eq_some_getKey]
     rw [getKey?_insertListConst_of_contains_eq_false]
     . rw [getKey?_eq_some_getKey]
-    . exact h'
+    . exact not_contains
 
 theorem getKey_insertListConst_of_mem [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
@@ -2411,12 +2314,12 @@ theorem getKey_insertListConst_of_mem [BEq α] [EquivBEq α]
 
 theorem getKey!_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α] [Inhabited α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
-    (h : (toInsert.map Prod.fst).contains k = false) :
+    (not_contains : (toInsert.map Prod.fst).contains k = false) :
     getKey! k (insertListConst l toInsert) = getKey! k l := by
   rw [getKey!_eq_getKey?]
   rw [getKey?_insertListConst_of_contains_eq_false]
   . rw [getKey!_eq_getKey?]
-  . exact h
+  . exact not_contains
 
 theorem getKey!_insertListConst_of_mem [BEq α] [EquivBEq α] [Inhabited α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
@@ -2435,12 +2338,12 @@ theorem getKey!_insertListConst_of_mem [BEq α] [EquivBEq α] [Inhabited α]
 
 theorem getKeyD_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k fallback : α}
-    (h : (toInsert.map Prod.fst).contains k = false) :
+    (not_contains : (toInsert.map Prod.fst).contains k = false) :
     getKeyD k (insertListConst l toInsert) fallback = getKeyD k l fallback := by
   rw [getKeyD_eq_getKey?]
   rw [getKey?_insertListConst_of_contains_eq_false]
   . rw [getKeyD_eq_getKey?]
-  . exact h
+  . exact not_contains
 
 theorem getKeyD_insertListConst_of_mem [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
@@ -2480,10 +2383,12 @@ theorem isEmpty_insertListConst [BEq α]
 
 theorem getValue?_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
-    (h : (toInsert.map Prod.fst).contains k = false) :
+    (not_contains : (toInsert.map Prod.fst).contains k = false) :
     getValue? k (insertListConst l toInsert) = getValue? k l := by
   unfold insertListConst
-  rw [getValue?_insertList_of_contains_eq_false]
+  rw [getValue?_eq_getEntry?, getValue?_eq_getEntry?]
+  rw [getEntry?_insertList_of_contains_eq_false]
+  rw [containsKey_eq_contains_map_fst]
   simpa
 
 theorem getValue?_insertListConst_of_mem [BEq α] [EquivBEq α]
@@ -2494,23 +2399,34 @@ theorem getValue?_insertListConst_of_mem [BEq α] [EquivBEq α]
     (mem : ⟨k, v⟩ ∈ toInsert) :
     getValue? k' (insertListConst l toInsert) = v := by
   unfold insertListConst
-  apply getValue?_insertList_of_mem (k_beq:=k_beq)
-  · exact distinct_l
-  · simpa [List.pairwise_map]
+  rw [getValue?_eq_getEntry?]
+  have : getEntry? k' (insertList l (toInsert.map Prod.toSigma_HashMapInternal)) = getEntry? k' (toInsert.map Prod.toSigma_HashMapInternal) := by
+    apply getEntry?_insertList_of_contains_eq_true distinct_l (by simpa [List.pairwise_map])
+    apply containsKey_of_beq _ k_beq
+    rw [containsKey_eq_contains_map_fst, List.map_map, Prod.fst_comp_toSigma_HashMapInternal, List.contains_iff_exists_mem_beq]
+    exists k
+    rw [List.mem_map]
+    constructor
+    . exists ⟨k, v⟩
+    . simp
+  rw [this]
+  rw [getEntry?_of_mem _ k_beq _]
+  . rfl
+  · simpa [DistinctKeys.def, List.pairwise_map]
   . simp only [List.mem_map]
     exists (k, v)
 
 theorem getValue_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
-    {h : (toInsert.map Prod.fst).contains k = false}
-    {h'} :
-    getValue k (insertListConst l toInsert) h' =
-    getValue k l (containsKey_of_containsKey_insertListConst h' h) := by
+    {not_contains : (toInsert.map Prod.fst).contains k = false}
+    {h} :
+    getValue k (insertListConst l toInsert) h =
+    getValue k l (containsKey_of_containsKey_insertListConst h not_contains) := by
   rw [← Option.some_inj]
   rw [← getValue?_eq_some_getValue]
   rw [← getValue?_eq_some_getValue]
   rw [getValue?_insertListConst_of_contains_eq_false]
-  exact h
+  exact not_contains
 
 theorem getValue_insertListConst_of_mem [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
@@ -2529,11 +2445,11 @@ theorem getValue_insertListConst_of_mem [BEq α] [EquivBEq α]
 
 theorem getValue!_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq α] [Inhabited β]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
-    (h : (toInsert.map Prod.fst).contains k = false) :
+    (not_contains : (toInsert.map Prod.fst).contains k = false) :
     getValue! k (insertListConst l toInsert) = getValue! k l := by
   simp only [getValue!_eq_getValue?]
   rw [getValue?_insertListConst_of_contains_eq_false]
-  exact h
+  exact not_contains
 
 theorem getValue!_insertListConst_of_mem [BEq α] [EquivBEq α] [Inhabited β]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v: β} (k_beq : k == k')
@@ -2551,11 +2467,11 @@ theorem getValue!_insertListConst_of_mem [BEq α] [EquivBEq α] [Inhabited β]
 
 theorem getValueD_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} {fallback : β}
-    (not_mem : (toInsert.map Prod.fst).contains k = false) :
+    (not_contains : (toInsert.map Prod.fst).contains k = false) :
     getValueD k (insertListConst l toInsert) fallback = getValueD k l fallback := by
   simp only [getValueD_eq_getValue?]
   rw [getValue?_insertListConst_of_contains_eq_false]
-  exact not_mem
+  exact not_contains
 
 theorem getValueD_insertListConst_of_mem [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v fallback: β} (k_beq : k == k')
@@ -2642,7 +2558,7 @@ theorem containsKey_of_containsKey_insertListIfNewUnit [BEq α] [PartialEquivBEq
 
 theorem getKey?_insertListIfNewUnit_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}
-    (not_mem : toInsert.contains k = false) :
+    (not_contains : toInsert.contains k = false) :
     getKey? k (insertListIfNewUnit l toInsert) = getKey? k l := by
   induction toInsert generalizing l with
   | nil => simp [insertListIfNewUnit]
@@ -2652,15 +2568,15 @@ theorem getKey?_insertListIfNewUnit_of_contains_eq_false [BEq α] [EquivBEq α]
     · rw [getKey?_insertEntryIfNew]
       split
       · rename_i hd_k
-        simp at not_mem
+        simp at not_contains
         exfalso
         rcases hd_k with ⟨h,_⟩
-        rcases not_mem with ⟨h',_⟩
+        rcases not_contains with ⟨h',_⟩
         rw [BEq.symm h] at h'
         simp at h'
       · rfl
-    · simp only [List.contains_cons, Bool.or_eq_false_iff] at not_mem
-      apply And.right not_mem
+    · simp only [List.contains_cons, Bool.or_eq_false_iff] at not_contains
+      apply And.right not_contains
 
 theorem getKey?_insertListIfNewUnit_of_mem_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
@@ -2742,15 +2658,15 @@ theorem getKey?_insertListIfNewUnit_of_contains_of_contains [BEq α] [EquivBEq 
 
 theorem getKey_insertListIfNewUnit_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}
-    {not_mem : toInsert.contains k = false}
+    {not_contains : toInsert.contains k = false}
     {h} :
     getKey k (insertListIfNewUnit l toInsert) h =
-      getKey k l (containsKey_of_containsKey_insertListIfNewUnit not_mem h) := by
+      getKey k l (containsKey_of_containsKey_insertListIfNewUnit not_contains h) := by
   rw [← Option.some_inj]
   rw [← getKey?_eq_some_getKey]
   rw [getKey?_insertListIfNewUnit_of_contains_eq_false]
   . rw [getKey?_eq_some_getKey]
-  . exact not_mem
+  . exact not_contains
 
 theorem getKey_insertListIfNewUnit_of_mem_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
@@ -2784,18 +2700,18 @@ theorem getKey_insertListIfNewUnit_of_contains_of_contains [BEq α] [EquivBEq α
 
 theorem getKey!_insertListIfNewUnit_of_contains_eq_false [BEq α] [EquivBEq α] [Inhabited α]
     {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}
-    (h : toInsert.contains k = false) :
+    (not_contains : toInsert.contains k = false) :
     getKey! k (insertListIfNewUnit l toInsert) = getKey! k l := by
   rw [getKey!_eq_getKey?]
   rw [getKey?_insertListIfNewUnit_of_contains_eq_false]
   . rw [getKey!_eq_getKey?]
-  . exact h
+  . exact not_contains
 
 theorem getKey!_insertListIfNewUnit_of_mem_of_contains_eq_false [BEq α] [EquivBEq α] [Inhabited α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
     {k k' : α} (k_beq : k == k')
     (distinct : toInsert.Pairwise (fun a b => (a == b) = false))
-    (mem : k ∈ toInsert) (h': containsKey k l = false) :
+    (mem : k ∈ toInsert) (h : containsKey k l = false) :
     getKey! k' (insertListIfNewUnit l toInsert) = k := by
   rw [getKey!_eq_getKey?]
   rw [getKey?_insertListIfNewUnit_of_mem_of_contains_eq_false]
@@ -2803,35 +2719,35 @@ theorem getKey!_insertListIfNewUnit_of_mem_of_contains_eq_false [BEq α] [EquivB
   . exact k_beq
   . exact distinct
   . exact mem
-  . exact h'
+  . exact h
 
 theorem getKey!_insertListIfNewUnit_of_contains_of_contains [BEq α] [EquivBEq α] [Inhabited α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
     {k : α}
     (distinct : toInsert.Pairwise (fun a b => (a == b) = false))
-    (mem : toInsert.contains k) (h' : containsKey k l = true) :
+    (mem : toInsert.contains k) (h : containsKey k l = true) :
     getKey! k (insertListIfNewUnit l toInsert) = getKey! k l  := by
   rw [getKey!_eq_getKey?]
   rw [getKey?_insertListIfNewUnit_of_contains_of_contains]
   . rw [getKey!_eq_getKey?]
   · exact distinct
   · exact mem
-  · exact h'
+  · exact h
 
 theorem getKeyD_insertListIfNewUnit_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α} {k fallback : α}
-    (h : toInsert.contains k = false) :
+    (not_contains : toInsert.contains k = false) :
     getKeyD k (insertListIfNewUnit l toInsert) fallback = getKeyD k l fallback := by
   rw [getKeyD_eq_getKey?]
   rw [getKey?_insertListIfNewUnit_of_contains_eq_false]
   . rw [getKeyD_eq_getKey?]
-  . exact h
+  . exact not_contains
 
 theorem getKeyD_insertListIfNewUnit_of_mem_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
     {k k' fallback : α} (k_beq : k == k')
     (distinct : toInsert.Pairwise (fun a b => (a == b) = false))
-    {mem : k ∈ toInsert } {h': containsKey k l = false} :
+    {mem : k ∈ toInsert } {h : containsKey k l = false} :
     getKeyD k' (insertListIfNewUnit l toInsert) fallback = k := by
   rw [getKeyD_eq_getKey?]
   rw [getKey?_insertListIfNewUnit_of_mem_of_contains_eq_false]
@@ -2839,7 +2755,7 @@ theorem getKeyD_insertListIfNewUnit_of_mem_of_contains_eq_false [BEq α] [EquivB
   . exact k_beq
   . exact distinct
   . exact mem
-  . exact h'
+  . exact h
 
 theorem getKeyD_insertListIfNewUnit_of_contains_of_contains [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index b896a45f63b0..a0c76f82347c 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -999,54 +999,6 @@ variable {β : Type v} (m : Raw₀ α (fun _ => β))
 
 namespace Const
 
-theorem get?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
-    {l : List ((_ : α) × β)} {k : α} (h : (l.map Sigma.fst).contains k = false) :
-    Const.get? (m.insertMany l).1 k = Const.get? m k := by
-  simp_to_model using getValue?_insertList_of_contains_eq_false
-
-theorem get?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
-    {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v : β} (mem : ⟨k, v⟩ ∈ l)
-    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
-    Const.get? (m.insertMany l).1 k' = v := by
-  simp_to_model using getValue?_insertList_of_mem
-
-theorem get_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
-    {l : List ((_ : α) × β)} {k : α}
-    (h₁ : (l.map Sigma.fst).contains k = false) {h'}:
-    Const.get (m.insertMany l).1 k h' =
-    Const.get m k (contains_of_contains_insertMany_list _ h h' h₁) := by
-  simp_to_model using getValue_insertList_of_contains_eq_false
-
-theorem get_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
-    {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v : β} (mem : ⟨k, v⟩ ∈ l)
-    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) {h'}:
-    Const.get (m.insertMany l).1 k' h' = v := by
-  simp_to_model using getValue_insertList_of_mem
-
-theorem get!_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
-    [Inhabited β] (h : m.1.WF) {l : List ((_ : α) × β)} {k : α}
-    (h' : (l.map Sigma.fst).contains k = false) :
-    Const.get! (m.insertMany l).1 k = Const.get! m k := by
-  simp_to_model using getValue!_insertList_of_contains_eq_false
-
-theorem get!_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF)
-    {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l)
-    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
-    Const.get! (m.insertMany l).1 k' = v := by
-  simp_to_model using getValue!_insertList_of_mem
-
-theorem getD_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
-    {l : List ((_ : α) × β)} {k : α} {fallback : β}
-    (h' : (l.map Sigma.fst).contains k = false) :
-    Const.getD (m.insertMany l).1 k fallback = Const.getD m k fallback := by
-  simp_to_model using getValueD_insertList_of_contains_eq_false
-
-theorem getD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
-    {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v fallback : β} (mem : ⟨k, v⟩ ∈ l)
-    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
-    Const.getD (m.insertMany l).1 k' fallback = v := by
-  simp_to_model using getValueD_insertList_of_mem
-
 @[simp]
 theorem insertMany_nil :
     insertMany m [] = m := by
@@ -1064,23 +1016,23 @@ theorem insertMany_cons {l : List (α × β)} {k : α} {v : β} :
   | nil => simp [insertListₘ]
   | cons hd tl => simp [insertListₘ]
 
-theorem contains_constInsertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k : α} :
     (Const.insertMany m l).1.contains k = (m.contains k || (l.map Prod.fst).contains k) := by
   simp_to_model using containsKey_insertListConst
 
-theorem contains_of_contains_constInsertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem contains_of_contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List ( α × β )} {k : α} :
     (insertMany m l).1.contains k → (l.map Prod.fst).contains k = false → m.contains k := by
   simp_to_model using containsKey_of_containsKey_insertListConst
 
-theorem getKey?_constInsertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem getKey?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k : α}
     (h' : (l.map Prod.fst).contains k = false) :
     (insertMany m l).1.getKey? k = m.getKey? k := by
   simp_to_model using getKey?_insertListConst_of_contains_eq_false
 
-theorem getKey?_constInsertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem getKey?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List  (α × β)}
     {k k' : α} (k_beq : k == k')
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
@@ -1088,15 +1040,15 @@ theorem getKey?_constInsertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h
     (insertMany m l).1.getKey? k' = some k := by
   simp_to_model using getKey?_insertListConst_of_mem
 
-theorem getKey_constInsertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem getKey_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k : α}
     {h₁ : (l.map Prod.fst).contains k = false}
     {h'} :
     (insertMany m l).1.getKey k h' =
-    m.getKey k (contains_of_contains_constInsertMany_list _ h h' h₁) := by
+    m.getKey k (contains_of_contains_insertMany_list _ h h' h₁) := by
   simp_to_model using getKey_insertListConst_of_contains_eq_false
 
-theorem getKey_constInsertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem getKey_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)}
     {k k' : α} (k_beq : k == k')
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
@@ -1105,13 +1057,13 @@ theorem getKey_constInsertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h
     (insertMany m l).1.getKey k' h' = k := by
   simp_to_model using getKey_insertListConst_of_mem
 
-theorem getKey!_constInsertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
+theorem getKey!_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
     (h : m.1.WF) {l : List (α × β)} {k : α}
     (h' : (l.map Prod.fst).contains k = false) :
     (insertMany m l).1.getKey! k = m.getKey! k := by
   simp_to_model using getKey!_insertListConst_of_contains_eq_false
 
-theorem getKey!_constInsertMany_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF)
+theorem getKey!_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF)
     {l : List (α × β)}
     {k k' : α} (k_beq : k == k')
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
@@ -1119,13 +1071,13 @@ theorem getKey!_constInsertMany_list_of_mem [EquivBEq α] [LawfulHashable α] [I
     (insertMany m l).1.getKey! k' = k := by
   simp_to_model using getKey!_insertListConst_of_mem
 
-theorem getKeyD_constInsertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem getKeyD_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k fallback : α}
     (h' : (l.map Prod.fst).contains k = false) :
     (insertMany m l).1.getKeyD k fallback = m.getKeyD k fallback := by
   simp_to_model using getKeyD_insertListConst_of_contains_eq_false
 
-theorem getKeyD_constInsertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem getKeyD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)}
     {k k' fallback : α} (k_beq : k == k')
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
@@ -1133,62 +1085,62 @@ theorem getKeyD_constInsertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h
     (insertMany m l).1.getKeyD k' fallback = k := by
   simp_to_model using getKeyD_insertListConst_of_mem
 
-theorem size_constInsertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)}
     {distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)} :
     (∀ (a : α), m.contains a → (l.map Prod.fst).contains a = false) →
     (insertMany m l).1.1.size = m.1.size + l.length := by
   simp_to_model using length_insertListConst
 
-theorem isEmpty_constInsertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} :
     (insertMany m l).1.1.isEmpty = (m.1.isEmpty && l.isEmpty) := by
   simp_to_model using isEmpty_insertListConst
 
-theorem get?_constInsertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem get?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k : α}
     (h' : (l.map Prod.fst).contains k = false) :
     get? (insertMany m l).1 k = get? m k := by
   simp_to_model using getValue?_insertListConst_of_contains_eq_false
 
-theorem get?_constInsertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem get?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l)
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
     get? (insertMany m l).1 k' = v := by
   simp_to_model using getValue?_insertListConst_of_mem
 
-theorem get_constInsertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem get_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k : α}
     (h₁ : (l.map Prod.fst).contains k = false)
     {h'}:
-    get (insertMany m l).1 k h' = get m k (contains_of_contains_constInsertMany_list _ h h' h₁) := by
+    get (insertMany m l).1 k h' = get m k (contains_of_contains_insertMany_list _ h h' h₁) := by
   simp_to_model using getValue_insertListConst_of_contains_eq_false
 
-theorem get_constInsertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem get_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l)
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) {h'}:
     get (insertMany m l).1 k' h' = v := by
   simp_to_model using getValue_insertListConst_of_mem
 
-theorem get!_constInsertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
+theorem get!_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     [Inhabited β]  (h : m.1.WF) {l : List (α × β)} {k : α}
     (h' : (l.map Prod.fst).contains k = false) :
     get! (insertMany m l).1 k = get! m k := by
   simp_to_model using getValue!_insertListConst_of_contains_eq_false
 
-theorem get!_constInsertMany_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF)
+theorem get!_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF)
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l)
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
     get! (insertMany m l).1 k' = v := by
   simp_to_model using getValue!_insertListConst_of_mem
 
-theorem getD_constInsertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem getD_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k : α} {fallback : β}
     (h' : (l.map Prod.fst).contains k = false) :
     getD (insertMany m l).1 k fallback = getD m k fallback := by
   simp_to_model using getValueD_insertListConst_of_contains_eq_false
 
-theorem getD_constInsertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem getD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k k' : α} (k_beq : k == k') {v fallback : β} (mem : ⟨k, v⟩ ∈ l)
     (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
     getD (insertMany m l).1 k' fallback = v := by