diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index 05f37bc422..9aac27f7e8 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -4301,6 +4301,20 @@ theorem filterMap_equiv_congr {γ : α → Type w} (h : m₁.1 ~m m₂.1)
     {f : (a : α) → β a → Option (γ a)} : (m₁.filterMap f).1 ~m (m₂.filterMap f).1 := by
   simp_to_model [filterMap, Equiv] using h.1.filterMap _
 
+theorem insertMany_list_equiv_foldl [BEq α] [Hashable α] {l : List ((a : α) × β a)} :
+    (m₁.insertMany l).1 ~m (l.foldl (init := m₁) (fun acc p => acc.insert p.1 p.2)) := by
+  rw [insertMany_list_eq_foldl, ← List.foldl_hom (g₂ := fun acc p => acc.insert p.1 p.2) Subtype.val]
+  · simp_to_model [Equiv] using List.Perm.refl
+  · intro x y
+    simp [Raw.insert, x.property]
+
+theorem insertManyIfNew_list_equiv_foldl [BEq α] [Hashable α] {l : List ((a : α) × β a)} :
+    (m₁.insertManyIfNew l).1 ~m (l.foldl (init := m₁) (fun acc p => acc.insertIfNew p.1 p.2)) := by
+  rw [insertManyIfNew_list_eq_foldl, ← List.foldl_hom (g₂ := fun acc p => acc.insertIfNew p.1 p.2) Subtype.val]
+  · simp_to_model [Equiv] using List.Perm.refl
+  · intro x y
+    simp [Raw.insertIfNew, x.property]
+
 namespace Const
 
 theorem equiv_iff_toList_perm_toList {β : Type v} (m₁ m₂ : Raw α fun _ => β) :
