chore: push work

Author: wkrozowski

src/Std/Data/DHashMap/Internal/RawLemmas.lean

@@ -2754,12 +2754,16 @@ theorem get?_union_of_contains_right_eq_false [LawfulBEq α] (h₁ : m₁.val.WF
   revert contains_eq_false
   simp_to_model [union, get?, contains]
   intro contains_eq_false
+  apply List.getValue?_insertSmallerList_of_contains_eq_false
+  exact contains_eq_false
 
 
 theorem get_union_of_contains_right_eq_false [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF)
     {k : α} (contains_eq_false : m₂.contains k = false) {h'} :
     (m₁.union m₂).get k h' = m₁.get k (contains_of_contains_union_of_contains_right_eq_false h₁ h₂ h' contains_eq_false) := by
-  sorry
+  revert contains_eq_false
+  simp_to_model [union, get]
+  intro contains_eq_false
 
 theorem union_insert_right_equiv_union_insert [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a}
     (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) :
@@ -2842,7 +2846,7 @@ theorem getKeyD_union_of_mem_left_of_contains_right_eq_false [EquivBEq α]
 theorem size_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF)
     (h₂ : m₂.val.WF) : (∀ (a : α), m₁.contains a → m₂.contains a = false) →
     (m₁.union m₂).1.size = m₁.1.size + m₂.1.size := by
-  sorry
+  simp_to_model [union, size]
 
 theorem size_left_le_size_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF)
     (h₂ : m₂.val.WF) : m₁.1.size ≤ (m₁.union m₂).1.size := by

src/Std/Data/Internal/List/Associative.lean

@@ -3218,6 +3218,15 @@ theorem getValue?_insertSmallerList_of_contains_eq_false [BEq α] [PartialEquivB
   case isFalse =>
     simp only [containsKey_eq_contains_map_fst] at not_contains
     simp [getValueCast?_insertList_of_contains_eq_false not_contains]
+
+theorem getValue_insertSmallerList_of_contains_eq_false [BEq α] [PartialEquivBEq α] [LawfulBEq α]
+    {l toInsert : List ((a : α) × β a)} {k : α}
+    (not_contains : containsKey k toInsert = false)
+    {p1 : containsKey k (insertSmallerList l toInsert) = true}
+    {p2 : containsKey k l = true}:
+    getValueCast k (insertSmallerList l toInsert) p1  = getValueCast k l p2  := by
+      sorry
+
 section
 
 variable {β : Type v}