From d789318f5be0baba524aa6996bd1c8b03389686d Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Sat, 26 Oct 2024 16:25:49 +0200
Subject: [PATCH 01/17] Messy proof of keys_perm_keys_toListModel

---
 src/Std/Data/DHashMap/Internal/WF.lean | 49 ++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)

diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 8ca6edb8a81c..725c56172aa3 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -59,6 +59,55 @@ theorem isEmpty_eq_isEmpty [BEq α] [Hashable α] {m : Raw α β} (h : Raw.WFImp
   rw [Raw.isEmpty, Bool.eq_iff_iff, List.isEmpty_iff_length_eq_zero, size_eq_length h,
     Nat.beq_eq_true_eq]
 
+-- TODO (Markus): clean up
+theorem toList_perm_toListModel {m : Raw α β} : Perm m.toList (toListModel m.buckets) := by
+  rw [Raw.toList, toListModel, List.flatMap_eq_foldl, Raw.fold, Raw.foldM,
+    Array.foldlM_eq_foldlM_toList, ← List.foldl_eq_foldlM, Id.run]
+  have h₁ : ∀ {l : AssocList α β} {acc : List (Σ a, β a)},
+      l.foldlM (m := Id) (fun acc k v => ⟨k, v⟩ :: acc) acc = l.toList.reverse ++ acc := by
+    intro l acc
+    induction l generalizing acc
+    · simp [AssocList.foldlM]
+    · simp_all [AssocList.foldlM]
+  simp only [h₁]
+  suffices ∀ (l : List (AssocList α β)) (l₁ l₂), Perm l₁ l₂ →
+      Perm (l.foldl (fun acc m => m.toList.reverse ++ acc) l₁)
+        (l.foldl (fun acc m => acc ++ m.toList) l₂) by
+    simpa using this m.buckets.toList [] [] (Perm.refl _)
+  intros l l₁ l₂ h
+  induction l generalizing l₁ l₂
+  · simpa
+  · next l t ih =>
+    simp only [foldl_cons]
+    apply ih
+    refine (reverse_perm _).append_right _ |>.trans perm_append_comm |>.trans ?_
+    exact h.append_right l.toList
+
+-- TODO (Markus): clean up
+theorem keys_perm_keys_toListModel {m : Raw α β} :
+    Perm m.keys (List.keys (toListModel m.buckets)) := by
+  rw [Raw.keys, List.keys_eq_map]
+  refine Perm.trans ?_ (toList_perm_toListModel.map _)
+  simp only [Raw.toList, Raw.fold, Raw.foldM, Array.foldlM_eq_foldlM_toList, ← List.foldl_eq_foldlM,
+    Id.run]
+  generalize m.buckets.toList = l
+  suffices ∀ l', foldl
+      (fun acc l => AssocList.foldlM (m := Id) (fun acc k x => k :: acc) acc l) (l'.map (·.1)) l =
+      map Sigma.fst (foldl
+        (fun acc l => AssocList.foldlM (m := Id) (fun acc k v => ⟨k, v⟩ :: acc) acc l) l' l) from
+    this [] ▸ Perm.refl _
+  intro l'
+  induction l generalizing l' with
+  | nil => simp
+  | cons h t ih =>
+    rw [foldl_cons, foldl_cons, ← ih]
+    congr
+    induction h generalizing l' with
+    | nil => simp [AssocList.foldlM]
+    | cons k v t' ih' =>
+      simp only [AssocList.foldlM, Id.bind_eq]
+      rw [← ih', map_cons]
+
 end Raw
 
 namespace Raw₀

From 62a883cab58fd2edfeb8fdb68cb3f478a9cffa14 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Mon, 28 Oct 2024 08:07:46 +0100
Subject: [PATCH 02/17] Express queries of keys in terms of list model

---
 src/Std/Data/DHashMap/Internal/WF.lean | 35 ++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 725c56172aa3..e715e8bb02f2 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 prelude
+import Init.Data.AC
 import Std.Data.DHashMap.Basic
 import Std.Data.DHashMap.Internal.Model
 import Std.Data.DHashMap.Internal.AssocList.Lemmas
@@ -24,6 +25,24 @@ universe u v w
 
 variable {α : Type u} {β : α → Type v} {γ : Type w} {δ : α → Type w}
 
+namespace List
+
+-- TODO(Markus): Move to the right place
+theorem Perm.contains_eq [BEq α] {l₁ l₂ : List α} (h : l₁ ~ l₂) {k : α} :
+    l₁.contains k = l₂.contains k := by
+  induction h with
+  | nil => rfl
+  | cons => simp_all
+  | swap => simp only [contains_cons]; ac_rfl
+  | trans => simp_all
+
+-- TODO(Markus): Move to the right place
+theorem List.contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {k : α} :
+    l.contains k ↔ k ∈ l := by
+  simp
+
+end List
+
 open List
 
 namespace Std.DHashMap.Internal
@@ -108,6 +127,22 @@ theorem keys_perm_keys_toListModel {m : Raw α β} :
       simp only [AssocList.foldlM, Id.bind_eq]
       rw [← ih', map_cons]
 
+theorem length_keys_eq_length_keys {m : Raw α β} :
+    m.keys.length = (List.keys (toListModel m.buckets)).length :=
+  keys_perm_keys_toListModel.length_eq
+
+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_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]
+
 end Raw
 
 namespace Raw₀

From e226241a66040635d8eaa76ae64178215400c122 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Mon, 28 Oct 2024 08:38:14 +0100
Subject: [PATCH 03/17] contains_keys as an example

---
 src/Std/Data/DHashMap/Internal/RawLemmas.lean | 9 ++++++++-
 src/Std/Data/DHashMap/Internal/WF.lean        | 2 +-
 src/Std/Data/DHashMap/Lemmas.lean             | 5 +++++
 src/Std/Data/DHashMap/RawLemmas.lean          | 5 +++++
 src/Std/Data/HashMap/Lemmas.lean              | 4 ++++
 src/Std/Data/HashMap/RawLemmas.lean           | 5 +++++
 6 files changed, 28 insertions(+), 2 deletions(-)

diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index eeb6d653c73b..5e69053f7b3e 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -84,7 +84,9 @@ private def queryNames : Array Name :=
     ``get?_eq_getValueCast?, ``Const.get?_eq_getValue?, ``get_eq_getValueCast,
     ``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!]
+    ``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]
 
 private def modifyNames : Array Name :=
   #[``toListModel_insert, ``toListModel_erase, ``toListModel_insertIfNew]
@@ -811,6 +813,11 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 
 end Const
 
+@[simp]
+theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
+    m.1.keys.contains k = m.contains k := by
+  simp_to_model using List.containsKey_eq_keys_contains.symm
+
 end Raw₀
 
 end Std.DHashMap.Internal
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index e715e8bb02f2..a06d48d5b562 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -139,7 +139,7 @@ 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_iff_contains_keys [BEq α] [LawfulBEq α] {m : Raw α β} {k : α} :
+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]
 
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 544b5eefe5f4..e777ac95937c 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -943,4 +943,9 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 
 end Const
 
+@[simp]
+theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
+    m.keys.contains k = m.contains k :=
+  Raw₀.contains_keys ⟨m.1, _⟩ m.2
+
 end Std.DHashMap
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 5813e5a86564..8ae4c1e43244 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1022,6 +1022,11 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
 
 end Const
 
+@[simp]
+theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+    m.keys.contains k = m.contains k := by
+  simp_to_raw using Raw₀.contains_keys ⟨m, _⟩ h
+
 end Raw
 
 end Std.DHashMap
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index e116921d2285..60ea17691078 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -677,6 +677,10 @@ instance [EquivBEq α] [LawfulHashable α] : LawfulGetElem (HashMap α β) α β
     rw [getElem!_eq_get!_getElem?]
     split <;> simp_all
 
+@[simp]
+theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} : m.keys.contains k = m.contains k :=
+  DHashMap.contains_keys
+
 end
 
 end Std.HashMap
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index 6b0849519164..be99a04b24ae 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -682,6 +682,11 @@ 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)
 