@@ -4420,6 +4434,22 @@ theorem equiv_of_forall_get?_eq [LawfulBEq α] (h₁ : m₁.1.WF) (h₂ : m₂.1
 namespace Const
 
 variable {β : Type v} (m₁ m₂ : Raw₀ α fun _ => β)
+
+theorem insertMany_list_equiv_foldl {l : List (α × β)} :
+    (insertMany m₁ l).1 ~m (l.foldl (init := m₁) (fun (acc : Raw α fun _ => β) p => acc.insert p.1 p.2)) := by
+  rw [insertMany_list_eq_foldl, ← List.foldl_hom (g₂ := fun acc p => acc.insert p.1 p.2) Subtype.val]
+  · simp_to_model [Equiv] using List.Perm.refl
+  · intro x y
+    simp [Raw.insert, x.property]
+
+theorem insertManyIfNewUnit_list_equiv_foldl (m₁ : Raw₀ α fun _ => Unit) {l : List α} :
+    (insertManyIfNewUnit m₁ l).1 ~m (l.foldl (init := m₁) (fun acc a => acc.insertIfNew a ())) := by
+  rw [insertManyIfNewUnit_list_eq_foldl,
+    ← List.foldl_hom (g₂ := fun acc a => acc.insertIfNew a ()) Subtype.val]
+  · simp_to_model [Equiv] using List.Perm.refl
+  · intro x y
+    simp [Raw.insertIfNew, x.property]
+
 variable [EquivBEq α] [LawfulHashable α]
 
 theorem get?_eq_of_equiv (h₁ : m₁.1.WF) (h₂ : m₂.1.WF) (h : m₁.1 ~m m₂.1) {k : α} :
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index b62c66248c..50609a718f 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -1347,6 +1347,11 @@ theorem toListModel_insertMany_list [BEq α] [Hashable α] [EquivBEq α] [Lawful
   apply toListModel_insertListₘ
   exact h
 
+theorem insertMany_list_eq_foldl [BEq α] [Hashable α]
+    {m : Raw₀ α β} {l : List ((a : α) × β a)} :
+    (insertMany m l).1 = l.foldl (init := m) fun a b => a.insert b.1 b.2 := by
+  simpa [insertMany] using (List.foldl_hom Subtype.val (by simp)).symm
+
 /-! # `eraseMany` -/
 
 theorem WF.eraseManyEntries [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Raw α β}
@@ -1445,6 +1450,11 @@ theorem toListModel_insertManyIfNew_list [BEq α] [Hashable α] [EquivBEq α] [L
   apply toListModel_insertListIfNewₘ
   exact h
 
+theorem insertManyIfNew_list_eq_foldl [BEq α] [Hashable α]
+    {m : Raw₀ α β} {l : List ((a : α) × β a)} :
+    (insertManyIfNew m l).1 = l.foldl (init := m) fun a b => a.insertIfNew b.1 b.2 := by
+  simpa [insertManyIfNew] using (List.foldl_hom Subtype.val (by simp)).symm
+
 /-! # `union` -/
 
 theorem wf_union₀ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
@@ -1567,6 +1577,11 @@ theorem Const.wf_insertMany₀ {β : Type v} [BEq α] [Hashable α] [EquivBEq α
     {l : ρ} (h' : m.WF) : (Const.insertMany ⟨m, h⟩ l).1.1.WF :=
   (Raw₀.Const.insertMany ⟨m, h⟩ l).2 _ Raw.WF.insert₀ h'
 
+theorem Const.insertMany_list_eq_foldl {β : Type v} [BEq α] [Hashable α]
+    {m : Raw₀ α (fun _ => β)} {l : List (α × β)} :
+    (Const.insertMany m l).1 = l.foldl (init := m) fun a b => a.insert b.1 b.2 := by
+  simpa [Const.insertMany] using (List.foldl_hom Subtype.val (by simp)).symm
+
 /-! # `Const.insertListIfNewUnitₘ` -/
 
 theorem Const.toListModel_insertListIfNewUnitₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α]
@@ -1600,6 +1615,11 @@ theorem Const.wf_insertManyIfNewUnit₀ [BEq α] [Hashable α] [EquivBEq α] [La
     {l : ρ} (h' : m.WF) : (Const.insertManyIfNewUnit ⟨m, h⟩ l).1.1.WF :=
   (Raw₀.Const.insertManyIfNewUnit ⟨m, h⟩ l).2 _ Raw.WF.insertIfNew₀ h'
 
+theorem Const.insertManyIfNewUnit_list_eq_foldl [BEq α] [Hashable α]
+    {m : Raw₀ α (fun _ => Unit)} {l : List α} :
+    (Const.insertManyIfNewUnit m l).1 = l.foldl (init := m) fun a b => a.insertIfNew b () := by
+  simpa [Const.insertManyIfNewUnit] using (List.foldl_hom Subtype.val (by simp)).symm
+
 theorem beq_eq_beqModel [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] {m₁ m₂ : Raw₀ α β}  (h₁ : Raw.WFImp m₁.1) (h₂ : Raw.WFImp m₂.1) :
     beq m₁ m₂ = beqModel (toListModel m₁.1.buckets) (toListModel m₂.1.buckets) := by
   simp [beq, beqModel, Raw.size_eq_length h₁, Raw.size_eq_length h₂, Raw.all_eq_all_toListModel,
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 467ce1e49b..1ea82a9674 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -3577,6 +3577,9 @@ theorem unitOfList_cons {hd : α} {tl : List α} :
       insertManyIfNewUnit ((∅ : DHashMap α (fun _ => Unit)).insertIfNew hd ()) tl :=
   ext <| congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_cons (α := α))
 
+theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} :
+    unitOfList l = insertManyIfNewUnit ∅ l := (rfl)
+
 @[simp]
 theorem contains_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
@@ -4572,6 +4575,42 @@ theorem equiv_iff_toList_perm {m₁ m₂ : DHashMap α β} [EquivBEq α] [Lawful
     m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList :=
   ⟨Equiv.toList_perm, Equiv.of_toList_perm⟩
 
+theorem insertMany_list_equiv_foldl {m : DHashMap α β} {l : List ((a : α) × β a)} :
+    m.insertMany l ~m l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)]
+  · exact Raw₀.insertMany_list_equiv_foldl ⟨m.1, m.2.size_buckets_pos⟩ (l := l)
+  · exact fun m _ => by simp [Raw.insert_eq m.2, insert]
+
+theorem ofList_equiv_foldl {l : List ((a : α) × β a)} :
+    ofList l ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 :=
+  insertMany_list_equiv_foldl
+
+theorem Const.insertMany_list_equiv_foldl {β : Type v} {m : DHashMap α fun _ => β}
+    {l : List (α × β)} :
+    insertMany m l ~m l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)]
+  · exact Raw₀.Const.insertMany_list_equiv_foldl ⟨m.1, m.2.size_buckets_pos⟩ (l := l)
+  · exact fun m _ => by simp [Raw.insert_eq m.2, insert]
+
+theorem Const.ofList_equiv_foldl {β : Type v} {l : List (α × β)} :
+    ofList l ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 :=
+  insertMany_list_equiv_foldl
+
+theorem Const.insertManyIfNewUnit_list_equiv_foldl {m : DHashMap α fun _ => Unit}
+    {l : List α} :
+    insertManyIfNewUnit m l ~m
+      l.foldl (init := m) fun acc a => acc.insertIfNew a () := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact Raw₀.Const.insertManyIfNewUnit_list_equiv_foldl ⟨m.1, m.2.size_buckets_pos⟩ (l := l)
+  · exact fun m _ => by simp [Raw.insertIfNew_eq m.2, insertIfNew]
+
+theorem Const.unitOfList_equiv_foldl {l : List α} :
+    unitOfList l ~m l.foldl (init := ∅) fun acc p => acc.insertIfNew p () :=
+  insertManyIfNewUnit_list_equiv_foldl
+
 namespace Const
 
 variable {β : Type v} {m₁ m₂ : DHashMap α fun _ => β}
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index f81d7eb622..76eb6cf820 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -4148,6 +4148,9 @@ theorem unitOfList_cons {hd : α} {tl : List α} :
   simp_to_raw
   rw [Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_cons]
 
+theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} :
+    unitOfList l = insertManyIfNewUnit ∅ l := (rfl)
+
 @[simp]
 theorem contains_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
@@ -5229,6 +5232,36 @@ theorem equiv_iff_toList_perm {m₁ m₂ : DHashMap.Raw α β} [EquivBEq α] [La
     m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList :=
   ⟨Equiv.toList_perm, Equiv.of_toList_perm⟩
 
+theorem insertMany_list_equiv_foldl {m : DHashMap.Raw α β} {l : List ((a : α) × β a)} (h : m.WF) :
+    m.insertMany l ~m l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by
+  rw [insertMany_eq h]
+  exact (Raw₀.insertMany_list_equiv_foldl ⟨m, h.size_buckets_pos⟩ (l := l))
+
+theorem ofList_equiv_foldl {l : List ((a : α) × β a)} :
+    ofList l ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 :=
+  insertMany_list_equiv_foldl .empty
+
+theorem Const.insertMany_list_equiv_foldl {β : Type v} {m : DHashMap.Raw α fun _ => β}
+    {l : List (α × β)} (h : m.WF) :
+    insertMany m l ~m l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by
+  rw [Const.insertMany_eq h]
+  exact (Raw₀.Const.insertMany_list_equiv_foldl ⟨m, h.size_buckets_pos⟩ (l := l))
+
+theorem Const.ofList_equiv_foldl {β : Type v} {l : List (α × β)} :
+    ofList l ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 :=
+  insertMany_list_equiv_foldl .empty
+
+theorem Const.insertManyIfNewUnit_list_equiv_foldl {m : DHashMap.Raw α fun _ => Unit}
+    {l : List α} (h : m.WF) :
+    insertManyIfNewUnit m l ~m
+      l.foldl (init := m) fun acc a => acc.insertIfNew a () := by
+  rw [Const.insertManyIfNewUnit_eq h]
+  exact (Raw₀.Const.insertManyIfNewUnit_list_equiv_foldl ⟨m, h.size_buckets_pos⟩ (l := l))
+
+theorem Const.unitOfList_equiv_foldl {l : List α} :
+    unitOfList l ~m l.foldl (init := ∅) fun acc a => acc.insertIfNew a () :=
+  insertManyIfNewUnit_list_equiv_foldl .empty
+
 namespace Const
 
 variable {β : Type v} {m₁ m₂ : DHashMap.Raw α fun _ => β}
diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
index ad89db5a18..136e6a9f3b 100644
--- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -2187,6 +2187,13 @@ theorem isEmpty_insertMany!_list [TransOrd α] (h : t.WF)
     (t.insertMany! l).1.isEmpty = (t.isEmpty && l.isEmpty) := by
   simpa only [insertMany_eq_insertMany!] using isEmpty_insertMany_list h
 
+theorem ofList_eq_insertMany {l : List ((a : α) × β a)} :
+    ofList l = insertMany .empty l balanced_empty := rfl
+
+theorem ofList_eq_insertMany! {l : List ((a : α) × β a)} :
+    ofList l = insertMany! .empty l := by
+  rw [ofList_eq_insertMany, insertMany_eq_insertMany!]
+
 namespace Const
 
 variable {β : Type v} {t : Impl α β}
@@ -2590,6 +2597,13 @@ theorem get!_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabite
       (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
 
+theorem ofList_eq_insertMany {l : List (α × β)} :
+    ofList l = insertMany .empty l balanced_empty := rfl
+
+theorem ofList_eq_insertMany! {l : List (α × β)} :
+    ofList l = insertMany! .empty l := by
+  rw [ofList_eq_insertMany, insertMany_eq_insertMany!]
+
 variable {t : Impl α Unit}
 
 theorem insertManyIfNewUnit_cons (h : t.WF) {l : List α} {k : α} :
@@ -2862,6 +2876,13 @@ theorem getD_insertManyIfNewUnit!_list
     getD (insertManyIfNewUnit! t l).1 k fallback = () :=
   rfl
 
+theorem unitOfList_eq_insertManyIfNewUnit {l : List α} :
+    unitOfList l = insertManyIfNewUnit .empty l balanced_empty := rfl
+
+theorem unitOfList_eq_insertManyIfNewUnit! {l : List α} :
+    unitOfList l = insertManyIfNewUnit! .empty l := by
+  rw [unitOfList_eq_insertManyIfNewUnit, insertManyIfNewUnit_eq_insertManyIfNewUnit!]
+
 end Const
 
 @[simp]
@@ -9286,6 +9307,22 @@ theorem equiv_iff_toList_eq [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) :
     t₁ ~m t₂ ↔ t₁.toList = t₂.toList :=
   ⟨Equiv.toList_eq h₁ h₂, .of_toList_perm ∘ .of_eq⟩
 
+theorem insertMany_list_equiv_foldl {l : List ((a : α) × β a)} (h : t₁.WF) :
+    t₁.insertMany l h.balanced ~m (l.foldl (init := t₁) fun acc p => acc.insert! p.1 p.2) := by
+  rw [insertMany_eq_foldl]
+
+theorem insertMany!_list_equiv_foldl {l : List ((a : α) × β a)} :
+    t₁.insertMany! l ~m (l.foldl (init := t₁) fun acc p => acc.insert! p.1 p.2) := by
+  rw [insertMany!_eq_foldl]
+
+theorem insertManyIfNew_list_equiv_foldl {l : List ((a : α) × β a)} (h : t₁.WF) :
+    t₁.insertManyIfNew l h.balanced ~m (l.foldl (init := t₁) fun acc p => acc.insertIfNew! p.1 p.2) := by
+  rw [insertManyIfNew_eq_foldl]
+
+theorem insertManyIfNew!_list_equiv_foldl {l : List ((a : α) × β a)} :
+    t₁.insertManyIfNew! l ~m (l.foldl (init := t₁) fun acc p => acc.insertIfNew! p.1 p.2) := by
+  rw [insertManyIfNew!_eq_foldl]
+
 section Const
 
 variable {β : Type v} {t₁ t₂ : Impl α β}
@@ -9321,6 +9358,22 @@ theorem Const.equiv_iff_keys_eq {t₁ t₂ : Impl α Unit} [TransOrd α] (h₁ :
   rw [List.map_inj_right fun _ _ => congrArg fun x : α => (⟨x, ()⟩ : (_ : α) × Unit)]
   exact ⟨(·.toListModel_eq h₁.ordered h₂.ordered), .mk ∘ .of_eq⟩
 
+theorem Const.insertMany_list_equiv_foldl {l : List (α × β)} (h : t₁.WF) :
+    insertMany t₁ l h.balanced ~m (l.foldl (init := t₁) fun acc p => acc.insert! p.1 p.2) := by
+  rw [insertMany_eq_foldl]
+
+theorem Const.insertMany!_list_equiv_foldl {l : List (α × β)} :
+    insertMany! t₁ l ~m (l.foldl (init := t₁) fun acc p => acc.insert! p.1 p.2) := by
+  rw [insertMany!_eq_foldl]
+
+theorem Const.insertManyIfNewUnit_list_equiv_foldl {t₁ : Impl α Unit} {l : List α} (h : t₁.WF) :
+    insertManyIfNewUnit t₁ l h.balanced ~m (l.foldl (init := t₁) fun acc a => acc.insertIfNew! a ()) := by
+  rw [insertManyIfNewUnit_eq_foldl]
+
+theorem Const.insertManyIfNewUnit!_list_equiv_foldl {t₁ : Impl α Unit} {l : List α} :
+    insertManyIfNewUnit! t₁ l ~m (l.foldl (init := t₁) fun acc a => acc.insertIfNew! a ()) := by
+  rw [insertManyIfNewUnit!_eq_foldl]
+
 end Const
 
 end Equiv
diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean
index 286cebe2d8..1c2a8fcb75 100644
--- a/src/Std/Data/DTreeMap/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Lemmas.lean
@@ -2140,6 +2140,9 @@ theorem unitOfList_cons {hd : α} {tl : List α} :
       insertManyIfNewUnit ((∅ : DTreeMap α Unit cmp).insertIfNew hd ()) tl :=
   ext Impl.Const.insertManyIfNewUnit_empty_list_cons
 
+theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} :
+    unitOfList l cmp = insertManyIfNewUnit ∅ l := rfl
+
 @[simp]
 theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
     (unitOfList l cmp).contains k = l.contains k :=
@@ -5904,6 +5907,26 @@ theorem equiv_iff_toList_eq [TransCmp cmp] :
     t₁ ~m t₂ ↔ t₁.toList = t₂.toList :=
   equiv_iff_equiv.trans (Impl.equiv_iff_toList_eq t₁.2 t₂.2)
 
+theorem insertMany_list_equiv_foldl {l : List ((a : α) × β a)} :
+    t₁.insertMany l ~m l.foldl (init := t₁) fun acc p => acc.insert p.1 p.2 := by
+  constructor
+  let : Ord α := ⟨cmp⟩
+  rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert! p.1 p.2)]
+  · exact Impl.insertMany_list_equiv_foldl t₁.wf
+  · exact fun _ _ => Impl.insert_eq_insert!.symm
+
+theorem ofList_equiv_foldl {l : List ((a : α) × β a)} :
+    ofList l cmp ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by
+  simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl
+
+theorem insertManyIfNew_list_equiv_foldl {l : List ((a : α) × β a)} :
+    t₁.insertManyIfNew l ~m l.foldl (init := t₁) fun acc p => acc.insertIfNew p.1 p.2 := by
+  constructor
+  let : Ord α := ⟨cmp⟩
+  rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insertIfNew! p.1 p.2)]
+  · exact Impl.insertManyIfNew_list_equiv_foldl t₁.wf
+  · exact fun _ _ => Impl.insertIfNew_eq_insertIfNew!.symm
+
 section Const
 
 variable {β : Type v} {t₁ t₂ : DTreeMap α β cmp}
