diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean
index 5cd62bae40d3..d52543f3d951 100644
--- a/src/Std/Data/DHashMap/Internal/List/Associative.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean
@@ -172,11 +172,11 @@ theorem getValueCast?_cons_self [BEq α] [LawfulBEq α] {l : List ((a : α) × 
     getValueCast? k (⟨k, v⟩ :: l) = some v := by
   rw [getValueCast?_cons_of_true BEq.refl, cast_eq]
 
-theorem getValueCast?_mem [BEq α] [LawfulBEq α]
+theorem getValueCast?_of_mem [BEq α] [LawfulBEq α]
     {l : List ((a : α) × β a)}
-    {k k' : α} {v : β k} {k_eq : k == k'} {mem : ⟨k,v⟩ ∈ l}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l} :
-    getValueCast? k' l = some (cast (by congr; apply LawfulBEq.eq_of_beq k_eq) v) := by
+    {k : α} (k' : α ) (v : β k) (k_beq : k == k') (mem : ⟨k, v⟩ ∈ l)
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l) :
+    getValueCast? k' l = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v) := by
   induction l with
   | nil => simp at mem
   | cons hd tl ih =>
@@ -185,25 +185,22 @@ theorem getValueCast?_mem [BEq α] [LawfulBEq α]
     cases mem with
     | inl mem =>
       rw [← mem]
-      simp [k_eq]
+      simp [k_beq]
     | inr mem =>
       have hd_k' : (hd.fst == k') = false := by
         simp only [beq_eq_false_iff_ne, ne_eq, pairwise_cons] at distinct
         simp only [beq_eq_false_iff_ne, ne_eq]
         rcases distinct with ⟨distinct, _⟩
-        specialize distinct ⟨k,v⟩ mem
+        specialize distinct ⟨k, v⟩ mem
         simp only at distinct
