feat: add ofList_eq_insertMany_empty lemmas for map types

src/Std/Data/DHashMap/Lemmas.lean

@@ -1961,6 +1961,9 @@ theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
     ofList (⟨k, v⟩ :: tl) = ((∅ : DHashMap α β).insert k v).insertMany tl :=
   Subtype.eq (congrArg Subtype.val (Raw₀.insertMany_emptyWithCapacity_list_cons (α := α)) :)
 
+theorem ofList_eq_insertMany_empty {l : List ((a : α) × β a)} :
+    ofList l = insertMany (∅ : DHashMap α β) l := rfl
+
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} {k : α} :
@@ -2105,6 +2108,9 @@ theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : DHashMap α (fun _ => β)).insert k v) tl :=
   Subtype.eq (congrArg Subtype.val (Raw₀.Const.insertMany_emptyWithCapacity_list_cons (α:= α)) :)
 
+theorem ofList_eq_insertMany_empty {l : List (α × β)} :
+    ofList l = insertMany (∅ : DHashMap α (fun _ => β)) l := rfl
+
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :

src/Std/Data/DHashMap/RawLemmas.lean

@@ -2089,6 +2089,9 @@ theorem ofList_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} {tl :
   simp_to_raw
   rw [Raw₀.insertMany_emptyWithCapacity_list_cons]
 
+theorem ofList_eq_insertMany_empty {l : List ((a : α) × (β a))} :
+    ofList l = insertMany (∅ : Raw α β) l := rfl
+
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} {k : α} :
@@ -2236,6 +2239,9 @@ theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
   simp_to_raw
   rw [Raw₀.Const.insertMany_emptyWithCapacity_list_cons]
 
+theorem ofList_eq_insertMany_empty {l : List (α × β)} :
+    ofList l = insertMany (∅ : Raw α (fun _ => β)) l := rfl
+
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :

src/Std/Data/DTreeMap/Lemmas.lean

@@ -1765,6 +1765,9 @@ theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
     ofList (⟨k, v⟩ :: tl) cmp = ((∅ : DTreeMap α β cmp).insert k v).insertMany tl :=
   ext <| Impl.insertMany_empty_list_cons
 
+theorem ofList_eq_insertMany_empty {l : List ((a : α) × (β a))} :
+    ofList l cmp = insertMany (∅ : DTreeMap α β cmp) l := rfl
+
 @[simp]
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
     {l : List ((a : α) × β a)} {k : α} :
@@ -1908,6 +1911,9 @@ theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) cmp = insertMany ((∅ : DTreeMap α β cmp).insert k v) tl :=
   ext Impl.Const.insertMany_empty_list_cons
 
+theorem ofList_eq_insertMany_empty {l : List (α × β)} :
+    ofList l cmp = insertMany (∅ : DTreeMap α β cmp) l := rfl
+
 @[simp]
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
     (ofList l cmp).contains k = (l.map Prod.fst).contains k :=

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

@@ -1772,6 +1772,12 @@ theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
     ofList (⟨k, v⟩ :: tl) cmp = ((∅ : Raw α β cmp).insert k v).insertMany tl :=
   ext Impl.insertMany_empty_list_cons_eq_insertMany!
 
+theorem ofList_eq_insertMany_empty {l : List ((a : α) × (β a))} :
+    ofList l cmp = insertMany (∅ : Raw α β cmp) l :=
+  match l with
+  | [] => by simp
+  | ⟨k, v⟩ :: tl => by simp [ofList_cons, insertMany_cons]
+
 @[simp]
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
     {l : List ((a : α) × β a)} {k : α} :
@@ -1915,6 +1921,12 @@ theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) cmp = insertMany ((∅ : Raw α β cmp).insert k v) tl :=
   ext <| Impl.Const.insertMany_empty_list_cons_eq_insertMany!
 
+theorem ofList_eq_insertMany_empty {l : List (α × β)} :
+    ofList l cmp = insertMany (∅ : Raw α β cmp) l :=
+  match l with
+  | [] => by simp
+  | ⟨k, v⟩ :: tl => by simp [ofList_cons, insertMany_cons]
+
 @[simp]
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
     (ofList l cmp).contains k = (l.map Prod.fst).contains k :=

src/Std/Data/ExtDHashMap/Lemmas.lean

@@ -1680,6 +1680,11 @@ theorem ofList_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} {tl :
   conv => rhs; apply insertMany_list_mk
   exact congrArg Quotient.mk' DHashMap.ofList_cons
 
+theorem ofList_eq_insertMany_empty [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} :
+    ofList l = insertMany (∅ : ExtDHashMap α β) l := by
+  conv => rhs; apply insertMany_list_mk
+  exact congrArg Quotient.mk' DHashMap.ofList_eq_insertMany_empty
+
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List ((a : α) × β a)} {k : α} :
@@ -1825,6 +1830,11 @@ theorem ofList_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β} {tl : Li
   conv => rhs; apply insertMany_list_mk
   exact congrArg Quotient.mk' DHashMap.Const.ofList_cons
 
+theorem ofList_eq_insertMany_empty [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
+    ofList l = insertMany (∅ : ExtDHashMap α (fun _ => β)) l := by
+  conv => rhs; apply insertMany_list_mk
+  exact congrArg Quotient.mk' DHashMap.Const.ofList_eq_insertMany_empty
+
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :

src/Std/Data/ExtHashMap/Lemmas.lean

@@ -1080,6 +1080,10 @@ theorem ofList_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β} {tl : Li
     ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : ExtHashMap α β).insert k v) tl :=
   ext ExtDHashMap.Const.ofList_cons
 