@@ -5927,6 +5950,30 @@ theorem Equiv.of_constToList_perm : (Const.toList t₁).Perm (Const.toList t₂)
 theorem Equiv.of_keys_unit_perm {t₁ t₂ : DTreeMap α Unit cmp} : t₁.keys.Perm t₂.keys → t₁ ~m t₂ :=
   Const.equiv_iff_keys_unit_perm.mpr
 
+theorem Const.insertMany_list_equiv_foldl {l : List (α × β)} :
+    insertMany t₁ l ~m l.foldl (init := t₁) (fun acc p => acc.insert p.1 p.2) := by
+  constructor
+  let : Ord α := ⟨cmp⟩
+  rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert! p.1 p.2)]
+  · exact Impl.Const.insertMany_list_equiv_foldl t₁.wf
+  · exact fun _ _ => Impl.insert_eq_insert!.symm
+
+theorem Const.ofList_equiv_foldl {l : List (α × β)} :
+    ofList l cmp ~m l.foldl (init := ∅) (fun acc p => acc.insert p.1 p.2) := by
+  simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl
+
+theorem Const.insertManyIfNewUnit_list_equiv_foldl {t₁ : DTreeMap α Unit cmp} {l : List α} :
+    insertManyIfNewUnit t₁ l ~m l.foldl (init := t₁) (fun acc a => acc.insertIfNew a ()) := by
+  constructor
+  let : Ord α := ⟨cmp⟩
+  rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew! a ())]
+  · exact Impl.Const.insertManyIfNewUnit_list_equiv_foldl t₁.wf
+  · exact fun _ _ => Impl.insertIfNew_eq_insertIfNew!.symm
+
+theorem Const.unitOfList_equiv_foldl {l : List α} :
+    unitOfList l cmp ~m l.foldl (init := ∅) (fun acc a => acc.insertIfNew a ()) := by
+  simpa only [unitOfList_eq_insertManyIfNewUnit_empty] using insertManyIfNewUnit_list_equiv_foldl
+
 end Const
 
 end Equiv
diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
index adee7aae69..7c387f65ab 100644
--- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean
@@ -1894,9 +1894,7 @@ theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
 
 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]
+  ext Impl.ofList_eq_insertMany!
 
 @[simp, grind =]
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
@@ -2190,6 +2188,10 @@ theorem unitOfList_cons {hd : α} {tl : List α} :
       insertManyIfNewUnit ((∅ : Raw α Unit cmp).insertIfNew hd ()) tl :=
   ext Impl.Const.insertManyIfNewUnit_empty_list_cons_eq_insertManyIfNewUnit!
 
+theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} :
+    unitOfList l cmp = insertManyIfNewUnit ∅ l :=
+  ext Impl.Const.unitOfList_eq_insertManyIfNewUnit!
+
 @[simp]
 theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
     (unitOfList l cmp).contains k = l.contains k :=
@@ -5760,6 +5762,18 @@ theorem equiv_iff_toList_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
     t₁ ~m t₂ ↔ t₁.toList = t₂.toList :=
   equiv_iff.trans (Impl.equiv_iff_toList_eq h₁.1 h₂.1)
 
+theorem insertMany_list_equiv_foldl {l : List ((a : α) × β a)} :
+    t₁.insertMany l ~m l.foldl (init := t₁) fun acc p => acc.insert p.1 p.2 := by
+  constructor
+  let : Ord α := ⟨cmp⟩
+  rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert! p.1 p.2)]
+  · exact Impl.insertMany!_list_equiv_foldl
+  · exact fun _ _ => rfl
+
+theorem ofList_equiv_foldl {l : List ((a : α) × β a)} :
+    ofList l cmp ~m l.foldl (init := ∅) (fun acc p => acc.insert p.1 p.2) := by
+  simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl
+
 section Const
 
 variable {β : Type v} {t₁ t₂ : Raw α β cmp}
@@ -5785,6 +5799,30 @@ theorem Equiv.of_constToList_perm : (Const.toList t₁).Perm (Const.toList t₂)
 theorem Equiv.of_keys_unit_perm {t₁ t₂ : Raw α Unit cmp} : t₁.keys.Perm t₂.keys → t₁ ~m t₂ :=
   Const.equiv_iff_keys_unit_perm.mpr
 
+theorem Const.insertMany_list_equiv_foldl {l : List (α × β)} :
+    insertMany t₁ l ~m l.foldl (init := t₁) (fun acc p => acc.insert p.1 p.2) := by
+  constructor
+  let : Ord α := ⟨cmp⟩
+  rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert! p.1 p.2)]
+  · exact Impl.Const.insertMany!_list_equiv_foldl
+  · exact fun _ _ => rfl
+
+theorem Const.ofList_equiv_foldl {l : List (α × β)} :
+    ofList l cmp ~m l.foldl (init := ∅) (fun acc p => acc.insert p.1 p.2) := by
+  simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl
+
+theorem Const.insertManyIfNewUnit_list_equiv_foldl {t₁ : Raw α Unit cmp} {l : List α} :
+    insertManyIfNewUnit t₁ l ~m l.foldl (init := t₁) fun acc a => acc.insertIfNew a () := by
+  constructor
+  let : Ord α := ⟨cmp⟩
+  rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew! a ())]
+  · exact Impl.Const.insertManyIfNewUnit!_list_equiv_foldl
+  · exact fun _ _ => rfl
+
+theorem Const.unitOfList_equiv_foldl {l : List α} :
+    unitOfList l cmp ~m l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by
+  simpa only [unitOfList_eq_insertManyIfNewUnit_empty] using insertManyIfNewUnit_list_equiv_foldl
+
 end Const
 
 end Equiv
diff --git a/src/Std/Data/ExtDHashMap/Lemmas.lean b/src/Std/Data/ExtDHashMap/Lemmas.lean
index d546275334..8af4e17da6 100644
--- a/src/Std/Data/ExtDHashMap/Lemmas.lean
+++ b/src/Std/Data/ExtDHashMap/Lemmas.lean
@@ -1230,6 +1230,13 @@ theorem eq_empty_of_insertMany_eq_empty [EquivBEq α] [LawfulHashable α] {l : 
     m.insertMany l = ∅ → m = ∅ :=
   insertMany_ind m l id fun _ _ _ _ h => absurd h not_insert_eq_empty
 
+theorem insertMany_list_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} :
+    m.insertMany l = l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by
+  refine m.inductionOn fun m => ?_
+  rw [insertMany_list_mk, List.foldl_hom (g₁ := fun acc p => acc.insert p.1 p.2)]
+  · exact sound DHashMap.insertMany_list_equiv_foldl
+  · exact fun _ _ => rfl
+
 namespace Const
 
 variable {β : Type v} {m : ExtDHashMap α (fun _ => β)}
@@ -1496,6 +1503,13 @@ theorem getD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α]
   simp only [insertMany_list_mk]
   exact DHashMap.Const.getD_insertMany_list_of_mem k_beq distinct mem
 
+theorem insertMany_list_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
+    insertMany m l = l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by
+  refine m.inductionOn fun m => ?_
+  rw [insertMany_list_mk, List.foldl_hom (g₁ := fun acc p => acc.insert p.1 p.2)]
+  · exact sound DHashMap.Const.insertMany_list_equiv_foldl
+  · exact fun _ _ => rfl
+
 variable {m : ExtDHashMap α (fun _ => Unit)}
 variable {ρ : Type w} [ForIn Id ρ α]
 
@@ -1713,6 +1727,13 @@ theorem getD_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α]
     getD (insertManyIfNewUnit m l) k fallback = () :=
   rfl
 
+theorem insertManyIfNewUnit_list_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List α} :
+    insertManyIfNewUnit m l = l.foldl (init := m) fun acc a => acc.insertIfNew a () := by
+  refine m.inductionOn fun m => ?_
+  rw [insertManyIfNewUnit_list_mk, List.foldl_hom (g₁ := fun acc a => acc.insertIfNew a ())]
+  · exact sound DHashMap.Const.insertManyIfNewUnit_list_equiv_foldl
+  · exact fun _ _ => rfl
+
 end Const
 
 end insertMany
@@ -1868,6 +1889,10 @@ theorem ofList_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List ((a : α
   simpa only [← isEmpty_iff, ← List.isEmpty_iff, Bool.coe_iff_coe] using
     DHashMap.isEmpty_ofList
 
+theorem ofList_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} :
+    ofList l = l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by
+  rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl]
+
 namespace Const
 
 variable {β : Type v}
@@ -2021,6 +2046,10 @@ theorem ofList_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List (α × 
   simpa only [← isEmpty_iff, ← List.isEmpty_iff, Bool.coe_iff_coe] using
     DHashMap.Const.isEmpty_ofList
 
+theorem ofList_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
+    ofList l = l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by
+  rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl]
+
 @[simp]
 theorem unitOfList_nil [EquivBEq α] [LawfulHashable α] :
     unitOfList ([] : List α) = ∅ :=
@@ -2037,6 +2066,11 @@ theorem unitOfList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List 
   conv => rhs; apply insertManyIfNewUnit_list_mk
   exact congrArg mk DHashMap.Const.unitOfList_cons
 
+theorem unitOfList_eq_insertManyIfNewUnit_empty [EquivBEq α] [LawfulHashable α] {l : List α} :
+    unitOfList l = insertManyIfNewUnit ∅ l := by
+  conv => rhs; apply insertManyIfNewUnit_list_mk
+  exact congrArg mk DHashMap.Const.unitOfList_eq_insertManyIfNewUnit_empty
+
 @[simp]
 theorem contains_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
@@ -2136,6 +2170,10 @@ theorem getD_unitOfList [EquivBEq α] [LawfulHashable α]
     getD (unitOfList l) k fallback = () :=
   DHashMap.Const.getD_unitOfList
 
