more

src/Init/Data/Option/Lemmas.lean

@@ -674,6 +674,11 @@ theorem or_of_isNone {o o' : Option α} (h : o.isNone) : o.or o' = o' := by
   match o, h with
   | none, _ => simp
 
+@[simp, grind]
+theorem getD_or {o o' : Option α} {fallback : α} :
+    (o.or o').getD fallback = o.getD (o'.getD fallback) := by
+  cases o <;> simp
+
 /-! ### beq -/
 
 section beq

src/Std/Data/DHashMap/Lemmas.lean

@@ -1721,6 +1721,18 @@ theorem get?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
     get? (insertMany m l) k' = some v :=
   Raw₀.Const.get?_insertMany_list_of_mem ⟨m.1, _⟩ m.2 k_beq distinct mem
 
+theorem get?_insertMany_list [EquivBEq α] [LawfulHashable α]
+    {l : List (α × β)} {k : α} :
+    get? (insertMany m l) k =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if a == k then some b else none)).or (get? m k) := by
+  induction l generalizing m with
+  | nil =>
+    rw [get?_insertMany_list_of_contains_eq_false] <;> simp
+  | cons x l ih =>
+    rcases x with ⟨a, b⟩
+    rw [insertMany_cons, ih, get?_insert]
+    by_cases h : a == k <;> simp [h]
+
 theorem get_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false)

src/Std/Data/DHashMap/RawLemmas.lean

@@ -1834,6 +1834,17 @@ theorem get?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
     get? (insertMany m l) k' = some v := by
   simp_to_raw using Raw₀.Const.get?_insertMany_list_of_mem
 
+theorem get?_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List (α × β)} {k : α} :
+    get? (insertMany m l) k =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if a == k then some b else none)).or (get? m k) := by
+  induction l generalizing m with
+  | nil =>
+    rw [get?_insertMany_list_of_contains_eq_false h] <;> simp
+  | cons x l ih =>
+    rcases x with ⟨a, b⟩
+    rw [insertMany_cons h, ih h.insert, get?_insert h]
+    by_cases h : a == k <;> simp [h]
+
 theorem get_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF)
     {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false)

src/Std/Data/DTreeMap/Internal/Lemmas.lean

@@ -2341,6 +2341,25 @@ theorem get?_insertMany!_list_of_mem [TransOrd α] (h : t.WF)
     get? (insertMany! t l).1 k' = some v := by
   simpa only [insertMany_eq_insertMany!] using get?_insertMany_list_of_mem h
 
+theorem get?_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF)
+    {l : List (α × β)} {k : α} :
+    get? (insertMany t l h.balanced).1 k =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if compare a k = .eq then some b else none)).or (get? t k) := by
+  induction l generalizing t with
+  | nil =>
+    rw [get?_insertMany_list_of_contains_eq_false h] <;> simp
+  | cons x l ih =>
+    rcases x with ⟨a, b⟩
+    rw [insertMany_cons h, ih (WF.insert h), get?_insert h]
+    simp
+    split <;> simp
+
+theorem get?_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF)
+    {l : List (α × β)} {k : α} :
+    get? (insertMany! t l).1 k =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if compare a k =.eq then some b else none)).or (get? t k) := by
+  simpa only [insertMany_eq_insertMany!] using get?_insertMany_list h
+
 theorem get_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF)
     {l : List (α × β)} {k : α}
     (h₁ : (l.map Prod.fst).contains k = false)
@@ -2369,6 +2388,37 @@ theorem get_insertMany!_list_of_mem [TransOrd α] (h : t.WF)
     get (insertMany! t l).1 k' h' = v := by
   simpa only [insertMany_eq_insertMany!] using get_insertMany_list_of_mem h
 