+theorem ofList_eq_insertMany_empty [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
+    ofList l = insertMany (∅ : ExtHashMap α β) l :=
+  ext ExtDHashMap.Const.ofList_eq_insertMany_empty
+
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :

src/Std/Data/ExtHashSet/Lemmas.lean

@@ -550,6 +550,12 @@ theorem ofList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List α} :
       insertMany ((∅ : ExtHashSet α).insert hd) tl :=
   ext ExtHashMap.unitOfList_cons
 
+theorem ofList_eq_insertMany_empty [EquivBEq α] [LawfulHashable α] {l : List α} :
+    ofList l = insertMany (∅ : ExtHashSet α) l :=
+  match l with
+  | [] => by simp
+  | hd :: tl => by simp [ofList_cons, insertMany_cons]
+
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :

src/Std/Data/HashMap/Lemmas.lean

@@ -1330,6 +1330,10 @@ theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : HashMap α β).insert k v) tl :=
   ext DHashMap.Const.ofList_cons
 
+theorem ofList_eq_insertMany_empty {l : List (α × β)} :
+    ofList l = insertMany (∅ : HashMap α β) l :=
+  ext DHashMap.Const.ofList_eq_insertMany_empty
+
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :

src/Std/Data/HashMap/RawLemmas.lean

@@ -1364,6 +1364,10 @@ theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) = insertMany ((∅ : Raw α β).insert k v) tl :=
   ext DHashMap.Raw.Const.ofList_cons
 
+theorem ofList_eq_insertMany_empty {l : List (α × β)} :
+    ofList l = insertMany (∅ : Raw α β) l :=
+  ext DHashMap.Raw.Const.ofList_eq_insertMany_empty
+
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} {k : α} :

src/Std/Data/HashSet/Lemmas.lean

@@ -678,6 +678,12 @@ theorem ofList_cons {hd : α} {tl : List α} :
       insertMany ((∅ : HashSet α).insert hd) tl :=
   ext HashMap.unitOfList_cons
 
+theorem ofList_eq_insertMany_empty {l : List α} :
+    ofList l = insertMany (∅ : HashSet α) l :=
+  match l with
+  | [] => by simp
+  | hd :: tl => by simp [ofList_cons, insertMany_cons]
+
 @[simp]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :

src/Std/Data/TreeMap/Lemmas.lean

@@ -1227,6 +1227,9 @@ theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) cmp = insertMany ((∅ : TreeMap α β cmp).insert k v) tl :=
   ext DTreeMap.Const.ofList_cons
 
+theorem ofList_eq_insertMany_empty {l : List (α × β)} :
+    ofList l cmp = insertMany (∅ : TreeMap α β cmp) l := rfl
+
 @[simp]
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
     (ofList l cmp).contains k = (l.map Prod.fst).contains k :=

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

@@ -1236,6 +1236,10 @@ theorem ofList_cons {k : α} {v : β} {tl : List (α × β)} :
     ofList (⟨k, v⟩ :: tl) cmp = insertMany ((∅ : Raw α β cmp).insert k v) tl :=
   ext DTreeMap.Raw.Const.ofList_cons
 
+theorem ofList_eq_insertMany_empty {l : List (α × β)} :
+    ofList l cmp = insertMany (∅ : Raw α β cmp) l :=
+  ext DTreeMap.Raw.Const.ofList_eq_insertMany_empty
+
 @[simp]
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
     (ofList l cmp).contains k = (l.map Prod.fst).contains k :=

src/Std/Data/TreeSet/Lemmas.lean

@@ -611,6 +611,12 @@ theorem ofList_cons {hd : α} {tl : List α} :
       insertMany ((∅ : TreeSet α cmp).insert hd) tl :=
   ext TreeMap.unitOfList_cons
 
+theorem ofList_eq_insertMany_empty {l : List α} :
+    ofList l cmp = insertMany (∅ : TreeSet α cmp) l :=
+  match l with
+  | [] => by simp
+  | hd :: tl => by simp [ofList_cons, insertMany_cons]
+
 @[simp]
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
     (ofList l cmp).contains k = l.contains k :=

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

@@ -609,6 +609,12 @@ theorem ofList_cons {hd : α} {tl : List α} :
       insertMany ((∅ : Raw α cmp).insert hd) tl :=
   ext TreeMap.Raw.unitOfList_cons
 
+theorem ofList_eq_insertMany_empty {l : List α} :
+    ofList l cmp = insertMany (∅ : Raw α cmp) l :=
+  match l with
+  | [] => by simp
+  | hd :: tl => by simp [ofList_cons, insertMany_cons]
+
 @[simp]
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
     (ofList l cmp).contains k = l.contains k :=