+theorem unitOfList_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List α} :
+    unitOfList l = l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by
+  rw [unitOfList_eq_insertManyIfNewUnit_empty, insertManyIfNewUnit_list_eq_foldl]
+
 end Const
 
 section Union
diff --git a/src/Std/Data/ExtDTreeMap/Lemmas.lean b/src/Std/Data/ExtDTreeMap/Lemmas.lean
index 29ae68d420..ebe6e505f6 100644
--- a/src/Std/Data/ExtDTreeMap/Lemmas.lean
+++ b/src/Std/Data/ExtDTreeMap/Lemmas.lean
@@ -1525,6 +1525,13 @@ theorem insertMany_list_eq_empty_iff [TransCmp cmp] {l : List ((a : α) × β a)
     t.insertMany l = ∅ ↔ t = ∅ ∧ l = [] := by
   simp only [← isEmpty_iff, isEmpty_insertMany_list, Bool.and_eq_true, List.isEmpty_iff]
 
+theorem insertMany_list_eq_foldl [TransCmp cmp] {l : List ((a : α) × β a)} :
+    t.insertMany l = l.foldl (init := t) fun acc p => acc.insert p.1 p.2 := by
+  refine t.inductionOn fun m => ?_
+  rw [insertMany_list_mk, List.foldl_hom (g₁ := fun acc p => acc.insert p.1 p.2)]
+  · exact sound DTreeMap.insertMany_list_equiv_foldl
+  · exact fun _ _ => rfl
+
 namespace Const
 
 variable {β : Type v} {t : ExtDTreeMap α β cmp}
@@ -1775,6 +1782,13 @@ theorem getD_insertMany_list_of_mem [TransCmp cmp]
   simp only [insertMany_list_mk]
   exact DTreeMap.Const.getD_insertMany_list_of_mem k_eq distinct mem
 
+theorem insertMany_list_eq_foldl [TransCmp cmp] {l : List (α × β)} :
+    insertMany t l = l.foldl (init := t) fun acc p => acc.insert p.1 p.2 := by
+  refine t.inductionOn fun m => ?_
+  rw [insertMany_list_mk, List.foldl_hom (g₁ := fun acc p => acc.insert p.1 p.2)]
+  · exact sound DTreeMap.Const.insertMany_list_equiv_foldl
+  · exact fun _ _ => rfl
+
 variable {t : ExtDTreeMap α Unit cmp}
 
 @[simp]
@@ -1968,6 +1982,13 @@ theorem getD_insertManyIfNewUnit_list [TransCmp cmp]
     getD (insertManyIfNewUnit t l) k fallback = () :=
   rfl
 
+theorem insertManyIfNewUnit_list_eq_foldl [TransCmp cmp] {l : List α} :
+    insertManyIfNewUnit t l = l.foldl (init := t) fun acc a => acc.insertIfNew a () := by
+  refine t.inductionOn fun t => ?_
+  rw [insertManyIfNewUnit_list_mk, List.foldl_hom (g₁ := fun acc a => acc.insertIfNew a ())]
+  · exact sound DTreeMap.Const.insertManyIfNewUnit_list_equiv_foldl
+  · exact fun _ _ => rfl
+
 end Const
 
 @[simp, grind =]
@@ -2114,6 +2135,10 @@ theorem ofList_eq_empty_iff [TransCmp cmp] {l : List ((a : α) × β a)} :
     ofList l cmp = ∅ ↔ l = [] := by
   simpa [← isEmpty_iff, ← List.isEmpty_iff] using DTreeMap.isEmpty_ofList
 
+theorem ofList_eq_foldl [TransCmp cmp] {l : List ((a : α) × β a)} :
+    ofList l cmp = l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by
+  rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl]
+
 namespace Const
 
 variable {β : Type v}
@@ -2260,6 +2285,10 @@ theorem ofList_eq_empty_iff [TransCmp cmp] {l : List (α × β)} :
     ofList l cmp = ∅ ↔ l = [] := by
   simpa only [← isEmpty_iff, ← List.isEmpty_iff, Bool.coe_iff_coe] using DTreeMap.Const.isEmpty_ofList
 
+theorem ofList_eq_foldl [TransCmp cmp] {l : List (α × β)} :
+    ofList l cmp = l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by
+  rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl]
+
 @[simp]
 theorem unitOfList_nil : unitOfList ([] : List α) cmp = (∅ : ExtDTreeMap α Unit cmp) := rfl
 
@@ -2274,6 +2303,11 @@ theorem unitOfList_cons [TransCmp cmp] {hd : α} {tl : List α} :
   conv => rhs; apply insertManyIfNewUnit_list_mk
   exact congrArg mk DTreeMap.Const.unitOfList_cons
 
+theorem unitOfList_eq_insertManyIfNewUnit_empty [TransCmp cmp] {l : List α} :
+    unitOfList l cmp = insertManyIfNewUnit ∅ l := by
+  conv => rhs; apply insertManyIfNewUnit_list_mk
+  exact congrArg mk DTreeMap.Const.unitOfList_eq_insertManyIfNewUnit_empty
+
 @[simp]
 theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
     (unitOfList l cmp).contains k = l.contains k :=
@@ -2364,6 +2398,10 @@ theorem getD_unitOfList [TransCmp cmp] {l : List α} {k : α} {fallback : Unit}
     getD (unitOfList l cmp) k fallback = () :=
   rfl
 
+theorem unitOfList_eq_foldl [TransCmp cmp] {l : List α} :
+    unitOfList l cmp = l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by
+  rw [unitOfList_eq_insertManyIfNewUnit_empty, insertManyIfNewUnit_list_eq_foldl]
+
 end Const
 
 section Union
diff --git a/src/Std/Data/ExtHashMap/Lemmas.lean b/src/Std/Data/ExtHashMap/Lemmas.lean
index 43c885f264..e26960d412 100644
--- a/src/Std/Data/ExtHashMap/Lemmas.lean
+++ b/src/Std/Data/ExtHashMap/Lemmas.lean
@@ -929,6 +929,12 @@ theorem eq_empty_of_insertMany_eq_empty [EquivBEq α] [LawfulHashable α] {l : 
     m.insertMany l = ∅ → m = ∅ := by
   simpa only [ext_iff] using ExtDHashMap.Const.eq_empty_of_insertMany_eq_empty
 
+theorem insertMany_list_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
+    m.insertMany l = l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by
+  rw [ext_iff, ← List.foldl_hom ExtHashMap.inner (g₂ := fun acc p => acc.insert p.1 p.2)]
+  · exact ExtDHashMap.Const.insertMany_list_eq_foldl
+  · exact fun _ _ => rfl
+
 variable {m : ExtHashMap α Unit}
 variable {ρ : Type w} [ForIn Id ρ α]
 
@@ -1097,6 +1103,12 @@ theorem eq_empty_of_insertManyIfNewUnit_eq_empty [EquivBEq α] [LawfulHashable 
     insertManyIfNewUnit m l = ∅ → m = ∅ := by
   simpa only [ext_iff] using ExtDHashMap.Const.eq_empty_of_insertManyIfNewUnit_eq_empty
 
+theorem insertManyIfNewUnit_list_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List α} :
+    insertManyIfNewUnit m l = l.foldl (init := m) fun acc a => acc.insertIfNew a () := by
+  rw [ext_iff, ← List.foldl_hom ExtHashMap.inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact ExtDHashMap.Const.insertManyIfNewUnit_list_eq_foldl
+  · exact fun _ _ => rfl
+
 end
 
 section
@@ -1247,6 +1259,10 @@ theorem ofList_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List (α × 
     ofList l = ∅ ↔ l = [] :=
   ext_iff.trans ExtDHashMap.Const.ofList_eq_empty_iff
 
+theorem ofList_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List (α × β)} :
+    ofList l = l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by
+  rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl]
+
 @[simp]
 theorem unitOfList_nil [EquivBEq α] [LawfulHashable α] :
     unitOfList ([] : List α) = ∅ :=
@@ -1262,6 +1278,10 @@ theorem unitOfList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List 
       insertManyIfNewUnit ((∅ : ExtHashMap α Unit).insertIfNew hd ()) tl :=
   ext ExtDHashMap.Const.unitOfList_cons
 
+theorem unitOfList_eq_insertManyIfNewUnit_empty [EquivBEq α] [LawfulHashable α] {l : List α} :
+    unitOfList l = insertManyIfNewUnit ∅ l :=
+  ext ExtDHashMap.Const.unitOfList_eq_insertManyIfNewUnit_empty
+
 @[simp]
 theorem contains_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
@@ -1360,6 +1380,10 @@ theorem unitOfList_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List α}
     unitOfList l = ∅ ↔ l = [] :=
   ext_iff.trans ExtDHashMap.Const.unitOfList_eq_empty_iff
 