+/-- A variant of `contains_of_contains_insertMany_list` used in `get_insertMany_list`. -/
+-- This should not really need `PartialEquivBEq`, but fixing it would require many changes.
+theorem contains_of_contains_insertMany_list' [TransOrd α] [BEq α] [PartialEquivBEq α] [LawfulBEqOrd α] (h : t.WF)
+    {l : List (α × β)} {k : α}
+    (h' : contains k (insertMany t l h.balanced).val = true)
+    (w : l.findSomeRev? (fun ⟨a, b⟩ => if compare a k = .eq then some b else none) = none) :
+    contains k t = true :=
+  contains_of_contains_insertMany_list h h' (by simpa [compare_eq_iff_beq, BEq.comm] using w)
+
+theorem get_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF)
+    {l : List (α × β)} {k : α} (h') :
+    get (insertMany t l h.balanced).1 k h' =
+      match w : l.findSomeRev? (fun ⟨a, b⟩ => if compare a k = .eq then some b else none) with
+      | some v => v
+      | none => get t k (contains_of_contains_insertMany_list' h h' w) := by
+  apply Option.some_inj.mp
+  rw [get_eq_get?, get?_insertMany_list h]
+  split <;> rename_i p
+  · rw [p]
+    simp
+  · simp only [p]
+    simp [get_eq_get?]
+
+theorem get_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF)
+    {l : List (α × β)} {k : α} {h'} :
+    get (insertMany! t l).1 k h' =
+      match w : l.findSomeRev? (fun ⟨a, b⟩ => if compare a k =.eq then some b else none) with
+      | some v => v
+      | none => get t k (contains_of_contains_insertMany_list' h (by simpa [insertMany_eq_insertMany!] using h') w) := by
+  simpa only [insertMany_eq_insertMany!] using get_insertMany_list h (by simpa [insertMany_eq_insertMany!] using h')
+
 theorem get!_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α]
     [Inhabited β] (h : t.WF) {l : List (α × β)} {k : α}
     (h' : (l.map Prod.fst).contains k = false) :
@@ -2418,6 +2468,35 @@ theorem getD_insertMany!_list_of_mem [TransOrd α] (h : t.WF)
     getD (insertMany! t l).1 k' fallback = v := by
   simpa only [insertMany_eq_insertMany!] using getD_insertMany_list_of_mem h
 
+theorem getD_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF)
+    {l : List (α × β)} {k : α} (fallback : β) :
+    getD (insertMany t l h.balanced).1 k fallback =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if compare a k = .eq then some b else none)).getD (getD t k fallback) := by
+  rw [getD_eq_getD_get? h.constInsertMany, get?_insertMany_list h]
+  simp [getD_eq_getD_get? h]
+
+theorem getD_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF)
+    {l : List (α × β)} {k : α} (fallback : β) :
+    getD (insertMany! t l).1 k fallback =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if compare a k = .eq then some b else none)).getD (getD t k fallback) := by
+  simpa only [insertMany_eq_insertMany!] using getD_insertMany_list h fallback
+
+-- Ideally the results about `getD` would come before those about `get!`, so we could conveniently use them;
+-- for now, these results have been slightly delayed:
+
+theorem get!_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited β] (h : t.WF)
+    {l : List (α × β)} {k : α} :
+    get! (insertMany t l h.balanced).1 k =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if compare a k = .eq then some b else none)).getD (get! t k) := by
+  rw [get!_eq_getD_default h.constInsertMany, getD_insertMany_list h]
+  simp [get!_eq_getD_default h]
+
+theorem get!_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited β] (h : t.WF)
+    {l : List (α × β)} {k : α} :
+    get! (insertMany! t l).1 k =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if compare a k =.eq then some b else none)).getD (get! t k) := by
+  simpa only [insertMany_eq_insertMany!] using get!_insertMany_list h
+
 variable {t : Impl α Unit}
 
 theorem insertManyIfNewUnit_cons (h : t.WF) {l : List α} {k : α} :

src/Std/Data/DTreeMap/Lemmas.lean

@@ -1573,6 +1573,12 @@ theorem get?_insertMany_list_of_mem [TransCmp cmp]
     get? (insertMany t l) k' = some v :=
   Impl.Const.get?_insertMany_list_of_mem t.wf k_eq distinct mem
 
+theorem get?_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
+    {l : List (α × β)} {k : α} :
+    get? (insertMany t l) k =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none)).or (get? t k) :=
+  Impl.Const.get?_insertMany_list t.wf
+
 theorem get_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
     {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false)

src/Std/Data/DTreeMap/Raw/Lemmas.lean

@@ -1580,6 +1580,12 @@ theorem get?_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
     get? (insertMany t l) k' = some v :=
   Impl.Const.get?_insertMany!_list_of_mem h k_eq distinct mem
 
+theorem get?_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
+    {l : List (α × β)} {k : α} :
+    get? (insertMany t l) k =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none)).or (get? t k) :=
+  Impl.Const.get?_insertMany!_list h (k := k)
+
 theorem get_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
     (h : t.WF) {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false)
