chore: refactor

Author: wkrozowski

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

@@ -2699,22 +2699,12 @@ theorem union_insert_emptyWithCapacity {k : α} {v : β k} [EquivBEq α] [Lawful
 theorem contains_union_of_left  [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF)
     (h₂ : m₂.val.WF) {k : α} :
     m₁.contains k → (m₁.union m₂).contains k := by
-  simp_to_model [contains, union]
-  simp only [List.containsKey_insertSmallerList]
-  intro h
-  simp only [Bool.or_eq_true]
-  apply Or.inl
-  exact h
+  simp_to_model [contains, union] using List.contains_insertSmallerList_of_left
 
 theorem contains_union_of_right  [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF)
     (h₂ : m₂.val.WF) {k : α} :
     m₂.contains k → (m₁.union m₂).contains k := by
-  simp_to_model [contains, union]
-  simp only [List.containsKey_insertSmallerList]
-  intro h
-  simp only [Bool.or_eq_true]
-  apply Or.inr
-  exact h
+  simp_to_model [contains, union] using List.contains_insertSmallerList_of_right
 
 @[simp]
 theorem contains_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF)
@@ -2726,51 +2716,33 @@ theorem contains_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF)
 theorem contains_union_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF)
     (h₂ : m₂.val.WF) {k : α} :
     (m₁.union m₂).contains k ↔ m₁.contains k ∨ m₂.contains k := by
-  apply Iff.trans
-  rotate_left
-  . apply iff_of_eq
-    apply Bool.or_eq_true
-  . rw [Bool.coe_iff_coe]
-    apply contains_union h₁ h₂
+  simp_to_model [union, contains] using List.contains_insertSmallerList_iff
 
 theorem contains_of_contains_union_of_contains_right_eq_false [EquivBEq α]
     [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} :
     (m₁.union m₂).contains k → m₂.contains k = false → m₁.contains k := by
-  intro h₃ h₄
-  apply Or.elim <| (@contains_union_iff α β _ _ _ _ _ _ h₁ h₂ k).1 h₃
-  . simp only [imp_self]
-  . intro n
-    rw [n] at h₄
-    contradiction
+  simp_to_model [union, contains] using List.contains_of_contains_insertSmallerList_of_contains_right_eq_false
 
 theorem contains_of_contains_union_of_contains_left_eq_false [EquivBEq α]
     [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} :
     (m₁.union m₂).contains k → m₁.contains k = false → m₂.contains k := by
-  intro h₃ h₄
-  apply Or.elim <| (@contains_union_iff α β _ _ _ _ _ _ h₁ h₂ k).1 h₃
-  . intro n
-    rw [n] at h₄
-    contradiction
-  . simp only [imp_self]
+  simp_to_model [union, contains] using List.contains_of_contains_insertSmallerList_of_contains_left_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) :
     (m₁.union m₂).get? k = m₁.get? k := by
   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
-
+  apply List.getValue?_insertSmallerList_of_contains_eq_false 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
   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
+  apply List.getValue_insertSmallerList_of_contains_eq_false contains_eq_false
 
 theorem union_insert_right_equiv_union_insert [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a}
     (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) :
@@ -2793,7 +2765,13 @@ theorem getKey!_union_of_contains_right_eq_false [Inhabited α]
     [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α}
     (h' : m₂.contains k = false) :
     (m₁.union m₂).getKey! k = m₁.getKey! k := by
+  simp_to_model
+  simp only [List.getKey!_eq_getKey?]
+  apply Option.get!.congr_simp
+  simp only [List.getKey?_eq_getEntry?]
+  congr 1
   sorry
+  --rw [List.getEntry?_eq_getValueCast?]
 
 theorem getKey!_union_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.1.WF)
     (h₂ : m₂.1.WF) {k : α} (mem : m₂.contains k) :

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

@@ -3056,6 +3056,32 @@ theorem containsKey_insertSmallerList [BEq α] [PartialEquivBEq α] {l₁ l₂ :
   · rw [containsKey_insertListIfNew, ← containsKey_eq_contains_map_fst, Bool.or_comm]
   · rw [containsKey_insertList, ← containsKey_eq_contains_map_fst]
 
+theorem contains_insertSmallerList_iff [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} :
+    containsKey k (insertSmallerList l toInsert) = true ↔ containsKey k l = true ∨ containsKey k toInsert = true := by
+  simp only [containsKey_insertSmallerList, Bool.or_eq_true]
+
+theorem contains_of_contains_insertSmallerList_of_contains_right_eq_false [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α}
+   (h₁ : containsKey k (insertSmallerList l toInsert) = true)
+   (h₂ : containsKey k toInsert = false) : containsKey k l = true := by
+    have := contains_insertSmallerList_iff.1 h₁
+    simpa only [h₂, Bool.false_eq_true, or_false]
+
+theorem contains_of_contains_insertSmallerList_of_contains_left_eq_false [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α}
+   (h₁ : containsKey k (insertSmallerList l toInsert) = true)
+   (h₂ : containsKey k l = false) : containsKey k toInsert = true := by
+    have := contains_insertSmallerList_iff.1 h₁
+    simpa only [h₂, Bool.false_eq_true, false_or]
+
+theorem contains_insertSmallerList_of_left [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α}
+   (contains : containsKey k l = true) : containsKey k (insertSmallerList l toInsert) = true := by
+    apply contains_insertSmallerList_iff.2
+    exact Or.inl contains
+
+theorem contains_insertSmallerList_of_right [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α}
+   (contains : containsKey k toInsert = true) : containsKey k (insertSmallerList l toInsert) = true := by
+    apply contains_insertSmallerList_iff.2
+    exact Or.inr contains
+
 theorem isEmpty_insertListIfNew [BEq α]
     {l toInsert : List ((a : α) × β a)} :
     (List.insertListIfNew l toInsert).isEmpty = (l.isEmpty && toInsert.isEmpty) := by
@@ -3128,7 +3154,7 @@ theorem length_right_le_length_insertSmallerList [BEq α] [EquivBEq α]
         . apply le_of_lt h
         . simp only [length_le_length_insertList]
 
-theorem getEntry?_insertListIfNew [BEq α] [PartialEquivBEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)}
+theorem getEntry?_insertListIfNew [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)}
     {k : α} :
     getEntry? k (insertListIfNew l toInsert) =
       (getEntry? k l).or (getEntry? k toInsert) := by
