From 8340caf43d2a5fa380ef103e8a5fabd45d4fca7f Mon Sep 17 00:00:00 2001
From: jt0202 <johannes.tantow@gmail.com>
Date: Mon, 2 Dec 2024 16:01:48 +0100
Subject: [PATCH] get results for insertManyIfNewUnit

---
 .../DHashMap/Internal/List/Associative.lean   | 50 +++++++++++++++++++
 src/Std/Data/DHashMap/Internal/RawLemmas.lean | 23 ++++++++-
 2 files changed, 71 insertions(+), 2 deletions(-)

diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean
index 2ffb77e16242..5cd62bae40d3 100644
--- a/src/Std/Data/DHashMap/Internal/List/Associative.lean
+++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean
@@ -3051,5 +3051,55 @@ theorem insertListIfNewUnit_isEmpty [BEq α]
     apply ne_true_of_eq_false
     apply insertListIfNewUnit_not_isEmpty_if_start_not_isEmpty
     simp
+
+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
+  | cons hd tl ih =>
+    simp only [getValue?, containsKey, Bool.or_eq_true, Bool.cond_eq_ite_iff]
+    by_cases hd_k: (hd.fst == k) = true
+    · simp [hd_k]
+    · simp [hd_k, ih]
+
+theorem getValue_list_unit [BEq α] {l : List ((_ : α) × Unit)} {k : α} {h}:
+    getValue k l h = ()  := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih => simp
+
+theorem getValue!_list_unit [BEq α] {l : List ((_ : α) × Unit)} {k : α} :
+    getValue! k l = ()  := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih => simp
+
+theorem getValueD_list_unit [BEq α] {l : List ((_ : α) × Unit)} {k : α} {fallback : Unit} :
+    getValueD k l fallback = ()  := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih => simp
+
+theorem getValue?_insertListIfNewUnit [BEq α] [PartialEquivBEq α]
+    {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}:
+    getValue? k (insertListIfNewUnit l toInsert) =
+    if (containsKey k l || toInsert.contains k) then some () else none := by
+  simp [← containsKey_insertListIfNewUnit, getValue?_list_unit]
+
+theorem getValue_insertListIfNewUnit [BEq α] [PartialEquivBEq α]
+    {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} {h}:
+    getValue k (insertListIfNewUnit l toInsert) h = ()  := by
+  rw [getValue_list_unit]
+
+theorem getValue!_insertListIfNewUnit [BEq α] [PartialEquivBEq α]
+    {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} :
+    getValue! k (insertListIfNewUnit l toInsert) = ()  := by
+  rw [getValue!_list_unit]
+
+theorem getValueD_insertListIfNewUnit [BEq α] [PartialEquivBEq α]
+    {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} {fallback : Unit}:
+    getValueD k (insertListIfNewUnit l toInsert) fallback = () := by
+  rw [getValueD_list_unit]
+
 end
 end List
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index a50052e73437..fd574828cfec 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -1212,7 +1212,6 @@ theorem getD_insertMany_list_mem_const [EquivBEq α] [LawfulHashable α]
     getD (insertMany m l).1 k' fallback = v := by
   simp_to_model using getValueD_insertListConst_mem
 
-
 variable (m: Raw₀ α (fun _ => Unit))
 
 @[simp]
@@ -1283,7 +1282,6 @@ theorem getKey!_insertManyIfNewUnit_list_not_mem [EquivBEq α] [LawfulHashable 
     getKey! (insertManyIfNewUnit m l).1 k = getKey! m k := by
   simp_to_model using getKey!_insertListIfNewUnit_not_mem
 
-
 theorem getKey!_insertManyIfNewUnit_list_mem [EquivBEq α] [LawfulHashable α] [Inhabited α]
     {l : List α} {k k' : α} {k_beq : k == k'}
     {distinct : l.Pairwise (fun a b => (a == b) = false)}
@@ -1335,6 +1333,27 @@ theorem insertManyIfNewUnit_list_isEmpty [EquivBEq α] [LawfulHashable α]
     (insertManyIfNewUnit m l).1.1.isEmpty ↔ m.1.isEmpty ∧ l.isEmpty := by
   simp_to_model using insertListIfNewUnit_isEmpty
 
+theorem get?_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α]
+    {l : List α} {k : α} (h : m.1.WF) :
+    get? (insertManyIfNewUnit m l).1 k =
+    if ( m.contains k || l.contains k) then some () else none := by
+  simp_to_model using getValue?_insertListIfNewUnit
+
+theorem getValue_insertManyIfNewUnit_list
+    {l : List α} {k : α} {h} :
+    get (insertManyIfNewUnit m l).1 k h = ()  := by
+  simp
+
+theorem getValue!_insertManyIfNewUnit_list
+    {l : List α} {k : α} :
+    get! (insertManyIfNewUnit m l).1 k = ()  := by
+  simp
+
+theorem getValueD_insertManyIfNewUnit_list
+    {l : List α} {k : α} {fallback : Unit} :
+    getD (insertManyIfNewUnit m l).1 k fallback = () := by
+  simp
+
 end Const
 end
 end Raw₀