@@ -1593,6 +1599,14 @@ theorem get_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
     get (insertMany t l) k' h' = v :=
   Impl.Const.get_insertMany!_list_of_mem h k_eq distinct mem
 
+theorem get_insertMany_list [TransCmp cmp] [BEq α] [PartialEquivBEq α] [LawfulBEqCmp cmp] (h : t.WF)
+    {l : List (α × β)} {k : α} {h'} :
+    get (insertMany t l) k h' =
+      match w : l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none) with
+      | some v => v
+      | none => get t k (Impl.Const.contains_of_contains_insertMany_list' h (by simpa [Impl.Const.insertMany_eq_insertMany!] using h') w) :=
+  Impl.Const.get_insertMany!_list h (k := k)
+
 theorem get!_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
     [Inhabited β] (h : t.WF) {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
@@ -1605,6 +1619,12 @@ theorem get!_insertMany_list_of_mem [TransCmp cmp] [Inhabited β] (h : t.WF)
     get! (insertMany t l) k' = v :=
   Impl.Const.get!_insertMany!_list_of_mem h k_eq distinct mem
 
+theorem get!_insertMany_list [TransCmp cmp] [Inhabited β] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
+    {l : List (α × β)} {k : α} :
+    get! (insertMany t l) k =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none)).getD (get! t k) :=
+  Impl.Const.get!_insertMany!_list h (k := k)
+
 theorem getD_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
     (h : t.WF) {l : List (α × β)} {k : α} {fallback : β}
     (contains_eq_false : (l.map Prod.fst).contains k = false) :
@@ -1617,6 +1637,12 @@ theorem getD_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
     getD (insertMany t l) k' fallback = v :=
   Impl.Const.getD_insertMany!_list_of_mem h k_eq distinct mem
 
+theorem getD_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
+    {l : List (α × β)} {k : α} {fallback : β} :
+    getD (insertMany t l) k fallback =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none)).getD (getD t k fallback) :=
+  Impl.Const.getD_insertMany!_list h (k := k) fallback
+
 variable {t : Raw α Unit cmp}
 
 @[simp]

src/Std/Data/ExtDHashMap/Lemmas.lean

@@ -1393,6 +1393,14 @@ theorem get?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
   simp only [insertMany_list_mk]
   exact DHashMap.Const.get?_insertMany_list_of_mem k_beq distinct mem
 
+theorem get?_insertMany_list [EquivBEq α] [LawfulHashable α]
+    {l : List (α × β)} {k : α} :
+    get? (insertMany m l) k =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if a == k then some b else none)).or (get? m k) := by
+  refine m.inductionOn (fun _ => ?_)
+  simp only [insertMany_list_mk]
+  exact DHashMap.Const.get?_insertMany_list
+
 theorem get_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false)

src/Std/Data/ExtHashMap/Lemmas.lean

@@ -768,6 +768,11 @@ theorem getElem?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
     (insertMany m l)[k']? = some v :=
   ExtDHashMap.Const.get?_insertMany_list_of_mem k_beq distinct mem
 
+theorem getElem?_insertMany_list [EquivBEq α] [LawfulHashable α]
+    {l : List (α × β)} {k : α} :
+    (insertMany m l)[k]? = (l.findSomeRev? (fun ⟨a, b⟩ => if a == k then some b else none)).or m[k]? :=
+  ExtDHashMap.Const.get?_insertMany_list
+
 theorem getElem_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false)

src/Std/Data/HashMap/Lemmas.lean

@@ -1017,6 +1017,11 @@ theorem getElem?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
     (insertMany m l)[k']? = some v :=
   DHashMap.Const.get?_insertMany_list_of_mem k_beq distinct mem
 
+theorem getElem?_insertMany_list [EquivBEq α] [LawfulHashable α]
+    {l : List (α × β)} {k : α} :
+    (insertMany m l)[k]? = (l.findSomeRev? (fun ⟨a, b⟩ => if a == k then some b else none)).or m[k]? :=
+  DHashMap.Const.get?_insertMany_list
+
 theorem getElem_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false)

src/Std/Data/HashMap/RawLemmas.lean