+theorem unitOfList_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List α} :
+    unitOfList l = l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by
+  rw [unitOfList_eq_insertManyIfNewUnit_empty, insertManyIfNewUnit_list_eq_foldl]
+
 end
 
 section Union
diff --git a/src/Std/Data/ExtHashSet/Lemmas.lean b/src/Std/Data/ExtHashSet/Lemmas.lean
index e15720822f..7d394342ee 100644
--- a/src/Std/Data/ExtHashSet/Lemmas.lean
+++ b/src/Std/Data/ExtHashSet/Lemmas.lean
@@ -566,6 +566,12 @@ theorem eq_empty_of_insertMany_eq_empty [EquivBEq α] [LawfulHashable α] {l : 
     m.insertMany l = ∅ → m = ∅ := by
   simpa only [ext_iff] using ExtHashMap.eq_empty_of_insertManyIfNewUnit_eq_empty
 
+theorem insertMany_list_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List α} :
+    m.insertMany l = l.foldl (init := m) fun acc a => acc.insert a := by
+  rw [ext_iff, ← List.foldl_hom ExtHashSet.inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact ExtHashMap.insertManyIfNewUnit_list_eq_foldl
+  · exact fun _ _ => rfl
+
 end
 
 section
@@ -588,9 +594,7 @@ theorem ofList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List α} :
 
 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]
+  ext ExtHashMap.unitOfList_eq_insertManyIfNewUnit_empty
 
 @[simp, grind =]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
@@ -667,6 +671,10 @@ theorem ofList_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List α} :
     ofList l = ∅ ↔ l = [] :=
   ext_iff.trans ExtHashMap.unitOfList_eq_empty_iff
 
+theorem ofList_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List α} :
+    ofList l = l.foldl (init := ∅) fun acc a => acc.insert a := by
+  rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl]
+
 end
 
 section Ext
diff --git a/src/Std/Data/ExtTreeMap/Lemmas.lean b/src/Std/Data/ExtTreeMap/Lemmas.lean
index f0b558f49a..bd227bd3f3 100644
--- a/src/Std/Data/ExtTreeMap/Lemmas.lean
+++ b/src/Std/Data/ExtTreeMap/Lemmas.lean
@@ -1111,6 +1111,12 @@ theorem getD_insertMany_list_of_mem [TransCmp cmp]
     (t.insertMany l).getD k' fallback = v :=
   ExtDTreeMap.Const.getD_insertMany_list_of_mem k_eq distinct mem
 
+theorem insertMany_list_eq_foldl [TransCmp cmp] {l : List (α × β)} :
+    t.insertMany l = l.foldl (init := t) fun acc p => acc.insert p.1 p.2 := by
+  rw [ext_iff, ← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)]
+  · exact ExtDTreeMap.Const.insertMany_list_eq_foldl
+  · exact fun _ _ => rfl
+
 section Unit
 
 variable {t : ExtTreeMap α Unit cmp}
@@ -1261,6 +1267,12 @@ theorem getD_insertManyIfNewUnit_list [TransCmp cmp]
     getD (insertManyIfNewUnit t l) k fallback = () :=
   rfl
 
+theorem insertManyIfNewUnit_list_eq_foldl [TransCmp cmp] {l : List α} :
+    insertManyIfNewUnit t l = l.foldl (init := t) fun acc a => acc.insertIfNew a () := by
+  rw [ext_iff, ← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact ExtDTreeMap.Const.insertManyIfNewUnit_list_eq_foldl
+  · exact fun _ _ => rfl
+
 end Unit
 
 @[simp, grind =]
@@ -1405,6 +1417,10 @@ theorem ofList_eq_empty_iff [TransCmp cmp] {l : List (α × β)} :
     ofList l cmp = ∅ ↔ l = [] :=
   ext_iff.trans ExtDTreeMap.Const.ofList_eq_empty_iff
 
+theorem ofList_eq_foldl [TransCmp cmp] {l : List (α × β)} :
+    ofList l cmp = l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by
+  rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl]
+
 @[simp]
 theorem unitOfList_nil :
     unitOfList ([] : List α) cmp =
@@ -1421,6 +1437,10 @@ theorem unitOfList_cons [TransCmp cmp] {hd : α} {tl : List α} :
       insertManyIfNewUnit ((∅ : ExtTreeMap α Unit cmp).insertIfNew hd ()) tl :=
   ext ExtDTreeMap.Const.unitOfList_cons
 
+theorem unitOfList_eq_insertManyIfNewUnit_empty [TransCmp cmp] {l : List α} :
+    unitOfList l cmp = insertManyIfNewUnit ∅ l :=
+  ext ExtDTreeMap.Const.unitOfList_eq_insertManyIfNewUnit_empty
+
 @[simp]
 theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
     (unitOfList l cmp).contains k = l.contains k :=
@@ -1511,6 +1531,10 @@ theorem getD_unitOfList [TransCmp cmp] {l : List α} {k : α} {fallback : Unit}
     getD (unitOfList l cmp) k fallback = () :=
   rfl
 
+theorem unitOfList_eq_foldl [TransCmp cmp] {l : List α} :
+    unitOfList l cmp = l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by
+  rw [unitOfList_eq_insertManyIfNewUnit_empty, insertManyIfNewUnit_list_eq_foldl]
+
 section Union
 
 variable {t₁ t₂ : ExtTreeMap α β cmp}
diff --git a/src/Std/Data/ExtTreeSet/Lemmas.lean b/src/Std/Data/ExtTreeSet/Lemmas.lean
index b08e9ba406..9b5d727029 100644
--- a/src/Std/Data/ExtTreeSet/Lemmas.lean
+++ b/src/Std/Data/ExtTreeSet/Lemmas.lean
@@ -1017,6 +1017,12 @@ theorem insertMany_list_eq_empty_iff [TransCmp cmp] {l : List α} :
     t.insertMany l = ∅ ↔ t = ∅ ∧ l = [] := by
   simpa only [ext_iff] using ExtTreeMap.insertManyIfNewUnit_list_eq_empty_iff
 