+@[simp]
+theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+    m.keys.contains k = m.contains k :=
+  DHashMap.Raw.contains_keys h.out
+
 end Raw
 
 end Std.HashMap

From d15dc406649d8a9ce5c054b1eb5cbea38420451f Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Mon, 28 Oct 2024 08:41:14 +0100
Subject: [PATCH 04/17] Move list lemmas

---
 src/Init/Data/List/Lemmas.lean         |  4 ++++
 src/Init/Data/List/Perm.lean           |  8 ++++++++
 src/Std/Data/DHashMap/Internal/WF.lean | 19 -------------------
 3 files changed, 12 insertions(+), 19 deletions(-)

diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 1112ba8f650a..afb325cf3a2d 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -2843,6 +2843,10 @@ theorem contains_iff_exists_mem_beq [BEq α] {l : List α} {a : α} :
     l.contains a ↔ ∃ a' ∈ l, a == a' := by
   induction l <;> simp_all
 
+theorem List.contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+    l.contains a ↔ a ∈ l := by
+  simp
+
 /-! ## Sublists -/
 
 /-! ### partition
diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean
index 8bb0f22d27c9..6373a6511d8d 100644
--- a/src/Init/Data/List/Perm.lean
+++ b/src/Init/Data/List/Perm.lean
@@ -114,6 +114,14 @@ theorem Perm.length_eq {l₁ l₂ : List α} (p : l₁ ~ l₂) : length l₁ = l
   | swap => rfl
   | trans _ _ ih₁ ih₂ => simp only [ih₁, ih₂]
 
+theorem Perm.contains_eq [BEq α] {l₁ l₂ : List α} (h : l₁ ~ l₂) {a : α} :
+    l₁.contains a = l₂.contains a := by
+  induction h with
+  | nil => rfl
+  | cons => simp_all
+  | swap => simp only [contains_cons, ← Bool.or_assoc, Bool.or_comm]
+  | trans => simp_all
+
 theorem Perm.eq_nil {l : List α} (p : l ~ []) : l = [] := eq_nil_of_length_eq_zero p.length_eq
 
 theorem Perm.nil_eq {l : List α} (p : [] ~ l) : [] = l := p.symm.eq_nil.symm
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index a06d48d5b562..342da89b93b5 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
 prelude
-import Init.Data.AC
 import Std.Data.DHashMap.Basic
 import Std.Data.DHashMap.Internal.Model
 import Std.Data.DHashMap.Internal.AssocList.Lemmas
@@ -25,24 +24,6 @@ universe u v w
 
 variable {α : Type u} {β : α → Type v} {γ : Type w} {δ : α → Type w}
 
-namespace List
-
--- TODO(Markus): Move to the right place
-theorem Perm.contains_eq [BEq α] {l₁ l₂ : List α} (h : l₁ ~ l₂) {k : α} :
-    l₁.contains k = l₂.contains k := by
-  induction h with
-  | nil => rfl
-  | cons => simp_all
-  | swap => simp only [contains_cons]; ac_rfl
-  | trans => simp_all
-
--- TODO(Markus): Move to the right place
-theorem List.contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {k : α} :
-    l.contains k ↔ k ∈ l := by
-  simp
-
-end List
-
 open List
 
 namespace Std.DHashMap.Internal

From c71fadf876db889e2a45f78c59ca5887122d3ca1 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Mon, 28 Oct 2024 09:18:33 +0100
Subject: [PATCH 05/17] Add pairwise distinct translation

---
 src/Std/Data/DHashMap/Internal/RawLemmas.lean | 3 ++-
 src/Std/Data/DHashMap/Internal/WF.lean        | 5 +++++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index 5e69053f7b3e..77b1948c428e 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -86,7 +86,8 @@ private def queryNames : Array Name :=
     ``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.contains_keys_eq_contains_keys, ``Raw.mem_keys_iff_contains_keys,
+    ``Raw.pairwise_keys_iff_pairwise_keys]
 
 private def modifyNames : Array Name :=
   #[``toListModel_insert, ``toListModel_erase, ``toListModel_insertIfNew]
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 342da89b93b5..ed21a0a1472c 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -124,6 +124,11 @@ 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
+
 end Raw
 
 namespace Raw₀

From f8080899eba42507c13e00463a9ef103eea47f1d Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Mon, 28 Oct 2024 09:46:03 +0100
Subject: [PATCH 06/17] Minor cleanup

---
 src/Std/Data/DHashMap/Internal/WF.lean | 31 +++++++++++++-------------
 1 file changed, 16 insertions(+), 15 deletions(-)

diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index ed21a0a1472c..39aa7c0e50b7 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -59,17 +59,24 @@ theorem isEmpty_eq_isEmpty [BEq α] [Hashable α] {m : Raw α β} (h : Raw.WFImp
   rw [Raw.isEmpty, Bool.eq_iff_iff, List.isEmpty_iff_length_eq_zero, size_eq_length h,
     Nat.beq_eq_true_eq]
 
+theorem AssocList.foldlM_apply {l : AssocList α β} {acc : List γ} (f : (a : α) → β a → γ) :
+    l.foldlM (m := Id) (fun acc k v => f k v :: acc) acc =
+      (l.toList.map (fun p => f p.1 p.2)).reverse ++ acc := by
+  induction l generalizing acc <;> simp_all [AssocList.foldlM]
+
+theorem AssocList.foldlM_cons {l : AssocList α β} {acc : List ((a : α) × β a)} :
+    l.foldlM (m := Id) (fun acc k v => ⟨k, v⟩ :: acc) acc = l.toList.reverse ++ acc := by
+  simp [AssocList.foldlM_apply]
+
+theorem AssocList.foldlM_cons_key {l : AssocList α β} {acc : List α} :
+    l.foldlM (m := Id) (fun acc k _ => k :: acc) acc = (List.keys l.toList).reverse ++ acc := by
+  rw [AssocList.foldlM_apply, keys_eq_map]
+
 -- TODO (Markus): clean up
 theorem toList_perm_toListModel {m : Raw α β} : Perm m.toList (toListModel m.buckets) := by
   rw [Raw.toList, toListModel, List.flatMap_eq_foldl, Raw.fold, Raw.foldM,
     Array.foldlM_eq_foldlM_toList, ← List.foldl_eq_foldlM, Id.run]
-  have h₁ : ∀ {l : AssocList α β} {acc : List (Σ a, β a)},
-      l.foldlM (m := Id) (fun acc k v => ⟨k, v⟩ :: acc) acc = l.toList.reverse ++ acc := by
-    intro l acc
-    induction l generalizing acc
-    · simp [AssocList.foldlM]
-    · simp_all [AssocList.foldlM]
-  simp only [h₁]
+  simp only [AssocList.foldlM_cons]
   suffices ∀ (l : List (AssocList α β)) (l₁ l₂), Perm l₁ l₂ →
       Perm (l.foldl (fun acc m => m.toList.reverse ++ acc) l₁)
         (l.foldl (fun acc m => acc ++ m.toList) l₂) by
@@ -97,16 +104,10 @@ theorem keys_perm_keys_toListModel {m : Raw α β} :
         (fun acc l => AssocList.foldlM (m := Id) (fun acc k v => ⟨k, v⟩ :: acc) acc l) l' l) from
     this [] ▸ Perm.refl _
   intro l'
+  simp [AssocList.foldlM_cons, AssocList.foldlM_cons_key]
   induction l generalizing l' with
   | nil => simp
-  | cons h t ih =>
-    rw [foldl_cons, foldl_cons, ← ih]
-    congr
-    induction h generalizing l' with
-    | nil => simp [AssocList.foldlM]
-    | cons k v t' ih' =>
-      simp only [AssocList.foldlM, Id.bind_eq]
-      rw [← ih', map_cons]
+  | cons h t ih => simp [List.keys_eq_map, ← ih]
 
 theorem length_keys_eq_length_keys {m : Raw α β} :
     m.keys.length = (List.keys (toListModel m.buckets)).length :=

From d9cac0c60cdcc98a47f514941f4db225e8aa0528 Mon Sep 17 00:00:00 2001
From: monsterkrampe <monsterkrampe@users.noreply.github.com>
Date: Mon, 28 Oct 2024 16:11:20 +0100
Subject: [PATCH 07/17] Add length_keys_eq_size to HashMap

---
 src/Std/Data/DHashMap/Internal/List/Associative.lean | 3 +++
 src/Std/Data/DHashMap/Internal/RawLemmas.lean        | 5 +++++
 src/Std/Data/DHashMap/Lemmas.lean                    | 5 +++++
 src/Std/Data/DHashMap/RawLemmas.lean                 | 5 +++++
 src/Std/Data/HashMap/Lemmas.lean                     | 8 +++++++-
 src/Std/Data/HashMap/RawLemmas.lean                  | 5 +++++
 6 files changed, 30 insertions(+), 1 deletion(-)

diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean
index 6a41c5b11ace..939778b52c50 100644
--- a/src/Std/Data/DHashMap/Internal/List/Associative.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean
@@ -849,6 +849,9 @@ theorem isEmpty_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
 theorem keys_eq_map (l : List ((a : α) × β a)) : keys l = l.map (·.1) := by
   induction l using assoc_induction <;> simp_all
 
+theorem length_keys_eq_length (l : List ((a : α) × β a)) : (keys l).length = l.length := by 
+  induction l using assoc_induction <;> simp_all
+
 theorem containsKey_eq_keys_contains [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
     {a : α} : containsKey a l = (keys l).contains a := by
   induction l using assoc_induction
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index 77b1948c428e..eecfe6c0e2f0 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -814,6 +814,11 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 
 end Const
 
+@[simp]
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.1.WF) : 
+    m.1.keys.length = m.1.size := by 
+  simp_to_model using List.length_keys_eq_length
+
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
     m.1.keys.contains k = m.contains k := by
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index e777ac95937c..31b2974a80b3 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -943,6 +943,11 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 
 end Const
 
+@[simp]
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] : 
+    m.keys.length = m.size := 
+  Raw₀.length_keys_eq_size ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
     m.keys.contains k = m.contains k :=
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 8ae4c1e43244..132e0ce1b618 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1022,6 +1022,11 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
 
 end Const
 
+@[simp]
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) : 
+    m.keys.length = m.size := by 
+  simp_to_raw using Raw₀.length_keys_eq_size ⟨m, h.size_buckets_pos⟩ h
+
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     m.keys.contains k = m.contains k := by
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 60ea17691078..bfd4fe9e04d5 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -678,7 +678,13 @@ instance [EquivBEq α] [LawfulHashable α] : LawfulGetElem (HashMap α β) α β
     split <;> simp_all
 
 @[simp]
-theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} : m.keys.contains k = m.contains k :=
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] : 
+    m.keys.length = m.size := 
+  DHashMap.length_keys_eq_size
+
+@[simp]
+theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} : 
+    m.keys.contains k = m.contains k :=
   DHashMap.contains_keys
 
 end
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index be99a04b24ae..edadac99d224 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -682,6 +682,11 @@ 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)
 
+@[simp]
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) : 
+    m.keys.length = m.size := 
+  DHashMap.Raw.length_keys_eq_size h.out
+
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     m.keys.contains k = m.contains k :=

From 7e231a3e2af4042a0510e95935c5565c89874785 Mon Sep 17 00:00:00 2001
From: jt0202 <johannes.tantow@gmail.com>
Date: Tue, 5 Nov 2024 18:22:39 +0100
Subject: [PATCH 08/17] Add keys_isEmpty to HashMap

---
 src/Std/Data/DHashMap/Internal/RawLemmas.lean | 11 +++++++++--
 src/Std/Data/DHashMap/Lemmas.lean             |  9 +++++++--
 src/Std/Data/DHashMap/RawLemmas.lean          |  8 ++++++--
 src/Std/Data/HashMap/Lemmas.lean              | 11 ++++++++---
 src/Std/Data/HashMap/RawLemmas.lean           |  9 +++++++--
 5 files changed, 37 insertions(+), 11 deletions(-)

diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index eecfe6c0e2f0..59e8bf65e081 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -815,8 +815,8 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.1.WF) : 
-    m.1.keys.length = m.1.size := by 
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    m.1.keys.length = m.1.size := by
   simp_to_model using List.length_keys_eq_length
 
 @[simp]
@@ -824,6 +824,13 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
     m.1.keys.contains k = m.contains k := by
   simp_to_model using List.containsKey_eq_keys_contains.symm
 
+@[simp]
+theorem keys_isEmpty [EquivBEq α] [LawfulHashable α] (h: m.1.WF):
+    m.1.keys.isEmpty = m.1.isEmpty:= by
+  rw [Bool.eq_iff_iff, List.isEmpty_iff_length_eq_zero, isEmpty_eq_size_eq_zero, length_keys_eq_size m h]
+  simp
+
+
 end Raw₀
 
 end Std.DHashMap.Internal
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 31b2974a80b3..fd0c20302d63 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -944,8 +944,8 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] : 
-    m.keys.length = m.size := 
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] :
+    m.keys.length = m.size :=
   Raw₀.length_keys_eq_size ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
 @[simp]
@@ -953,4 +953,9 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
     m.keys.contains k = m.contains k :=
   Raw₀.contains_keys ⟨m.1, _⟩ m.2
 
+@[simp]
+theorem keys_isEmpty [EquivBEq α] [LawfulHashable α]:
+    m.keys.isEmpty = m.isEmpty  :=
+  Raw₀.keys_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
 end Std.DHashMap
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 132e0ce1b618..16a4885b4121 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1023,8 +1023,8 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) : 
-    m.keys.length = m.size := by 
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.keys.length = m.size := by
   simp_to_raw using Raw₀.length_keys_eq_size ⟨m, h.size_buckets_pos⟩ h
 
 @[simp]
@@ -1032,6 +1032,10 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     m.keys.contains k = m.contains k := by
   simp_to_raw using Raw₀.contains_keys ⟨m, _⟩ h
 
+@[simp]
+theorem keys_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.keys.isEmpty = m.isEmpty := by
+  simp_to_raw using Raw₀.keys_isEmpty ⟨m, h.size_buckets_pos⟩
 end Raw
 
 end Std.DHashMap
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index bfd4fe9e04d5..bcea7b07de89 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -678,15 +678,20 @@ instance [EquivBEq α] [LawfulHashable α] : LawfulGetElem (HashMap α β) α β
     split <;> simp_all
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] : 
-    m.keys.length = m.size := 
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] :
+    m.keys.length = m.size :=
   DHashMap.length_keys_eq_size
 
 @[simp]
-theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} : 
+theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
     m.keys.contains k = m.contains k :=
   DHashMap.contains_keys
 
+@[simp]
+theorem keys_isEmpty [EquivBEq α] [LawfulHashable α]:
+    m.keys.isEmpty = m.isEmpty :=
+  DHashMap.keys_isEmpty
+
 end
 
 end Std.HashMap
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index edadac99d224..e1ebe2dd7105 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -683,8 +683,8 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
   ext (DHashMap.Raw.Const.getThenInsertIfNew?_snd h.out)
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) : 
-    m.keys.length = m.size := 
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.keys.length = m.size :=
   DHashMap.Raw.length_keys_eq_size h.out
 
 @[simp]