@@ -1131,6 +1131,11 @@ theorem getElem?_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
     (insertMany m l)[k']? = some v :=
   DHashMap.Raw.Const.get?_insertMany_list_of_mem h.out k_beq distinct mem
 
+theorem getElem?_insertMany_list [EquivBEq α] [LawfulHashable α]
+    (h : m.WF) {l : List (α × β)} {k : α} :
+    (insertMany m l)[k]? = (l.findSomeRev? (fun ⟨a, b⟩ => if a == k then some b else none)).or m[k]? :=
+  DHashMap.Raw.Const.get?_insertMany_list h.out
+
 theorem getElem_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
     (h : m.WF) {l : List (α × β)} {k : α}
     (contains_eq_false : (l.map Prod.fst).contains k = false)

src/Std/Data/TreeMap/Lemmas.lean

@@ -1021,6 +1021,12 @@ theorem getElem?_insertMany_list_of_mem [TransCmp cmp] [BEq α] [LawfulBEqCmp cm
     (t.insertMany l)[k']? = some v :=
   DTreeMap.Const.get?_insertMany_list_of_mem k_eq distinct mem
 
+theorem getElem?_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
+    {l : List (α × β)} {k : α} :
+    (t.insertMany l)[k]? =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none)).or (t[k]?) :=
+  DTreeMap.Const.get?_insertMany_list
+
 theorem getElem_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α]
     [LawfulBEqCmp cmp]
     {l : List (α × β)} {k : α}

src/Std/Data/TreeMap/Raw/Lemmas.lean

@@ -1030,6 +1030,12 @@ theorem getElem?_insertMany_list_of_mem [TransCmp cmp] [BEq α] [LawfulBEqCmp cm
     (t.insertMany l)[k']? = some v :=
   DTreeMap.Raw.Const.get?_insertMany_list_of_mem h k_eq distinct mem
 
+theorem getElem?_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
+    (h : t.WF) {l : List (α × β)} {k : α} :
+    (insertMany t l)[k]? =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none)).or t[k]? :=
+  DTreeMap.Raw.Const.get?_insertMany_list h
+
 theorem getElem_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α]
     [LawfulBEqCmp cmp] (h : t.WF)
     {l : List (α × β)} {k : α}
@@ -1047,6 +1053,14 @@ theorem getElem_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
     (t.insertMany l)[k']'h' = v :=
   DTreeMap.Raw.Const.get_insertMany_list_of_mem h k_eq distinct mem
 
+theorem getElem_insertMany_list [TransCmp cmp] [BEq α] [PartialEquivBEq α] [LawfulBEqCmp cmp]
+    (h : t.WF) {l : List (α × β)} {k : α} {h'} :
+    (insertMany t l)[k]'h' =
+      match w : l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none) with
+      | some v => v
+      | none => t[k]'(mem_of_mem_insertMany_list h h' (by simpa [LawfulBEqCmp.compare_eq_iff_beq, BEq.comm] using w)) :=
+  DTreeMap.Raw.Const.get_insertMany_list h
+
 theorem getElem!_insertMany_list_of_contains_eq_false [TransCmp cmp]
     [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
     {l : List (α × β)} {k : α} [Inhabited β]
@@ -1061,6 +1075,12 @@ theorem getElem!_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
     (t.insertMany l)[k']! = v :=
   DTreeMap.Raw.Const.get!_insertMany_list_of_mem h k_eq distinct mem
 
+theorem getElem!_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited β]
+    (h : t.WF) {l : List (α × β)} {k : α} :
+    (insertMany t l)[k]! =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none)).getD t[k]! :=
+  DTreeMap.Raw.Const.get!_insertMany_list h
+
 theorem getD_insertMany_list_of_contains_eq_false [TransCmp cmp]
     [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
     {l : List (α × β)} {k : α} {fallback : β}
@@ -1075,6 +1095,12 @@ theorem getD_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
     (t.insertMany l).getD k' fallback = v :=
   DTreeMap.Raw.Const.getD_insertMany_list_of_mem h k_eq distinct mem
 
+theorem getD_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
+    (h : t.WF) {l : List (α × β)} {k : α} {fallback : β} :
+    (insertMany t l).getD k fallback =
+      (l.findSomeRev? (fun ⟨a, b⟩ => if cmp a k = .eq then some b else none)).getD (t.getD k fallback) :=
+  DTreeMap.Raw.Const.getD_insertMany_list h
+
 section Unit
 
 variable {t : Raw α Unit cmp}