+theorem insertMany_list_eq_foldl [TransCmp cmp] {l : List α} :
+    t.insertMany l = l.foldl (init := t) fun acc a => acc.insert a := by
+  rw [ext_iff, ← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact ExtTreeMap.insertManyIfNewUnit_list_eq_foldl
+  · exact fun _ _ => rfl
+
 @[simp, grind =]
 theorem ofList_nil :
     ofList ([] : List α) cmp =
@@ -1036,9 +1042,7 @@ theorem ofList_cons [TransCmp cmp] {hd : α} {tl : List α} :
 
 theorem ofList_eq_insertMany_empty [TransCmp cmp] {l : List α} :
     ofList l cmp = insertMany (∅ : ExtTreeSet α cmp) l :=
-  match l with
-  | [] => by simp
-  | hd :: tl => by simp [ofList_cons, insertMany_cons]
+  ext ExtTreeMap.unitOfList_eq_insertManyIfNewUnit_empty
 
 @[simp, grind =]
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
@@ -1112,6 +1116,10 @@ theorem ofList_eq_empty_iff [TransCmp cmp] {l : List α} :
     ofList l cmp = ∅ ↔ l = [] :=
   ext_iff.trans ExtTreeMap.unitOfList_eq_empty_iff
 
+theorem ofList_eq_foldl [TransCmp cmp] {l : List α} :
+    ofList l cmp = l.foldl (init := ∅) fun acc a => acc.insert a := by
+  rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl]
+
 section Min
 
 @[simp, grind =]
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 8b23eb5102..f10d3323bc 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -2540,6 +2540,10 @@ theorem unitOfList_cons {hd : α} {tl : List α} :
       insertManyIfNewUnit ((∅ : HashMap α Unit).insertIfNew hd ()) tl :=
   ext DHashMap.Const.unitOfList_cons
 
+theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} :
+    unitOfList l = insertManyIfNewUnit ∅ l :=
+  ext DHashMap.Const.unitOfList_eq_insertManyIfNewUnit_empty
+
 @[simp]
 theorem contains_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
@@ -3165,6 +3169,29 @@ theorem equiv_iff_keys_unit_perm {m₁ m₂ : HashMap α Unit} [EquivBEq α] [La
     m₁ ~m m₂ ↔ m₁.keys.Perm m₂.keys :=
   ⟨Equiv.keys_perm, Equiv.of_keys_unit_perm⟩
 
+theorem insertMany_list_equiv_foldl {m : HashMap α β} {l : List (α × β)} :
+    m.insertMany l ~m l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)]
+  · exact DHashMap.Const.insertMany_list_equiv_foldl
+  · exact fun _ _ => rfl
+
+theorem ofList_equiv_foldl {l : List (α × β)} :
+    ofList l ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 :=
+  insertMany_list_equiv_foldl
+
+theorem insertManyIfNewUnit_list_equiv_foldl {m : HashMap α Unit}
+    {l : List α} :
+    insertManyIfNewUnit m l ~m l.foldl (init := m) fun acc a=> acc.insertIfNew a () := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact DHashMap.Const.insertManyIfNewUnit_list_equiv_foldl
+  · exact fun _ _ => rfl
+
+theorem unitOfList_equiv_foldl {l : List α} :
+    unitOfList l ~m l.foldl (init := ∅) fun acc a => acc.insertIfNew a () :=
+  insertManyIfNewUnit_list_equiv_foldl
+
 end Equiv
 
 section filterMap
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index 37bbc386ee..e154b2e3fa 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -2598,6 +2598,10 @@ theorem unitOfList_cons {hd : α} {tl : List α} :
     unitOfList (hd :: tl) = insertManyIfNewUnit ((∅ : Raw α Unit).insertIfNew hd ()) tl :=
   ext DHashMap.Raw.Const.unitOfList_cons
 
+theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} :
+    unitOfList l = insertManyIfNewUnit ∅ l :=
+  ext DHashMap.Raw.Const.unitOfList_eq_insertManyIfNewUnit_empty
+
 @[simp]
 theorem contains_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} {k : α} :
@@ -3231,6 +3235,29 @@ theorem equiv_iff_keys_unit_perm [EquivBEq α] [LawfulHashable α] {m₁ m₂ :
     m₁ ~m m₂ ↔ m₁.keys.Perm m₂.keys :=
   ⟨Equiv.keys_perm, Equiv.of_keys_unit_perm⟩
 
+theorem insertMany_list_equiv_foldl {m : HashMap.Raw α β} {l : List (α × β)} (h : m.WF) :
+    m.insertMany l ~m l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)]
+  · exact DHashMap.Raw.Const.insertMany_list_equiv_foldl h.1
+  · exact fun _ _ => rfl
+
+theorem ofList_equiv_foldl {l : List (α × β)} :
+    ofList l ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 :=
+  insertMany_list_equiv_foldl .empty
+
+theorem insertManyIfNewUnit_list_equiv_foldl {m : HashMap.Raw α Unit}
+    {l : List α} (h : m.WF) :
+    insertManyIfNewUnit m l ~m l.foldl (init := m) fun acc a => acc.insertIfNew a () := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact DHashMap.Raw.Const.insertManyIfNewUnit_list_equiv_foldl h.1
+  · exact fun _ _ => rfl
+
+theorem unitOfList_equiv_foldl {l : List α} :
+    unitOfList l ~m l.foldl (init := ∅) fun acc a => acc.insertIfNew a () :=
+  insertManyIfNewUnit_list_equiv_foldl .empty
+
 section filterMap
 
 theorem toList_filterMap {f : α → β → Option γ} (h : m.WF) :
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index 661baf78cf..005a9edae7 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -1271,9 +1271,7 @@ theorem ofList_singleton {k : α} :
 
 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]
+  ext HashMap.unitOfList_eq_insertManyIfNewUnit_empty
 
 @[simp, grind =]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
@@ -1460,6 +1458,20 @@ theorem equiv_iff_toList_perm [EquivBEq α] [LawfulHashable α] :
     m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList :=
   ⟨Equiv.toList_perm, Equiv.of_toList_perm⟩
 
+theorem insertMany_list_equiv_foldl {m : HashSet α} {l : List α} :
+    m.insertMany l ~m l.foldl (init := m) fun acc a => acc.insert a := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact HashMap.insertManyIfNewUnit_list_equiv_foldl
+  · exact fun _ _ => rfl
+
+theorem ofList_equiv_foldl {l : List α} :
+    ofList l ~m l.foldl (init := ∅) fun acc a => acc.insert a := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact HashMap.unitOfList_equiv_foldl
+  · exact fun _ _ => rfl
+
 end Equiv
 
 section filter
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index bfb5b13e7f..db38785692 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -1353,9 +1353,7 @@ theorem ofList_cons {hd : α} {tl : List α} :
 
 theorem ofList_eq_insertMany_empty {l : List α} :
     ofList l = insertMany (∅ : Raw α) l :=
-  match l with
-  | [] => by simp [insertMany_nil .empty]
-  | hd :: tl => by simp [ofList_cons, insertMany_cons .empty]
+  ext HashMap.Raw.unitOfList_eq_insertManyIfNewUnit_empty
 
 @[simp, grind =]
 theorem contains_ofList [EquivBEq α] [LawfulHashable α]