@@ -692,6 +692,11 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     m.keys.contains k = m.contains k :=
   DHashMap.Raw.contains_keys h.out
 
+@[simp]
+theorem keys_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.keys.isEmpty = m.isEmpty :=
+  DHashMap.Raw.keys_isEmpty h.out
+
 end Raw
 
 end Std.HashMap

From 43ec5b3f3f031afa97f83d7926b65cedde2858c8 Mon Sep 17 00:00:00 2001
From: monsterkrampe <monsterkrampe@users.noreply.github.com>
Date: Wed, 6 Nov 2024 09:02:13 +0100
Subject: [PATCH 09/17] Idiomatize isEmpty_keys_eq_isEmpty for HashMap

---
 src/Std/Data/DHashMap/Internal/List/Associative.lean | 3 +++
 src/Std/Data/DHashMap/Internal/RawLemmas.lean        | 5 ++---
 src/Std/Data/DHashMap/Lemmas.lean                    | 4 ++--
 src/Std/Data/DHashMap/RawLemmas.lean                 | 4 ++--
 src/Std/Data/HashMap/Lemmas.lean                     | 4 ++--
 src/Std/Data/HashMap/RawLemmas.lean                  | 4 ++--
 6 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean
index 939778b52c50..97bbaf230ace 100644
--- a/src/Std/Data/DHashMap/Internal/List/Associative.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean
@@ -852,6 +852,9 @@ theorem keys_eq_map (l : List ((a : α) × β a)) : keys l = l.map (·.1) := by
 theorem length_keys_eq_length (l : List ((a : α) × β a)) : (keys l).length = l.length := by 
   induction l using assoc_induction <;> simp_all
 
+theorem isEmpty_keys_eq_isEmpty (l : List ((a : α) × β a)) : (keys l).isEmpty = l.isEmpty := by 
+  induction l using assoc_induction <;> simp_all
+
 theorem containsKey_eq_keys_contains [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
     {a : α} : containsKey a l = (keys l).contains a := by
   induction l using assoc_induction
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index 59e8bf65e081..bc287e1e8ce0 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -825,10 +825,9 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
   simp_to_model using List.containsKey_eq_keys_contains.symm
 
 @[simp]
-theorem keys_isEmpty [EquivBEq α] [LawfulHashable α] (h: m.1.WF):
+theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h: m.1.WF):
     m.1.keys.isEmpty = m.1.isEmpty:= by
-  rw [Bool.eq_iff_iff, List.isEmpty_iff_length_eq_zero, isEmpty_eq_size_eq_zero, length_keys_eq_size m h]
-  simp
+  simp_to_model using List.isEmpty_keys_eq_isEmpty
 
 
 end Raw₀
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index fd0c20302d63..d0f2f43a1531 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -954,8 +954,8 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
   Raw₀.contains_keys ⟨m.1, _⟩ m.2
 
 @[simp]
-theorem keys_isEmpty [EquivBEq α] [LawfulHashable α]:
+theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α]:
     m.keys.isEmpty = m.isEmpty  :=
-  Raw₀.keys_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2
+  Raw₀.isEmpty_keys_eq_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
 end Std.DHashMap
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 16a4885b4121..abe4a2702fa3 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1033,9 +1033,9 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
   simp_to_raw using Raw₀.contains_keys ⟨m, _⟩ h
 
 @[simp]
-theorem keys_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
+theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
     m.keys.isEmpty = m.isEmpty := by
-  simp_to_raw using Raw₀.keys_isEmpty ⟨m, h.size_buckets_pos⟩
+  simp_to_raw using Raw₀.isEmpty_keys_eq_isEmpty ⟨m, h.size_buckets_pos⟩
 end Raw
 
 end Std.DHashMap
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index bcea7b07de89..13ab95fb5ee7 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -688,9 +688,9 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
   DHashMap.contains_keys
 
 @[simp]
-theorem keys_isEmpty [EquivBEq α] [LawfulHashable α]:
+theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α]:
     m.keys.isEmpty = m.isEmpty :=
-  DHashMap.keys_isEmpty
+  DHashMap.isEmpty_keys_eq_isEmpty
 
 end
 
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index e1ebe2dd7105..737f205778ab 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -693,9 +693,9 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
   DHashMap.Raw.contains_keys h.out
 
 @[simp]
-theorem keys_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
+theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
     m.keys.isEmpty = m.isEmpty :=
-  DHashMap.Raw.keys_isEmpty h.out
+  DHashMap.Raw.isEmpty_keys_eq_isEmpty h.out
 
 end Raw
 

From 353bbda1adf06381da32319dd8e7f1facdc2b363 Mon Sep 17 00:00:00 2001
From: monsterkrampe <monsterkrampe@users.noreply.github.com>
Date: Wed, 6 Nov 2024 09:30:58 +0100
Subject: [PATCH 10/17] Add mem_keys_iff_mem to HashMap

---
 src/Std/Data/DHashMap/Internal/RawLemmas.lean | 5 +++++
 src/Std/Data/DHashMap/Lemmas.lean             | 6 ++++++
 src/Std/Data/DHashMap/RawLemmas.lean          | 7 +++++++
 src/Std/Data/HashMap/Lemmas.lean              | 5 +++++
 src/Std/Data/HashMap/RawLemmas.lean           | 5 +++++
 5 files changed, 28 insertions(+)

diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index bc287e1e8ce0..df0af40337be 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -829,6 +829,11 @@ theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h: m.1.WF):
     m.1.keys.isEmpty = m.1.isEmpty:= by
   simp_to_model using List.isEmpty_keys_eq_isEmpty
 
+@[simp]
+theorem mem_keys_iff_contains [LawfulBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
+    k ∈ m.1.keys ↔ m.contains k := by
+  simp_to_model 
+  rw [List.containsKey_eq_keys_contains]
 
 end Raw₀
 
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index d0f2f43a1531..398fa2d5fbf4 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -958,4 +958,10 @@ theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α]:
     m.keys.isEmpty = m.isEmpty  :=
   Raw₀.isEmpty_keys_eq_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
+@[simp]
+theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] {k : α} :
+    k ∈ m.keys ↔ k ∈ m := by 
+  rw [mem_iff_contains]
+  exact Raw₀.mem_keys_iff_contains ⟨m.1, _⟩ m.2
+
 end Std.DHashMap
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index abe4a2702fa3..5754f80db9ba 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1036,6 +1036,13 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
 theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
     m.keys.isEmpty = m.isEmpty := by
   simp_to_raw using Raw₀.isEmpty_keys_eq_isEmpty ⟨m, h.size_buckets_pos⟩
+
+@[simp]
+theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+    k ∈ m.keys ↔ k ∈ m := by 
+  rw [mem_iff_contains]
+  simp_to_raw using Raw₀.mem_keys_iff_contains ⟨m, _⟩ h
+
 end Raw
 
 end Std.DHashMap
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 13ab95fb5ee7..54b68bedfb9f 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -692,6 +692,11 @@ theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α]:
     m.keys.isEmpty = m.isEmpty :=
   DHashMap.isEmpty_keys_eq_isEmpty
 
+@[simp]
+theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] {k : α} :
+    k ∈ m.keys ↔ k ∈ m := 
+  DHashMap.mem_keys_iff_mem
+
 end
 
 end Std.HashMap
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index 737f205778ab..f3ae6f2730a2 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -697,6 +697,11 @@ theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
     m.keys.isEmpty = m.isEmpty :=
   DHashMap.Raw.isEmpty_keys_eq_isEmpty h.out
 
