diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index 06525d82840b..da5267580100 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -89,9 +89,8 @@ private def queryNames : Array Name :=
     ``Const.get_eq_getValue, ``get!_eq_getValueCast!, ``getD_eq_getValueCastD,
     ``Const.get!_eq_getValue!, ``Const.getD_eq_getValueD, ``getKey?_eq_getKey?,
     ``getKey_eq_getKey, ``getKeyD_eq_getKeyD, ``getKey!_eq_getKey!,
-    ``Raw.length_keys_eq_length_keys, ``Raw.isEmpty_keys_eq_isEmpty_keys,
-    ``Raw.contains_keys_eq_contains_keys, ``Raw.mem_keys_iff_contains_keys,
-    ``Raw.pairwise_keys_iff_pairwise_keys]
+    ``Raw.toList_eq_toListModel, ``Raw.keys_eq_keys_toListModel,
+    ``Raw.Const.toList_eq_toListModel_map]
 
 private def modifyMap : Std.DHashMap Name (fun _ => Name) :=
   .ofList
@@ -830,6 +829,10 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 
 end Const
 
+theorem keys_eq_map_toList [EquivBEq α] [LawfulHashable α] :
+    m.1.keys = m.1.toList.map Sigma.fst := by
+  simp_to_model using List.keys_eq_map
+
 @[simp]
 theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
     m.1.keys.length = m.1.size := by
@@ -848,6 +851,7 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
 @[simp]
 theorem mem_keys [LawfulBEq α] (h : m.1.WF) {k : α} :
     k ∈ m.1.keys ↔ m.contains k := by
+  rw [← List.contains_iff]
   simp_to_model
   rw [List.containsKey_eq_keys_contains]
 
@@ -855,6 +859,82 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
     m.1.keys.Pairwise (fun a b => (a == b) = false) := by
   simp_to_model using (Raw.WF.out h).distinct.distinct
 
+theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    m.1.toList.length = m.1.size := by
+  simp_to_model
+
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    m.1.toList.isEmpty = m.1.isEmpty := by
+  simp_to_model
+
+theorem mem_toList_iff_get?_eq_some [LawfulBEq α] (h : m.1.WF)
+    {k : α} {v : β k} :
+    ⟨k, v⟩ ∈ m.1.toList ↔ m.get? k = some v := by
+  simp_to_model using List.mem_iff_getValueCast?_eq_some
+
+theorem find?_toList_eq_some_iff_get?_eq_some [LawfulBEq α]
+    (h : m.1.WF) {k : α} {v : β k} :
+    m.1.toList.find? (·.1 == k) = some ⟨k, v⟩ ↔ m.get? k = some v := by
+  simp_to_model using List.find?_eq_some_iff_getValueCast?_eq_some
+
+theorem find?_toList_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {k : α} :
+    m.1.toList.find? (·.1 == k) = none ↔ m.contains k = false := by
+  simp_to_model using List.find?_eq_none_iff_containsKey_eq_false
+
+theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    m.1.toList.Pairwise (fun a b => (a.1 == b.1) = false) := by
+  simp_to_model using List.pairwise_fst_eq_false
+
+namespace Const
+
+variable {β : Type v} (m : Raw₀ α (fun _ => β))
+
+theorem keys_eq_map_toList [EquivBEq α] [LawfulHashable α] :
+    m.1.keys = (Raw.Const.toList m.1).map Prod.fst := by
+  simp_to_model using List.keys_eq_map_prod_fst_map_toProd
+
+theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    (Raw.Const.toList m.1).length = m.1.size := by
+  simp_to_model using List.length_map
+
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    (Raw.Const.toList m.1).isEmpty = m.1.isEmpty := by
+  simp_to_model
+  rw [Bool.eq_iff_iff, List.isEmpty_iff,List.isEmpty_iff, List.map_eq_nil_iff]
+
+theorem mem_toList_iff_get?_eq_some [LawfulBEq α] (h : m.1.WF)
+    {k : α} {v : β} :
+    (k, v) ∈ Raw.Const.toList m.1 ↔ get? m k = some v := by
+  simp_to_model using List.mem_map_toProd_iff_getValue?_eq_some
+
+theorem get?_eq_some_iff_exists_beq_and_mem_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {k : α} {v : β} :
+    get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ Raw.Const.toList m.1 := by
+  simp_to_model using getValue?_eq_some_iff_exists_beq_and_mem_toList
+
+theorem find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+    [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k k' : α} {v : β} :
+    (Raw.Const.toList m.1).find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
+      m.getKey? k = some k' ∧ get? m k = some v := by
+  simp_to_model using List.find?_map_toProd_eq_some_iff_getKey?_eq_some_and_getValue?_eq_some
+
+theorem find?_toList_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {k : α} :
+    (Raw.Const.toList m.1).find? (·.1 == k) = none ↔ m.contains k = false := by
+  simp_to_model using List.find?_map_eq_none_iff_containsKey_eq_false
+
+theorem mem_toList_iff_getKey?_eq_some_and_get?_eq_some [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {k: α} {v : β} :
+    (k, v) ∈ (Raw.Const.toList m.1) ↔ m.getKey? k = some k ∧ get? m k = some v := by
+  simp_to_model using List.mem_map_toProd_iff_getKey?_eq_some_and_getValue?_eq_some
+
+theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    (Raw.Const.toList m.1).Pairwise (fun a b => (a.1 == b.1) = false) := by
+  simp_to_model using List.pairwise_fst_eq_false_map_toProd
+
+end Const
+
 @[simp]
 theorem insertMany_nil :
     m.insertMany [] = m := by
@@ -1230,7 +1310,7 @@ theorem getKey?_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashab
   simp_to_model [Const.insertManyIfNewUnit] using List.getKey?_insertListIfNewUnit_of_contains
 
 theorem getKey_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashable α]
-    (h : m.1.WF) {l : List α} {k : α} {h'} (contains : m.contains k):
+    (h : m.1.WF) {l : List α} {k : α} {h'} (contains : m.contains k) :
     getKey (insertManyIfNewUnit m l).1 k h' = getKey m k contains := by
   simp_to_model [Const.insertManyIfNewUnit] using List.getKey_insertListIfNewUnit_of_contains
 
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 3e49018f7a51..34952f7c721e 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -104,37 +104,25 @@ theorem foldRev_cons {l : Raw α β} {acc : List ((a : α) × β a)} :
     l.foldRev (fun acc k v => ⟨k, v⟩ :: acc) acc = toListModel l.buckets ++ acc := by
   simp [foldRev_cons_apply]
 
+theorem foldRev_cons_mk {β : Type v} {l : Raw α (fun _ => β)} {acc : List (α × β)} :
+    l.foldRev (fun acc k v => (k, v) :: acc) acc =
+      (toListModel l.buckets).map (fun ⟨k, v⟩ => (k, v)) ++ acc := by
+  simp [foldRev_cons_apply]
+
 theorem foldRev_cons_key {l : Raw α β} {acc : List α} :
     l.foldRev (fun acc k _ => k :: acc) acc = List.keys (toListModel l.buckets) ++ acc := by
   rw [foldRev_cons_apply, keys_eq_map]
 
-theorem toList_perm_toListModel {m : Raw α β} : Perm m.toList (toListModel m.buckets) := by
+theorem toList_eq_toListModel {m : Raw α β} : m.toList = toListModel m.buckets := by
   simp [Raw.toList, foldRev_cons]
 
-theorem keys_perm_keys_toListModel {m : Raw α β} :
-    Perm m.keys (List.keys (toListModel m.buckets)) := by
-  simp [Raw.keys, foldRev_cons_key, keys_eq_map]
-
-theorem length_keys_eq_length_keys {m : Raw α β} :
-    m.keys.length = (List.keys (toListModel m.buckets)).length :=
-  keys_perm_keys_toListModel.length_eq
+theorem Const.toList_eq_toListModel_map {β : Type v} {m : Raw α (fun _ => β)} :
+    Raw.Const.toList m = (toListModel m.buckets).map (fun ⟨k, v⟩ => ⟨k, v⟩) := by
+  simp [Raw.Const.toList, foldRev_cons_mk]
 
-theorem isEmpty_keys_eq_isEmpty_keys {m : Raw α β} :
-    m.keys.isEmpty = (List.keys (toListModel m.buckets)).isEmpty :=
-  keys_perm_keys_toListModel.isEmpty_eq
-
-theorem contains_keys_eq_contains_keys [BEq α] {m : Raw α β} {k : α} :
-    m.keys.contains k = (List.keys (toListModel m.buckets)).contains k :=
-  keys_perm_keys_toListModel.contains_eq
-
-theorem mem_keys_iff_contains_keys [BEq α] [LawfulBEq α] {m : Raw α β} {k : α} :
-    k ∈ m.keys ↔ (List.keys (toListModel m.buckets)).contains k := by
-  rw [← List.contains_iff_mem, contains_keys_eq_contains_keys]
-
-theorem pairwise_keys_iff_pairwise_keys [BEq α] [PartialEquivBEq α] {m : Raw α β} :
-    m.keys.Pairwise (fun a b => (a == b) = false) ↔
-      (List.keys (toListModel m.buckets)).Pairwise (fun a b => (a == b) = false) :=
-  keys_perm_keys_toListModel.pairwise_iff BEq.symm_false
+theorem keys_eq_keys_toListModel {m : Raw α β }:
+    m.keys = List.keys (toListModel m.buckets) := by
+  simp [Raw.keys, foldRev_cons_key, keys_eq_map]
 
 end Raw
 
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 4c86c0a17251..1cc68c37966b 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -938,6 +938,10 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 
 end Const
 
+theorem keys_eq_map_toList [EquivBEq α] [LawfulHashable α] :
+    m.1.keys = m.1.toList.map Sigma.fst :=
+  Raw₀.keys_eq_map_toList ⟨m.1, m.2.size_buckets_pos⟩
+
 @[simp]
 theorem length_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.length = m.size :=
@@ -963,6 +967,98 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) :=
   Raw₀.distinct_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
+@[simp]
+theorem length_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.length = m.size :=
+  Raw₀.length_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.isEmpty = m.isEmpty :=
+  Raw₀.isEmpty_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem mem_toList_iff_get?_eq_some [LawfulBEq α]
+    {k : α} {v : β k} :
+    ⟨k, v⟩ ∈ m.toList ↔ m.get? k = some v :=
+  Raw₀.mem_toList_iff_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toList_eq_some_iff_get?_eq_some [LawfulBEq α]
+    {k : α} {v : β k} :
+    m.toList.find? (·.1 == k) = some ⟨k, v⟩ ↔ m.get? k = some v :=
+  Raw₀.find?_toList_eq_some_iff_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toList_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    m.toList.find? (·.1 == k) = none ↔ m.contains k = false :=
+  Raw₀.find?_toList_eq_none_iff_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toList_eq_none_iff_not_mem [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    m.toList.find? (·.1 == k) = none ↔ ¬ k ∈ m := by
+  simp only [Bool.not_eq_true, mem_iff_contains]
+  apply Raw₀.find?_toList_eq_none_iff_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.Pairwise (fun a b => (a.1 == b.1) = false) :=
+  Raw₀.distinct_keys_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+namespace Const
+
+variable {β : Type v} {m : DHashMap α (fun _ => β)}
+
+theorem keys_eq_map_toList [EquivBEq α] [LawfulHashable α] :
+    m.keys = (toList m).map Prod.fst :=
+  Raw₀.Const.keys_eq_map_toList ⟨m.1, m.2.size_buckets_pos⟩
+
+@[simp]
+theorem length_toList [EquivBEq α] [LawfulHashable α] :
+    (toList m).length = m.size :=
+  Raw₀.Const.length_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] :
+    (toList m).isEmpty = m.isEmpty :=
+  Raw₀.Const.isEmpty_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem mem_toList_iff_get?_eq_some [LawfulBEq α]
+    {k : α} {v : β} :
+    (k, v) ∈ toList m ↔ get? m k = some v :=
+  Raw₀.Const.mem_toList_iff_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem get?_eq_some_iff_exists_beq_and_mem_toList [EquivBEq α] [LawfulHashable α]
+    {k : α} {v : β} :
+    get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ toList m :=
+  Raw₀.Const.get?_eq_some_iff_exists_beq_and_mem_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+    [EquivBEq α] [LawfulHashable α] {k k' : α} {v : β} :
+    (toList m).find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
+      m.getKey? k = some k' ∧ get? m k = some v :=
+  Raw₀.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+    ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toList_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    (toList m).find? (·.1 == k) = none ↔ m.contains k = false :=
+  Raw₀.Const.find?_toList_eq_none_iff_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toList_eq_none_iff_not_mem [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    (toList m).find? (·.1 == k) = none ↔ ¬ k ∈ m := by
+  simp only [Bool.not_eq_true, mem_iff_contains]
+  apply Raw₀.Const.find?_toList_eq_none_iff_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem mem_toList_iff_getKey?_eq_some_and_get?_eq_some [EquivBEq α] [LawfulHashable α]
+    {k: α} {v : β} :
+    (k, v) ∈ toList m ↔ m.getKey? k = some k ∧ get? m k = some v :=
+  Raw₀.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
+    (toList m).Pairwise (fun a b => (a.1 == b.1) = false) :=
+  Raw₀.Const.distinct_keys_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+end Const
+
 @[simp]
 theorem insertMany_nil :
     m.insertMany [] = m :=
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 603103498b6c..75c42c6e0f60 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1027,6 +1027,10 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
 
 end Const
 
+theorem keys_eq_map_toList [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.keys = m.toList.map Sigma.fst := by
+  apply Raw₀.keys_eq_map_toList ⟨m, h.size_buckets_pos⟩
+
 @[simp]
 theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.length = m.size := by
@@ -1052,6 +1056,101 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.Pairwise (fun a b => (a == b) = false) := by
   simp_to_raw using Raw₀.distinct_keys ⟨m, h.size_buckets_pos⟩ h
 
+@[simp]
+theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toList.length = m.size := by
+  apply Raw₀.length_toList ⟨m, h.size_buckets_pos⟩ h
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toList.isEmpty = m.isEmpty := by
+  apply Raw₀.isEmpty_toList ⟨m, h.size_buckets_pos⟩ h
+
+theorem mem_toList_iff_get?_eq_some [LawfulBEq α] (h : m.WF)
+    {k : α} {v : β k} :
+    ⟨k, v⟩ ∈ m.toList ↔ m.get? k = some v := by
+  simp_to_raw using Raw₀.mem_toList_iff_get?_eq_some ⟨m, _⟩ h
+
+theorem find?_toList_eq_some_iff_get?_eq_some [LawfulBEq α]
+    (h : m.WF) {k : α} {v : β k} :
+    m.toList.find? (·.1 == k) = some ⟨k, v⟩ ↔ m.get? k = some v := by
+  simp_to_raw using Raw₀.find?_toList_eq_some_iff_get?_eq_some ⟨m, _⟩ h
+
+theorem find?_toList_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.WF) {k : α} :
+    m.toList.find? (·.1 == k) = none ↔ m.contains k = false := by
+  simp_to_raw using Raw₀.find?_toList_eq_none_iff_contains_eq_false ⟨m, _⟩ h
+
+theorem find?_toList_eq_none_iff_not_mem [EquivBEq α] [LawfulHashable α]
+    (h : m.WF) {k : α} :
+    m.toList.find? (·.1 == k) = none ↔ ¬ k ∈ m := by
+  simp only [Bool.not_eq_true, mem_iff_contains]
+  simp_to_raw using Raw₀.find?_toList_eq_none_iff_contains_eq_false ⟨m, h.size_buckets_pos⟩ h
+
+theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toList.Pairwise (fun a b => (a.1 == b.1) = false) := by
+  apply Raw₀.distinct_keys_toList ⟨m, h.size_buckets_pos⟩ h
+
+namespace Const
+
+variable {β : Type v} {m : Raw α (fun _ => β)}
+
+theorem keys_eq_map_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.keys = (Raw.Const.toList m).map Prod.fst := by
+  apply Raw₀.Const.keys_eq_map_toList ⟨m, h.size_buckets_pos⟩
+
+@[simp]
+theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    (Raw.Const.toList m).length = m.size := by
+  apply Raw₀.Const.length_toList ⟨m, h.size_buckets_pos⟩ h
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    (Raw.Const.toList m).isEmpty = m.isEmpty := by
+  apply Raw₀.Const.isEmpty_toList ⟨m, h.size_buckets_pos⟩ h
+
+theorem mem_toList_iff_get?_eq_some [LawfulBEq α] (h : m.WF)
+    {k : α} {v : β} :
+    (k, v) ∈ Raw.Const.toList m ↔ get? m k = some v := by
+  simp_to_raw using Raw₀.Const.mem_toList_iff_get?_eq_some ⟨m, h.size_buckets_pos⟩ h
+
+theorem get?_eq_some_iff_exists_beq_and_mem_toList [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    {k : α} {v : β} :
+    get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ Raw.Const.toList m := by
+  simp_to_raw using Raw₀.Const.get?_eq_some_iff_exists_beq_and_mem_toList ⟨m, h.size_buckets_pos⟩ h
+
+theorem find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+    [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} {v : β} :
+    (Raw.Const.toList m).find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
+      m.getKey? k = some k' ∧ get? m k = some v := by
+  simp_to_raw using Raw₀.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+    ⟨m, h.size_buckets_pos⟩ h
+
+theorem find?_toList_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.WF) {k : α} :
+    (Raw.Const.toList m).find? (·.1 == k) = none ↔ m.contains k = false := by
+  simp_to_raw using Raw₀.Const.find?_toList_eq_none_iff_contains_eq_false
+    ⟨m, h.size_buckets_pos⟩ h
+
+theorem find?_toList_eq_none_iff_not_mem [EquivBEq α] [LawfulHashable α]
+    (h : m.WF) {k : α} :
+    (Raw.Const.toList m).find? (·.1 == k) = none ↔ ¬ k ∈ m := by
+  simp only [Bool.not_eq_true, mem_iff_contains]
+  simp_to_raw using Raw₀.Const.find?_toList_eq_none_iff_contains_eq_false
+    ⟨m, h.size_buckets_pos⟩ h
+
+theorem mem_toList_iff_getKey?_eq_some_and_get?_eq_some [EquivBEq α] [LawfulHashable α]
+    (h : m.WF) {k: α} {v : β} :
+    (k, v) ∈ Raw.Const.toList m ↔ m.getKey? k = some k ∧ get? m k = some v := by
+  simp_to_raw using Raw₀.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some
+    ⟨m, h.size_buckets_pos⟩ h
+
+theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    (Raw.Const.toList m).Pairwise (fun a b => (a.1 == b.1) = false) := by
+  apply Raw₀.Const.distinct_keys_toList ⟨m, h.size_buckets_pos⟩ h
+
+end Const
+
 @[simp]
 theorem insertMany_nil [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.insertMany [] = m := by
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index a525a23b3465..dc9b5c60bdd4 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -674,6 +674,10 @@ instance [EquivBEq α] [LawfulHashable α] : LawfulGetElem (HashMap α β) α β
     rw [getElem!_eq_get!_getElem?]
     split <;> simp_all
 
+theorem keys_eq_map_toList [EquivBEq α] [LawfulHashable α] :
+    m.keys = (toList m).map Prod.fst :=
+  DHashMap.Const.keys_eq_map_toList
+
 @[simp]
 theorem length_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.length = m.size :=
@@ -698,6 +702,51 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) :=
   DHashMap.distinct_keys
 
+@[simp]
+theorem length_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.length = m.size :=
+  DHashMap.Const.length_toList
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.isEmpty = m.isEmpty :=
+  DHashMap.Const.isEmpty_toList
+
+theorem mem_toList_iff_get?_eq_some [LawfulBEq α]
+    {k : α} {v : β} :
+    (k, v) ∈ m.toList ↔  m[k]? = some v :=
+  DHashMap.Const.mem_toList_iff_get?_eq_some
+
+theorem get?_eq_some_iff_exists_beq_and_mem_toList [EquivBEq α] [LawfulHashable α]
+    {k : α} {v : β} :
+    m[k]? = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ m.toList :=
+  DHashMap.Const.get?_eq_some_iff_exists_beq_and_mem_toList
+
+theorem find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some
+    [EquivBEq α] [LawfulHashable α] {k k' : α} {v : β} :
+    m.toList.find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
+      m.getKey? k = some k' ∧ get? m k = some v :=
+  DHashMap.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+
+theorem find?_toList_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    m.toList.find? (·.1 == k) = none ↔ m.contains k = false :=
+  DHashMap.Const.find?_toList_eq_none_iff_contains_eq_false
+
+theorem find?_toList_eq_none_iff_not_mem [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    m.toList.find? (·.1 == k) = none ↔ ¬ k ∈ m :=
+  DHashMap.Const.find?_toList_eq_none_iff_not_mem
+
+theorem mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some [EquivBEq α] [LawfulHashable α]
+    {k: α} {v : β} :
+    (k, v) ∈ m.toList ↔ m.getKey? k = some k ∧ get? m k = some v :=
+  DHashMap.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some
+
+theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.Pairwise (fun a b => (a.1 == b.1) = false) :=
+  DHashMap.Const.distinct_keys_toList
+
 @[simp]
 theorem insertMany_nil :
     insertMany m [] = m :=
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index 48860d56bab3..af0a608e60ce 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -681,6 +681,10 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
     (getThenInsertIfNew? m k v).2 = m.insertIfNew k v :=
   ext (DHashMap.Raw.Const.getThenInsertIfNew?_snd h.out)
 
+theorem keys_eq_map_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.keys = m.toList.map Prod.fst :=
+  DHashMap.Raw.Const.keys_eq_map_toList h.out
+
 @[simp]
 theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.length = m.size :=
@@ -705,6 +709,51 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.Pairwise (fun a b => (a == b) = false) :=
   DHashMap.Raw.distinct_keys h.out
 
+@[simp]
+theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toList.length = m.size :=
+  DHashMap.Raw.Const.length_toList h.out
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toList.isEmpty = m.isEmpty :=
+  DHashMap.Raw.Const.isEmpty_toList h.out
+
+theorem mem_toList_iff_getElem?_eq_some [LawfulBEq α] (h : m.WF)
+    {k : α} {v : β} :
+    (k, v) ∈ m.toList ↔ m[k]? = some v :=
+  DHashMap.Raw.Const.mem_toList_iff_get?_eq_some h.out
+
+theorem getElem?_eq_some_iff_exists_beq_and_mem_toList [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    {k : α} {v : β} :
+    m[k]? = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ m.toList :=
+  DHashMap.Raw.Const.get?_eq_some_iff_exists_beq_and_mem_toList h.out
+
+theorem find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some
+    [EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} {v : β} :
+    m.toList.find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
+      m.getKey? k = some k' ∧ m[k]? = some v :=
+  DHashMap.Raw.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some h.out
+
+theorem find?_toList_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.WF) {k : α} :
+    m.toList.find? (·.1 == k) = none ↔ m.contains k = false :=
+  DHashMap.Raw.Const.find?_toList_eq_none_iff_contains_eq_false h.out
+
+theorem find?_toList_eq_none_iff_not_mem [EquivBEq α] [LawfulHashable α]
+    (h : m.WF) {k : α} :
+    m.toList.find? (·.1 == k) = none ↔ ¬ k ∈ m :=
+  DHashMap.Raw.Const.find?_toList_eq_none_iff_not_mem h.out
+
+theorem mem_toList_iff_getKey?_eq_some_and_getElem_eq_some [EquivBEq α] [LawfulHashable α]
+    (h : m.WF) {k: α} {v : β} :
+    (k, v) ∈ m.toList ↔ m.getKey? k = some k ∧ m[k]? = some v :=
+  DHashMap.Raw.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some h.out
+
+theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toList.Pairwise (fun a b => (a.1 == b.1) = false) :=
+  DHashMap.Raw.Const.distinct_keys_toList h.out
+
 @[simp]
 theorem insertMany_nil (h : m.WF) :
     insertMany m [] = m :=
diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean
index 88c2dfa3956e..f822594a7d62 100644
--- a/src/Std/Data/Internal/List/Associative.lean
+++ b/src/Std/Data/Internal/List/Associative.lean
@@ -1303,7 +1303,7 @@ theorem insertEntryIfNew_of_containsKey_eq_false [BEq α] {l : List ((a : α) ×
   simp_all [insertEntryIfNew]
 
 theorem DistinctKeys.insertEntryIfNew [BEq α] [PartialEquivBEq α] {k : α} {v : β k}
-    {l : List ((a : α) × β a)} (h: DistinctKeys l):
+    {l : List ((a : α) × β a)} (h: DistinctKeys l) :
     DistinctKeys (insertEntryIfNew k v l) := by
   simp only [Std.Internal.List.insertEntryIfNew, cond_eq_if]
   split
@@ -1943,6 +1943,251 @@ theorem eraseKey_append_of_containsKey_right_eq_false [BEq α] {l l' : List ((a
     · rw [cond_false, cond_false, ih, List.cons_append]
     · rw [cond_true, cond_true]
 
+theorem mem_iff_getValueCast?_eq_some [BEq α] [LawfulBEq α] {k : α} {v : β k}
+    {l : List ((a : α) × β a)} (h : DistinctKeys l) :
+    ⟨k, v⟩ ∈ l ↔ getValueCast? k l = some v := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [List.mem_cons]
+    by_cases kv_hd: ⟨k, v⟩ = hd
+    · rw [← kv_hd]
+      simp
+    · simp only [kv_hd, false_or]
+      rw [distinctKeys_cons_iff] at h
+      by_cases k_hdfst: k == hd.fst
+      · simp only [beq_iff_eq] at k_hdfst
+        have : ∃ (v' : β k), ⟨k, v'⟩ = hd := by
+          exists cast (by congr;symm;exact k_hdfst) hd.snd
+          refine Sigma.ext k_hdfst ?_
+          simp
+        rcases this with ⟨v', h'⟩
+        rw [← h']
+        simp only [getValueCast?_cons_self, Option.some.injEq]
+        have h₁ : ¬ ⟨k,v⟩ ∈ tl := by
+          rw [containsKey_eq_false_iff] at h
+          false_or_by_contra
+          rename_i p
+          rcases h with ⟨_, h⟩
+          specialize h ⟨k, v⟩ p
+          simp [k_hdfst] at h
+        have h₂ : ¬ v' = v := by
+          false_or_by_contra
+          rename_i p
+          rw [← p, h'] at kv_hd
+          contradiction
+        simp [h₁, h₂]
+      · simp only [getValueCast?, beq_iff_eq]
+        split
+        · rename_i h
+          simp only [beq_iff_eq] at k_hdfst
+          simp only [beq_iff_eq] at h
+          rw [h] at k_hdfst
+          simp at k_hdfst
+        · apply ih (And.left h)
+
+theorem find?_eq_some_iff_getValueCast?_eq_some [BEq α] [LawfulBEq α]
+    {l : List ((a : α) × β a)} {k : α} {v : β k} (h : DistinctKeys l) :
+    List.find? (fun x => x.fst == k) l = some ⟨k, v⟩ ↔ getValueCast? k l = some v := by
+  rw [← mem_iff_getValueCast?_eq_some h]
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    rw [distinctKeys_cons_iff] at h
+    simp only [List.find?_cons_eq_some, beq_iff_eq, Bool.not_eq_eq_eq_not, Bool.not_true,
+      beq_eq_false_iff_ne, ne_eq, List.mem_cons]
+    by_cases hd_kv : hd = ⟨k, v⟩
+    · simp [hd_kv]
+    · simp only [hd_kv, and_false, ih (And.left h), false_or, Ne.symm hd_kv, and_iff_right_iff_imp]
+      intro kv_tl
+      false_or_by_contra
+      rename_i p
+      rcases h with ⟨_, h⟩
+      rw [containsKey_eq_false_iff] at h
+      specialize h ⟨k, v⟩ kv_tl
+      simp [p] at h
+
+theorem find?_eq_none_iff_containsKey_eq_false [BEq α] [PartialEquivBEq α]
+    {l : List ((a : α) × β a)} {k : α} :
+    List.find? (fun x => x.fst == k) l = none ↔ containsKey k l = false := by
+  simp [List.find?_eq_none, containsKey_eq_false_iff, BEq.comm]
+
+theorem pairwise_fst_eq_false [BEq α] {l : List ((a : α) × β a)} (h : DistinctKeys l) :
+    List.Pairwise (fun a b => (a.fst == b.fst) = false) l := by
+  rw [DistinctKeys.def] at h
+  assumption
+
+theorem keys_eq_map_prod_fst_map_toProd {β : Type v} {l : List ((_ : α) × β)} :
+    List.keys l = List.map Prod.fst (List.map (fun x => (x.fst, x.snd)) l) := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [List.map_cons, keys]
+    congr
+
+theorem find?_map_eq_none_iff_containsKey_eq_false [BEq α] [PartialEquivBEq α]
+    {β : Type v} {l : List ((_ : α) × β)} {k : α} :
+    List.find? (fun x => x.fst == k) (l.map (fun x => (x.fst, x.snd))) = none ↔
+      containsKey k l = false := by
+  simp [List.find?_eq_none, containsKey_eq_false_iff, BEq.comm]
+
+theorem mem_map_toProd_iff_mem {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)} :
+    ⟨k, v⟩ ∈ l ↔ (k, v) ∈ l.map (fun x => (x.fst, x.snd)) := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [List.mem_cons, List.map_cons, Prod.mk.injEq]
+    by_cases hd_kv: hd = ⟨k, v⟩
+    · simp [hd_kv]
+    · simp only [Ne.symm hd_kv, ih, List.mem_map, Prod.mk.injEq, false_or, iff_or_self, and_imp]
+      intro h₁ h₂
+      simp [h₁, h₂] at hd_kv
+
+theorem mem_iff_getValue?_eq_some [BEq α] [LawfulBEq α] {β : Type v} {k : α} {v : β}
+    {l : List ((_ : α) × β)} (h : DistinctKeys l) :
+    ⟨k, v⟩ ∈ l ↔ getValue? k l = some v := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [List.mem_cons]
+    by_cases kv_hd: ⟨k, v⟩ = hd
+    · rw [← kv_hd]
+      simp
+    · simp only [kv_hd, false_or, getValue?, cond_eq_if]
+      rw [distinctKeys_cons_iff] at h
+      by_cases hdfst_k: hd.fst == k
+      · simp only [hdfst_k, ↓reduceIte, Option.some.injEq]
+        simp only [beq_iff_eq] at hdfst_k
+        rw [containsKey_eq_false_iff] at h
+        constructor
+        · intro h'
+          rcases h with ⟨_, h⟩
+          specialize h ⟨hd.fst, v⟩
+          rw [hdfst_k] at h
+          simp only [beq_self_eq_true, Bool.true_eq_false, imp_false] at h
+          contradiction
+        · intro h'
+          rw [← hdfst_k, ← h'] at kv_hd
+          simp at kv_hd
+      · simp only [hdfst_k, Bool.false_eq_true, ↓reduceIte]
+        apply ih (And.left h)
+
+theorem mem_map_toProd_iff_getValue?_eq_some [BEq α] [LawfulBEq α] {β : Type v} {k : α} {v : β}
+    {l : List ((_ : α) × β)} (h : DistinctKeys l) :
+    ⟨k, v⟩ ∈ l.map (fun x => (x.fst, x.snd)) ↔ getValue? k l = some v := by
+  rw [← mem_map_toProd_iff_mem]
+  exact mem_iff_getValue?_eq_some h
+
+theorem find?_map_toProd_eq_some_iff_getKey?_eq_some_and_getValue?_eq_some [BEq α] [EquivBEq α]
+    {β : Type v} {k k': α} {v : β} {l : List ((_ : α) × β)} :
+    (l.map (fun x => (x.fst, x.snd))).find? (fun a => a.1 == k) = some (k', v)
+    ↔ getKey? k l = some k' ∧ getValue? k l = some v := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [List.map_cons, List.find?_cons_eq_some, Prod.mk.injEq, Bool.not_eq_eq_eq_not,
+      Bool.not_true, Option.map_eq_some', getKey?, cond_eq_if, getValue?]
+    by_cases hdfst_k: hd.fst == k
+    · simp only [hdfst_k, true_and, Bool.true_eq_false, false_and, or_false, ↓reduceIte,
+      Option.some.injEq]
+    · simp only [hdfst_k, Bool.false_eq_true, false_and, true_and, false_or, ↓reduceIte]
+      rw [ih]
+
+theorem mem_iff_getKey?_eq_some_and_getValue?_eq_some [BEq α] [EquivBEq α]
+    {β : Type v} {k: α} {v : β} {l : List ((_ : α) × β)} (h : DistinctKeys l) :
+    ⟨k, v⟩ ∈ l ↔ getKey? k l = some k ∧ getValue? k l = some v := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [List.mem_cons, getKey?, cond_eq_if, getValue?]
+    rw [distinctKeys_cons_iff] at h
+    specialize ih (And.left h)
+    by_cases hdfst_k : hd.fst == k
+    · simp only [hdfst_k, ↓reduceIte, Option.some.injEq]
+      rcases h with ⟨_, h⟩
+      constructor
+      · intro h'
+        cases h' with
+        | inl h' =>
+          rw [← h']
+          simp
+        | inr h' =>
+          rw [containsKey_eq_false_iff] at h
+          specialize h ⟨k, v⟩ h'
+          simp only at h
+          rw [hdfst_k] at h
+          contradiction
+      · intro h'
+        left
+        rw [Sigma.ext_iff]
+        simp [h']
+    · simp only [hdfst_k, Bool.false_eq_true, ↓reduceIte]
+      rw [ih]
+      simp only [or_iff_right_iff_imp]
+      intro h'
+      rw [← h'] at hdfst_k
+      simp at hdfst_k
+
+theorem getValue?_eq_some_iff_exists_beq_and_mem_toList {β : Type v} [BEq α] [PartialEquivBEq α]
+    {l : List ((_ : α) × β)} {k: α} {v : β} (h : DistinctKeys l) :
+    getValue? k l = some v ↔ ∃ k', (k == k') = true ∧ (k', v) ∈ l.map (fun x => (x.fst, x.snd)) := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    rw [distinctKeys_cons_iff] at h
+    simp only [getValue?, cond_eq_if, List.map_cons, List.mem_cons, Prod.mk.injEq, List.mem_map]
+    by_cases hdfst_k : hd.fst == k
+    · simp only [hdfst_k, ↓reduceIte, Option.some.injEq]
+      constructor
+      · intro h'
+        exists hd.fst
+        apply And.intro (PartialEquivBEq.symm hdfst_k)
+        simp [h']
+      · intro h'
+        rcases h' with ⟨k', k_k', h'⟩
+        cases h' with
+        | inl h' => exact Eq.symm (And.right h')
+        | inr h' =>
+          rcases h with ⟨_, h⟩
+          rcases h' with ⟨a, a_tl, a_k', a_v⟩
+          rw [containsKey_eq_false_iff] at h
+          specialize h a a_tl
+          rw [a_k'] at h
+          have := BEq.neq_of_neq_of_beq h (BEq.symm k_k')
+          simp [this] at hdfst_k
+    · simp only [hdfst_k, Bool.false_eq_true, ↓reduceIte, ih (And.left h), List.mem_map,
+        Prod.mk.injEq]
+      constructor
+      · intro h'
+        rcases h' with ⟨k', k_k', h'⟩
+        exists k'
+        apply And.intro k_k'
+        right
+        exact h'
+      · intro h'
+        rcases h' with ⟨k', k_k', h'⟩
+        exists k'
+        apply And.intro k_k'
+        cases h' with
+        | inl h' =>
+          rw [And.left h'] at k_k'
+          simp [BEq.symm k_k'] at hdfst_k
+        | inr h' => exact h'
+
+theorem mem_map_toProd_iff_getKey?_eq_some_and_getValue?_eq_some [BEq α] [EquivBEq α]
+    {β : Type v} {k: α} {v : β} {l : List ((_ : α) × β)} (h : DistinctKeys l) :
+    (k, v) ∈ l.map (fun x => (x.fst, x.snd)) ↔ getKey? k l = some k ∧ getValue? k l = some v := by
+  rw [← mem_map_toProd_iff_mem]
+  exact mem_iff_getKey?_eq_some_and_getValue?_eq_some h
+
+theorem pairwise_fst_eq_false_map_toProd [BEq α] {β : Type v}
+    {l : List ((_ : α) × β)} (h : DistinctKeys l) :
+    List.Pairwise (fun a b => (a.fst == b.fst) = false) (List.map (fun x => (x.fst, x.snd)) l)
+ := by
+  rw [DistinctKeys.def] at h
+  simp [List.pairwise_map]
+  assumption
+
 /-- Internal implementation detail of the hash map -/
 def insertList [BEq α] (l toInsert : List ((a : α) × β a)) : List ((a : α) × β a) :=
   match toInsert with
@@ -2464,7 +2709,7 @@ theorem getValue!_insertListConst_of_mem [BEq α] [EquivBEq α] [Inhabited β]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v: β} (k_beq : k == k')
     (distinct_l : DistinctKeys l)
     (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
-    (mem : ⟨k, v⟩ ∈ toInsert):
+    (mem : ⟨k, v⟩ ∈ toInsert) :
     getValue! k' (insertListConst l toInsert) = v := by
   rw [getValue!_eq_getValue?,
     getValue?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem, Option.get!_some]
@@ -2480,7 +2725,7 @@ theorem getValueD_insertListConst_of_mem [BEq α] [EquivBEq α]
     {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v fallback: β} (k_beq : k == k')
     (distinct_l : DistinctKeys l)
     (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
-    (mem : ⟨k, v⟩ ∈ toInsert):
+    (mem : ⟨k, v⟩ ∈ toInsert) :
     getValueD k' (insertListConst l toInsert) fallback= v := by
   simp only [getValueD_eq_getValue?]
   rw [getValue?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem, Option.getD_some]
@@ -2511,7 +2756,7 @@ theorem insertListIfNewUnit_perm_of_perm_first [BEq α] [EquivBEq α] {l1 l2 : L
     · apply DistinctKeys.insertEntryIfNew distinct
 
 theorem DistinctKeys.insertListIfNewUnit [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)}
-    {toInsert : List α} (distinct: DistinctKeys l):
+    {toInsert : List α} (distinct: DistinctKeys l) :
     DistinctKeys (insertListIfNewUnit l toInsert) := by
   induction toInsert generalizing l with
   | nil => simp [List.insertListIfNewUnit, distinct]
@@ -2592,7 +2837,7 @@ theorem getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivB
     {l : List ((_ : α) × Unit)} {toInsert : List α}
     {k k' : α} (k_beq : k == k')
     (mem' : containsKey k l = false)
-    (distinct : toInsert.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ toInsert):
+    (distinct : toInsert.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ toInsert) :
     getKey? k' (insertListIfNewUnit l toInsert) = some k := by
   simp only [getKey?_eq_getEntry?, getEntry?_insertListIfNewUnit, Option.map_eq_some',
     Option.or_eq_some, getEntry?_eq_none]
@@ -2609,7 +2854,7 @@ theorem getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivB
 theorem getKey?_insertListIfNewUnit_of_contains [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
     {k : α}
-    (h : containsKey k l = true):
+    (h : containsKey k l = true) :
     getKey? k (insertListIfNewUnit l toInsert) = getKey? k l := by
   rw [containsKey_eq_isSome_getEntry?] at h
   simp [getKey?_eq_getEntry?, getEntry?_insertListIfNewUnit, Option.or_of_isSome h]
@@ -2627,7 +2872,7 @@ theorem getKey_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivBE
 theorem getKey_insertListIfNewUnit_of_contains [BEq α] [EquivBEq α]
     {l : List ((_ : α) × Unit)} {toInsert : List α}
     {k : α}
-    (contains : containsKey k l = true) {h}:
+    (contains : containsKey k l = true) {h} :
     getKey k (insertListIfNewUnit l toInsert) h = getKey k l contains := by
   rw [← Option.some_inj, ← getKey?_eq_some_getKey, ← getKey?_eq_some_getKey,
     getKey?_insertListIfNewUnit_of_contains contains]
@@ -2728,14 +2973,14 @@ theorem length_insertListIfNewUnit [BEq α] [EquivBEq α]
         apply And.right distinct_both
 
 theorem length_le_length_insertListIfNewUnit [BEq α] [EquivBEq α]
-    {l : List ((_ : α) × Unit)} {toInsert : List α}:
+    {l : List ((_ : α) × Unit)} {toInsert : List α} :
     l.length ≤ (insertListIfNewUnit l toInsert).length := by
   induction toInsert generalizing l with
   | nil => apply Nat.le_refl
   | cons hd tl ih => exact Nat.le_trans length_le_length_insertEntryIfNew ih
 
 theorem length_insertListIfNewUnit_le [BEq α] [EquivBEq α]
-    {l : List ((_ : α) × Unit)} {toInsert : List α}:
+    {l : List ((_ : α) × Unit)} {toInsert : List α} :
     (insertListIfNewUnit l toInsert).length ≤ l.length + toInsert.length := by
   induction toInsert generalizing l with
   | nil => simp only [insertListIfNewUnit, List.length_nil, Nat.add_zero, Nat.le_refl]
@@ -2755,7 +3000,7 @@ theorem isEmpty_insertListIfNewUnit [BEq α]
     rw [insertListIfNewUnit, List.isEmpty_cons, ih, isEmpty_insertEntryIfNew]
     simp
 
-theorem getValue?_list_unit [BEq α] {l : List ((_ : α) × Unit)} {k : α}:
+theorem getValue?_list_unit [BEq α] {l : List ((_ : α) × Unit)} {k : α} :
     getValue? k l = if containsKey k l = true then some () else none := by
   induction l with
   | nil => simp
@@ -2766,7 +3011,7 @@ theorem getValue?_list_unit [BEq α] {l : List ((_ : α) × Unit)} {k : α}:
     · simp [hd_k, ih]
 
 theorem getValue?_insertListIfNewUnit [BEq α] [PartialEquivBEq α]
-    {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}:
+    {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]
@@ -3376,7 +3621,7 @@ theorem modifyKey_eq_alterKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β
     simp [h, insertEntry, containsKey_eq_isSome_getValueCast?, eraseKey_of_containsKey_eq_false]
 
 theorem getValueCast?_modifyKey [BEq α] [LawfulBEq α] {k k' : α} {f : β k → β k}
-    (l : List ((a : α) × β a)) (hl : DistinctKeys l):
+    (l : List ((a : α) × β a)) (hl : DistinctKeys l) :
     getValueCast? k' (modifyKey k f l) =
       if h : k == k' then
         (cast (congrArg (Option ∘ β) (eq_of_beq h)) ((getValueCast? k l).map f))