-        simp only [beq_iff_eq] at k_eq
-        rw [k_eq] at distinct
+        simp only [beq_iff_eq] at k_beq
+        rw [k_beq] at distinct
         apply distinct
       simp only [hd_k', Bool.false_eq_true, ↓reduceDIte]
       apply ih
       · exact mem
       · exact List.Pairwise.of_cons distinct
 
-
-
-
 theorem getValue?_eq_getValueCast? [BEq α] [LawfulBEq α] {β : Type v} {l : List ((_ : α) × β)}
     {a : α} : getValue? a l = getValueCast? a l := by
   induction l using assoc_induction <;> simp_all [getValueCast?_cons, getValue?_cons]
@@ -930,7 +927,8 @@ theorem containsKey_of_mem [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {
 theorem DistinctKeys.nil [BEq α] : DistinctKeys ([] : List ((a : α) × β a)) :=
   ⟨by simp⟩
 
-theorem DistinctKeys.def [BEq α] {l : List ((a : α) × β a)} : DistinctKeys l ↔ List.Pairwise (fun a b => (a.1 == b.1) = false) l :=
+theorem DistinctKeys.def [BEq α] {l : List ((a : α) × β a)} :
+    DistinctKeys l ↔ List.Pairwise (fun a b => (a.1 == b.1) = false) l :=
   ⟨fun h => by simpa [keys_eq_map, List.pairwise_map] using h.distinct,
   fun h => ⟨by simpa [keys_eq_map, List.pairwise_map] using h⟩⟩
 
@@ -960,7 +958,6 @@ theorem DistinctKeys.of_keys_eq [BEq α] {l : List ((a : α) × β a)} {l' : Lis
     (h : keys l = keys l') : DistinctKeys l → DistinctKeys l' :=
   distinctKeys_of_sublist_keys (h ▸ Sublist.refl _)
 
-
 theorem containsKey_iff_exists [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} :
     containsKey a l ↔ ∃ a' ∈ keys l, a == a' := by
   rw [containsKey_eq_keys_contains, List.contains_iff_exists_mem_beq]
@@ -1041,8 +1038,9 @@ theorem insertEntry_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β a
     (h : containsKey k l = false) : insertEntry k v l = ⟨k, v⟩ :: l := by
   simp [insertEntry, h]
 
-theorem insertEntry_of_containsKey_eq_false_perm [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k}
-    (h : containsKey k l = false) : Perm (insertEntry k v l) (⟨k,v⟩ :: l) := by
+theorem perm_insertEntry_of_containsKey_eq_false [BEq α]
+    {l : List ((a : α) × β a)} {k : α} {v : β k}
+    (h : containsKey k l = false) : Perm (insertEntry k v l) (⟨k, v⟩ :: l) := by
   cases l with
   | nil => simp
   | cons hd tl => simp [insertEntry, h]
@@ -1264,7 +1262,8 @@ theorem insertEntryIfNew_of_containsKey_eq_false [BEq α] {l : List ((a : α) ×
     {v : β k} (h : containsKey k l = false) : insertEntryIfNew k v l = ⟨k, v⟩ :: l := by
   simp_all [insertEntryIfNew]
 
-theorem DistinctKeys.insertEntryIfNew [BEq α] [PartialEquivBEq α] {k : α} {v : β k} {l : List ((a : α) × β a)} (h: DistinctKeys l):
+theorem DistinctKeys.insertEntryIfNew [BEq α] [PartialEquivBEq α] {k : α} {v : β k}
+    {l : List ((a : α) × β a)} (h: DistinctKeys l):
     DistinctKeys (insertEntryIfNew k v l) := by
   simp only [Std.DHashMap.Internal.List.insertEntryIfNew, cond_eq_if]
   split
@@ -1910,7 +1909,8 @@ def insertList [BEq α] (l toInsert : List ((a : α) × β a)) : List ((a : α)
   | .nil => l
   | .cons ⟨k, v⟩ toInsert => insertList (insertEntry k v l) toInsert
 
-theorem DistinctKeys.insertList [BEq α] [PartialEquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (h : DistinctKeys l₁) :
+theorem DistinctKeys.insertList [BEq α] [PartialEquivBEq α] {l₁ l₂ : List ((a : α) × β a)}
+    (h : DistinctKeys l₁) :
     DistinctKeys (insertList l₁ l₂) := by
   induction l₂ using assoc_induction generalizing l₁
   · simpa [insertList]
@@ -1918,8 +1918,9 @@ theorem DistinctKeys.insertList [BEq α] [PartialEquivBEq α] {l₁ l₂ : List
     rw [insertList.eq_def]
     exact ih h.insertEntry
 
-theorem insertList_perm_of_perm_first [BEq α] [EquivBEq α] {l1 l2 toInsert : List ((a : α) × β a)} (h : Perm l1 l2)
-    (distinct : DistinctKeys l1) : Perm (insertList l1 toInsert) (insertList l2 toInsert) := by
+theorem insertList_perm_of_perm_first [BEq α] [EquivBEq α] {l1 l2 toInsert : List ((a : α) × β a)}
+    (h : Perm l1 l2) (distinct : DistinctKeys l1) :
+    Perm (insertList l1 toInsert) (insertList l2 toInsert) := by
   induction toInsert generalizing l1 l2 with
   | nil => simp [insertList, h]
   | cons hd tl ih =>
@@ -1930,18 +1931,18 @@ theorem insertList_perm_of_perm_first [BEq α] [EquivBEq α] {l1 l2 toInsert : L
     exact h
     apply DistinctKeys.insertEntry distinct
 
-theorem insertList_cons_perm [BEq α] [EquivBEq α] (l₁ l₂ : List ((a : α) × β a))
-    (p : (a : α) × β a) (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys (p :: l₂)) :
+theorem insertList_cons_perm [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)}
+    {p : (a : α) × β a} (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys (p :: l₂)) :
     (insertList l₁ (p :: l₂)).Perm (insertEntry p.1 p.2 (insertList l₁ l₂)) := by
   induction l₂ generalizing p l₁
   · simp [insertList]
   · rename_i h t ih
     rw [insertList]
-    refine (ih _ _ hl₁.insertEntry hl₂.tail).trans
+    refine (ih hl₁.insertEntry hl₂.tail).trans
       ((insertEntry_of_perm hl₁.insertList
-        (ih _ _ hl₁ (distinctKeys_of_sublist (by simp) hl₂))).trans
+        (ih hl₁ (distinctKeys_of_sublist (by simp) hl₂))).trans
       (List.Perm.trans ?_ (insertEntry_of_perm hl₁.insertList.insertEntry
-        (ih _ _ hl₁ (distinctKeys_of_sublist (by simp) hl₂)).symm)))
+        (ih hl₁ (distinctKeys_of_sublist (by simp) hl₂)).symm)))
     apply getEntry?_ext hl₁.insertList.insertEntry.insertEntry
       hl₁.insertList.insertEntry.insertEntry (fun k => ?_)
     simp only [getEntry?_insertEntry]
@@ -1950,8 +1951,8 @@ theorem insertList_cons_perm [BEq α] [EquivBEq α] (l₁ l₂ : List ((a : α)
     have := List.rel_of_pairwise_cons hl₂ (List.mem_cons_self _ _)
     simp [BEq.trans hh (BEq.symm hp)] at this
 
-theorem containsKey_eq_contains_map_fst [BEq α] [PartialEquivBEq α] (l : List ((a : α) × β a)) (k : α) : containsKey k l =
-(l.map Sigma.fst).contains k := by
+theorem containsKey_eq_contains_map_fst [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
+    {k : α} : containsKey k l = (l.map Sigma.fst).contains k := by
   induction l with
   | nil => simp
   | cons hd tl ih =>
@@ -1959,8 +1960,9 @@ theorem containsKey_eq_contains_map_fst [BEq α] [PartialEquivBEq α] (l : List
     simp only [List.map_cons, List.contains_cons]
     rw [BEq.comm]
 
-theorem containsKey_insertList [BEq α] [PartialEquivBEq α] (l toInsert : List ((a : α) × β a)) (k : α) :
-    containsKey k (List.insertList l toInsert) = (containsKey k l || (toInsert.map Sigma.fst).contains k) := by
+theorem containsKey_insertList [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)}
+    {k : α} : containsKey k (List.insertList l toInsert) =
+    (containsKey k l || (toInsert.map Sigma.fst).contains k) := by
   induction toInsert generalizing l with
   | nil =>  simp only [insertList, List.map_nil, List.elem_nil, Bool.or_false]
   | cons hd tl ih =>
@@ -1977,32 +1979,33 @@ theorem containsKey_of_containsKey_insertList [BEq α] [PartialEquivBEq α]
     (h₂ : (toInsert.map Sigma.fst).contains k = false) : containsKey k l := by
   rw [containsKey_insertList, h₂] at h₁; simp at h₁; exact h₁
 
-theorem getValueCast?_insertList_not_mem [BEq α] [LawfulBEq α]
+theorem getValueCast?_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
     {l toInsert : List ((a : α) × β a)} {k : α}
-    {not_mem : (toInsert.map Sigma.fst).contains k = false} :
+    (not_contains : (toInsert.map Sigma.fst).contains k = false) :
     getValueCast? k (insertList l toInsert) = getValueCast? k l := by
-  rw [← containsKey_eq_contains_map_fst] at not_mem
+  rw [← containsKey_eq_contains_map_fst] at not_contains
   induction toInsert generalizing l with
   | nil => simp [insertList]
   | cons hd tl ih =>
-    rw [containsKey_cons, Bool.or_eq_false_iff] at not_mem
+    rw [containsKey_cons, Bool.or_eq_false_iff] at not_contains
     simp only [insertList]
-    rw [ih (And.right not_mem)]
+    rw [ih (And.right not_contains)]
     rw [getValueCast?_insertEntry]
-    simp [And.left not_mem]
+    simp [And.left not_contains]
 
-theorem getValueCast?_insertList_mem [BEq α] [LawfulBEq α]
+theorem getValueCast?_insertList_of_mem [BEq α] [LawfulBEq α]
     {l toInsert : List ((a : α) × β a)}
-    {k k' : α} {k_beq : k == k'} {v : β k}
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {distinct2 : DistinctKeys l}
-    {mem : ⟨k,v⟩ ∈ toInsert} :
-    getValueCast? k' (insertList l toInsert) = some (cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v) := by
+    {k k' : α} (k_beq : k == k') (v : β k)
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
+    (distinct2 : DistinctKeys l)
+    (mem : ⟨k, v⟩ ∈ toInsert) :
+    getValueCast? k' (insertList l toInsert) =
+    some (cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v) := by
   rw [← DistinctKeys.def] at distinct
   induction toInsert generalizing l with
   | nil => simp at mem
   | cons hd tl ih =>
-    rw [getValueCast?_of_perm distinct2.insertList (insertList_cons_perm l tl hd distinct2 distinct)]
+    rw [getValueCast?_of_perm distinct2.insertList (insertList_cons_perm distinct2 distinct)]
     rw [getValueCast?_insertEntry]
     rw [List.mem_cons] at mem
     cases mem with
@@ -2018,101 +2021,107 @@ theorem getValueCast?_insertList_mem [BEq α] [LawfulBEq α]
         . apply this; exact mem
         . simp [k_beq]
 
-theorem getValueCast_insertList_not_mem [BEq α] [LawfulBEq α]
+theorem getValueCast_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
     {l toInsert : List ((a : α) × β a)} {k : α}
-    {not_mem : (toInsert.map Sigma.fst).contains k = false}
+    (not_contains : (toInsert.map Sigma.fst).contains k = false)
     {h} :
-    getValueCast k (insertList l toInsert) h = getValueCast k l (containsKey_of_containsKey_insertList h not_mem) := by
+    getValueCast k (insertList l toInsert) h =
+    getValueCast k l (containsKey_of_containsKey_insertList h not_contains) := by
   rw [← Option.some_inj]
   rw [← getValueCast?_eq_some_getValueCast]
   rw [← getValueCast?_eq_some_getValueCast]
-  rw [getValueCast?_insertList_not_mem]
-  exact not_mem
+  rw [getValueCast?_insertList_of_contains_eq_false]
+  exact not_contains
 
-theorem getValueCast_insertList_mem [BEq α] [LawfulBEq α]
+theorem getValueCast_insertList_of_mem [BEq α] [LawfulBEq α]
     {l toInsert : List ((a : α) × β a)}
-    {k k' : α} {k_beq : k == k'} {v : β k}
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {distinct2 : DistinctKeys l}
-    {mem : ⟨k,v⟩ ∈ toInsert}
+    {k k' : α} (k_beq : k == k') (v : β k)
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
+    (distinct2 : DistinctKeys l)
+    (mem : ⟨k, v⟩ ∈ toInsert)
     {h} :
-    getValueCast k' (insertList l toInsert) h = cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v := by
+    getValueCast k' (insertList l toInsert) h =
+    cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v := by
   rw [← Option.some_inj]
   rw [← getValueCast?_eq_some_getValueCast]
-  rw [getValueCast?_insertList_mem]
+  rw [getValueCast?_insertList_of_mem]
   . exact k_beq
   . exact distinct
   . exact distinct2
   . exact mem
 
-theorem getValueCast!_insertList_not_mem [BEq α] [LawfulBEq α]
+theorem getValueCast!_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
     {l toInsert : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
-    {not_mem : (toInsert.map Sigma.fst).contains k = false} :
+    (not_contains : (toInsert.map Sigma.fst).contains k = false) :
     getValueCast! k (insertList l toInsert) = getValueCast! k l := by
-  rw [getValueCast!_eq_getValueCast?, getValueCast!_eq_getValueCast?, getValueCast?_insertList_not_mem]
-  exact not_mem
+  rw [getValueCast!_eq_getValueCast?, getValueCast!_eq_getValueCast?,
+    getValueCast?_insertList_of_contains_eq_false]
+  exact not_contains
 
-theorem getValueCast!_insertList_mem [BEq α] [LawfulBEq α]
+theorem getValueCast!_insertList_of_mem [BEq α] [LawfulBEq α]
     {l toInsert : List ((a : α) × β a)}
-    {k k' : α} {k_beq : k == k'} {v : β k} [Inhabited (β k')]
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {distinct2 : DistinctKeys l}
-    {mem : ⟨k,v⟩ ∈ toInsert} :
-    getValueCast! k' (insertList l toInsert) = cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v := by
-  rw [getValueCast!_eq_getValueCast?, getValueCast?_insertList_mem]
+    {k k' : α} (k_beq : k == k') (v : β k) [Inhabited (β k')]
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
+    (distinct2 : DistinctKeys l)
+    (mem : ⟨k, v⟩ ∈ toInsert) :
+    getValueCast! k' (insertList l toInsert) =
+    cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v := by
+  rw [getValueCast!_eq_getValueCast?, getValueCast?_insertList_of_mem]
   . rw [Option.get!_some]; exact k_beq
   . exact distinct
   . exact distinct2
   . exact mem
 
-theorem getValueCastD_insertList_not_mem [BEq α] [LawfulBEq α]
+theorem getValueCastD_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
     {l toInsert : List ((a : α) × β a)} {k : α} {fallback : β k}
-    {not_mem : (toInsert.map Sigma.fst).contains k = false} :
+    (not_mem : (toInsert.map Sigma.fst).contains k = false) :
     getValueCastD k (insertList l toInsert) fallback = getValueCastD k l fallback := by
-  rw [getValueCastD_eq_getValueCast?, getValueCastD_eq_getValueCast?, getValueCast?_insertList_not_mem]
+  rw [getValueCastD_eq_getValueCast?, getValueCastD_eq_getValueCast?,
+    getValueCast?_insertList_of_contains_eq_false]
   exact not_mem
 
-theorem getValueCastD_insertList_mem [BEq α] [LawfulBEq α]
+theorem getValueCastD_insertList_of_mem [BEq α] [LawfulBEq α]
     {l toInsert : List ((a : α) × β a)}
-    {k k' : α} {k_beq : k == k'} {v : β k} {fallback : β k'}
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {distinct2 : DistinctKeys l}
-    {mem : ⟨k,v⟩ ∈ toInsert} :
-    getValueCastD k' (insertList l toInsert) fallback = cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v := by
-  rw [getValueCastD_eq_getValueCast?, getValueCast?_insertList_mem]
+    {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'}
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
+    (distinct2 : DistinctKeys l)
+    (mem : ⟨k, v⟩ ∈ toInsert) :
+    getValueCastD k' (insertList l toInsert) fallback =
+    cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v := by
+  rw [getValueCastD_eq_getValueCast?, getValueCast?_insertList_of_mem]
   . rw [Option.getD_some]; exact k_beq
   . exact distinct
   . exact distinct2
   . exact mem
 
-theorem getKey?_insertList_not_mem [BEq α] [EquivBEq α]
+theorem getKey?_insertList_of_contains_eq_false [BEq α] [EquivBEq α]
     {l toInsert : List ((a : α) × β a)} {k : α}
-    {not_mem : (toInsert.map Sigma.fst).contains k = false} :
+    (not_contains : (toInsert.map Sigma.fst).contains k = false) :
     getKey? k (insertList l toInsert) = getKey? k l := by
-  rw [← containsKey_eq_contains_map_fst] at not_mem
+  rw [← containsKey_eq_contains_map_fst] at not_contains
   induction toInsert generalizing l with
   | nil => simp [insertList]
   | cons hd tl ih =>
     simp only [insertList]
     rw [ih]
     · rw [getKey?_insertEntry]
-      simp only [containsKey, Bool.or_eq_false_iff] at not_mem
-      simp [And.left not_mem]
-    · simp only [containsKey, Bool.or_eq_false_iff] at not_mem
-      apply And.right not_mem
+      simp only [containsKey, Bool.or_eq_false_iff] at not_contains
+      simp [And.left not_contains]
+    · simp only [containsKey, Bool.or_eq_false_iff] at not_contains
+      apply And.right not_contains
 
-theorem getKey?_insertList_mem [BEq α] [EquivBEq α]
+theorem getKey?_insertList_of_mem [BEq α] [EquivBEq α]
     {l toInsert : List ((a : α) × β a)}
-    {k k' : α} {k_beq : k == k'}
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {distinct2 : DistinctKeys l}
-    {mem : k ∈ (toInsert.map Sigma.fst)} :
+    {k k' : α} (k_beq : k == k')
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
+    (distinct2 : DistinctKeys l)
+    (mem : k ∈ (toInsert.map Sigma.fst)) :
     getKey? k' (insertList l toInsert) = some k := by
   rw [← DistinctKeys.def] at distinct
   induction toInsert generalizing l with
   | nil => simp at mem
   | cons hd tl ih =>
-    rw [getKey?_of_perm distinct2.insertList (insertList_cons_perm l tl hd distinct2 distinct)]
+    rw [getKey?_of_perm distinct2.insertList (insertList_cons_perm distinct2 distinct)]
     rw [getKey?_insertEntry]
     rw [List.map_cons, List.mem_cons] at mem
     cases mem with
@@ -2130,84 +2139,84 @@ theorem getKey?_insertList_mem [BEq α] [EquivBEq α]
         . apply this; exact pair_mem
         . rw [pair_eq]; exact k_beq
 
-theorem getKey_insertList_not_mem [BEq α] [EquivBEq α]
+theorem getKey_insertList_of_contains_eq_false [BEq α] [EquivBEq α]
     {l toInsert : List ((a : α) × β a)} {k : α}
-    {not_mem : (toInsert.map Sigma.fst).contains k = false}
+    (not_contains : (toInsert.map Sigma.fst).contains k = false)
     {h} :
     getKey k (insertList l toInsert) h =
-      getKey k l (containsKey_of_containsKey_insertList h not_mem) := by
+      getKey k l (containsKey_of_containsKey_insertList h not_contains) := by
   rw [← Option.some_inj]
   rw [← getKey?_eq_some_getKey]
-  rw [getKey?_insertList_not_mem]
+  rw [getKey?_insertList_of_contains_eq_false]
   . rw [getKey?_eq_some_getKey]
-  . exact not_mem
+  . exact not_contains
 
-theorem getKey_insertList_mem [BEq α] [EquivBEq α]
+theorem getKey_insertList_of_mem [BEq α] [EquivBEq α]
     {l toInsert : List ((a : α) × β a)}
-    {k k' : α} {k_beq : k == k'}
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {distinct2 : DistinctKeys l}
-    {mem : k ∈ (toInsert.map Sigma.fst)}
+    {k k' : α} (k_beq : k == k')
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
+    (distinct2 : DistinctKeys l)
+    (mem : k ∈ (toInsert.map Sigma.fst))
     {h} :
     getKey k' (insertList l toInsert) h = k := by
   rw [← Option.some_inj]
   rw [← getKey?_eq_some_getKey]
-  rw [getKey?_insertList_mem]
+  rw [getKey?_insertList_of_mem]
   . exact k_beq
   . exact distinct
   . exact distinct2
   . exact mem
 
-theorem getKey!_insertList_not_mem [BEq α] [EquivBEq α] [Inhabited α]
+theorem getKey!_insertList_of_contains_eq_false [BEq α] [EquivBEq α] [Inhabited α]
     {l toInsert : List ((a : α) × β a)} {k : α}
-    {not_mem : (toInsert.map Sigma.fst).contains k = false} :
+    (contains_false : (toInsert.map Sigma.fst).contains k = false) :
     getKey! k (insertList l toInsert) = getKey! k l := by
   rw [getKey!_eq_getKey?]
-  rw [getKey?_insertList_not_mem]
+  rw [getKey?_insertList_of_contains_eq_false]
   . rw [getKey!_eq_getKey?]
-  . exact not_mem
+  . exact contains_false
 
-theorem getKey!_insertList_mem [BEq α] [EquivBEq α] [Inhabited α]
+theorem getKey!_insertList_of_mem [BEq α] [EquivBEq α] [Inhabited α]
     {l toInsert : List ((a : α) × β a)}
-    {k k' : α} {k_beq : k == k'}
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {distinct2 : DistinctKeys l}
-    {mem : k ∈ (toInsert.map Sigma.fst)} :
+    {k k' : α} (k_beq : k == k')
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
+    (distinct2 : DistinctKeys l)
+    (mem : k ∈ (toInsert.map Sigma.fst)) :
     getKey! k' (insertList l toInsert) = k := by
   rw [getKey!_eq_getKey?]
-  rw [getKey?_insertList_mem]
+  rw [getKey?_insertList_of_mem]
   . rw [Option.get!_some]
   . exact k_beq
   . exact distinct
   . exact distinct2
   . exact mem
 
-theorem getKeyD_insertList_not_mem [BEq α] [EquivBEq α]
+theorem getKeyD_insertList_of_contains_eq_false [BEq α] [EquivBEq α]
     {l toInsert : List ((a : α) × β a)} {k fallback : α}
-    {not_mem : (toInsert.map Sigma.fst).contains k = false} :
+    (h : (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_not_mem]
+  rw [getKey?_insertList_of_contains_eq_false]
   . rw [getKeyD_eq_getKey?]
-  . exact not_mem
+  . exact h
 
-theorem getKeyD_insertList_mem [BEq α] [EquivBEq α]
+theorem getKeyD_insertList_of_mem [BEq α] [EquivBEq α]
     {l toInsert : List ((a : α) × β a)}
-    {k k' fallback : α} {k_beq : k == k'}
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {distinct2 : DistinctKeys l}
-    {mem : k ∈ (toInsert.map Sigma.fst)} :
+    {k k' fallback : α} (k_beq : k == k')
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
+    (distinct2 : DistinctKeys l)
+    (mem : k ∈ (toInsert.map Sigma.fst)) :
     getKeyD k' (insertList l toInsert) fallback = k := by
   rw [getKeyD_eq_getKey?]
-  rw [getKey?_insertList_mem]
+  rw [getKey?_insertList_of_mem]
   . rw [Option.getD_some]
   . exact k_beq
   . exact distinct
   . exact distinct2
   . exact mem
 
-theorem insertList_perm [BEq α] [ReflBEq α] [PartialEquivBEq α]
-    (l toInsert : List ((a : α) × β a))
+theorem perm_insertList [BEq α] [ReflBEq α] [PartialEquivBEq α]
+    {l toInsert : List ((a : α) × β a)}
     (distinct_l : DistinctKeys l)
     (distinct_toInsert : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert)
     (distinct_both : ∀ (a : α), ¬ (containsKey a l ∧ containsKey a toInsert)) :
@@ -2217,7 +2226,6 @@ theorem insertList_perm [BEq α] [ReflBEq α] [PartialEquivBEq α]
   | nil => simp only [insertList, List.append_nil, Perm.refl]
   | cons hd tl ih =>
     simp only [insertList]
-    specialize ih (insertEntry hd.fst hd.snd l)
     apply Perm.trans
     · apply ih
       · simp only [insertEntry]
@@ -2252,9 +2260,9 @@ theorem insertList_perm [BEq α] [ReflBEq α] [PartialEquivBEq α]
       apply Perm.symm
       apply List.perm_middle
 
-theorem insertList_length [BEq α] [EquivBEq α]
+theorem length_insertList [BEq α] [EquivBEq α]
     {l toInsert : List ((a : α) × β a)}
-    {distinct_l : DistinctKeys l}
+    (distinct_l : DistinctKeys l)
     (distinct_toInsert : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert)
     (distinct_both : ∀ (a : α), ¬ (containsKey a l ∧ (toInsert.map Sigma.fst).contains a)) :
     (insertList l toInsert).length = l.length + toInsert.length := by
@@ -2272,6 +2280,7 @@ theorem insertList_length [BEq α] [EquivBEq α]
         specialize distinct_both h
         simp [containsKey] at distinct_both
       · rw [Nat.add_assoc, Nat.add_comm 1 _]
+    · apply DistinctKeys.insertEntry distinct_l
     · apply DistinctKeys.tail distinct_toInsert
     · intro a
       specialize distinct_both a
@@ -2296,19 +2305,18 @@ theorem insertList_length [BEq α] [EquivBEq α]
         simp only [Bool.true_eq_false] at left
       | inr h =>
         apply And.right (distinct_both h)
-    · apply DistinctKeys.insertEntry distinct_l
 
 
-theorem insertList_not_isEmpty_if_start_not_isEmpty [BEq α]
+theorem isEmpty_insertList_eq_false_of_isEmpty_eq_false [BEq α]
     {l toInsert : List ((a : α) × β a)}
-    {h : l.isEmpty = false} :
+    (h : l.isEmpty = false) :
     (List.insertList l toInsert).isEmpty = false := by
   induction toInsert generalizing l with
   | nil => simp [insertList, h]
   | cons hd tl ih =>
     simp [insertList, ih]
 
-theorem insertList_isEmpty [BEq α]
+theorem isEmpty_insertList [BEq α]
     {l toInsert : List ((a : α) × β a)} :
     (List.insertList l toInsert).isEmpty ↔ l.isEmpty ∧ toInsert.isEmpty := by
   induction toInsert with
@@ -2317,15 +2325,15 @@ theorem insertList_isEmpty [BEq α]
     simp only [insertList, List.isEmpty_cons, Bool.false_eq_true, and_false,
       iff_false]
     apply ne_true_of_eq_false
-    apply insertList_not_isEmpty_if_start_not_isEmpty
+    apply isEmpty_insertList_eq_false_of_isEmpty_eq_false
     simp
 
 section
 variable {β: Type v}
 
-theorem getValue?_insertList_not_mem [BEq α] [PartialEquivBEq α]
+theorem getValue?_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α]
     {l toInsert : List ((_ : α) × β)} {k : α}
-    {not_mem : (toInsert.map Sigma.fst).contains k = false} :
+    (h : (toInsert.map Sigma.fst).contains k = false) :
     getValue? k (insertList l toInsert) = getValue? k l := by
   induction toInsert generalizing l with
   | nil => simp [insertList]
@@ -2333,17 +2341,17 @@ theorem getValue?_insertList_not_mem [BEq α] [PartialEquivBEq α]
     simp only [insertList]
     rw [ih]
     · apply getValue?_insertEntry_of_false
-      simp only [List.map_cons, List.contains_cons, Bool.or_eq_false_iff] at not_mem
+      simp only [List.map_cons, List.contains_cons, Bool.or_eq_false_iff] at h
       apply BEq.symm_false
-      apply (And.left not_mem)
-    · simp only [List.map_cons, List.contains_cons, Bool.or_eq_false_iff] at not_mem
-      apply And.right not_mem
+      apply (And.left h)
+    · simp only [List.map_cons, List.contains_cons, Bool.or_eq_false_iff] at h
+      apply And.right h
 
-theorem getValue?_insertList_mem [BEq α] [PartialEquivBEq α]
+theorem getValue?_insertList_of_mem [BEq α] [PartialEquivBEq α]
     {l toInsert : List ((_ : α) × β )}
-    {k k' : α} {k_beq : k == k'} {v : β}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert}
-    {mem : ⟨k,v⟩ ∈ toInsert} :
+    {k k' : α} (k_beq : k == k') {v : β}
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert)
+    (mem : ⟨k, v⟩ ∈ toInsert) :
     getValue? k' (insertList l toInsert) = v := by
   induction toInsert generalizing l with
   | nil => simp at mem
@@ -2352,7 +2360,7 @@ theorem getValue?_insertList_mem [BEq α] [PartialEquivBEq α]
     simp only [List.mem_cons] at mem
     cases mem with
     | inl mem =>
-      rw [getValue?_insertList_not_mem]
+      rw [getValue?_insertList_of_contains_eq_false]
       simp only [← mem]
       · rw [getValue?_insertEntry_of_beq]
         exact k_beq
@@ -2376,61 +2384,64 @@ theorem getValue?_insertList_mem [BEq α] [PartialEquivBEq α]
         apply And.right distinct
       · exact mem
 
-theorem getValue!_insertList_not_mem [BEq α] [PartialEquivBEq α] [Inhabited β]
+theorem getValue!_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α] [Inhabited β]
     {l toInsert : List ((_ : α) × β)} {k : α}
-    {not_mem : (toInsert.map Sigma.fst).contains k = false} :
+    (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_not_mem]
-  exact not_mem
+  rw [getValue?_insertList_of_contains_eq_false]
+  exact h
 
-theorem getValue!_insertList_mem [BEq α] [PartialEquivBEq α] [Inhabited β]
-    {l toInsert : List ((_ : α) × β)} {k k' : α} {v: β} {k_eq : k == k'} {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert } {mem : ⟨k,v⟩ ∈ toInsert}:
+theorem getValue!_insertList_of_mem [BEq α] [PartialEquivBEq α] [Inhabited β]
+    {l toInsert : List ((_ : α) × β)} {k k' : α} {v: β} (k_beq : k == k')
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert):
     getValue! k' (insertList l toInsert) = v := by
   simp only [getValue!_eq_getValue?]
-  rw [getValue?_insertList_mem (mem:= mem)]
+  rw [getValue?_insertList_of_mem (mem:= mem)]
   · simp
-  · exact k_eq
+  · exact k_beq
   · exact distinct
 
-theorem getValueD_insertList_not_mem [BEq α] [PartialEquivBEq α]
+theorem getValueD_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α]
     {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β}
-    {not_mem : (toInsert.map Sigma.fst).contains k = false} :
+    (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_not_mem]
-  exact not_mem
+  rw [getValue?_insertList_of_contains_eq_false]
+  exact h
 
-theorem getValueD_insertList_mem [BEq α] [PartialEquivBEq α]
-    {l toInsert : List ((_ : α) × β)} {k k' : α} {v fallback: β} {k_eq : k == k'} {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert } {mem : ⟨k,v⟩ ∈ toInsert}:
+theorem getValueD_insertList_of_mem [BEq α] [PartialEquivBEq α]
+    {l toInsert : List ((_ : α) × β)} {k k' : α} {v fallback: β} (k_beq : k == k')
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert):
     getValueD k' (insertList l toInsert) fallback= v := by
   simp only [getValueD_eq_getValue?]
-  rw [getValue?_insertList_mem (mem:= mem)]
+  rw [getValue?_insertList_of_mem (mem:= mem)]
   · simp
-  · exact k_eq
+  · exact k_beq
   · exact distinct
 
-theorem getValue_insertList_not_mem [BEq α] [PartialEquivBEq α]
+theorem getValue_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α]
     {l toInsert : List ((_ : α) × β)} {k : α}
-    {not_mem : (toInsert.map Sigma.fst).contains k = false}
+    (h' : (toInsert.map Sigma.fst).contains k = false)
     {h} :
-    getValue k (insertList l toInsert) h = getValue k l (containsKey_of_containsKey_insertList h not_mem) := by
+    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_not_mem]
-  exact not_mem
+  rw [getValue?_insertList_of_contains_eq_false]
+  exact h'
 
-theorem getValue_insertList_mem [BEq α] [PartialEquivBEq α]
+theorem getValue_insertList_of_mem [BEq α] [PartialEquivBEq α]
     {l toInsert : List ((_ : α) × β)}
-    {k k' : α} {k_beq : k == k'} {v : β}
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {mem : ⟨k,v⟩ ∈ toInsert}
+    {k k' : α} (k_beq : k == k') {v : β}
+    (distinct : 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_mem (mem:=mem)]
+  rw [getValue?_insertList_of_mem (mem:=mem)]
   . exact k_beq
   . exact distinct
 
@@ -2448,30 +2459,38 @@ theorem insertListConst_eq_insertList [BEq α] {l : List ((_ : α) × β)} {toIn
       simp [insertList, insertListConst]
       apply ih
 
-theorem DistinctKeys.insertListConst [BEq α] [PartialEquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List (α × β)} (h : DistinctKeys l₁) :
+theorem DistinctKeys.insertListConst [BEq α] [PartialEquivBEq α] {l₁ : List ((_ : α) × β)}
+    {l₂ : List (α × β)} (h : DistinctKeys l₁) :
     DistinctKeys (insertListConst l₁ l₂) := by
   rw [insertListConst_eq_insertList]
   apply DistinctKeys.insertList h
 
-theorem insertListConst_perm_of_perm_first [BEq α] [EquivBEq α] (l1 l2: List ((_ : α) × β)) (toInsert : List (α × β)) (h : Perm l1 l2)
-    (distinct : DistinctKeys l1) : Perm (insertListConst l1 toInsert) (insertListConst l2 toInsert) := by
+theorem insertListConst_perm_of_perm_first [BEq α] [EquivBEq α] {l1 l2: List ((_ : α) × β)}
+    {toInsert : List (α × β)} (h : Perm l1 l2) (distinct : DistinctKeys l1) :
+    Perm (insertListConst l1 toInsert) (insertListConst l2 toInsert) := by
   simp only [insertListConst_eq_insertList]
   apply insertList_perm_of_perm_first h distinct
 
-theorem list_conversion_insertListConst {toInsert : List (α × β)}: (List.map Sigma.fst (List.map (fun a => (⟨a.fst, a.snd⟩ : (_ : α ) × β )) toInsert)) = (List.map Prod.fst toInsert) := by
+theorem list_conversion_insertListConst {toInsert : List (α × β)}:
+    (List.map Sigma.fst (List.map (fun a => (⟨a.fst, a.snd⟩ : (_ : α ) × β )) toInsert)) =
+    (List.map Prod.fst toInsert) := by
   apply List.ext_get
   · simp
   · intro n h1 h2
     simp
 
-theorem list_conversion_insertListConst_contains [BEq α] [PartialEquivBEq α] {toInsert : List (α × β)} {a : α}:
-    containsKey a (List.map (fun a => (⟨a.fst, a.snd⟩ : ((_ : α ) × β) )) toInsert) = true ↔ (toInsert.map Prod.fst).contains a = true := by
+theorem list_conversion_insertListConst_containsKey_true_iff [BEq α] [PartialEquivBEq α]
+    {toInsert : List (α × β)} {a : α}:
+    containsKey a (List.map (fun a => (⟨a.fst, a.snd⟩ : ((_ : α ) × β) )) toInsert) = true ↔
+    (toInsert.map Prod.fst).contains a = true := by
   rw [List.contains_iff_exists_mem_beq]
   rw [containsKey_iff_exists]
   simp only [keys_def, list_conversion_insertListConst]
 
-theorem pairwise_list_conversion_insertListConst [BEq α] {toInsert : List (α × β)} (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false) ):
-    List.Pairwise (fun a b => (a.1 == b.1) = false) (List.map (fun a => (⟨a.1, a.2⟩ : ((_ : α ) × β)) ) toInsert) := by
+theorem pairwise_list_conversion_insertListConst [BEq α] {toInsert : List (α × β)}
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false) ):
+    List.Pairwise (fun a b => (a.1 == b.1) = false)
+    (List.map (fun a => (⟨a.1, a.2⟩ : ((_ : α ) × β)) ) toInsert) := by
   induction toInsert with
   | nil => simp
   | cons hd tl ih =>
@@ -2488,87 +2507,91 @@ theorem pairwise_list_conversion_insertListConst [BEq α] {toInsert : List (α 
       apply left
     · apply ih right
 
-theorem containsKey_insertListConst [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} :
-    containsKey k (insertListConst l toInsert) = (containsKey k l || (toInsert.map Prod.fst).contains k) := by
+theorem containsKey_insertListConst [BEq α] [PartialEquivBEq α]
+    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} :
+    containsKey k (insertListConst l toInsert) =
+    (containsKey k l || (toInsert.map Prod.fst).contains k) := by
   rw [insertListConst_eq_insertList, containsKey_insertList,list_conversion_insertListConst]
 
-theorem containsKey_of_containsKey_insertListConst [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} (h₁ : containsKey k (insertListConst l toInsert))
+theorem containsKey_of_containsKey_insertListConst [BEq α] [PartialEquivBEq α]
+    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
+    (h₁ : containsKey k (insertListConst l toInsert))
     (h₂ : (toInsert.map Prod.fst).contains k = false) : containsKey k l := by
   rw [insertListConst_eq_insertList] at h₁
   apply containsKey_of_containsKey_insertList h₁
   rw [list_conversion_insertListConst]
   exact h₂
 
-theorem getKey?_insertListConst_not_mem [BEq α] [EquivBEq α]
+theorem getKey?_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
-    {not_mem : (toInsert.map Prod.fst).contains k = false} :
+    (h : (toInsert.map Prod.fst).contains k = false) :
     getKey? k (insertListConst l toInsert) = getKey? k l := by
   rw [insertListConst_eq_insertList]
-  apply getKey?_insertList_not_mem
+  apply getKey?_insertList_of_contains_eq_false
   rw [list_conversion_insertListConst]
-  exact not_mem
+  exact h
 
-theorem getKey?_insertListConst_mem [BEq α] [EquivBEq α]
+theorem getKey?_insertListConst_of_mem [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
-    {k k' : α} {k_beq : k == k'}
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {distinct2 : DistinctKeys l}
-    {mem : k ∈ (toInsert.map Prod.fst)} :
+    {k k' : α} (k_beq : k == k')
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
+    (distinct2 : DistinctKeys l)
+    (mem : k ∈ (toInsert.map Prod.fst)) :
     getKey? k' (insertListConst l toInsert) = some k := by
   rw [insertListConst_eq_insertList]
-  apply getKey?_insertList_mem
+  apply getKey?_insertList_of_mem
   · exact k_beq
   · apply pairwise_list_conversion_insertListConst distinct
   · exact distinct2
   · rw [list_conversion_insertListConst]
     assumption
 
-theorem getKey_insertListConst_not_mem [BEq α] [EquivBEq α]
+theorem getKey_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
-    {not_mem : (toInsert.map Prod.fst).contains k = false}
+    (h' : (toInsert.map Prod.fst).contains k = false)
     {h} :
     getKey k (insertListConst l toInsert) h =
-      getKey k l (containsKey_of_containsKey_insertListConst h not_mem) := by
+      getKey k l (containsKey_of_containsKey_insertListConst h h') := by
     rw [← Option.some_inj]
     rw [← getKey?_eq_some_getKey]
-    rw [getKey?_insertListConst_not_mem]
+    rw [getKey?_insertListConst_of_contains_eq_false]
     . rw [getKey?_eq_some_getKey]
-    . exact not_mem
+    . exact h'
 
-theorem getKey_insertListConst_mem [BEq α] [EquivBEq α]
+theorem getKey_insertListConst_of_mem [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
-    {k k' : α} {k_beq : k == k'}
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {distinct2 : DistinctKeys l}
-    {mem : k ∈ (toInsert.map Prod.fst)}
+    {k k' : α} (k_beq : k == k')
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
+    (distinct2 : DistinctKeys l)
+    (mem : k ∈ (toInsert.map Prod.fst))
     {h} :
     getKey k' (insertListConst l toInsert) h = k := by
   rw [← Option.some_inj]
   rw [← getKey?_eq_some_getKey]
-  rw [getKey?_insertListConst_mem]
+  rw [getKey?_insertListConst_of_mem]
   . exact k_beq
   . exact distinct
   . exact distinct2
   . exact mem
 
-theorem getKey!_insertListConst_not_mem [BEq α] [EquivBEq α] [Inhabited α]
+theorem getKey!_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α] [Inhabited α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
-    {not_mem : (toInsert.map Prod.fst).contains k = false} :
+    (h : (toInsert.map Prod.fst).contains k = false) :
     getKey! k (insertListConst l toInsert) = getKey! k l := by
   rw [insertListConst_eq_insertList]
-  apply getKey!_insertList_not_mem
+  apply getKey!_insertList_of_contains_eq_false
   rw [list_conversion_insertListConst]
-  exact not_mem
+  exact h
 
-theorem getKey!_insertListConst_mem [BEq α] [EquivBEq α] [Inhabited α]
+theorem getKey!_insertListConst_of_mem [BEq α] [EquivBEq α] [Inhabited α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
-    {k k' : α} {k_beq : k == k'}
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {distinct2 : DistinctKeys l}
-    {mem : k ∈ (toInsert.map Prod.fst)} :
+    {k k' : α} (k_beq : k == k')
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
+    (distinct2 : DistinctKeys l)
+    (mem : k ∈ (toInsert.map Prod.fst)) :
     getKey! k' (insertListConst l toInsert) = k := by
   rw [insertListConst_eq_insertList]
-  apply getKey!_insertList_mem
+  apply getKey!_insertList_of_mem
   · exact k_beq
   · apply pairwise_list_conversion_insertListConst
     exact distinct
@@ -2576,24 +2599,24 @@ theorem getKey!_insertListConst_mem [BEq α] [EquivBEq α] [Inhabited α]
   · rw [list_conversion_insertListConst]
     exact mem
 
-theorem getKeyD_insertListConst_not_mem [BEq α] [EquivBEq α]
+theorem getKeyD_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k fallback : α}
-    {not_mem : (toInsert.map Prod.fst).contains k = false} :
+    (h : (toInsert.map Prod.fst).contains k = false) :
     getKeyD k (insertListConst l toInsert) fallback = getKeyD k l fallback := by
   rw [insertListConst_eq_insertList]
-  apply getKeyD_insertList_not_mem
+  apply getKeyD_insertList_of_contains_eq_false
   rw [list_conversion_insertListConst]
-  exact not_mem
+  exact h
 
-theorem getKeyD_insertListConst_mem [BEq α] [EquivBEq α]
+theorem getKeyD_insertListConst_of_mem [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
-    {k k' fallback : α} {k_beq : k == k'}
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {distinct2 : DistinctKeys l}
-    {mem : k ∈ (toInsert.map Prod.fst)} :
+    {k k' fallback : α} (k_beq : k == k')
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
+    (distinct2 : DistinctKeys l)
+    (mem : k ∈ (toInsert.map Prod.fst)) :
     getKeyD k' (insertListConst l toInsert) fallback = k := by
   rw [insertListConst_eq_insertList]
-  apply getKeyD_insertList_mem
+  apply getKeyD_insertList_of_mem
   · exact k_beq
   · apply pairwise_list_conversion_insertListConst
     exact distinct
@@ -2601,15 +2624,16 @@ theorem getKeyD_insertListConst_mem [BEq α] [EquivBEq α]
   · rw [list_conversion_insertListConst]
     exact mem
 
-theorem insertListConst_length [BEq α] [EquivBEq α]
+theorem length_insertListConst [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
-    {distinct_l : DistinctKeys l}
+    (distinct_l : DistinctKeys l)
     (distinct_toInsert : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert)
     (distinct_both : ∀ (a : α), ¬ (containsKey a l ∧ (toInsert.map Prod.fst).contains a)) :
     (insertListConst l toInsert).length = l.length + toInsert.length := by
   rw [insertListConst_eq_insertList]
-  rw [insertList_length]
+  rw [length_insertList]
   · simp
+  · exact distinct_l
   · apply pairwise_list_conversion_insertListConst distinct_toInsert
   · intro a
     simp only [not_and, Bool.not_eq_true]
@@ -2624,113 +2648,117 @@ theorem insertListConst_length [BEq α] [EquivBEq α]
     simp only [List.any_map, List.any_eq_false, Function.comp_apply, Bool.not_eq_true,
       Prod.forall] at distinct_both
     apply distinct_both
-  · exact distinct_l
 
-theorem insertListConst_not_isEmpty_if_start_not_isEmpty [BEq α]
+theorem isEmpty_insertListConst_eq_false_of_isEmpty_eq_false [BEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
-    {h : l.isEmpty = false} :
+    (h : l.isEmpty = false) :
     (List.insertListConst l toInsert).isEmpty = false := by
   induction toInsert generalizing l with
   | nil => simp [insertListConst, h]
   | cons hd tl ih =>
     simp [insertListConst, ih]
 
-theorem insertListConst_isEmpty [BEq α]
+theorem isEmpty_insertListConst [BEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} :
     (List.insertListConst l toInsert).isEmpty ↔ l.isEmpty ∧ toInsert.isEmpty := by
   rw [insertListConst_eq_insertList]
-  rw [insertList_isEmpty]
+  rw [isEmpty_insertList]
   simp only [List.isEmpty_eq_true, List.map_eq_nil_iff]
 
-theorem getValue?_insertListConst_not_mem [BEq α] [PartialEquivBEq α]
+theorem getValue?_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
-    {not_mem : (toInsert.map Prod.fst).contains k = false} :
+    (h : (toInsert.map Prod.fst).contains k = false) :
     getValue? k (insertListConst l toInsert) = getValue? k l := by
   rw [insertListConst_eq_insertList]
-  rw [getValue?_insertList_not_mem]
+  rw [getValue?_insertList_of_contains_eq_false]
   rw [list_conversion_insertListConst]
-  exact not_mem
+  exact h
 
-theorem getValue?_insertListConst_mem [BEq α] [PartialEquivBEq α]
+theorem getValue?_insertListConst_of_mem [BEq α] [PartialEquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
-    {k k' : α} {k_beq : k == k'} {v : β}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert}
-    {mem : ⟨k,v⟩ ∈ toInsert} :
+    {k k' : α} (k_beq : k == k') {v : β}
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert)
+    (mem : ⟨k, v⟩ ∈ toInsert) :
     getValue? k' (insertListConst l toInsert) = v := by
   rw [insertListConst_eq_insertList]
-  apply getValue?_insertList_mem (k_beq:=k_beq)
+  apply getValue?_insertList_of_mem (k_beq:=k_beq)
   · apply pairwise_list_conversion_insertListConst distinct
   · simp only [List.mem_map, Prod.exists]
     exists k
     exists v
 
-theorem getValue!_insertListConst_not_mem [BEq α] [PartialEquivBEq α] [Inhabited β]
+theorem getValue!_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq α] [Inhabited β]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
-    {not_mem : (toInsert.map Prod.fst).contains k = false} :
+    (h : (toInsert.map Prod.fst).contains k = false) :
     getValue! k (insertListConst l toInsert) = getValue! k l := by
   rw [insertListConst_eq_insertList]
-  rw [getValue!_insertList_not_mem]
+  rw [getValue!_insertList_of_contains_eq_false]
   rw [list_conversion_insertListConst]
-  exact not_mem
+  exact h
 
-theorem getValue!_insertListConst_mem [BEq α] [PartialEquivBEq α] [Inhabited β]
-    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v: β} {k_eq : k == k'} {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert } {mem : ⟨k,v⟩ ∈ toInsert}:
+theorem getValue!_insertListConst_of_mem [BEq α] [PartialEquivBEq α] [Inhabited β]
+    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v: β} (k_beq : k == k')
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert):
     getValue! k' (insertListConst l toInsert) = v := by
-  rw [insertListConst_eq_insertList, getValue!_insertList_mem (k_eq:=k_eq)]
+  rw [insertListConst_eq_insertList, getValue!_insertList_of_mem (k_beq:=k_beq)]
   · apply pairwise_list_conversion_insertListConst distinct
   · simp only [List.mem_map, Prod.exists]
     exists k
     exists v
 
-theorem getValueD_insertListConst_not_mem [BEq α] [PartialEquivBEq α]
+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_mem : (toInsert.map Prod.fst).contains k = false) :
     getValueD k (insertListConst l toInsert) fallback = getValueD k l fallback := by
-  rw [insertListConst_eq_insertList, getValueD_insertList_not_mem]
+  rw [insertListConst_eq_insertList, getValueD_insertList_of_contains_eq_false]
   rw [list_conversion_insertListConst]
   exact not_mem
 
-theorem getValueD_insertListConst_mem [BEq α] [PartialEquivBEq α]
-    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v fallback: β} {k_eq : k == k'} {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert } {mem : ⟨k,v⟩ ∈ toInsert}:
+theorem getValueD_insertListConst_of_mem [BEq α] [PartialEquivBEq α]
+    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v fallback: β} (k_beq : k == k')
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) toInsert) (mem : ⟨k, v⟩ ∈ toInsert):
     getValueD k' (insertListConst l toInsert) fallback= v := by
-  rw [insertListConst_eq_insertList, getValueD_insertList_mem (k_eq:= k_eq)]
+  rw [insertListConst_eq_insertList, getValueD_insertList_of_mem (k_beq:= k_beq)]
   · apply pairwise_list_conversion_insertListConst distinct
   · simp
     exists k
     exists v
 
-theorem getValue_insertListConst_not_mem [BEq α] [PartialEquivBEq α]
+theorem getValue_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
-    {not_mem : (toInsert.map Prod.fst).contains k = false}
-    {h} :
-    getValue k (insertListConst l toInsert) h = getValue k l (containsKey_of_containsKey_insertListConst h not_mem) := by
+    {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
   rw [← Option.some_inj]
   rw [← getValue?_eq_some_getValue]
   rw [← getValue?_eq_some_getValue]
-  rw [getValue?_insertListConst_not_mem]
-  exact not_mem
+  rw [getValue?_insertListConst_of_contains_eq_false]
+  exact h
 
-theorem getValue_insertListConst_mem [BEq α] [PartialEquivBEq α]
+theorem getValue_insertListConst_of_mem [BEq α] [PartialEquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)}
-    {k k' : α} {k_beq : k == k'} {v : β}
-    {distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {mem : ⟨k,v⟩ ∈ toInsert}
+    {k k' : α} (k_beq : k == k') {v : β}
+    (distinct : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
+    (mem : ⟨k, v⟩ ∈ toInsert)
     {h} :
     getValue k' (insertListConst l toInsert) h = v := by
   rw [← Option.some_inj]
   rw [← getValue?_eq_some_getValue]
-  rw [getValue?_insertListConst_mem (mem:=mem)]
+  rw [getValue?_insertListConst_of_mem (mem:=mem)]
   . exact k_beq
   . exact distinct
 
 /-- Internal implementation detail of the hash map -/
-def insertListIfNewUnit [BEq α] (l: List ((_ : α) × Unit))(toInsert: List α) : List ((_ : α) × Unit) :=
+def insertListIfNewUnit [BEq α] (l: List ((_ : α) × Unit))(toInsert: List α) :
+    List ((_ : α) × Unit) :=
   match toInsert with
   | .nil => l
   | .cons hd tl => insertListIfNewUnit (insertEntryIfNew hd () l) tl
 
-theorem insertListIfNewUnit_perm_of_perm_first [BEq α] [EquivBEq α] {l1 l2 : List ((_ : α) × Unit)} {toInsert : List α } (h : Perm l1 l2)
-    (distinct : DistinctKeys l1) : Perm (insertListIfNewUnit l1 toInsert) (insertListIfNewUnit l2 toInsert) := by
+theorem insertListIfNewUnit_perm_of_perm_first [BEq α] [EquivBEq α] {l1 l2 : List ((_ : α) × Unit)}
+    {toInsert : List α } (h : Perm l1 l2) (distinct : DistinctKeys l1) :
+    Perm (insertListIfNewUnit l1 toInsert) (insertListIfNewUnit l2 toInsert) := by
   induction toInsert generalizing l1 l2 with
   | nil => simp [insertListIfNewUnit, h]
   | cons hd tl ih =>
@@ -2746,7 +2774,8 @@ theorem insertListIfNewUnit_perm_of_perm_first [BEq α] [EquivBEq α] {l1 l2 : L
         exact h
     · apply DistinctKeys.insertEntryIfNew distinct
 
-theorem DistinctKeys.insertListIfNewUnit [BEq α] [PartialEquivBEq α] (l : List ((_ : α) × Unit))(toInsert : List α) (distinct: DistinctKeys l):
+theorem DistinctKeys.insertListIfNewUnit [BEq α] [PartialEquivBEq α] (l : List ((_ : α) × Unit))
+    (toInsert : List α) (distinct: DistinctKeys l):
     DistinctKeys (insertListIfNewUnit l toInsert) := by
   induction toInsert generalizing l with
   | nil => simp [List.insertListIfNewUnit, distinct]
@@ -2756,7 +2785,8 @@ theorem DistinctKeys.insertListIfNewUnit [BEq α] [PartialEquivBEq α] (l : List
     apply insertEntryIfNew
     exact distinct
 
-theorem containsKey_insertListIfNewUnit [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} :
+theorem containsKey_insertListIfNewUnit [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)}
+    {toInsert : List α} {k : α} :
     containsKey k (insertListIfNewUnit l toInsert) = (containsKey k l || toInsert.contains k) := by
   induction toInsert generalizing l with
   | nil => simp [insertListIfNewUnit]
@@ -2765,8 +2795,20 @@ theorem containsKey_insertListIfNewUnit [BEq α] [PartialEquivBEq α] {l : List
     rw [ih, containsKey_insertEntryIfNew]
     rw [Bool.or_comm (hd == k), Bool.or_assoc, BEq.comm (a:=hd)]
 
+theorem containsKey_insertListIfNewUnit_iff [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)}
+    {toInsert : List α} {k : α} :
+    containsKey k (insertListIfNewUnit l toInsert) ↔ containsKey k l ∨ toInsert.contains k := by
+  induction toInsert generalizing l with
+  | nil => simp [insertListIfNewUnit]
+  | cons hd tl ih =>
+    simp only [insertListIfNewUnit, List.contains_cons]
+    rw [ih, containsKey_insertEntryIfNew]
+    simp only [Bool.or_eq_true]
+    rw [or_comm (a:= (hd == k)= true), or_assoc, BEq.comm]
+
 theorem containsKey_of_containsKey_insertListIfNewUnit [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}
-    (h₂ : toInsert.contains k = false) : containsKey k (insertListIfNewUnit l toInsert) →  containsKey k l := by
+    (h₂ : toInsert.contains k = false) : containsKey k (insertListIfNewUnit l toInsert) →
+    containsKey k l := by
   intro h₁
   rw [containsKey_insertListIfNewUnit] at h₁
   simp only [Bool.or_eq_true] at h₁
@@ -2775,9 +2817,9 @@ theorem containsKey_of_containsKey_insertListIfNewUnit [BEq α] [PartialEquivBEq
   | inr h =>
     simp only [h, Bool.true_eq_false] at h₂
 
-theorem getKey?_insertListIfNewUnit_not_mem [BEq α] [EquivBEq α]
+theorem getKey?_insertListIfNewUnit_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}
-    {not_mem : toInsert.contains k = false} :
+    (not_mem : toInsert.contains k = false) :
     getKey? k (insertListIfNewUnit l toInsert) = getKey? k l := by
   induction toInsert generalizing l with
   | nil => simp [insertListIfNewUnit]
@@ -2797,11 +2839,11 @@ theorem getKey?_insertListIfNewUnit_not_mem [BEq α] [EquivBEq α]
     · simp only [List.contains_cons, Bool.or_eq_false_iff] at not_mem
       apply And.right not_mem
 
-theorem getKey?_insertListIfNewUnit_mem [BEq α] [EquivBEq α]
+theorem getKey?_insertListIfNewUnit_of_mem_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
-    {k k' : α} {k_beq : k == k'}
-    {distinct : toInsert.Pairwise (fun a b => (a == b) = false)}
-    {mem : k ∈ toInsert} {mem' : containsKey k l = false}:
+    {k k' : α} (k_beq : k == k')
+    (distinct : toInsert.Pairwise (fun a b => (a == b) = false))
+    (mem : k ∈ toInsert) (mem' : containsKey k l = false) :
     getKey? k' (insertListIfNewUnit l toInsert) = some k := by
   induction toInsert generalizing l with
   | nil => simp at mem
@@ -2810,7 +2852,7 @@ theorem getKey?_insertListIfNewUnit_mem [BEq α] [EquivBEq α]
     simp only [List.mem_cons] at mem
     cases mem with
     | inl mem =>
-      rw [getKey?_insertListIfNewUnit_not_mem, ← mem]
+      rw [getKey?_insertListIfNewUnit_of_contains_eq_false, ← mem]
       · simp only [insertEntryIfNew, mem', cond_eq_if, Bool.false_eq_true, ↓reduceIte,
         getKey?_cons, ite_eq_left_iff, Bool.not_eq_true]
         intro h
@@ -2835,11 +2877,11 @@ theorem getKey?_insertListIfNewUnit_mem [BEq α] [EquivBEq α]
           apply (And.left distinct) k mem
         · exact mem'
 
-theorem getKey?_insertListIfNewUnit_mem_both [BEq α] [EquivBEq α]
+theorem getKey?_insertListIfNewUnit_of_mem_of_contains [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
     {k : α}
-    {distinct : toInsert.Pairwise (fun a b => (a == b) = false)}
-    {mem : toInsert.contains k} {mem' : containsKey k l = true}:
+    (distinct : toInsert.Pairwise (fun a b => (a == b) = false))
+    (mem : toInsert.contains k) (mem' : containsKey k l = true):
     getKey? k (insertListIfNewUnit l toInsert) = getKey? k l := by
   induction toInsert generalizing l with
   | nil => simp at mem
@@ -2848,7 +2890,7 @@ theorem getKey?_insertListIfNewUnit_mem_both [BEq α] [EquivBEq α]
     cases mem with
     | inl mem =>
       simp only [insertListIfNewUnit]
-      rw [getKey?_insertListIfNewUnit_not_mem, getKey?_insertEntryIfNew]
+      rw [getKey?_insertListIfNewUnit_of_contains_eq_false, getKey?_insertEntryIfNew]
       · simp only [BEq.symm mem, true_and, ite_eq_right_iff]
         have h':= containsKey_of_beq mem' mem
         intro h
@@ -2875,7 +2917,7 @@ theorem getKey?_insertListIfNewUnit_mem_both [BEq α] [EquivBEq α]
         right
         apply mem'
 
-theorem getKey_insertListIfNewUnit_not_mem [BEq α] [EquivBEq α]
+theorem getKey_insertListIfNewUnit_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}
     {not_mem : toInsert.contains k = false}
     {h} :
@@ -2883,115 +2925,115 @@ theorem getKey_insertListIfNewUnit_not_mem [BEq α] [EquivBEq α]
       getKey k l (containsKey_of_containsKey_insertListIfNewUnit not_mem h) := by
   rw [← Option.some_inj]
   rw [← getKey?_eq_some_getKey]
-  rw [getKey?_insertListIfNewUnit_not_mem]
+  rw [getKey?_insertListIfNewUnit_of_contains_eq_false]
   . rw [getKey?_eq_some_getKey]
   . exact not_mem
 
-theorem getKey_insertListIfNewUnit_mem [BEq α] [EquivBEq α]
+theorem getKey_insertListIfNewUnit_of_mem_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
-    {k k' : α} {k_beq : k == k'}
-    {distinct : toInsert.Pairwise (fun a b => (a == b) = false)}
-    {mem : k ∈ toInsert}
+    {k k' : α} (k_beq : k == k')
+    (distinct : toInsert.Pairwise (fun a b => (a == b) = false))
+    (mem : k ∈ toInsert)
     {h} : containsKey k l = false →
     getKey k' (insertListIfNewUnit l toInsert) h = k := by
   intro mem'
   rw [← Option.some_inj]
   rw [← getKey?_eq_some_getKey]
-  rw [getKey?_insertListIfNewUnit_mem]
+  rw [getKey?_insertListIfNewUnit_of_mem_of_contains_eq_false]
   . exact k_beq
   . exact distinct
   . exact mem
   . exact mem'
 
-theorem getKey_insertListIfNewUnit_mem_both [BEq α] [EquivBEq α]
+theorem getKey_insertListIfNewUnit_of_mem_of_contains [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
     {k : α}
-    {distinct : toInsert.Pairwise (fun a b => (a == b) = false)}
-    {mem : toInsert.contains k} {mem' : containsKey k l = true} {h}:
+    (distinct : toInsert.Pairwise (fun a b => (a == b) = false))
+    (mem : toInsert.contains k) (mem' : containsKey k l = true) {h}:
     getKey k (insertListIfNewUnit l toInsert) h = getKey k l mem' := by
   rw [← Option.some_inj]
   rw [← getKey?_eq_some_getKey]
   rw [← getKey?_eq_some_getKey]
-  rw [getKey?_insertListIfNewUnit_mem_both]
+  rw [getKey?_insertListIfNewUnit_of_mem_of_contains]
   · exact distinct
   · exact mem
   · exact mem'
 
-theorem getKey!_insertListIfNewUnit_not_mem [BEq α] [EquivBEq α] [Inhabited α]
+theorem getKey!_insertListIfNewUnit_of_contains_eq_false [BEq α] [EquivBEq α] [Inhabited α]
     {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}
-    {not_mem : toInsert.contains k = false} :
+    (h : toInsert.contains k = false) :
     getKey! k (insertListIfNewUnit l toInsert) = getKey! k l := by
   rw [getKey!_eq_getKey?]
-  rw [getKey?_insertListIfNewUnit_not_mem]
+  rw [getKey?_insertListIfNewUnit_of_contains_eq_false]
   . rw [getKey!_eq_getKey?]
-  . exact not_mem
+  . exact h
 
-theorem getKey!_insertListIfNewUnit_mem [BEq α] [EquivBEq α] [Inhabited α]
+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} {mem': containsKey k l = false} :
+    {k k' : α} (k_beq : k == k')
+    (distinct : toInsert.Pairwise (fun a b => (a == b) = false))
+    (mem : k ∈ toInsert) (h': containsKey k l = false) :
     getKey! k' (insertListIfNewUnit l toInsert) = k := by
   rw [getKey!_eq_getKey?]
-  rw [getKey?_insertListIfNewUnit_mem]
+  rw [getKey?_insertListIfNewUnit_of_mem_of_contains_eq_false]
   . rw [Option.get!_some]
   . exact k_beq
   . exact distinct
   . exact mem
-  . exact mem'
+  . exact h'
 
-theorem getKey!_insertListIfNewUnit_mem_both [BEq α] [EquivBEq α] [Inhabited α]
+theorem getKey!_insertListIfNewUnit_of_mem_of_contains [BEq α] [EquivBEq α] [Inhabited α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
     {k : α}
-    {distinct : toInsert.Pairwise (fun a b => (a == b) = false)}
-    {mem : toInsert.contains k} {mem' : containsKey k l = true} :
+    (distinct : toInsert.Pairwise (fun a b => (a == b) = false))
+    (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_mem_both]
+  rw [getKey?_insertListIfNewUnit_of_mem_of_contains]
   . rw [getKey!_eq_getKey?]
   · exact distinct
   · exact mem
-  · exact mem'
+  · exact h'
 
-theorem getKeyD_insertListIfNewUnit_not_mem [BEq α] [EquivBEq α]
+theorem getKeyD_insertListIfNewUnit_of_contains_eq_false [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α} {k fallback : α}
-    {not_mem : toInsert.contains k = false} :
+    (h : toInsert.contains k = false) :
     getKeyD k (insertListIfNewUnit l toInsert) fallback = getKeyD k l fallback := by
   rw [getKeyD_eq_getKey?]
-  rw [getKey?_insertListIfNewUnit_not_mem]
+  rw [getKey?_insertListIfNewUnit_of_contains_eq_false]
   . rw [getKeyD_eq_getKey?]
-  . exact not_mem
+  . exact h
 
-theorem getKeyD_insertListIfNewUnit_mem [BEq α] [EquivBEq α]
+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 } {mem': containsKey k l = false} :
+    {k k' fallback : α} (k_beq : k == k')
+    (distinct : toInsert.Pairwise (fun a b => (a == b) = false))
+    {mem : k ∈ toInsert } {h': containsKey k l = false} :
     getKeyD k' (insertListIfNewUnit l toInsert) fallback = k := by
   rw [getKeyD_eq_getKey?]
-  rw [getKey?_insertListIfNewUnit_mem]
+  rw [getKey?_insertListIfNewUnit_of_mem_of_contains_eq_false]
   . rw [Option.getD_some]
   . exact k_beq
   . exact distinct
   . exact mem
-  . exact mem'
+  . exact h'
 
-theorem getKeyD_insertListIfNewUnit_mem_both [BEq α] [EquivBEq α]
+theorem getKeyD_insertListIfNewUnit_of_mem_of_contains [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
     {k fallback : α}
-    {distinct : toInsert.Pairwise (fun a b => (a == b) = false)}
-    {mem : toInsert.contains k} {mem' : containsKey k l = true} :
+    (distinct : toInsert.Pairwise (fun a b => (a == b) = false))
+    (mem : toInsert.contains k) (mem' : containsKey k l = true) :
     getKeyD k (insertListIfNewUnit l toInsert) fallback = getKeyD k l fallback := by
   rw [getKeyD_eq_getKey?]
-  rw [getKey?_insertListIfNewUnit_mem_both]
+  rw [getKey?_insertListIfNewUnit_of_mem_of_contains]
   . rw [getKeyD_eq_getKey?]
   · exact distinct
   · exact mem
   · exact mem'
 
-theorem insertListIfNewUnit_length [BEq α] [EquivBEq α]
+theorem length_insertListIfNewUnit [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
-    {distinct_l : DistinctKeys l}
+    (distinct_l : DistinctKeys l)
     (distinct_toInsert : List.Pairwise (fun a b => (a == b) = false) toInsert)
     (distinct_both : ∀ (a : α), ¬ (containsKey a l ∧ toInsert.contains a)) :
     (insertListIfNewUnit l toInsert).length = l.length + toInsert.length := by
@@ -3006,6 +3048,7 @@ theorem insertListIfNewUnit_length [BEq α] [EquivBEq α]
         Bool.not_eq_true] at distinct_both
       simp only [distinct_both, Bool.false_eq_true, ↓reduceIte]
       rw [Nat.add_assoc, Nat.add_comm 1 _]
+    · apply DistinctKeys.insertEntryIfNew distinct_l
     · simp only [pairwise_cons] at distinct_toInsert
       apply And.right distinct_toInsert
     · intro a
@@ -3029,18 +3072,17 @@ theorem insertListIfNewUnit_length [BEq α] [EquivBEq α]
       | inr h =>
         specialize distinct_both a h
         apply And.right distinct_both
-    · apply DistinctKeys.insertEntryIfNew distinct_l
 
-theorem insertListIfNewUnit_not_isEmpty_if_start_not_isEmpty [BEq α]
+theorem isEmpty_insertListIfNewUnit_eq_false_of_isEmpty_eq_false [BEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
-    {h : l.isEmpty = false} :
+    (h : l.isEmpty = false) :
     (List.insertListIfNewUnit l toInsert).isEmpty = false := by
   induction toInsert generalizing l with
   | nil => simp [insertListIfNewUnit, h]
   | cons hd tl ih =>
     simp [insertListIfNewUnit, ih]
 
-theorem insertListIfNewUnit_isEmpty [BEq α]
+theorem isEmpty_insertListIfNewUnit [BEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α} :
     (List.insertListIfNewUnit l toInsert).isEmpty ↔ l.isEmpty ∧ toInsert.isEmpty := by
   induction toInsert with
@@ -3049,7 +3091,7 @@ theorem insertListIfNewUnit_isEmpty [BEq α]
     simp only [insertListIfNewUnit, List.isEmpty_cons, Bool.false_eq_true, and_false,
       iff_false]
     apply ne_true_of_eq_false
-    apply insertListIfNewUnit_not_isEmpty_if_start_not_isEmpty
+    apply isEmpty_insertListIfNewUnit_eq_false_of_isEmpty_eq_false
     simp
 
 theorem getValue?_list_unit [BEq α] {l : List ((_ : α) × Unit)} {k : α}:
@@ -3083,8 +3125,8 @@ theorem getValueD_list_unit [BEq α] {l : List ((_ : α) × Unit)} {k : α} {fal
 theorem getValue?_insertListIfNewUnit [BEq α] [PartialEquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}:
     getValue? k (insertListIfNewUnit l toInsert) =
-    if (containsKey k l || toInsert.contains k) then some () else none := by
-  simp [← containsKey_insertListIfNewUnit, getValue?_list_unit]
+    if containsKey k l ∨ toInsert.contains k then some () else none := by
+  simp [← containsKey_insertListIfNewUnit_iff, getValue?_list_unit]
 
 theorem getValue_insertListIfNewUnit [BEq α] [PartialEquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} {h}:
diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean
index b221595ae2ff..8b7eb32018a0 100644
--- a/src/Std/Data/DHashMap/Internal/Model.lean
+++ b/src/Std/Data/DHashMap/Internal/Model.lean
@@ -529,7 +529,7 @@ theorem Const.insertMany_eq_insertListₘ [BEq α] [Hashable α] (m : Raw₀ α
     simp only [List.foldl_cons,insertListₘ]
     apply ih
 
-theorem Const.insertManyIfNewUnit_eq_insertListIfNewUnit [BEq α] [Hashable α] (m : Raw₀ α (fun _ => Unit)) (l: List α):
+theorem Const.insertManyIfNewUnit_eq_insertListIfNewUnitₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => Unit)) (l: List α):
     (Const.insertManyIfNewUnit m l).1 = Const.insertListIfNewUnitₘ m l := by
   simp only [insertManyIfNewUnit, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl]
   suffices ∀ (t : { m' // ∀ (P : Raw₀ α (fun _ => Unit) → Prop),
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index fd574828cfec..cedc1b443c4a 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -70,9 +70,10 @@ variable [BEq α] [Hashable α]
 /-- Internal implementation detail of the hash map -/
 scoped macro "wf_trivial" : tactic => `(tactic|
   repeat (first
-    | apply Raw₀.wfImp_insert | apply Raw₀.wfImp_insertIfNew | apply Raw₀.wfImp_insertMany | apply Raw₀.Const.wfImp_insertMany| apply Raw₀.Const.wfImp_insertManyIfNewUnit | apply Raw₀.wfImp_erase
-    | apply Raw.WF.out | assumption | apply Raw₀.wfImp_empty | apply Raw.WFImp.distinct
-    | apply Raw.WF.empty₀))
+    | apply Raw₀.wfImp_insert | apply Raw₀.wfImp_insertIfNew | apply Raw₀.wfImp_insertMany
+    | apply Raw₀.Const.wfImp_insertMany| apply Raw₀.Const.wfImp_insertManyIfNewUnit
+    | apply Raw₀.wfImp_erase | apply Raw.WF.out | assumption | apply Raw₀.wfImp_empty
+    | apply Raw.WFImp.distinct | apply Raw.WF.empty₀))
 
 /-- Internal implementation detail of the hash map -/
 scoped macro "empty" : tactic => `(tactic| { intros; simp_all [List.isEmpty_iff] } )
@@ -90,8 +91,9 @@ private def queryNames : Array Name :=
     ``Raw.pairwise_keys_iff_pairwise_keys]
 
 private def modifyNames : Array Name :=
-  #[``toListModel_insert, ``toListModel_erase, ``toListModel_insertIfNew, ``toListModel_insertMany_list,
-  ``Const.toListModel_insertMany_list, ``Const.toListModel_insertManyIfNewUnit_list]
+  #[``toListModel_insert, ``toListModel_erase, ``toListModel_insertIfNew,
+  ``toListModel_insertMany_list, ``Const.toListModel_insertMany_list,
+  ``Const.toListModel_insertManyIfNewUnit_list]
 
 private def congrNames : MacroM (Array (TSyntax `term)) := do
   return #[← `(_root_.List.Perm.isEmpty_eq), ← `(containsKey_of_perm),
@@ -841,381 +843,370 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
   simp_to_model using (Raw.WF.out h).distinct.distinct
 
 @[simp]
-theorem insertMany_list_nil :
+theorem insertMany_nil :
     m.insertMany [] = m := by
   simp [insertMany, Id.run]
 
 @[simp]
-theorem insertMany_list_singleton [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} :
-    m.insertMany [⟨k,v⟩] = m.insert k v := by
+theorem insertMany_list_singleton {k : α} {v : β k} :
+    m.insertMany [⟨k, v⟩] = m.insert k v := by
   simp [insertMany, Id.run]
 
-theorem insertMany_list_cons {l : List ((a : α) × (β a))} {k : α} {v : β k} :
-    (m.insertMany (⟨k,v⟩ :: l)).1 = ((m.insert k v).insertMany l).1 := by
+theorem insertMany_cons {l : List ((a : α) × β a)} {k : α} {v : β k} :
+    (m.insertMany (⟨k, v⟩ :: l)).1 = ((m.insert k v).insertMany l).1 := by
   simp only [insertMany_eq_insertListₘ]
   cases l with
   | nil => simp [insertListₘ]
   | cons hd tl => simp [insertListₘ]
 
-theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List ((a : α) × (β a))} {k : α} :
+theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {k : α} :
     (m.insertMany l).1.contains k = (m.contains k || (l.map Sigma.fst).contains k) := by
   simp_to_model using List.containsKey_insertList
 
-theorem contains_of_contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List ((a : α) × (β a))} {k : α} :
+theorem contains_of_contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {k : α} :
     (m.insertMany l).1.contains k → (l.map Sigma.fst).contains k = false → m.contains k := by
   simp_to_model using List.containsKey_of_containsKey_insertList
 
-theorem get?_insertMany_list_not_mem [LawfulBEq α]
-    {l : List ((a : α) × (β a))} {k : α}
-    {not_mem : (l.map (Sigma.fst)).contains k = false}
-    (h : m.1.WF) :
+theorem get?_insertMany_list_of_contains_eq_false [LawfulBEq α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {k : α}
+    (h' : (l.map (Sigma.fst)).contains k = false) :
     (m.insertMany l).1.get? k = m.get? k := by
-  simp_to_model using getValueCast?_insertList_not_mem
-
-theorem get?_insertMany_list_mem [LawfulBEq α]
-    {l : List ((a : α) × (β a))} {k k' : α} {k_eq : k == k'} {v : β k}
-    {distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {mem : ⟨k,v⟩ ∈ l}
-    (h : m.1.WF) :
-    (m.insertMany l).1.get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_eq) v) := by
-  simp_to_model using getValueCast?_insertList_mem
-
-theorem get_insertMany_list_not_mem [LawfulBEq α]
-    {l : List ((a : α) × (β a))} {k : α}
-    {not_mem : (l.map (Sigma.fst)).contains k = false}
-    {h'}
-    (h : m.1.WF) :
-    (m.insertMany l).1.get k h' = m.get k (contains_of_contains_insertMany_list _ h h' not_mem) := by
-  simp_to_model using getValueCast_insertList_not_mem
-
-theorem get_insertMany_list_mem [LawfulBEq α]
-    {l : List ((a : α) × (β a))} {k k' : α} {k_eq : k == k'} {v : β k}
-    {distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {mem : ⟨k,v⟩ ∈ l}
-    {h'}
-    (h : m.1.WF) :
-    (m.insertMany l).1.get k' h' = cast (by congr; apply LawfulBEq.eq_of_beq k_eq) v := by
-  simp_to_model using getValueCast_insertList_mem
-
-theorem get!_insertMany_list_not_mem [LawfulBEq α]
-    {l : List ((a : α) × (β a))} {k : α} [Inhabited (β k)]
-    {not_mem : (l.map (Sigma.fst)).contains k = false}
-    (h : m.1.WF) :
+  simp_to_model using getValueCast?_insertList_of_contains_eq_false
+
+theorem get?_insertMany_list_of_mem [LawfulBEq α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
+    (mem : ⟨k, v⟩ ∈ l) :
+    (m.insertMany l).1.get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v) := by
+  simp_to_model using getValueCast?_insertList_of_mem
+
+theorem get_insertMany_list_of_contains_eq_false [LawfulBEq α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {k : α}
+    (contains : (l.map (Sigma.fst)).contains k = false)
+    {h'} :
+    (m.insertMany l).1.get k h' =
+    m.get k (contains_of_contains_insertMany_list _ h h' contains) := by
+  simp_to_model using getValueCast_insertList_of_contains_eq_false
+
+theorem get_insertMany_list_of_mem [LawfulBEq α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
+    (mem : ⟨k, v⟩ ∈ l)
+    {h'} :
+    (m.insertMany l).1.get k' h' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by
+  simp_to_model using getValueCast_insertList_of_mem
+
+theorem get!_insertMany_list_of_contains_eq_false [LawfulBEq α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
+    (h' : (l.map (Sigma.fst)).contains k = false) :
     (m.insertMany l).1.get! k = m.get! k := by
-  simp_to_model using getValueCast!_insertList_not_mem
-
-theorem get!_insertMany_list_mem [LawfulBEq α]
-    {l : List ((a : α) × (β a))} {k k' : α} {k_eq : k == k'} {v : β k} [Inhabited (β k')]
-    {distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {mem : ⟨k,v⟩ ∈ l}
-    (h : m.1.WF) :
-    (m.insertMany l).1.get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_eq) v := by
-  simp_to_model using getValueCast!_insertList_mem
-
-theorem getD_insertMany_list_not_mem [LawfulBEq α]
-    {l : List ((a : α) × (β a))} {k : α} {fallback : β k}
-    {not_mem : (l.map (Sigma.fst)).contains k = false}
-    (h : m.1.WF) :
+  simp_to_model using getValueCast!_insertList_of_contains_eq_false
+
+theorem get!_insertMany_list_of_mem [LawfulBEq α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} [Inhabited (β k')]
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
+    (mem : ⟨k, v⟩ ∈ l) :
+    (m.insertMany l).1.get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by
+  simp_to_model using getValueCast!_insertList_of_mem
+
+theorem getD_insertMany_list_of_contains_eq_false [LawfulBEq α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {k : α} {fallback : β k}
+    (not_mem : (l.map (Sigma.fst)).contains k = false) :
     (m.insertMany l).1.getD k fallback = m.getD k fallback := by
-  simp_to_model using getValueCastD_insertList_not_mem
-
-theorem getD_insertMany_list_mem [LawfulBEq α]
-    {l : List ((a : α) × (β a))} {k k' : α} {k_eq : k == k'} {v : β k} {fallback : β k'}
-    {distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {mem : ⟨k,v⟩ ∈ l}
-    (h : m.1.WF) :
-    (m.insertMany l).1.getD k' fallback = cast (by congr; apply LawfulBEq.eq_of_beq k_eq) v := by
-  simp_to_model using getValueCastD_insertList_mem
-
-theorem getKey?_insertMany_list_not_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
-    {l : List ((a : α) × (β a))} {k : α}
-    {not_mem : (l.map Sigma.fst).contains k = false} :
+  simp_to_model using getValueCastD_insertList_of_contains_eq_false
+
+theorem getD_insertMany_list_of_mem [LawfulBEq α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'}
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
+    (mem : ⟨k, v⟩ ∈ l) :
+    (m.insertMany l).1.getD k' fallback = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v := by
+  simp_to_model using getValueCastD_insertList_of_mem
+
+theorem getKey?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {k : α}
+    (h : (l.map Sigma.fst).contains k = false) :
     (m.insertMany l).1.getKey? k = m.getKey? k := by
-  simp_to_model using List.getKey?_insertList_not_mem
+  simp_to_model using getKey?_insertList_of_contains_eq_false
 
-theorem getKey?_insertMany_list_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
-    {l : List ((a : α) × (β a))}
-    {k k' : α} {k_beq : k == k'}
-    {distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {mem : k ∈ (l.map Sigma.fst)} :
+theorem getKey?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List ((a : α) × β a)}
+    {k k' : α} (k_beq : k == k')
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
+    (mem : k ∈ (l.map Sigma.fst)) :
     (m.insertMany l).1.getKey? k' = some k := by
-  simp_to_model using List.getKey?_insertList_mem
+  simp_to_model using getKey?_insertList_of_mem
 
-theorem getKey_insertMany_list_not_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
-    {l : List ((a : α) × (β a))} {k : α}
-    {not_mem : (l.map Sigma.fst).contains k = false}
+theorem getKey_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {k : α}
+    (h₁ : (l.map Sigma.fst).contains k = false)
     {h'} :
-    (m.insertMany l).1.getKey k h' = m.getKey k (contains_of_contains_insertMany_list _ h h' not_mem) := by
-  simp_to_model using List.getKey_insertList_not_mem
-
-theorem getKey_insertMany_list_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
-    {l : List ((a : α) × (β a))}
-    {k k' : α} {k_beq : k == k'}
-    {distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {mem : k ∈ (l.map Sigma.fst)}
+    (m.insertMany l).1.getKey k h' =
+    m.getKey k (contains_of_contains_insertMany_list _ h h' h₁) := by
+  simp_to_model using getKey_insertList_of_contains_eq_false
+
+theorem getKey_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List ((a : α) × β a)}
+    {k k' : α} (k_beq : k == k')
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
+    (mem : k ∈ (l.map Sigma.fst))
     {h'} :
     (m.insertMany l).1.getKey k' h' = k := by
-  simp_to_model using List.getKey_insertList_mem
+  simp_to_model using getKey_insertList_of_mem
 
-theorem getKey!_insertMany_list_not_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF)
-    {l : List ((a : α) × (β a))} {k : α}
-    {not_mem : (l.map Sigma.fst).contains k = false} :
+theorem getKey!_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
+    (h : m.1.WF) {l : List ((a : α) × β a)} {k : α}
+    (h' : (l.map Sigma.fst).contains k = false) :
     (m.insertMany l).1.getKey! k = m.getKey! k := by
-  simp_to_model using List.getKey!_insertList_not_mem
+  simp_to_model using getKey!_insertList_of_contains_eq_false
 
-theorem getKey!_insertMany_list_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF)
-    {l : List ((a : α) × (β a))}
-    {k k' : α} {k_beq : k == k'}
-    {distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {mem : k ∈ (l.map Sigma.fst)} :
+theorem getKey!_insertMany_listof_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF)
+    {l : List ((a : α) × β a)}
+    {k k' : α} (k_beq : k == k')
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
+    (mem : k ∈ (l.map Sigma.fst)) :
     (m.insertMany l).1.getKey! k' = k := by
-  simp_to_model using List.getKey!_insertList_mem
+  simp_to_model using getKey!_insertList_of_mem
 
-theorem getKeyD_insertMany_list_not_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
-    {l : List ((a : α) × (β a))} {k fallback : α}
-    {not_mem : (l.map Sigma.fst).contains k = false} :
+theorem getKeyD_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {k fallback : α}
+    (h' : (l.map Sigma.fst).contains k = false) :
     (m.insertMany l).1.getKeyD k fallback = m.getKeyD k fallback := by
-  simp_to_model using List.getKeyD_insertList_not_mem
+  simp_to_model using getKeyD_insertList_of_contains_eq_false
 
-theorem getKeyD_insertMany_list_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
-    {l : List ((a : α) × (β a))}
-    {k k' fallback : α} {k_beq : k == k'}
-    {distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)}
-    {mem : k ∈ (l.map Sigma.fst)} :
+theorem getKeyD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List ((a : α) × β a)}
+    {k k' fallback : α} (k_beq : k == k')
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
+    (mem : k ∈ (l.map Sigma.fst)) :
     (m.insertMany l).1.getKeyD k' fallback = k := by
-  simp_to_model using List.getKeyD_insertList_mem
+  simp_to_model using getKeyD_insertList_of_mem
 
-theorem size_insertMany_list [EquivBEq α] [LawfulHashable α]
-    {l : List ((a : α) × (β a))}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l}
-    (h : m.1.WF) :
-    (∀ (a : α), ¬ (m.contains a = true ∧ (l.map Sigma.fst).contains a = true)) →
+theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l}:
+    (∀ (a : α), ¬ (m.contains a ∧ (l.map Sigma.fst).contains a)) →
     (m.insertMany l).1.1.size = m.1.size + l.length := by
-  simp_to_model using List.insertList_length
+  simp_to_model using length_insertList
 
-theorem insertMany_list_notEmpty_if_map_notEmpty [EquivBEq α] [LawfulHashable α]
-    {l : List ((a : α) × (β a))} (h : m.1.WF) :
+theorem isEmpty_insertMany_list_eq_false_of_isEmpty_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {l : List ((a : α) × β a)}:
     (m.1.isEmpty = false) → (m.insertMany l).1.1.isEmpty  = false := by
-  simp_to_model using List.insertList_not_isEmpty_if_start_not_isEmpty
+  simp_to_model using isEmpty_insertList_eq_false_of_isEmpty_eq_false
 
-theorem insertMany_list_isEmpty [EquivBEq α] [LawfulHashable α]
-    {l : List ((a : α) × (β a))} (h : m.1.WF) :
+theorem isEmpty_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List ((a : α) × β a)} :
     (m.insertMany l).1.1.isEmpty ↔ m.1.isEmpty ∧ l.isEmpty := by
-  simp_to_model using List.insertList_isEmpty
+  simp_to_model using isEmpty_insertList
 
 section
 variable {β: Type v} (m: Raw₀ α (fun _ => β))
 
-theorem get?_insertMany_list_not_mem_const [EquivBEq α] [LawfulHashable α]
-    {l : List ((_ : α) × β)} {k : α}
-    {not_mem : (l.map Sigma.fst).contains k = false}
-    (h : m.1.WF) :
+theorem get?_insertMany_list_of_contains_eq_false_const [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_not_mem
+  simp_to_model using getValue?_insertList_of_contains_eq_false
 
-theorem get?_insertMany_list_mem_const [EquivBEq α] [LawfulHashable α]
-    {l : List ((_ : α) × β)} {k k' : α} {k_eq:  k == k'} {v : β} {mem : ⟨k,v⟩ ∈ l}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l} (h : m.1.WF):
+theorem get?_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v : β} (mem : ⟨k, v⟩ ∈ l)
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) :
     Const.get? (m.insertMany l).1 k' = v := by
-  simp_to_model using getValue?_insertList_mem
+  simp_to_model using getValue?_insertList_of_mem
 
-theorem get_insertMany_list_not_mem_const [EquivBEq α] [LawfulHashable α]
+theorem get_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List ((_ : α) × β)} {k : α}
-    {not_mem : (l.map Sigma.fst).contains k = false}
-    (h : m.1.WF) {h'}:
-    Const.get (m.insertMany l).1 k h' = Const.get m k (contains_of_contains_insertMany_list _ h h' not_mem) := by
-  simp_to_model using getValue_insertList_not_mem
-
-theorem get_insertMany_list_mem_const [EquivBEq α] [LawfulHashable α]
-    {l : List ((_ : α) × β)} {k k' : α} {k_eq:  k == k'} {v : β} {mem : ⟨k,v⟩ ∈ l}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l} (h : m.1.WF) {h'}:
+    (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_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v : β} (mem : ⟨k, v⟩ ∈ l)
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) {h'}:
     Const.get (m.insertMany l).1 k' h' = v := by
-  simp_to_model using getValue_insertList_mem
+  simp_to_model using getValue_insertList_of_mem
 
-theorem get!_insertMany_list_not_mem_const [EquivBEq α] [LawfulHashable α] [Inhabited β]
-    {l : List ((_ : α) × β)} {k : α}
-    {not_mem : (l.map Sigma.fst).contains k = false}
-    (h : m.1.WF) :
+theorem get!_insertMany_list_of_contains_eq_false_const [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_not_mem
+  simp_to_model using getValue!_insertList_of_contains_eq_false
 
-theorem get!_insertMany_list_mem_const [EquivBEq α] [LawfulHashable α] [Inhabited β]
-    {l : List ((_ : α) × β)} {k k' : α} {k_eq:  k == k'} {v : β} {mem : ⟨k,v⟩ ∈ l}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l} (h : m.1.WF):
+theorem get!_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF)
+    {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l)
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) :
     Const.get! (m.insertMany l).1 k' = v := by
-  simp_to_model using getValue!_insertList_mem
+  simp_to_model using getValue!_insertList_of_mem
 
-theorem getD_insertMany_list_not_mem_const [EquivBEq α] [LawfulHashable α]
+theorem getD_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List ((_ : α) × β)} {k : α} {fallback : β}
-    {not_mem : (l.map Sigma.fst).contains k = false}
-    (h : m.1.WF) :
+    (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_not_mem
+  simp_to_model using getValueD_insertList_of_contains_eq_false
 
-theorem getD_insertMany_list_mem_const [EquivBEq α] [LawfulHashable α]
-    {l : List ((_ : α) × β)} {k k' : α} {k_eq:  k == k'} {v fallback: β} {mem : ⟨k,v⟩ ∈ l}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l} (h : m.1.WF):
+theorem getD_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List ((_ : α) × β)} {k k' : α} (k_beq : k == k') {v fallback: β} (mem: ⟨k, v⟩ ∈ l)
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) :
     Const.getD (m.insertMany l).1 k' fallback = v := by
-  simp_to_model using getValueD_insertList_mem
+  simp_to_model using getValueD_insertList_of_mem
 
 namespace Const
 @[simp]
-theorem insertMany_list_nil :
+theorem insertMany_nil :
     insertMany m [] = m := by
   simp [insertMany, Id.run]
 
 @[simp]
-theorem insertMany_list_singleton [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
-    insertMany m [⟨k,v⟩] = m.insert k v := by
+theorem insertMany_list_singleton {k : α} {v : β} :
+    insertMany m [⟨k, v⟩] = m.insert k v := by
   simp [insertMany, Id.run]
 
-theorem insertMany_list_cons {l : List (α × β)} {k : α} {v : β} :
-    (insertMany m (⟨k,v⟩ :: l)).1 = (insertMany (m.insert k v) l).1 := by
+theorem insertMany_cons {l : List (α × β)} {k : α} {v : β} :
+    (insertMany m (⟨k, v⟩ :: l)).1 = (insertMany (m.insert k v) l).1 := by
   simp only [insertMany_eq_insertListₘ]
   cases l with
   | nil => simp [insertListₘ]
   | cons hd tl => simp [insertListₘ]
 
-theorem contains_insertMany_list [EquivBEq α] [LawfulHashable α]  {l : List (α × β)} {k : α} (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 List.containsKey_insertListConst
+  simp_to_model using containsKey_insertListConst
 
-theorem contains_of_contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {l : List ( α × β )} {k : α} :
+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 List.containsKey_of_containsKey_insertListConst
+  simp_to_model using containsKey_of_containsKey_insertListConst
 
-theorem getKey?_insertMany_list_not_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem getKey?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k : α}
-    {not_mem : (l.map Prod.fst).contains k = false} :
+    (h' : (l.map Prod.fst).contains k = false) :
     (insertMany m l).1.getKey? k = m.getKey? k := by
-  simp_to_model using List.getKey?_insertListConst_not_mem
+  simp_to_model using getKey?_insertListConst_of_contains_eq_false
 
-theorem getKey?_insertMany_list_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)}
-    {mem : k ∈ (l.map Prod.fst)} :
+    {k k' : α} (k_beq : k == k')
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
+    (mem : k ∈ (l.map Prod.fst)) :
     (insertMany m l).1.getKey? k' = some k := by
-  simp_to_model using List.getKey?_insertListConst_mem
+  simp_to_model using getKey?_insertListConst_of_mem
 
-theorem getKey_insertMany_list_not_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem getKey_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k : α}
-    {not_mem : (l.map Prod.fst).contains k = false}
+    {h₁ : (l.map Prod.fst).contains k = false}
     {h'} :
-    (insertMany m l).1.getKey k h' = m.getKey k (contains_of_contains_insertMany_list _ h h' not_mem) := by
-  simp_to_model using List.getKey_insertListConst_not_mem
+    (insertMany m l).1.getKey k h' =
+    m.getKey k (contains_of_contains_insertMany_list _ h h' h₁) := by
+  simp_to_model using getKey_insertListConst_of_contains_eq_false
 
-theorem getKey_insertMany_list_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)}
-    {mem : k ∈ (l.map Prod.fst)}
+    {k k' : α} (k_beq : k == k')
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
+    (mem : k ∈ (l.map Prod.fst))
     {h'} :
     (insertMany m l).1.getKey k' h' = k := by
-  simp_to_model using List.getKey_insertListConst_mem
+  simp_to_model using getKey_insertListConst_of_mem
 
-theorem getKey!_insertMany_list_not_mem [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF)
-    {l : List (α × β)} {k : α}
-    {not_mem : (l.map Prod.fst).contains k = false} :
+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 List.getKey!_insertListConst_not_mem
+  simp_to_model using getKey!_insertListConst_of_contains_eq_false
 
-theorem getKey!_insertMany_list_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)}
-    {mem : k ∈ (l.map Prod.fst)} :
+    {k k' : α} (k_beq : k == k')
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
+    (mem : k ∈ (l.map Prod.fst)) :
     (insertMany m l).1.getKey! k' = k := by
-  simp_to_model using List.getKey!_insertListConst_mem
+  simp_to_model using getKey!_insertListConst_of_mem
 
-theorem getKeyD_insertMany_list_not_mem [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+theorem getKeyD_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k fallback : α}
-    {not_mem : (l.map Prod.fst).contains k = false} :
+    (h' : (l.map Prod.fst).contains k = false) :
     (insertMany m l).1.getKeyD k fallback = m.getKeyD k fallback := by
-  simp_to_model using List.getKeyD_insertListConst_not_mem
+  simp_to_model using getKeyD_insertListConst_of_contains_eq_false
 
-theorem getKeyD_insertMany_list_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)}
-    {mem : k ∈ (l.map Prod.fst)} :
+    {k k' fallback : α} (k_beq : k == k')
+    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
+    (mem : k ∈ (l.map Prod.fst)) :
     (insertMany m l).1.getKeyD k' fallback = k := by
-  simp_to_model using List.getKeyD_insertListConst_mem
+  simp_to_model using getKeyD_insertListConst_of_mem
 
-theorem size_insertMany_list [EquivBEq α] [LawfulHashable α]
+theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l}
-    (h : m.1.WF) :
-    (∀ (a : α), ¬ (m.contains a = true ∧ (l.map Prod.fst).contains a = true)) →
+    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false) l} :
+    (∀ (a : α), ¬ (m.contains a ∧ (l.map Prod.fst).contains a)) →
     (insertMany m l).1.1.size = m.1.size + l.length := by
-  simp_to_model using List.insertListConst_length
+  simp_to_model using length_insertListConst
 
-theorem insertMany_list_notEmpty_if_map_notEmpty [EquivBEq α] [LawfulHashable α]
-    {l : List (α × β)} (h : m.1.WF) :
+theorem isEmpty_insertMany_list_eq_false_of_isEmpty_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {l : List (α × β)} :
     (m.1.isEmpty = false) → (insertMany m l).1.1.isEmpty  = false := by
-  simp_to_model using List.insertListConst_not_isEmpty_if_start_not_isEmpty
+  simp_to_model using isEmpty_insertListConst_eq_false_of_isEmpty_eq_false
 
-theorem insertMany_list_isEmpty [EquivBEq α] [LawfulHashable α]
-    {l : List (α × β)} (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 List.insertListConst_isEmpty
+  simp_to_model using isEmpty_insertListConst
 
-theorem get?_insertMany_list_not_mem_const [EquivBEq α] [LawfulHashable α]
+theorem get?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k : α}
-    {not_mem : (l.map Prod.fst).contains k = false}
-    (h : m.1.WF) :
+    (h' : (l.map Prod.fst).contains k = false) :
     get? (insertMany m l).1 k = get? m k := by
-  simp_to_model using getValue?_insertListConst_not_mem
+  simp_to_model using getValue?_insertListConst_of_contains_eq_false
 
-theorem get?_insertMany_list_mem_const [EquivBEq α] [LawfulHashable α]
-    {l : List (α × β)} {k k' : α} {k_eq:  k == k'} {v : β} {mem : ⟨k,v⟩ ∈ l}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l} (h : m.1.WF):
+theorem get?_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l)
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) :
     get? (insertMany m l).1 k' = v := by
-  simp_to_model using getValue?_insertListConst_mem
+  simp_to_model using getValue?_insertListConst_of_mem
 
-theorem get_insertMany_list_not_mem_const [EquivBEq α] [LawfulHashable α]
+theorem get_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k : α}
-    {not_mem : (l.map Prod.fst).contains k = false}
-    (h : m.1.WF) {h'}:
-    get (insertMany m l).1 k h' = get m k (contains_of_contains_insertMany_list _ h h' not_mem) := by
-  simp_to_model using getValue_insertListConst_not_mem
-
-theorem get_insertMany_list_mem_const [EquivBEq α] [LawfulHashable α]
-    {l : List (α × β)} {k k' : α} {k_eq:  k == k'} {v : β} {mem : ⟨k,v⟩ ∈ l}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l} (h : m.1.WF) {h'}:
+    (h₁ : (l.map Prod.fst).contains k = false)
+    {h'}:
+    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_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l)
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) {h'}:
     get (insertMany m l).1 k' h' = v := by
-  simp_to_model using getValue_insertListConst_mem
+  simp_to_model using getValue_insertListConst_of_mem
 
-theorem get!_insertMany_list_not_mem_const [EquivBEq α] [LawfulHashable α] [Inhabited β]
-    {l : List (α × β)} {k : α}
-    {not_mem : (l.map Prod.fst).contains k = false}
-    (h : m.1.WF) :
+theorem get!_insertMany_list_of_contains_eq_false_const [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_not_mem
+  simp_to_model using getValue!_insertListConst_of_contains_eq_false
 
-theorem get!_insertMany_list_mem_const [EquivBEq α] [LawfulHashable α] [Inhabited β]
-    {l : List (α × β)} {k k' : α} {k_eq:  k == k'} {v : β} {mem : ⟨k,v⟩ ∈ l}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l} (h : m.1.WF):
+theorem get!_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF)
+    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v : β} (mem: ⟨k, v⟩ ∈ l)
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) :
     get! (insertMany m l).1 k' = v := by
-  simp_to_model using getValue!_insertListConst_mem
+  simp_to_model using getValue!_insertListConst_of_mem
 
-theorem getD_insertMany_list_not_mem_const [EquivBEq α] [LawfulHashable α]
+theorem getD_insertMany_list_of_contains_eq_false_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List (α × β)} {k : α} {fallback : β}
-    {not_mem : (l.map Prod.fst).contains k = false}
-    (h : m.1.WF) :
+    (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_not_mem
+  simp_to_model using getValueD_insertListConst_of_contains_eq_false
 
-theorem getD_insertMany_list_mem_const [EquivBEq α] [LawfulHashable α]
-    {l : List (α × β)} {k k' : α} {k_eq:  k == k'} {v fallback: β} {mem : ⟨k,v⟩ ∈ l}
-    {distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l} (h : m.1.WF):
+theorem getD_insertMany_list_of_mem_const [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List (α × β)} {k k' : α} (k_beq : k == k') {v fallback: β} (mem: ⟨k, v⟩ ∈ l)
+    (distinct : List.Pairwise (fun a b => (a.1 == b.1) = false ) l) :
     getD (insertMany m l).1 k' fallback = v := by
-  simp_to_model using getValueD_insertListConst_mem
+  simp_to_model using getValueD_insertListConst_of_mem
 
 variable (m: Raw₀ α (fun _ => Unit))
 
 @[simp]
-theorem insertManyIfNewUnit_list_nil :
+theorem insertManyIfNewUnit_nil :
     insertManyIfNewUnit m [] = m := by
   simp [insertManyIfNewUnit, Id.run]
 
@@ -1224,119 +1215,124 @@ theorem insertManyIfNewUnit_list_singleton [EquivBEq α] [LawfulHashable α] {k
     insertManyIfNewUnit m [k] = m.insertIfNew k () := by
   simp [insertManyIfNewUnit, Id.run]
 
-theorem contains_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (h : m.1.WF):
+theorem insertManyIfNewUnit_cons {l : List α} {k : α} :
+    (insertManyIfNewUnit m (k :: l)).1 = (insertManyIfNewUnit (m.insertIfNew k ()) l).1 := by
+  simp only [insertManyIfNewUnit_eq_insertListIfNewUnitₘ]
+  cases l with
+  | nil => simp [insertListIfNewUnitₘ]
+  | cons hd tl => simp [insertListIfNewUnitₘ]
+
+theorem contains_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List α} {k : α}:
     (insertManyIfNewUnit m l).1.contains k = (m.contains k || l.contains k) := by
   simp_to_model using containsKey_insertListIfNewUnit
 
-theorem contains_of_contains_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (h : m.1.WF)
-    (h₂ : l.contains k = false) : (insertManyIfNewUnit m l).1.contains k = true →  m.contains k := by
+theorem contains_of_contains_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List α} {k : α} (h₂ : l.contains k = false) :
+    (insertManyIfNewUnit m l).1.contains k →  m.contains k := by
   simp_to_model using containsKey_of_containsKey_insertListIfNewUnit
 
-theorem getKey?_insertManyIfNewUnit_list_not_mem [EquivBEq α] [LawfulHashable α]
-    {l : List α} {k : α}
-    {not_mem : l.contains k = false} (h : m.1.WF) :
+theorem getKey?_insertManyIfNewUnit_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {l : List α} {k : α} (h' : l.contains k = false) :
     getKey? (insertManyIfNewUnit m l).1 k = getKey? m k := by
-  simp_to_model using getKey?_insertListIfNewUnit_not_mem
-
-theorem getKey?_insertManyIfNewUnit_list_mem [EquivBEq α] [LawfulHashable α]
-    {l : List α} {k k' : α} {k_beq : k == k'}
-    {distinct : l.Pairwise (fun a b => (a == b) = false)}
-    {mem : k ∈ l} (h : m.1.WF) : m.contains k = false →
-    getKey? (insertManyIfNewUnit m l).1 k' = some k := by
-  simp_to_model using getKey?_insertListIfNewUnit_mem
-
-theorem getKey?_insertManyIfNewUnit_list_mem_both [EquivBEq α] [LawfulHashable α]
-    {l : List α} {k : α}
-    {distinct : l.Pairwise (fun a b => (a == b) = false)}
-    {mem : l.contains k} (h : m.1.WF):
-    m.contains k = true → getKey? (insertManyIfNewUnit m l).1 k = getKey? m k := by
-  simp_to_model using getKey?_insertListIfNewUnit_mem_both
-
-theorem getKey_insertManyIfNewUnit_list_not_mem [EquivBEq α] [LawfulHashable α]
-    {l : List α} {k : α}
-    {not_mem : l.contains k = false}
-    {h'} (h: m.1.WF):
+  simp_to_model using getKey?_insertListIfNewUnit_of_contains_eq_false
+
+theorem getKey?_insertManyIfNewUnit_list_of_mem_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {l : List α} {k k' : α} (k_beq : k == k')
+    (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
+    m.contains k = false → getKey? (insertManyIfNewUnit m l).1 k' = some k := by
+  simp_to_model using getKey?_insertListIfNewUnit_of_mem_of_contains_eq_false
+
+theorem getKey?_insertManyIfNewUnit_list_of_mem_of_contains [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {l : List α} {k : α}
+    (distinct : l.Pairwise (fun a b => (a == b) = false))
+    (h': l.contains k) :
+    m.contains k  → getKey? (insertManyIfNewUnit m l).1 k = getKey? m k := by
+  simp_to_model using getKey?_insertListIfNewUnit_of_mem_of_contains
+
+theorem getKey_insertManyIfNewUnit_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {l : List α} {k : α} (h₁ : l.contains k = false) {h'} :
     getKey (insertManyIfNewUnit m l).1 k h' =
-      getKey m k (contains_of_contains_insertManyIfNewUnit_list m h not_mem h') := by
-  simp_to_model using getKey_insertListIfNewUnit_not_mem
-
-theorem getKey_insertManyIfNewUnit_list_mem [EquivBEq α] [LawfulHashable α]
-    {l : List α}
-    {k k' : α} {k_beq : k == k'}
-    {distinct : l.Pairwise (fun a b => (a == b) = false)}
-    {mem : k ∈ l}{h'} (h: m.1.WF):
+      getKey m k (contains_of_contains_insertManyIfNewUnit_list m h h₁ h') := by
+  simp_to_model using getKey_insertListIfNewUnit_of_contains_eq_false
+
+theorem getKey_insertManyIfNewUnit_list_of_mem_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {l : List α}
+    {k k' : α} (k_beq : k == k')
+    (distinct : l.Pairwise (fun a b => (a == b) = false))
+    (mem : k ∈ l) {h'} :
     m.contains k  = false →
     getKey (insertManyIfNewUnit m l).1 k' h' = k := by
-  simp_to_model using getKey_insertListIfNewUnit_mem
+  simp_to_model using getKey_insertListIfNewUnit_of_mem_of_contains_eq_false
 
-theorem getKey_insertManyIfNewUnit_list_mem_both [EquivBEq α] [LawfulHashable α]
-    {l : List α} {k : α}
-    {distinct : l.Pairwise (fun a b => (a == b) = false)}
-    {mem : l.contains k} {mem' : m.contains k = true} {h'} (h : m.1.WF):
+theorem getKey_insertManyIfNewUnit_list_mem_of_mem_of_contains [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {l : List α} {k : α}
+    (distinct : l.Pairwise (fun a b => (a == b) = false))
+    (h': l.contains k) {mem' : m.contains k} {h'} :
     getKey (insertManyIfNewUnit m l).1 k h' = getKey m k mem' := by
-  simp_to_model using getKey_insertListIfNewUnit_mem_both
+  simp_to_model using getKey_insertListIfNewUnit_of_mem_of_contains
 
-theorem getKey!_insertManyIfNewUnit_list_not_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
-    {l : List α} {k : α}
-    {not_mem : l.contains k = false} (h : m.1.WF) :
+theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    [Inhabited α] (h : m.1.WF) {l : List α} {k : α}
+    (h' : l.contains k = false) :
     getKey! (insertManyIfNewUnit m l).1 k = getKey! m k := by
-  simp_to_model using getKey!_insertListIfNewUnit_not_mem
+  simp_to_model using getKey!_insertListIfNewUnit_of_contains_eq_false
 
-theorem getKey!_insertManyIfNewUnit_list_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
-    {l : List α} {k k' : α} {k_beq : k == k'}
-    {distinct : l.Pairwise (fun a b => (a == b) = false)}
-    {mem : k ∈ l} (h : m.1.WF) : contains m k = false →
+theorem getKey!_insertManyIfNewUnit_list_of_mem_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    [Inhabited α] (h : m.1.WF) {l : List α} {k k' : α} (k_beq : k == k')
+    (distinct : l.Pairwise (fun a b => (a == b) = false))
+    (mem : k ∈ l) : contains m k = false →
     getKey! (insertManyIfNewUnit m l).1 k' = k := by
-  simp_to_model using getKey!_insertListIfNewUnit_mem
+  simp_to_model using getKey!_insertListIfNewUnit_of_mem_of_contains_eq_false
 
-theorem getKey!_insertManyIfNewUnit_list_mem_both [EquivBEq α] [LawfulHashable α] [Inhabited α]
-    {l : List α} {k : α}
-    {distinct : l.Pairwise (fun a b => (a == b) = false)}
-    {mem : l.contains k} (h : m.1.WF) : m.contains k = true →
+theorem getKey!_insertManyIfNewUnit_list_mem_of_mem_of_contains [EquivBEq α] [LawfulHashable α]
+    [Inhabited α] (h : m.1.WF) {l : List α} {k : α}
+    (distinct : l.Pairwise (fun a b => (a == b) = false))
+    (h': l.contains k) : m.contains k →
     getKey! (insertManyIfNewUnit m l).1 k = getKey! m k  := by
-  simp_to_model using getKey!_insertListIfNewUnit_mem_both
+  simp_to_model using getKey!_insertListIfNewUnit_of_mem_of_contains
 
-theorem getKeyD_insertManyIfNewUnit_list_not_mem [EquivBEq α] [LawfulHashable α]
-    {l : List α} {k fallback : α}
-    {not_mem : l.contains k = false} (h : m.1.WF):
+theorem getKeyD_insertManyIfNewUnit_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {l : List α} {k fallback : α}
+    (h' : l.contains k = false):
     getKeyD (insertManyIfNewUnit m l).1 k fallback = getKeyD m k fallback := by
-  simp_to_model using getKeyD_insertListIfNewUnit_not_mem
+  simp_to_model using getKeyD_insertListIfNewUnit_of_contains_eq_false
 
-theorem getKeyD_insertManyIfNewUnit_list_mem [EquivBEq α] [LawfulHashable α]
-    {l : List α} {k k' fallback : α} {k_beq : k == k'}
-    {distinct : l.Pairwise (fun a b => (a == b) = false)}
-    {mem : k ∈ l } (h : m.1.WF) : m.contains k = false →
+theorem getKeyD_insertManyIfNewUnit_list_of_mem_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {l : List α} {k k' fallback : α} (k_beq : k == k')
+    (distinct : l.Pairwise (fun a b => (a == b) = false))
+    {mem : k ∈ l } : m.contains k = false →
     getKeyD (insertManyIfNewUnit m l).1 k' fallback = k := by
-  simp_to_model using getKeyD_insertListIfNewUnit_mem
+  simp_to_model using getKeyD_insertListIfNewUnit_of_mem_of_contains_eq_false
 
-theorem getKeyD_insertManyIfNewUnit_list_mem_both [EquivBEq α] [LawfulHashable α]
-    {l : List α} {k fallback : α}
-    {distinct : l.Pairwise (fun a b => (a == b) = false)}
-    {mem : l.contains k} (h : m.1.WF) : m.contains k = true →
+theorem getKeyD_insertManyIfNewUnit_list_of_mem_of_contains [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {l : List α} {k fallback : α}
+    (distinct : l.Pairwise (fun a b => (a == b) = false))
+    (h': l.contains k) : m.contains k →
     getKeyD (insertManyIfNewUnit m l).1 k fallback = getKeyD m k fallback := by
-  simp_to_model using getKeyD_insertListIfNewUnit_mem_both
+  simp_to_model using getKeyD_insertListIfNewUnit_of_mem_of_contains
 
-theorem insertManyIfNewUnit_list_length [EquivBEq α] [LawfulHashable α]
+theorem size_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
     {l : List α}
-    (distinct : List.Pairwise (fun a b => (a == b) = false) l)
-    (h : m.1.WF) : (∀ (a : α), ¬ (m.contains a = true ∧ l.contains a = true)) →
+    (distinct : List.Pairwise (fun a b => (a == b) = false) l):
+    (∀ (a : α), ¬ (m.contains a ∧ l.contains a)) →
     (insertManyIfNewUnit m l).1.1.size = m.1.size + l.length := by
-  simp_to_model using insertListIfNewUnit_length
+  simp_to_model using length_insertListIfNewUnit
 
-theorem insertManyIfNewUnit_list_not_isEmpty_if_start_not_isEmpty [EquivBEq α] [LawfulHashable α]
-    {l : List α} (h : m.1.WF) : m.1.isEmpty = false →
+theorem isEmpty_insertManyIfNewUnit_list_eq_false_of_isEmpty_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {l : List α} : m.1.isEmpty = false →
     (insertManyIfNewUnit m l).1.1.isEmpty = false := by
-  simp_to_model using insertListIfNewUnit_not_isEmpty_if_start_not_isEmpty
+  simp_to_model using isEmpty_insertListIfNewUnit_eq_false_of_isEmpty_eq_false
 
-theorem insertManyIfNewUnit_list_isEmpty [EquivBEq α] [LawfulHashable α]
-    {l : List α} (h : m.1.WF) :
+theorem isEmpty_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List α} :
     (insertManyIfNewUnit m l).1.1.isEmpty ↔ m.1.isEmpty ∧ l.isEmpty := by
-  simp_to_model using insertListIfNewUnit_isEmpty
+  simp_to_model using isEmpty_insertListIfNewUnit
 
-theorem get?_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α]
-    {l : List α} {k : α} (h : m.1.WF) :
+theorem get?_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {l : List α} {k : α} :
     get? (insertManyIfNewUnit m l).1 k =
-    if ( m.contains k || l.contains k) then some () else none := by
+    if m.contains k ∨ l.contains k then some () else none := by
   simp_to_model using getValue?_insertListIfNewUnit
 
 theorem getValue_insertManyIfNewUnit_list
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index e70b20fda488..97b135282e0e 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -707,7 +707,9 @@ theorem wfImp_filter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m
   exact wfImp_filterₘ h
 
 /-! # `insertListₘ` -/
-theorem wfImp_insertListₘ [BEq α] [Hashable α] [EquivBEq α][LawfulHashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.1) : Raw.WFImp (m.insertListₘ l).1 := by
+
+theorem wfImp_insertListₘ [BEq α] [Hashable α] [EquivBEq α][LawfulHashable α] {m : Raw₀ α β}
+    {l : List ((a : α) × β a)} (h : Raw.WFImp m.1) : Raw.WFImp (m.insertListₘ l).1 := by
   induction l generalizing m with
   | nil =>
     simp only [insertListₘ]
@@ -718,17 +720,18 @@ theorem wfImp_insertListₘ [BEq α] [Hashable α] [EquivBEq α][LawfulHashable
     apply wfImp_insert h
 
 theorem toListModel_insertListₘ [BEq α] [Hashable α] [EquivBEq α][LawfulHashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.1) :
-  Perm (toListModel (insertListₘ m l).1.buckets) (List.insertList (toListModel m.1.buckets) l) := by
-induction l generalizing m with
-| nil =>
-  simp[insertListₘ, List.insertList]
-| cons hd tl ih =>
-  simp only [insertListₘ, List.insertList]
-  apply Perm.trans
-  apply ih (wfImp_insert h)
-  apply List.insertList_perm_of_perm_first
-  apply toListModel_insert h
-  apply (wfImp_insert h).distinct
+    Perm (toListModel (insertListₘ m l).1.buckets) (List.insertList (toListModel m.1.buckets) l) := by
+  induction l generalizing m with
+  | nil =>
+    simp[insertListₘ, List.insertList]
+  | cons hd tl ih =>
+    simp only [insertListₘ, List.insertList]
+    apply Perm.trans
+    apply ih (wfImp_insert h)
+    apply List.insertList_perm_of_perm_first
+    apply toListModel_insert h
+    apply (wfImp_insert h).distinct
+
 end Raw₀
 
 namespace Raw
@@ -765,7 +768,9 @@ theorem toListModel_insertMany_list [BEq α] [Hashable α] [EquivBEq α] [Lawful
   exact h
 
 /-! # `Const.insertListₘ` -/
-theorem Const.toListModel_insertListₘ {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)}{l : List (α × β)} (h : Raw.WFImp m.1):
+
+theorem Const.toListModel_insertListₘ {β : Type v} [BEq α] [Hashable α] [EquivBEq α]
+    [LawfulHashable α] {m : Raw₀ α (fun _ => β)}{l : List (α × β)} (h : Raw.WFImp m.1):
     Perm (toListModel (Const.insertListₘ m l).1.buckets) (insertListConst (toListModel m.1.buckets) l) := by
   induction l generalizing m with
   | nil => simp [Const.insertListₘ, insertListConst]
@@ -778,7 +783,9 @@ theorem Const.toListModel_insertListₘ {β : Type v} [BEq α] [Hashable α] [Eq
     apply (wfImp_insert h).distinct
 
 /-! # `Const.insertMany` -/
-theorem Const.toListModel_insertMany_list {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)} {l : List (α × β)} (h : Raw.WFImp m.1):
+
+theorem Const.toListModel_insertMany_list {β : Type v} [BEq α] [Hashable α] [EquivBEq α]
+    [LawfulHashable α] {m : Raw₀ α (fun _ => β)} {l : List (α × β)} (h : Raw.WFImp m.1):
     Perm (toListModel (Const.insertMany m l).1.1.buckets) (insertListConst (toListModel m.1.buckets) l) := by
   rw [Const.insertMany_eq_insertListₘ]
   apply toListModel_insertListₘ h
@@ -789,8 +796,11 @@ theorem Const.wfImp_insertMany {β : Type v} [BEq α] [Hashable α] [EquivBEq α
   Raw.WF.out ((Const.insertMany m l).2 _ Raw.WF.insert₀ (.wf m.2 h))
 
 /-! # `Const.insertListIfNewUnitₘ` -/
-theorem Const.toListModel_insertListIfNewUnitₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α (fun _ => Unit)} {l : List α} (h : Raw.WFImp m.1):
-    Perm (toListModel (Const.insertListIfNewUnitₘ m l).1.buckets) (List.insertListIfNewUnit (toListModel m.1.buckets) l) := by
+
+theorem Const.toListModel_insertListIfNewUnitₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
+    {m : Raw₀ α (fun _ => Unit)} {l : List α} (h : Raw.WFImp m.1):
+    Perm (toListModel (Const.insertListIfNewUnitₘ m l).1.buckets)
+    (List.insertListIfNewUnit (toListModel m.1.buckets) l) := by
   induction l generalizing m with
   | nil => simp [insertListIfNewUnitₘ, List.insertListIfNewUnit]
   | cons hd tl ih =>
@@ -802,13 +812,16 @@ theorem Const.toListModel_insertListIfNewUnitₘ [BEq α] [Hashable α] [EquivBE
     apply (wfImp_insertIfNew h).distinct
 
 /-! # `Const.insertManyIfNewUnit` -/
-theorem Const.toListModel_insertManyIfNewUnit_list [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α (fun _ => Unit)} {l : List α} (h : Raw.WFImp m.1):
-    Perm (toListModel (Const.insertManyIfNewUnit m l).1.1.buckets) (List.insertListIfNewUnit (toListModel m.1.buckets) l) := by
-  rw [Const.insertManyIfNewUnit_eq_insertListIfNewUnit]
+
+theorem Const.toListModel_insertManyIfNewUnit_list [BEq α] [Hashable α] [EquivBEq α]
+    [LawfulHashable α] {m : Raw₀ α (fun _ => Unit)} {l : List α} (h : Raw.WFImp m.1):
+    Perm (toListModel (Const.insertManyIfNewUnit m l).1.1.buckets)
+    (List.insertListIfNewUnit (toListModel m.1.buckets) l) := by
+  rw [Const.insertManyIfNewUnit_eq_insertListIfNewUnitₘ]
   apply toListModel_insertListIfNewUnitₘ h
 
-theorem Const.wfImp_insertManyIfNewUnit [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w}
-    [ForIn Id ρ α] {m : Raw₀ α (fun _ => Unit)} {l : ρ} (h : Raw.WFImp m.1) :
+theorem Const.wfImp_insertManyIfNewUnit [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
+    {ρ : Type w} [ForIn Id ρ α] {m : Raw₀ α (fun _ => Unit)} {l : ρ} (h : Raw.WFImp m.1) :
     Raw.WFImp (Const.insertManyIfNewUnit m l).1.1 :=
   Raw.WF.out ((Const.insertManyIfNewUnit m l).2 _ Raw.WF.insertIfNew₀ (.wf m.2 h))
 
diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean
index 0f92a8c194ba..967dc4797d5b 100644
--- a/src/Std/Data/DHashMap/Raw.lean
+++ b/src/Std/Data/DHashMap/Raw.lean
@@ -389,7 +389,6 @@ appearance.
     (Raw₀.insertMany ⟨m, h⟩ l).1
   else m -- will never happen for well-formed inputs
 
-
 @[inline, inherit_doc Raw.insertMany] def Const.insertMany {β : Type v} [BEq α] [Hashable α]
     {ρ : Type w} [ForIn Id ρ (α × β)] (m : Raw α (fun _ => β)) (l : ρ) : Raw α (fun _ => β) :=
   if h : 0 < m.buckets.size then