+@[simp]
+theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+    k ∈ m.keys ↔ k ∈ m := 
+  DHashMap.Raw.mem_keys_iff_mem h.out
+
 end Raw
 
 end Std.HashMap

From 2532bb5598ebc87b67e3bf50f12044f794837b85 Mon Sep 17 00:00:00 2001
From: monsterkrampe <monsterkrampe@users.noreply.github.com>
Date: Wed, 6 Nov 2024 10:52:36 +0100
Subject: [PATCH 11/17] Add distinct_keys to HashMap

---
 src/Std/Data/DHashMap/Internal/RawLemmas.lean | 4 ++++
 src/Std/Data/DHashMap/Lemmas.lean             | 4 ++++
 src/Std/Data/DHashMap/RawLemmas.lean          | 4 ++++
 src/Std/Data/HashMap/Lemmas.lean              | 4 ++++
 src/Std/Data/HashMap/RawLemmas.lean           | 4 ++++
 5 files changed, 20 insertions(+)

diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index df0af40337be..471fca9ed8b9 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -835,6 +835,10 @@ theorem mem_keys_iff_contains [LawfulBEq α] [LawfulHashable α] (h : m.1.WF) {k
   simp_to_model 
   rw [List.containsKey_eq_keys_contains]
 
+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
+
 end Raw₀
 
 end Std.DHashMap.Internal
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 398fa2d5fbf4..a1a583f21928 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -964,4 +964,8 @@ theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] {k : α} :
   rw [mem_iff_contains]
   exact Raw₀.mem_keys_iff_contains ⟨m.1, _⟩ m.2
 
+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
+
 end Std.DHashMap
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 5754f80db9ba..f890d36423c5 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1043,6 +1043,10 @@ theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α}
   rw [mem_iff_contains]
   simp_to_raw using Raw₀.mem_keys_iff_contains ⟨m, _⟩ h
 
+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
+
 end Raw
 
 end Std.DHashMap
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 54b68bedfb9f..6f9fa63dcf8e 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -697,6 +697,10 @@ theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] {k : α} :
     k ∈ m.keys ↔ k ∈ m := 
   DHashMap.mem_keys_iff_mem
 
+theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
+    m.keys.Pairwise (fun a b => (a == b) = false) := 
+  DHashMap.distinct_keys
+
 end
 
 end Std.HashMap
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index f3ae6f2730a2..b13932fb51c7 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -702,6 +702,10 @@ theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α}
     k ∈ m.keys ↔ k ∈ m := 
   DHashMap.Raw.mem_keys_iff_mem h.out
 
+theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.keys.Pairwise (fun a b => (a == b) = false) := 
+  DHashMap.Raw.distinct_keys h.out
+
 end Raw
 
 end Std.HashMap

From dff162bdebe9fa99fc4d9054156a7ac1d78c7753 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Wed, 6 Nov 2024 16:56:50 +0100
Subject: [PATCH 12/17] fix contains_iff_mem lemma name

---
 src/Init/Data/List/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index b9b7f6c91485..956f331a277f 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -2849,7 +2849,7 @@ theorem contains_iff_exists_mem_beq [BEq α] {l : List α} {a : α} :
     l.contains a ↔ ∃ a' ∈ l, a == a' := by
   induction l <;> simp_all
 
-theorem List.contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
+theorem contains_iff_mem [BEq α] [LawfulBEq α] {l : List α} {a : α} :
     l.contains a ↔ a ∈ l := by
   simp
 

From bfebae8f7aba96d5b0ce6abe4e1d43fad162277c Mon Sep 17 00:00:00 2001
From: jt0202 <johannes.tantow@gmail.com>
Date: Wed, 6 Nov 2024 17:38:12 +0100
Subject: [PATCH 13/17] Added toList lemmas for HashSet

---
 src/Std/Data/HashSet/Lemmas.lean    | 22 ++++++++++++++++++++++
 src/Std/Data/HashSet/RawLemmas.lean | 23 +++++++++++++++++++++++
 2 files changed, 45 insertions(+)

diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index 972990cbef84..4aa626725aef 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -353,6 +353,28 @@ theorem containsThenInsert_fst {k : α} : (m.containsThenInsert k).1 = m.contain
 theorem containsThenInsert_snd {k : α} : (m.containsThenInsert k).2 = m.insert k :=
   ext HashMap.containsThenInsertIfNew_snd
 
+@[simp]
+theorem toList_length_eq_size [EquivBEq α] [LawfulHashable α] : m.toList.length = m.size :=
+  HashMap.length_keys_eq_size
+
+@[simp]
+theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α}:
+    m.toList.contains k = m.contains k :=
+  HashMap.contains_keys
+
+@[simp]
+theorem isEmpty_toList_eq_isEmpty [EquivBEq α] [LawfulHashable α] :
+    m.toList.isEmpty = m.isEmpty :=
+  HashMap.isEmpty_keys_eq_isEmpty
+
+@[simp]
+theorem mem_toList_iff_mem [LawfulBEq α] [LawfulHashable α]  {k : α}:
+    k ∈ m.toList ↔ k ∈ m :=
+  HashMap.mem_keys_iff_mem
+
+theorem distinct_toList [EquivBEq α] [LawfulHashable α]:
+    m.toList.Pairwise (fun a b => (a == b) = false) :=
+  HashMap.distinct_keys
 end
 
 end Std.HashSet
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index 43edb645fa7d..f652c3a081fe 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -366,6 +366,29 @@ theorem containsThenInsert_fst (h : m.WF) {k : α} : (m.containsThenInsert k).1
 theorem containsThenInsert_snd (h : m.WF) {k : α} : (m.containsThenInsert k).2 = m.insert k :=
   ext (HashMap.Raw.containsThenInsertIfNew_snd h.out)
 
+@[simp]
+theorem toList_length_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF): m.toList.length = m.size :=
+  HashMap.Raw.length_keys_eq_size h.1
+
+@[simp]
+theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α} (h : m.WF):
+    m.toList.contains k = m.contains k :=
+  HashMap.Raw.contains_keys h.1
+
+@[simp]
+theorem isEmpty_toList_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.toList.isEmpty = m.isEmpty :=
+  HashMap.Raw.isEmpty_keys_eq_isEmpty h.1
+
+@[simp]
+theorem mem_toList_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α}:
+    k ∈ m.toList ↔ k ∈ m :=
+  HashMap.Raw.mem_keys_iff_mem h.1
+
+theorem distinct_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toList.Pairwise (fun a b => (a == b) = false) :=
+  HashMap.Raw.distinct_keys h.1
+
 end Raw
 
 end Std.HashSet

From 4f4d7aa1ae6275b8a3cdda0439b8d65d6810e517 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Thu, 7 Nov 2024 08:12:49 +0100
Subject: [PATCH 14/17] Clean up proofs in WF.lean

---
 .../DHashMap/Internal/AssocList/Lemmas.lean   |  5 ++
 src/Std/Data/DHashMap/Internal/WF.lean        | 67 +++++++------------
 2 files changed, 29 insertions(+), 43 deletions(-)

diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
index 866208b00789..39f299727acc 100644
--- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
@@ -199,4 +199,9 @@ theorem toList_filter {f : (a : α) → β a → Bool} {l : AssocList α β} :
     · exact (ih _).trans (by simpa using perm_middle.symm)
     · exact ih _
 