@@ -1539,6 +1537,20 @@ theorem equiv_iff_toList_perm {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable
     m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList :=
   ⟨Equiv.toList_perm, Equiv.of_toList_perm⟩
 
+theorem insertMany_list_equiv_foldl {l : List α} (h : m.WF) :
+    insertMany m l ~m l.foldl (init := m) fun acc a => acc.insert a := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact HashMap.Raw.insertManyIfNewUnit_list_equiv_foldl h.1
+  · exact fun _ _ => rfl
+
+theorem ofList_equiv_foldl {l : List α} :
+    ofList l ~m l.foldl (init := ∅) fun acc a => acc.insert a := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact HashMap.Raw.unitOfList_equiv_foldl
+  · exact fun _ _ => rfl
+
 section filter
 
 theorem toList_filter {f : α → Bool} (h : m.WF) :
diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean
index f771b0b2f6..4476a7aae6 100644
--- a/src/Std/Data/TreeMap/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Lemmas.lean
@@ -1440,6 +1440,9 @@ theorem unitOfList_cons {hd : α} {tl : List α} :
       insertManyIfNewUnit ((∅ : TreeMap α Unit cmp).insertIfNew hd ()) tl :=
   ext DTreeMap.Const.unitOfList_cons
 
+theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} :
+    unitOfList l cmp = insertManyIfNewUnit ∅ l := rfl
+
 @[simp]
 theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
     (unitOfList l cmp).contains k = l.contains k :=
@@ -4354,6 +4357,28 @@ theorem equiv_iff_keys_unit_eq [TransCmp cmp] {t₁ t₂ : TreeMap α Unit cmp}
 theorem Equiv.of_keys_unit_perm {t₁ t₂ : TreeMap α Unit cmp} : t₁.keys.Perm t₂.keys → t₁ ~m t₂ :=
   equiv_iff_keys_unit_perm.mpr
 
+theorem insertMany_list_equiv_foldl {l : List (α × β)} :
+    insertMany t₁ l ~m l.foldl (init := t₁) (fun acc p => acc.insert p.1 p.2) := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)]
+  · exact DTreeMap.Const.insertMany_list_equiv_foldl
+  · exact fun _ _ => rfl
+
+theorem ofList_equiv_foldl {l : List (α × β)} :
+    ofList l cmp ~m l.foldl (init := ∅) (fun acc p => acc.insert p.1 p.2) := by
+  simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl
+
+theorem insertManyIfNewUnit_list_equiv_foldl {t₁ : TreeMap α Unit cmp} {l : List α} :
+    insertManyIfNewUnit t₁ l ~m l.foldl (init := t₁) fun acc a => acc.insertIfNew a () := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact DTreeMap.Const.insertManyIfNewUnit_list_equiv_foldl
+  · exact fun _ _ => rfl
+
+theorem unitOfList_equiv_foldl {l : List α} :
+    unitOfList l cmp ~m l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by
+  simpa only [unitOfList_eq_insertManyIfNewUnit_empty] using insertManyIfNewUnit_list_equiv_foldl
+
 end Equiv
 
 section filterMap
diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean
index a302501b92..debe687b75 100644
--- a/src/Std/Data/TreeMap/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean
@@ -1465,6 +1465,10 @@ theorem unitOfList_cons {hd : α} {tl : List α} :
       insertManyIfNewUnit ((∅ : Raw α Unit cmp).insertIfNew hd ()) tl :=
   ext DTreeMap.Raw.Const.unitOfList_cons
 
+theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} :
+    unitOfList l cmp = insertManyIfNewUnit ∅ l :=
+  ext DTreeMap.Raw.Const.unitOfList_eq_insertManyIfNewUnit_empty
+
 @[simp]
 theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
     (unitOfList l cmp).contains k = l.contains k :=
@@ -4098,6 +4102,28 @@ theorem equiv_iff_keys_unit_eq {t₁ t₂ : Raw α Unit cmp} [TransCmp cmp] (h
 theorem Equiv.of_keys_unit_perm {t₁ t₂ : Raw α Unit cmp} : t₁.keys.Perm t₂.keys → t₁ ~m t₂ :=
   equiv_iff_keys_unit_perm.mpr
 
+theorem insertMany_list_equiv_foldl {l : List (α × β)} :
+    insertMany t₁ l ~m l.foldl (init := t₁) (fun acc p => acc.insert p.1 p.2) := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)]
+  · exact DTreeMap.Raw.Const.insertMany_list_equiv_foldl
+  · exact fun _ _ => rfl
+
+theorem ofList_equiv_foldl {l : List (α × β)} :
+    ofList l cmp ~m l.foldl (init := ∅) (fun acc p => acc.insert p.1 p.2) := by
+  simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl
+
+theorem insertManyIfNewUnit_list_equiv_foldl {t₁ : Raw α Unit cmp} {l : List α} :
+    insertManyIfNewUnit t₁ l ~m l.foldl (init := t₁) fun acc a => acc.insertIfNew a () := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact DTreeMap.Raw.Const.insertManyIfNewUnit_list_equiv_foldl
+  · exact fun _ _ => rfl
+
+theorem unitOfList_equiv_foldl {l : List α} :
+    unitOfList l cmp ~m l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by
+  simpa only [unitOfList_eq_insertManyIfNewUnit_empty] using insertManyIfNewUnit_list_equiv_foldl
+
 end Equiv
 
 section filterMap
diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean
index d71ac6edd9..bb89b63391 100644
--- a/src/Std/Data/TreeSet/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Lemmas.lean
@@ -1126,9 +1126,7 @@ theorem ofList_cons {hd : α} {tl : List α} :
 
 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]
+  ext TreeMap.unitOfList_eq_insertManyIfNewUnit_empty
 
 @[simp, grind =]
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
@@ -2304,6 +2302,17 @@ theorem equiv_iff_toList_eq [TransCmp cmp] :
     t₁ ~m t₂ ↔ t₁.toList = t₂.toList :=
   equiv_iff_equiv.trans TreeMap.equiv_iff_keys_unit_eq
 
+theorem insertMany_list_equiv_foldl {l : List α} :
+    insertMany t₁ l ~m l.foldl (init := t₁) fun acc a => acc.insert a := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact TreeMap.insertManyIfNewUnit_list_equiv_foldl
+  · exact fun _ _ => rfl
+
+theorem ofList_equiv_foldl {l : List α} :
+    ofList l cmp ~m l.foldl (init := ∅) fun acc a => acc.insert a := by
+  simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl
+
 end Equiv
 
 section filter
diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean
index 8ddb016bd7..1a8e8b9f3a 100644
--- a/src/Std/Data/TreeSet/Raw/Lemmas.lean
+++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean
@@ -1176,9 +1176,7 @@ theorem ofList_cons {hd : α} {tl : List α} :
 
 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]
+  ext TreeMap.Raw.unitOfList_eq_insertManyIfNewUnit_empty
 
 @[simp, grind =]
 theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
@@ -2145,6 +2143,17 @@ theorem equiv_iff_toList_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
     t₁ ~m t₂ ↔ t₁.toList = t₂.toList :=
   equiv_iff.trans (TreeMap.Raw.equiv_iff_keys_unit_eq h₁.1 h₂.1)
 
+theorem insertMany_list_equiv_foldl {l : List α} :
+    insertMany t₁ l ~m l.foldl (init := t₁) fun acc a => acc.insert a := by
+  constructor
+  rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())]
+  · exact TreeMap.Raw.insertManyIfNewUnit_list_equiv_foldl
+  · exact fun _ _ => rfl
+
+theorem ofList_equiv_foldl {l : List α} :
+    ofList l cmp ~m l.foldl (init := ∅) fun acc a => acc.insert a := by
+  simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl
+
 end Equiv
 
 section filter