@@ -3145,41 +3171,25 @@ theorem getEntry?_insertListIfNew [BEq α] [PartialEquivBEq α] [LawfulBEq α] {
         rw [getEntry?_eq_none.2]
         . simp only [Option.none_or]
           rw [←@getEntry?_congr _ _ _ _ (hd :: tl) hd.fst k hhd]
-          simp [@getEntry?_cons_self _ _ _ _ tl hd.fst hd.snd]
+          simp only [@getEntry?_cons_self _ _ _ _ tl hd.fst hd.snd]
         . simp only [←containsKey_congr hhd, hc]
       . simp only [Bool.not_true, Bool.and_false, Bool.false_eq_true, ↓reduceIte]
         rw [containsKey_congr hhd, containsKey_eq_isSome_getEntry?] at hc
         obtain ⟨v, hv⟩ := Option.isSome_iff_exists.1 hc
         simp [hv]
 
-theorem getEntry?_insertListIfNew_of_same_elem [BEq α] [PartialEquivBEq α] [LawfulBEq α] {l t : List ((a : α) × β a)} {k : α} {v : β k}:
+theorem getEntry?_insertListIfNew_of_same_elem [BEq α] [LawfulBEq α] {l t : List ((a : α) × β a)} {k : α} {v : β k}:
   getEntry? k (insertListIfNew (⟨k, v⟩ :: l) t) = .some ⟨k, v⟩ := by
-  simp [getEntry?_insertListIfNew]
+  simp only [getEntry?_insertListIfNew, getEntry?_cons_self, Option.some_or]
 
-theorem getEntry?_insertListIfNew_of_contains_eq_false_right [BEq α] [PartialEquivBEq α] [LawfulBEq α]
+theorem getEntry?_insertListIfNew_of_contains_eq_false_right [BEq α] [LawfulBEq α]
     {l toInsert : List ((a : α) × β a)} {k : α}
     (not_contains : containsKey k l = false) :
     getEntry? k (insertListIfNew l toInsert) = getEntry? k toInsert := by
-  induction toInsert generalizing l with
-  | nil => simpa [insertListIfNew]
-  | cons h t ih =>
-    unfold insertListIfNew
-    by_cases (k = h.fst)
-    case pos h_eq =>
-      rw [h_eq]
-      rw [h_eq] at not_contains
-      simp only [@insertEntryIfNew_of_containsKey_eq_false α β _ l h.fst h.snd not_contains]
-      simp only [getEntry?_insertListIfNew_of_same_elem]
-      simp [getEntry?]
-    case neg h_ne =>
-      have := @getEntry?_cons_of_false α β _  t h.fst k h.snd (by simp; rw [Eq.comm]; exact h_ne)
-      simp [this]
-      apply ih
-      have := @containsKey_insertEntryIfNew α β _ _ l h.fst k h.snd
-      simp [not_contains] at this
-      simp [this]
-      rw [Eq.comm]
-      exact h_ne
+  rw [getEntry?_insertListIfNew]
+  simp only [containsKey_eq_isSome_getEntry?] at not_contains
+  rw [(@Option.not_isSome_iff_eq_none  ((a : α) × β a) (getEntry? k l)).1 (by simp [not_contains])]
+  simp only [Option.none_or]
 
 theorem getEntry?_insertListIfNew_of_contains_eq_false [BEq α] [PartialEquivBEq α]
     {l toInsert : List ((a : α) × β a)} {k : α}
@@ -3193,14 +3203,14 @@ theorem getEntry?_insertListIfNew_of_contains_eq_false [BEq α] [PartialEquivBEq
     rw [ih not_contains.right, getEntry?_insertEntryIfNew]
     simp [not_contains]
 
-theorem getValueCast?_insertListIfNew_of_contains_eq_false [BEq α] [PartialEquivBEq α] [LawfulBEq α]
+theorem getValueCast?_insertListIfNew_of_contains_eq_false [BEq α] [LawfulBEq α]
     {l toInsert : List ((a : α) × β a)}  {k : α}
     (not_contains : containsKey k toInsert = false) :
     getValueCast? k (insertListIfNew toInsert l) = getValueCast? k l := by
   rw [getValueCast?_eq_getEntry?, getValueCast?_eq_getEntry?]
   simp only [getEntry?_insertListIfNew_of_contains_eq_false_right not_contains]
 
-theorem getValue?_insertSmallerList_of_contains_eq_false [BEq α] [PartialEquivBEq α] [LawfulBEq α]
+theorem getValue?_insertSmallerList_of_contains_eq_false [BEq α] [LawfulBEq α]
     {l toInsert : List ((a : α) × β a)} {k : α}
     (not_contains : containsKey k toInsert = false) :
     getValueCast? k (insertSmallerList l toInsert) = getValueCast? k l := by