+theorem foldl_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a → δ) :
+    l.foldl (fun acc k v => f k v :: acc) acc =
+      (l.toList.map (fun p => f p.1 p.2)).reverse ++ acc := by
+  induction l generalizing acc <;> simp_all [AssocList.foldl, AssocList.foldlM, Id.run]
+
 end Std.DHashMap.Internal.AssocList
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 39aa7c0e50b7..f72c379904b3 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -59,55 +59,36 @@ theorem isEmpty_eq_isEmpty [BEq α] [Hashable α] {m : Raw α β} (h : Raw.WFImp
   rw [Raw.isEmpty, Bool.eq_iff_iff, List.isEmpty_iff_length_eq_zero, size_eq_length h,
     Nat.beq_eq_true_eq]
 
-theorem AssocList.foldlM_apply {l : AssocList α β} {acc : List γ} (f : (a : α) → β a → γ) :
-    l.foldlM (m := Id) (fun acc k v => f k v :: acc) acc =
-      (l.toList.map (fun p => f p.1 p.2)).reverse ++ acc := by
-  induction l generalizing acc <;> simp_all [AssocList.foldlM]
+theorem fold_eq {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} :
+    l.fold f init = l.buckets.foldl (fun acc l => l.foldl f acc) init := by
+  simp only [Raw.fold, Raw.foldM, Array.foldlM_eq_foldlM_toList, Array.foldl_eq_foldl_toList,
+    ← List.foldl_eq_foldlM, Id.run, AssocList.foldl]
+
+theorem fold_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β a → γ) :
+    l.fold (fun acc k v => f k v :: acc) acc =
+      ((toListModel l.buckets).reverse.map (fun p => f p.1 p.2)) ++ acc := by
+  rw [fold_eq, Array.foldl_eq_foldl_toList, toListModel]
+  generalize l.buckets.toList = l
+  induction l generalizing acc with
+  | nil => simp
+  | cons x xs ih =>
+      rw [foldl_cons, ih, AssocList.foldl_apply]
+      simp
 
-theorem AssocList.foldlM_cons {l : AssocList α β} {acc : List ((a : α) × β a)} :
-    l.foldlM (m := Id) (fun acc k v => ⟨k, v⟩ :: acc) acc = l.toList.reverse ++ acc := by
-  simp [AssocList.foldlM_apply]
+theorem fold_cons {l : Raw α β} {acc : List ((a : α) × β a)} :
+    l.fold (fun acc k v => ⟨k, v⟩ :: acc) acc = (toListModel l.buckets).reverse ++ acc := by
+  simp [fold_cons_apply]
 
-theorem AssocList.foldlM_cons_key {l : AssocList α β} {acc : List α} :
-    l.foldlM (m := Id) (fun acc k _ => k :: acc) acc = (List.keys l.toList).reverse ++ acc := by
-  rw [AssocList.foldlM_apply, keys_eq_map]
+theorem fold_cons_key {l : Raw α β} {acc : List α} :
+    l.fold (fun acc k _ => k :: acc) acc = List.keys (toListModel l.buckets).reverse ++ acc := by
+  rw [fold_cons_apply, keys_eq_map, map_reverse]
 
--- TODO (Markus): clean up
 theorem toList_perm_toListModel {m : Raw α β} : Perm m.toList (toListModel m.buckets) := by
-  rw [Raw.toList, toListModel, List.flatMap_eq_foldl, Raw.fold, Raw.foldM,
-    Array.foldlM_eq_foldlM_toList, ← List.foldl_eq_foldlM, Id.run]
-  simp only [AssocList.foldlM_cons]
-  suffices ∀ (l : List (AssocList α β)) (l₁ l₂), Perm l₁ l₂ →
-      Perm (l.foldl (fun acc m => m.toList.reverse ++ acc) l₁)
-        (l.foldl (fun acc m => acc ++ m.toList) l₂) by
-    simpa using this m.buckets.toList [] [] (Perm.refl _)
-  intros l l₁ l₂ h
-  induction l generalizing l₁ l₂
-  · simpa
-  · next l t ih =>
-    simp only [foldl_cons]
-    apply ih
-    refine (reverse_perm _).append_right _ |>.trans perm_append_comm |>.trans ?_
-    exact h.append_right l.toList
-
--- TODO (Markus): clean up
+  simp [Raw.toList, fold_cons]
+
 theorem keys_perm_keys_toListModel {m : Raw α β} :
     Perm m.keys (List.keys (toListModel m.buckets)) := by
-  rw [Raw.keys, List.keys_eq_map]
-  refine Perm.trans ?_ (toList_perm_toListModel.map _)
-  simp only [Raw.toList, Raw.fold, Raw.foldM, Array.foldlM_eq_foldlM_toList, ← List.foldl_eq_foldlM,
-    Id.run]
-  generalize m.buckets.toList = l
-  suffices ∀ l', foldl
-      (fun acc l => AssocList.foldlM (m := Id) (fun acc k x => k :: acc) acc l) (l'.map (·.1)) l =
-      map Sigma.fst (foldl
-        (fun acc l => AssocList.foldlM (m := Id) (fun acc k v => ⟨k, v⟩ :: acc) acc l) l' l) from
-    this [] ▸ Perm.refl _
-  intro l'
-  simp [AssocList.foldlM_cons, AssocList.foldlM_cons_key]
-  induction l generalizing l' with
-  | nil => simp
-  | cons h t ih => simp [List.keys_eq_map, ← ih]
+  simp [Raw.keys, fold_cons_key, keys_eq_map]
 
 theorem length_keys_eq_length_keys {m : Raw α β} :
     m.keys.length = (List.keys (toListModel m.buckets)).length :=

From 01b95c3e23fd01d7fbce91e6f480f7655c3c6881 Mon Sep 17 00:00:00 2001
From: monsterkrampe <monsterkrampe@users.noreply.github.com>
Date: Fri, 8 Nov 2024 06:32:00 +0100
Subject: [PATCH 15/17] Rename results around HashMap keys method

---
 src/Std/Data/DHashMap/Internal/RawLemmas.lean | 14 +++++++-------
 src/Std/Data/DHashMap/Lemmas.lean             | 18 +++++++++---------
 src/Std/Data/DHashMap/RawLemmas.lean          | 18 +++++++++---------
 src/Std/Data/HashMap/Lemmas.lean              | 18 +++++++++---------
 src/Std/Data/HashMap/RawLemmas.lean           | 18 +++++++++---------
 src/Std/Data/HashSet/Lemmas.lean              | 19 ++++++++++---------
 src/Std/Data/HashSet/RawLemmas.lean           | 19 ++++++++++---------
 7 files changed, 63 insertions(+), 61 deletions(-)

diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index 471fca9ed8b9..837b6c76545c 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -815,22 +815,22 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
     m.1.keys.length = m.1.size := by
   simp_to_model using List.length_keys_eq_length
 
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α] (h: m.1.WF):
+    m.1.keys.isEmpty = m.1.isEmpty:= by
+  simp_to_model using List.isEmpty_keys_eq_isEmpty
+
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
     m.1.keys.contains k = m.contains k := by
   simp_to_model using List.containsKey_eq_keys_contains.symm
 
 @[simp]
-theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h: m.1.WF):
-    m.1.keys.isEmpty = m.1.isEmpty:= by
-  simp_to_model using List.isEmpty_keys_eq_isEmpty
-
-@[simp]
-theorem mem_keys_iff_contains [LawfulBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
     k ∈ m.1.keys ↔ m.contains k := by
   simp_to_model 
   rw [List.containsKey_eq_keys_contains]
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index a1a583f21928..e6016179028c 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -944,9 +944,14 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] :
+theorem length_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.length = m.size :=
-  Raw₀.length_keys_eq_size ⟨m.1, m.2.size_buckets_pos⟩ m.2
+  Raw₀.length_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α]:
+    m.keys.isEmpty = m.isEmpty  :=
+  Raw₀.isEmpty_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
@@ -954,15 +959,10 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
   Raw₀.contains_keys ⟨m.1, _⟩ m.2
 
 @[simp]
-theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α]:
-    m.keys.isEmpty = m.isEmpty  :=
-  Raw₀.isEmpty_keys_eq_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2
-
-@[simp]
-theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] {k : α} :
     k ∈ m.keys ↔ k ∈ m := by 
   rw [mem_iff_contains]
-  exact Raw₀.mem_keys_iff_contains ⟨m.1, _⟩ m.2
+  exact Raw₀.mem_keys ⟨m.1, _⟩ m.2
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) := 
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index f890d36423c5..42d4db498753 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1023,9 +1023,14 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.length = m.size := by
-  simp_to_raw using Raw₀.length_keys_eq_size ⟨m, h.size_buckets_pos⟩ h
+  simp_to_raw using Raw₀.length_keys ⟨m, h.size_buckets_pos⟩ h
+
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.keys.isEmpty = m.isEmpty := by
+  simp_to_raw using Raw₀.isEmpty_keys ⟨m, h.size_buckets_pos⟩
 
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
@@ -1033,15 +1038,10 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
   simp_to_raw using Raw₀.contains_keys ⟨m, _⟩ h
 
 @[simp]
-theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
-    m.keys.isEmpty = m.isEmpty := by
-  simp_to_raw using Raw₀.isEmpty_keys_eq_isEmpty ⟨m, h.size_buckets_pos⟩
-
-@[simp]
-theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     k ∈ m.keys ↔ k ∈ m := by 
   rw [mem_iff_contains]
-  simp_to_raw using Raw₀.mem_keys_iff_contains ⟨m, _⟩ h
+  simp_to_raw using Raw₀.mem_keys ⟨m, _⟩ h
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.Pairwise (fun a b => (a == b) = false) := by
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 6f9fa63dcf8e..077a51c74b02 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -678,9 +678,14 @@ instance [EquivBEq α] [LawfulHashable α] : LawfulGetElem (HashMap α β) α β
     split <;> simp_all
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] :
+theorem length_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.length = m.size :=
-  DHashMap.length_keys_eq_size
+  DHashMap.length_keys
+
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α]:
+    m.keys.isEmpty = m.isEmpty :=
+  DHashMap.isEmpty_keys
 
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
@@ -688,14 +693,9 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
   DHashMap.contains_keys
 
 @[simp]
-theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α]:
-    m.keys.isEmpty = m.isEmpty :=
-  DHashMap.isEmpty_keys_eq_isEmpty
-
-@[simp]
-theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] {k : α} :
     k ∈ m.keys ↔ k ∈ m := 
-  DHashMap.mem_keys_iff_mem
+  DHashMap.mem_keys
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) := 
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index b13932fb51c7..cc0816a966c7 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -683,9 +683,14 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
   ext (DHashMap.Raw.Const.getThenInsertIfNew?_snd h.out)
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.length = m.size :=
-  DHashMap.Raw.length_keys_eq_size h.out
+  DHashMap.Raw.length_keys h.out
+
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.keys.isEmpty = m.isEmpty :=
+  DHashMap.Raw.isEmpty_keys h.out
 
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
@@ -693,14 +698,9 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
   DHashMap.Raw.contains_keys h.out
 
 @[simp]
-theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
-    m.keys.isEmpty = m.isEmpty :=
-  DHashMap.Raw.isEmpty_keys_eq_isEmpty h.out
-
-@[simp]
-theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     k ∈ m.keys ↔ k ∈ m := 
-  DHashMap.Raw.mem_keys_iff_mem h.out
+  DHashMap.Raw.mem_keys h.out
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.Pairwise (fun a b => (a == b) = false) := 
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index 4aa626725aef..b0318c0f47ce 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -354,8 +354,14 @@ theorem containsThenInsert_snd {k : α} : (m.containsThenInsert k).2 = m.insert
   ext HashMap.containsThenInsertIfNew_snd
 
 @[simp]
-theorem toList_length_eq_size [EquivBEq α] [LawfulHashable α] : m.toList.length = m.size :=
-  HashMap.length_keys_eq_size
+theorem length_toList [EquivBEq α] [LawfulHashable α] : 
+    m.toList.length = m.size :=
+  HashMap.length_keys
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.isEmpty = m.isEmpty :=
+  HashMap.isEmpty_keys
 
 @[simp]
 theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α}:
@@ -363,14 +369,9 @@ theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α}:
   HashMap.contains_keys
 
 @[simp]
-theorem isEmpty_toList_eq_isEmpty [EquivBEq α] [LawfulHashable α] :
-    m.toList.isEmpty = m.isEmpty :=
-  HashMap.isEmpty_keys_eq_isEmpty
-
-@[simp]
-theorem mem_toList_iff_mem [LawfulBEq α] [LawfulHashable α]  {k : α}:
+theorem mem_toList [LawfulBEq α] [LawfulHashable α]  {k : α}:
     k ∈ m.toList ↔ k ∈ m :=
-  HashMap.mem_keys_iff_mem
+  HashMap.mem_keys
 
 theorem distinct_toList [EquivBEq α] [LawfulHashable α]:
     m.toList.Pairwise (fun a b => (a == b) = false) :=
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index f652c3a081fe..77dcaa5bcfd8 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -367,8 +367,14 @@ theorem containsThenInsert_snd (h : m.WF) {k : α} : (m.containsThenInsert k).2
   ext (HashMap.Raw.containsThenInsertIfNew_snd h.out)
 
 @[simp]
-theorem toList_length_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF): m.toList.length = m.size :=
-  HashMap.Raw.length_keys_eq_size h.1
+theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF): 
+    m.toList.length = m.size :=
+  HashMap.Raw.length_keys h.1
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.toList.isEmpty = m.isEmpty :=
+  HashMap.Raw.isEmpty_keys h.1
 
 @[simp]
 theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α} (h : m.WF):
@@ -376,14 +382,9 @@ theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α} (h : m.WF):
   HashMap.Raw.contains_keys h.1
 
 @[simp]
-theorem isEmpty_toList_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
-    m.toList.isEmpty = m.isEmpty :=
-  HashMap.Raw.isEmpty_keys_eq_isEmpty h.1
-
-@[simp]
-theorem mem_toList_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α}:
+theorem mem_toList [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α}:
     k ∈ m.toList ↔ k ∈ m :=
-  HashMap.Raw.mem_keys_iff_mem h.1
+  HashMap.Raw.mem_keys h.1
 
 theorem distinct_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.Pairwise (fun a b => (a == b) = false) :=

From 32b351e920513842870f369bec2db55d3d2ba75b Mon Sep 17 00:00:00 2001
From: jt0202 <johannes.tantow@gmail.com>
Date: Fri, 8 Nov 2024 07:46:48 +0100
Subject: [PATCH 16/17] Move HashMap.keys/HashSet.toList and predecessors out
 of unverified section

---
 src/Std/Data/DHashMap/Basic.lean |  6 +++---
 src/Std/Data/DHashMap/Raw.lean   | 10 +++++++---
 src/Std/Data/HashMap/Basic.lean  |  6 ++++--
 src/Std/Data/HashMap/Raw.lean    |  6 +++---
 src/Std/Data/HashSet/Basic.lean  |  8 +++++---
 src/Std/Data/HashSet/Raw.lean    |  7 ++++---
 6 files changed, 26 insertions(+), 17 deletions(-)

diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean
index 125111fe2287..9f9b26ef73b0 100644
--- a/src/Std/Data/DHashMap/Basic.lean
+++ b/src/Std/Data/DHashMap/Basic.lean
@@ -177,6 +177,9 @@ end
 @[inline, inherit_doc Raw.isEmpty] def isEmpty (m : DHashMap α β) : Bool :=
   m.1.isEmpty
 
+@[inline, inherit_doc Raw.keys] def keys (m : DHashMap α β) : List α :=
+  m.1.keys
+
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -232,9 +235,6 @@ instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) wh
     (m : DHashMap α (fun _ => β)) : Array (α × β) :=
   Raw.Const.toArray m.1
 
-@[inline, inherit_doc Raw.keys] def keys (m : DHashMap α β) : List α :=
-  m.1.keys
-
 @[inline, inherit_doc Raw.keysArray] def keysArray (m : DHashMap α β) :
     Array α :=
   m.1.keysArray
diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean
index 08bbc72035e0..db64b6b5854c 100644
--- a/src/Std/Data/DHashMap/Raw.lean
+++ b/src/Std/Data/DHashMap/Raw.lean
@@ -291,6 +291,8 @@ to get anything out of the hash map.
 @[inline] def isEmpty (m : Raw α β) : Bool :=
   m.size == 0
 
+
+
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -358,9 +360,7 @@ instance : ForIn m (Raw α β) ((a : α) × β a) where
     Array (α × β) :=
   m.fold (fun acc k v => acc.push ⟨k, v⟩) #[]
 
-/-- Returns a list of all keys present in the hash map in some order. -/
-@[inline] def keys (m : Raw α β) : List α :=
-  m.fold (fun acc k _ => k :: acc) []
+
 
 /-- Returns an array of all keys present in the hash map in some order. -/
 @[inline] def keysArray (m : Raw α β) : Array α :=
@@ -447,6 +447,10 @@ instance [Repr α] [(a : α) → Repr (β a)] : Repr (Raw α β) where
 
 end Unverified
 
+/-- Returns a list of all keys present in the hash map in some order. -/
+@[inline] def keys (m : Raw α β) : List α :=
+  m.fold (fun acc k _ => k :: acc) []
+
 section WF
 
 /--
diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean
index 8156f10bbc5f..da1680acbb79 100644
--- a/src/Std/Data/HashMap/Basic.lean
+++ b/src/Std/Data/HashMap/Basic.lean
@@ -188,6 +188,9 @@ instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a 
 @[inline, inherit_doc DHashMap.isEmpty] def isEmpty (m : HashMap α β) : Bool :=
   m.inner.isEmpty
 
+@[inline, inherit_doc DHashMap.keys] def keys (m : HashMap α β) : List α :=
+  m.inner.keys
+
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -231,8 +234,7 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
     Array (α × β) :=
   DHashMap.Const.toArray m.inner
 
-@[inline, inherit_doc DHashMap.keys] def keys (m : HashMap α β) : List α :=
-  m.inner.keys
+
 
 @[inline, inherit_doc DHashMap.keysArray] def keysArray (m : HashMap α β) :
     Array α :=
diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean
index 825ce0a314ed..07cfe66dbb19 100644
--- a/src/Std/Data/HashMap/Raw.lean
+++ b/src/Std/Data/HashMap/Raw.lean
@@ -170,6 +170,9 @@ instance [BEq α] [Hashable α] : GetElem? (Raw α β) α β (fun m a => a ∈ m
 @[inline, inherit_doc DHashMap.Raw.isEmpty] def isEmpty (m : Raw α β) : Bool :=
   m.inner.isEmpty
 
+@[inline, inherit_doc DHashMap.Raw.keys] def keys (m : Raw α β) : List α :=
+  m.inner.keys
+
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -213,9 +216,6 @@ instance {m : Type w → Type w} : ForIn m (Raw α β) (α × β) where
 @[inline, inherit_doc DHashMap.Raw.Const.toArray] def toArray (m : Raw α β) : Array (α × β) :=
   DHashMap.Raw.Const.toArray m.inner
 
-@[inline, inherit_doc DHashMap.Raw.keys] def keys (m : Raw α β) : List α :=
-  m.inner.keys
-
 @[inline, inherit_doc DHashMap.Raw.keysArray] def keysArray (m : Raw α β) : Array α :=
   m.inner.keysArray
 
diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean
index 762ea2f11306..e684257282f6 100644
--- a/src/Std/Data/HashSet/Basic.lean
+++ b/src/Std/Data/HashSet/Basic.lean
@@ -154,6 +154,11 @@ for all `a`.
 @[inline] def isEmpty (m : HashSet α) : Bool :=
   m.inner.isEmpty
 
+/-- Transforms the hash set into a list of elements in some order. -/
+@[inline] def toList (m : HashSet α) : List α :=
+  m.inner.keys
+
+
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -208,9 +213,6 @@ instance [BEq α] [Hashable α] {m : Type v → Type v} : ForIn m (HashSet α) 
     if p a then return true
   return false
 
-/-- Transforms the hash set into a list of elements in some order. -/
-@[inline] def toList (m : HashSet α) : List α :=
-  m.inner.keys
 
 /-- Transforms the hash set into an array of elements in some order. -/
 @[inline] def toArray (m : HashSet α) : Array α :=
diff --git a/src/Std/Data/HashSet/Raw.lean b/src/Std/Data/HashSet/Raw.lean
index 6becfc534f20..c4f506ffdfec 100644
--- a/src/Std/Data/HashSet/Raw.lean
+++ b/src/Std/Data/HashSet/Raw.lean
@@ -157,6 +157,10 @@ for all `a`.
 @[inline] def isEmpty (m : Raw α) : Bool :=
   m.inner.isEmpty
 
+/-- Transforms the hash set into a list of elements in some order. -/
+@[inline] def toList (m : Raw α) : List α :=
+  m.inner.keys
+
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -206,9 +210,6 @@ instance {m : Type v → Type v} : ForIn m (Raw α) α where
     if p a then return true
   return false
 
-/-- Transforms the hash set into a list of elements in some order. -/
-@[inline] def toList (m : Raw α) : List α :=
-  m.inner.keys
 
 /-- Transforms the hash set into an array of elements in some order. -/
 @[inline] def toArray (m : Raw α) : Array α :=

From bd99de0e4cf24e951a6953ccddab06f42aee9041 Mon Sep 17 00:00:00 2001
From: jt0202 <johannes.tantow@gmail.com>
Date: Fri, 8 Nov 2024 08:03:29 +0100
Subject: [PATCH 17/17] Removed unnecessary white spaces

---
 src/Std/Data/DHashMap/Raw.lean  | 4 ----
 src/Std/Data/HashMap/Basic.lean | 2 --
 src/Std/Data/HashSet/Basic.lean | 1 -
 3 files changed, 7 deletions(-)

diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean
index db64b6b5854c..4e1bbd1a4044 100644
--- a/src/Std/Data/DHashMap/Raw.lean
+++ b/src/Std/Data/DHashMap/Raw.lean
@@ -291,8 +291,6 @@ to get anything out of the hash map.
 @[inline] def isEmpty (m : Raw α β) : Bool :=
   m.size == 0
 
-
-
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -360,8 +358,6 @@ instance : ForIn m (Raw α β) ((a : α) × β a) where
     Array (α × β) :=
   m.fold (fun acc k v => acc.push ⟨k, v⟩) #[]
 
-
-
 /-- Returns an array of all keys present in the hash map in some order. -/
 @[inline] def keysArray (m : Raw α β) : Array α :=
   m.fold (fun acc k _ => acc.push k) #[]
diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean
index da1680acbb79..5fd777e386c9 100644
--- a/src/Std/Data/HashMap/Basic.lean
+++ b/src/Std/Data/HashMap/Basic.lean
@@ -234,8 +234,6 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
     Array (α × β) :=
   DHashMap.Const.toArray m.inner
 
-
-
 @[inline, inherit_doc DHashMap.keysArray] def keysArray (m : HashMap α β) :
     Array α :=
   m.inner.keysArray
diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean
index e684257282f6..55d529ec0ab5 100644
--- a/src/Std/Data/HashSet/Basic.lean
+++ b/src/Std/Data/HashSet/Basic.lean
@@ -158,7 +158,6 @@ for all `a`.
 @[inline] def toList (m : HashSet α) : List α :=
   m.inner.keys
 
-
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/