feat: tree map toArray/keysArray lemmas (#12481)

This PR provides lemmas about `toArray` and `keysArray` on tree maps and
tree sets that are analogous to the existing `toList` and `keys` lemmas.

src/Init/Data/Array/Basic.lean

@@ -148,6 +148,9 @@ end List
 
 namespace Array
 
+@[simp, grind =] theorem getElem!_toList [Inhabited α] {xs : Array α} {i : Nat} : xs.toList[i]! = xs[i]! := by
+  rw [List.getElem!_toArray]
+
 theorem size_eq_length_toList {xs : Array α} : xs.size = xs.toList.length := rfl
 
 /-! ### Externs -/

src/Init/Data/List/Lemmas.lean

@@ -936,6 +936,12 @@ theorem getElem_zero_eq_head {l : List α} (h : 0 < l.length) :
   | nil => simp at h
   | cons _ _ => simp
 
+theorem head!_eq_getElem! [Inhabited α] {l : List α} : head! l = l[0]! := by
+  cases l <;> rfl
+
+theorem headD_eq_getD {l : List α} {fallback} : headD l fallback = l.getD 0 fallback := by
+  cases l <;> rfl
+
 theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head? = some a := by
   cases xs with
   | nil => simp at h

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

@@ -8,6 +8,7 @@ module
 prelude
 public import Std.Data.HashMap.Basic
 public import Std.Data.DTreeMap.Internal.WF.Lemmas
+public import Init.Data.Array.Perm
 public meta import Std.Data.HashMap.Basic
 import Init.Data.List.Find
 import Init.Data.List.Pairwise
@@ -104,10 +105,13 @@ private meta def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (T
      ⟨`getKeyD, (``getKeyD_eq_getKeyD, #[``(getKeyD_of_perm _)])⟩,
      ⟨`getKey!, (``getKey!_eq_getKey!, #[``(getKey!_of_perm _)])⟩,
      ⟨`toList, (``toList_eq_toListModel, #[])⟩,
+     ⟨`toArray, (``toArray_eq_toArray, #[])⟩,
      ⟨`beq, (``beq_eq_beqModel, #[])⟩,
      ⟨`Const.beq, (``Internal.Impl.Const.beq_eq_beqModel, #[])⟩,
      ⟨`keys, (``keys_eq_keys, #[])⟩,
+     ⟨`keysArray, (``keysArray_eq_toArray_keys, #[])⟩,
      ⟨`Const.toList, (``Const.toList_eq_toListModel_map, #[])⟩,
+     ⟨`Const.toArray, (``Const.toArray_eq_toArray_map, #[])⟩,
      ⟨`foldlM, (``foldlM_eq_foldlM_toListModel, #[])⟩,
      ⟨`foldl, (``foldl_eq_foldl, #[])⟩,
      ⟨`foldrM, (``foldrM_eq_foldrM, #[])⟩,
@@ -228,6 +232,18 @@ theorem isEmpty_iff_forall_not_mem [TransOrd α] (h : t.WF) :
     t.isEmpty = true ↔ ∀ a, ¬a ∈ t := by
   simpa only [mem_iff_contains, Bool.not_eq_true] using isEmpty_iff_forall_contains h
 
+theorem toArray_toList : t.toList.toArray = t.toArray := by
+  simp_to_model [toList, toArray]
+
+theorem toList_toArray : t.toArray.toList = t.toList := by
+  simp_to_model [toList, toArray]
+
+theorem toArray_keys : t.keys.toArray = t.keysArray := by
+  simp_to_model [Const.toList, keys, keysArray]
+
+theorem toList_keysArray : t.keysArray.toList = t.keys := by
+  simp_to_model [Const.toList, keys, keysArray]
+
 theorem contains_insert [TransOrd α] (h : t.WF) {k a : α} {v : β k} :
     (t.insert k v h.balanced).impl.contains a = (compare k a == .eq || t.contains a) := by
   simp_to_model [insert, contains] using List.containsKey_insertEntry
@@ -580,6 +596,12 @@ namespace Const
 
 variable {β : Type v} {t : Impl α β}
 
+theorem toArray_toList : (toList t).toArray = toArray t := by
+  simp_to_model [Const.toList, Const.toArray]
+
+theorem toList_toArray : (toArray t).toList = toList t := by
+  simp_to_model [Const.toList, Const.toArray]
+
 theorem get?_empty [TransOrd α] {a : α} : get? (empty : Impl α β) a = none := by
   simp_to_model [Const.get?] using List.getValue?_nil
 
@@ -676,6 +698,18 @@ theorem toList_insert!_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF)
     (t.insert! k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) := by
   simpa only [insert_eq_insert!] using toList_insert_perm h
 
+theorem toArray_insert_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insert k v h.balanced).1.toArray.Perm (t.toArray.filter (¬k == ·.1) |>.push ⟨k, v⟩) := by
+  simp only [← toArray_toList, List.filter_toArray', List.push_toArray,
+    ← List.perm_iff_toArray_perm, List.size_toArray]
+  refine (toList_insert_perm h).trans ?_
+  rw [← List.singleton_append]
+  apply List.perm_append_comm
+
+theorem toArray_insert!_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insert! k v).toArray.Perm (t.toArray.filter (¬k == ·.1) |>.push ⟨k, v⟩) := by
+  simpa only [insert_eq_insert!] using toArray_insert_perm h
+
 theorem Const.toList_insert_perm {β : Type v} {t : Impl α (fun _ => β)} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β} :
     (Const.toList (t.insert k v h.balanced).1).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) := by
   simp_to_model
@@ -687,6 +721,18 @@ theorem Const.toList_insert!_perm {β : Type v} {t : Impl α (fun _ => β)} [BEq
     (Const.toList (t.insert! k v)).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) := by
   simpa only [insert_eq_insert!] using Const.toList_insert_perm h
 
+theorem Const.toArray_insert_perm {β : Type v} {t : Impl α (fun _ => β)} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β} :
+    (Const.toArray (t.insert k v h.balanced).1).Perm ((Const.toArray t).filter (¬k == ·.1) |>.push ⟨k, v⟩) := by
+  simp only [← toArray_toList, List.size_toArray, List.filter_toArray', List.push_toArray,
+    ← List.perm_iff_toArray_perm]
+  refine (toList_insert_perm h).trans ?_
+  rw [← List.singleton_append]
+  apply List.perm_append_comm
+
+theorem Const.toArray_insert!_perm {β : Type v} {t : Impl α (fun _ => β)} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β} :
+    (Const.toArray (t.insert! k v)).Perm ((Const.toArray t).filter (¬k == ·.1) |>.push ⟨k, v⟩) := by
+  simpa only [insert_eq_insert!] using Const.toArray_insert_perm h
+
 theorem keys_insertIfNew_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
     (t.insertIfNew k v h.balanced).1.keys.Perm (if t.contains k then t.keys else k :: t.keys) := by
   simp_to_model
@@ -698,10 +744,22 @@ theorem keys_insertIfNew_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF
   apply List.keys_insertEntryIfNew_perm
   simp
 
+theorem keysArray_insertIfNew_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v h.balanced).1.keysArray.Perm (if t.contains k then t.keysArray else t.keysArray.push k) := by
+  rw [← toArray_keys, ← toArray_keys, Array.perm_iff_toList_perm, List.toList_toArray]
+  refine (keys_insertIfNew_perm h).trans ?_
+  split
+  · simp
+  · simpa using (List.perm_append_singleton ..).symm
+
 theorem keys_insertIfNew!_perm {t : Impl α β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
     (t.insertIfNew! k v).keys.Perm (if t.contains k then t.keys else k :: t.keys) := by
     simpa only [insertIfNew_eq_insertIfNew!] using keys_insertIfNew_perm h
 
+theorem keysArray_insertIfNew!_perm {t : Impl α β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew! k v).keysArray.Perm (if t.contains k then t.keysArray else t.keysArray.push k) := by
+    simpa only [insertIfNew_eq_insertIfNew!] using keysArray_insertIfNew_perm h
+
 theorem get_insert_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} :
     (t.insert k v h.balanced).impl.get k (contains_insert_self h) = v := by
   simp_to_model [insert, get] using List.getValueCast_insertEntry_self
@@ -1638,22 +1696,43 @@ theorem length_keys [TransOrd α] (h : t.WF) :
     t.keys.length = t.size := by
   simp_to_model [size, keys] using List.length_keys_eq_length
 
+theorem size_keysArray [TransOrd α] (h : t.WF) :
+    t.keysArray.size = t.size := by
+  rw [← toArray_keys, List.size_toArray, length_keys h]
+
 theorem isEmpty_keys :
     t.keys.isEmpty = t.isEmpty := by
   simp_to_model [isEmpty, keys] using List.isEmpty_keys_eq_isEmpty
 
+theorem isEmpty_keysArray :
+    t.keysArray.isEmpty = t.isEmpty := by
+  rw [← toArray_keys, List.isEmpty_toArray, isEmpty_keys]
+
 theorem contains_keys [BEq α] [beqOrd : LawfulBEqOrd α] [TransOrd α] {k : α} (h : t.WF) :
     t.keys.contains k = t.contains k := by
   simp_to_model [contains, keys] using (List.containsKey_eq_keys_contains).symm
 
+theorem contains_keysArray [BEq α] [beqOrd : LawfulBEqOrd α] [TransOrd α] {k : α} (h : t.WF) :
+    t.keysArray.contains k = t.contains k := by
+  rw [← toArray_keys, List.contains_toArray, contains_keys h]
+
 theorem mem_keys [LawfulEqOrd α] [TransOrd α] {k : α} (h : t.WF) :
     k ∈ t.keys ↔ k ∈ t := by
   simpa only [mem_iff_contains, ← List.contains_iff_mem, ← Bool.eq_iff_iff] using contains_keys h
 
+theorem mem_keysArray [LawfulEqOrd α] [TransOrd α] {k : α} (h : t.WF) :
+    k ∈ t.keysArray ↔ k ∈ t := by
+  rw [← toArray_keys, List.mem_toArray, mem_keys h]
+
 theorem mem_of_mem_keys [TransOrd α] (h : t.WF) {k : α}
     (h' : k ∈ t.keys) : k ∈ t :=
   (contains_keys h).symm.trans (List.elem_eq_true_of_mem h')
 
+theorem mem_of_mem_keysArray [TransOrd α] (h : t.WF) {k : α}
+    (h' : k ∈ t.keysArray) : k ∈ t := by
+  rw [← toArray_keys, List.mem_toArray] at h'
+  exact mem_of_mem_keys h h'
+
 theorem distinct_keys [TransOrd α] (h : t.WF) :
     t.keys.Pairwise (fun a b => ¬ compare a b = .eq) := by
   simp_to_model [keys] using h.ordered.distinctKeys.distinct
@@ -1667,31 +1746,60 @@ theorem map_fst_toList_eq_keys :
     t.toList.map Sigma.fst = t.keys := by
   simp_to_model [toList, keys] using (List.keys_eq_map ..).symm
 
+theorem map_fst_toArray_eq_keysArray :
+    t.toArray.map Sigma.fst = t.keysArray := by
+  rw [← toArray_toList, List.map_toArray, map_fst_toList_eq_keys, toArray_keys]
+
 theorem length_toList [TransOrd α] (h : t.WF) :
     t.toList.length = t.size := by
   simp_to_model [toList, size]
 
+theorem size_toArray [TransOrd α] (h : t.WF) :
+    t.toArray.size = t.size := by
+  rw [← toArray_toList, List.size_toArray, length_toList h]
+
 theorem isEmpty_toList :
     t.toList.isEmpty = t.isEmpty := by
   simp_to_model [toList, isEmpty]
 
+theorem isEmpty_toArray :
+    t.toArray.isEmpty = t.isEmpty := by
+  rw [← toArray_toList, List.isEmpty_toArray, isEmpty_toList]
+
 theorem mem_toList_iff_get?_eq_some [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k} (h : t.WF) :
     ⟨k, v⟩ ∈ t.toList ↔ t.get? k = some v := by
   simp_to_model [toList, get?] using List.mem_iff_getValueCast?_eq_some
 
+theorem mem_toArray_iff_get?_eq_some [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k} (h : t.WF) :
+    ⟨k, v⟩ ∈ t.toArray ↔ t.get? k = some v := by
+  rw [← toArray_toList, List.mem_toArray, mem_toList_iff_get?_eq_some h]
+
 theorem find?_toList_eq_some_iff_get?_eq_some [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k}
     (h : t.WF) :
     t.toList.find? (compare ·.1 k == .eq) = some ⟨k, v⟩ ↔ t.get? k = some v := by
   simp_to_model [toList, get?] using List.find?_eq_some_iff_getValueCast?_eq_some
 
+theorem find?_toArray_eq_some_iff_get?_eq_some [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k}
+    (h : t.WF) :
+    t.toArray.find? (compare ·.1 k == .eq) = some ⟨k, v⟩ ↔ t.get? k = some v := by
+  rw [← toArray_toList, List.find?_toArray, find?_toList_eq_some_iff_get?_eq_some h]
+
 theorem find?_toList_eq_none_iff_contains_eq_false [TransOrd α] {k : α} (h : t.WF) :
     t.toList.find? (compare ·.1 k == .eq) = none ↔ t.contains k = false := by
   simp_to_model [toList, contains] using List.find?_eq_none_iff_containsKey_eq_false
 
+theorem find?_toArray_eq_none_iff_contains_eq_false [TransOrd α] {k : α} (h : t.WF) :
+    t.toArray.find? (compare ·.1 k == .eq) = none ↔ t.contains k = false := by
+  rw [← toArray_toList, List.find?_toArray, find?_toList_eq_none_iff_contains_eq_false h]
+
 theorem find?_toList_eq_none_iff_not_mem [TransOrd α] {k : α} (h : t.WF) :
     t.toList.find? (compare ·.1 k == .eq) = none ↔ ¬ k ∈ t := by
   simpa only [Bool.not_eq_true, mem_iff_contains] using find?_toList_eq_none_iff_contains_eq_false h
 
+theorem find?_toArray_eq_none_iff_not_mem [TransOrd α] {k : α} (h : t.WF) :
+    t.toArray.find? (compare ·.1 k == .eq) = none ↔ ¬ k ∈ t := by
+  simpa only [Bool.not_eq_true, mem_iff_contains] using find?_toArray_eq_none_iff_contains_eq_false h
+
 theorem distinct_keys_toList [TransOrd α] (h : t.WF) :
     t.toList.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq) := by
   simp_to_model [toList] using List.pairwise_fst_eq_false
@@ -1708,52 +1816,97 @@ theorem map_fst_toList_eq_keys :
     (toList t).map Prod.fst = t.keys := by
   simp_to_model [Const.toList, keys] using List.map_fst_map_toProd_eq_keys
 
+theorem map_fst_toArray_eq_keysArray :
+    (toArray t).map Prod.fst = t.keysArray := by
+  rw [← toArray_toList, List.map_toArray, map_fst_toList_eq_keys, toArray_keys]
+
 theorem length_toList (h : t.WF) :
     (toList t).length = t.size := by
   simp_to_model [Const.toList, size] using List.length_map
 
+theorem size_toArray (h : t.WF) :
+    (toArray t).size = t.size := by
+  rw [← toArray_toList, List.size_toArray, length_toList h]
+
 theorem isEmpty_toList :
     (toList t).isEmpty = t.isEmpty := by
   rw [Bool.eq_iff_iff, List.isEmpty_iff, isEmpty_eq_isEmpty, List.isEmpty_iff]
   simp_to_model [Const.toList, isEmpty] using List.map_eq_nil_iff
 
+theorem isEmpty_toArray :
+    (toArray t).isEmpty = t.isEmpty := by
+  rw [← toArray_toList, List.isEmpty_toArray, isEmpty_toList]
+
 theorem mem_toList_iff_get?_eq_some [TransOrd α] [LawfulEqOrd α] {k : α} {v : β} (h : t.WF) :
     (k, v) ∈ toList t ↔ get? t k = some v := by
   simp_to_model [Const.toList, Const.get?] using List.mem_map_toProd_iff_getValue?_eq_some
 
+theorem mem_toArray_iff_get?_eq_some [TransOrd α] [LawfulEqOrd α] {k : α} {v : β} (h : t.WF) :
+    (k, v) ∈ toArray t ↔ get? t k = some v := by
+  rw [← toArray_toList, List.mem_toArray, mem_toList_iff_get?_eq_some h]
+
 theorem mem_toList_iff_getKey?_eq_some_and_get?_eq_some [TransOrd α] {k : α} {v : β} (h : t.WF) :
     (k, v) ∈ toList t ↔ t.getKey? k = some k ∧ get? t k = some v := by
   simp_to_model [Const.toList, getKey?, Const.get?]
     using List.mem_map_toProd_iff_getKey?_eq_some_and_getValue?_eq_some
 
+theorem mem_toArray_iff_getKey?_eq_some_and_get?_eq_some [TransOrd α] {k : α} {v : β} (h : t.WF) :
+    (k, v) ∈ toArray t ↔ t.getKey? k = some k ∧ get? t k = some v := by
+  rw [← toArray_toList, List.mem_toArray, mem_toList_iff_getKey?_eq_some_and_get?_eq_some h]
+
 theorem get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList [TransOrd α] {k : α} {v : β} (h : t.WF) :
     get? t k = some v ↔ ∃ (k' : α), compare k k' = .eq ∧ (k', v) ∈ toList t := by
   simp_to_model [Const.toList, Const.get?]
     using List.getValue?_eq_some_iff_exists_beq_and_mem_toList
 
+theorem get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray [TransOrd α] {k : α} {v : β} (h : t.WF) :
+    get? t k = some v ↔ ∃ (k' : α), compare k k' = .eq ∧ (k', v) ∈ toArray t := by
+  simp [← toArray_toList, List.mem_toArray, ← get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList h]
+
 theorem find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some [TransOrd α] {k k' : α} {v : β}
     (h : t.WF) : (toList t).find? (fun a => compare a.1 k == .eq) = some ⟨k', v⟩ ↔
       t.getKey? k = some k' ∧ get? t k = some v := by
   simp_to_model [Const.toList, getKey?, Const.get?]
     using List.find?_map_toProd_eq_some_iff_getKey?_eq_some_and_getValue?_eq_some
 
+theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some [TransOrd α] {k k' : α} {v : β}
+    (h : t.WF) : (toArray t).find? (fun a => compare a.1 k == .eq) = some ⟨k', v⟩ ↔
+      t.getKey? k = some k' ∧ get? t k = some v := by
+  rw [← toArray_toList, List.find?_toArray, find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some h]
+
 theorem find?_toList_eq_none_iff_contains_eq_false [TransOrd α] {k : α} (h : t.WF) :
     (toList t).find? (compare ·.1 k == .eq) = none ↔ t.contains k = false := by
   simp_to_model [Const.toList, contains] using List.find?_map_eq_none_iff_containsKey_eq_false
 
+theorem find?_toArray_eq_none_iff_contains_eq_false [TransOrd α] {k : α} (h : t.WF) :
+    (toArray t).find? (compare ·.1 k == .eq) = none ↔ t.contains k = false := by
+  rw [← toArray_toList, List.find?_toArray, find?_toList_eq_none_iff_contains_eq_false h]
+
 theorem find?_toList_eq_none_iff_not_mem [TransOrd α] {k : α} (h : t.WF) :
     (toList t).find? (compare ·.1 k == .eq) = none ↔ ¬ k ∈ t := by
   simpa only [Bool.not_eq_true, mem_iff_contains] using find?_toList_eq_none_iff_contains_eq_false h
 
+theorem find?_toArray_eq_none_iff_not_mem [TransOrd α] {k : α} (h : t.WF) :
+    (toArray t).find? (compare ·.1 k == .eq) = none ↔ ¬ k ∈ t := by
+  simpa only [Bool.not_eq_true, mem_iff_contains] using find?_toArray_eq_none_iff_contains_eq_false h
+
 theorem distinct_keys_toList [TransOrd α] (h : t.WF) :
     (toList t).Pairwise (fun a b => ¬ compare a.1 b.1 = .eq) := by
   simp_to_model [Const.toList] using List.pairwise_fst_eq_false_map_toProd
 
+theorem distinct_keys_toArray [TransOrd α] (h : t.WF) :
+    (toArray t).toList.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq) := by
+  simp [toList_toArray, distinct_keys_toList h]
+
 theorem ordered_keys_toList [TransOrd α] (h : t.WF) :
     (toList t).Pairwise (fun a b => compare a.1 b.1 = .lt) := by
   simp_to_model [Const.toList]
   exact h.ordered.map _ fun _ _ hcmp => hcmp
 
+theorem ordered_keys_toArray [TransOrd α] (h : t.WF) :
+    (toArray t).toList.Pairwise (fun a b => compare a.1 b.1 = .lt) := by
+  simp [toList_toArray, ordered_keys_toList h]
+
 end Const
 
 section monadic
@@ -1765,53 +1918,105 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m]
     t.foldlM f init = t.toList.foldlM (fun a b => f a b.1 b.2) init := by
   simp_to_model [toList, foldlM]
 
+theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m]
+    {f : δ → (a : α) → β a → m δ} {init : δ} :
+    t.foldlM f init = t.toArray.foldlM (fun a b => f a b.1 b.2) init := by
+  rw [foldlM_eq_foldlM_toList, ← toArray_toList, List.foldlM_toArray]
+
 theorem foldl_eq_foldl_toList {f : δ → (a : α) → β a → δ} {init : δ} :
     t.foldl f init = t.toList.foldl (fun a b => f a b.1 b.2) init := by
   simp_to_model [toList, foldl]
 
+theorem foldl_eq_foldl_toArray {f : δ → (a : α) → β a → δ} {init : δ} :
+    t.foldl f init = t.toArray.foldl (fun a b => f a b.1 b.2) init := by
+  rw [foldl_eq_foldl_toList, ← toArray_toList, List.foldl_toArray]
+
 theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m]
     {f : (a : α) → β a → δ → m δ} {init : δ} :
     t.foldrM f init = t.toList.foldrM (fun a b => f a.1 a.2 b) init := by
   simp_to_model [toList, foldrM]
 
+theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m]
+    {f : (a : α) → β a → δ → m δ} {init : δ} :
+    t.foldrM f init = t.toArray.foldrM (fun a b => f a.1 a.2 b) init := by
+  rw [foldrM_eq_foldrM_toList, ← toArray_toList, List.foldrM_toArray]
+
 theorem foldr_eq_foldr_toList {f : (a : α) → β a → δ → δ} {init : δ} :
     t.foldr f init = t.toList.foldr (fun a b => f a.1 a.2 b) init := by
   simp_to_model [toList, foldr]
 
+theorem foldr_eq_foldr_toArray {f : (a : α) → β a → δ → δ} {init : δ} :
+    t.foldr f init = t.toArray.foldr (fun a b => f a.1 a.2 b) init := by
+  rw [foldr_eq_foldr_toList, ← toArray_toList, List.foldr_toArray]
+
 theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit} :
     t.forM (fun k v => f ⟨k, v⟩) = ForM.forM t.toList f := by
   simp_to_model [toList, forM] using rfl
 
+theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit} :
+    t.forM (fun k v => f ⟨k, v⟩) = ForM.forM t.toArray f := by
+  simp [forM_eq_forM_toList, ← toArray_toList, List.forM_toArray]
+
 theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m]
     {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ} :
     t.forIn (fun k v => f ⟨k, v⟩) init = ForIn.forIn t.toList init f := by
   simp_to_model [toList, forIn]
 
+theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m]
+    {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ} :
+    t.forIn (fun k v => f ⟨k, v⟩) init = ForIn.forIn t.toArray init f := by
+  rw [forIn_eq_forIn_toList, ← toArray_toList, List.forIn_toArray]
+
 theorem foldlM_eq_foldlM_keys [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
     t.foldlM (fun d a _ => f d a) init = t.keys.foldlM f init := by
   simp_to_model [foldlM, keys] using List.foldlM_eq_foldlM_keys
 
+theorem foldlM_eq_foldlM_keysArray [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
+    t.foldlM (fun d a _ => f d a) init = t.keysArray.foldlM f init := by
+  rw [foldlM_eq_foldlM_keys, ← toArray_keys, List.foldlM_toArray]
+
 theorem foldl_eq_foldl_keys {f : δ → α → δ} {init : δ} :
     t.foldl (fun d a _ => f d a) init = t.keys.foldl f init := by
   simp_to_model [foldl, keys] using List.foldl_eq_foldl_keys
 
+theorem foldl_eq_foldl_keysArray {f : δ → α → δ} {init : δ} :
+    t.foldl (fun d a _ => f d a) init = t.keysArray.foldl f init := by
+  rw [foldl_eq_foldl_keys, ← toArray_keys, List.foldl_toArray]
+
 theorem foldrM_eq_foldrM_keys [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
     t.foldrM (fun a _ d => f a d) init = t.keys.foldrM f init := by
   simp_to_model [foldrM, keys] using List.foldrM_eq_foldrM_keys
 
+theorem foldrM_eq_foldrM_keysArray [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
+    t.foldrM (fun a _ d => f a d) init = t.keysArray.foldrM f init := by
+  rw [foldrM_eq_foldrM_keys, ← toArray_keys, List.foldrM_toArray]
+
 theorem foldr_eq_foldr_keys {f : α → δ → δ} {init : δ} :
     t.foldr (fun a _ d => f a d) init = t.keys.foldr f init := by
   simp_to_model [foldr, keys] using List.foldr_eq_foldr_keys
 
+theorem foldr_eq_foldr_keysArray {f : α → δ → δ} {init : δ} :
+    t.foldr (fun a _ d => f a d) init = t.keysArray.foldr f init := by
+  rw [foldr_eq_foldr_keys, ← toArray_keys, List.foldr_toArray]
+
 theorem forM_eq_forM_keys [Monad m] [LawfulMonad m] {f : α → m PUnit} :
     t.forM (fun a _ => f a) = t.keys.forM f := by
   simp_to_model [forM, keys] using List.forM_eq_forM_keys
 
+theorem forM_eq_forM_keysArray [Monad m] [LawfulMonad m] {f : α → m PUnit} :
+    t.forM (fun a _ => f a) = t.keysArray.forM f := by
+  rw [forM_eq_forM_keys, ← toArray_keys, List.forM_toArray' _ _ rfl]
+
 theorem forIn_eq_forIn_keys [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)}
     {init : δ} :
     t.forIn (fun a _ d => f a d) init = ForIn.forIn t.keys init f := by
   simp_to_model [forIn, keys] using List.forIn_eq_forIn_keys
 
+theorem forIn_eq_forIn_keysArray [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)}
+    {init : δ} :
+    t.forIn (fun a _ d => f a d) init = ForIn.forIn t.keysArray init f := by
+  rw [forIn_eq_forIn_keys, ← toArray_keys, List.forIn_toArray]
+
 namespace Const
 
 variable {β : Type v} {t : Impl α β}
@@ -1821,28 +2026,55 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m]
     t.foldlM f init = (Const.toList t).foldlM (fun a b => f a b.1 b.2) init := by
   simp_to_model [foldlM, Const.toList] using List.foldlM_eq_foldlM_toProd
 
+theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m]
+    {f : δ → (a : α) → β → m δ} {init : δ} :
+    t.foldlM f init = (Const.toArray t).foldlM (fun a b => f a b.1 b.2) init := by
+  rw [foldlM_eq_foldlM_toList, ← toArray_toList, List.foldlM_toArray]
+
 theorem foldl_eq_foldl_toList {f : δ → (a : α) → β → δ} {init : δ} :
     t.foldl f init = (Const.toList t).foldl (fun a b => f a b.1 b.2) init := by
   simp_to_model [foldl, Const.toList] using List.foldl_eq_foldl_toProd
 
+theorem foldl_eq_foldl_toArray {f : δ → (a : α) → β → δ} {init : δ} :
+    t.foldl f init = (Const.toArray t).foldl (fun a b => f a b.1 b.2) init := by
+  rw [foldl_eq_foldl_toList, ← toArray_toList, List.foldl_toArray]
+
 theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m]
     {f : (a : α) → β → δ → m δ} {init : δ} :
     t.foldrM f init = (Const.toList t).foldrM (fun a b => f a.1 a.2 b) init := by
   simp_to_model [foldrM, Const.toList] using List.foldrM_eq_foldrM_toProd
 
+theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m]
+    {f : (a : α) → β → δ → m δ} {init : δ} :
+    t.foldrM f init = (Const.toArray t).foldrM (fun a b => f a.1 a.2 b) init := by
+  rw [foldrM_eq_foldrM_toList, ← toArray_toList, List.foldrM_toArray]
+
 theorem foldr_eq_foldr_toList {f : (a : α) → β → δ → δ} {init : δ} :
     t.foldr f init = (Const.toList t).foldr (fun a b => f a.1 a.2 b) init := by
   simp_to_model [foldr, Const.toList] using List.foldr_eq_foldr_toProd
 
+theorem foldr_eq_foldr_toArray {f : (a : α) → β → δ → δ} {init : δ} :
+    t.foldr f init = (Const.toArray t).foldr (fun a b => f a.1 a.2 b) init := by
+  rw [foldr_eq_foldr_toList, ← toArray_toList, List.foldr_toArray]
+
 theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : (a : α) → β → m PUnit} :
     t.forM f = (Const.toList t).forM (fun a => f a.1 a.2) := by
   simp_to_model [forM, Const.toList] using List.forM_eq_forM_toProd
 
+theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : (a : α) → β → m PUnit} :
+    t.forM f = (Const.toArray t).forM (fun a => f a.1 a.2) := by
+  rw [forM_eq_forM_toList, ← toArray_toList, List.forM_toArray' _ _ rfl]
+
 theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m]
     {f : α → β → δ → m (ForInStep δ)} {init : δ} :
     t.forIn f init = ForIn.forIn (Const.toList t) init (fun a b => f a.1 a.2 b) := by
   simp_to_model [forIn, Const.toList] using List.forIn_eq_forIn_toProd
 
+theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m]
+    {f : α → β → δ → m (ForInStep δ)} {init : δ} :
+    t.forIn f init = ForIn.forIn (Const.toArray t) init (fun a b => f a.1 a.2 b) := by
+  rw [forIn_eq_forIn_toList, ← toArray_toList, List.forIn_toArray]
+
 end Const
 
 end monadic
@@ -7108,6 +7340,10 @@ theorem minKey?_eq_head?_keys [TransOrd α] (h : t.WF) :
     t.minKey? = t.keys.head? := by
   simp_to_model [minKey?, keys] using List.minKey?_eq_head?_keys h.ordered
 
+theorem minKey?_eq_getElem?_keysArray [TransOrd α] (h : t.WF) :
+    t.minKey? = t.keysArray[0]? := by
+  simp [minKey?_eq_head?_keys h, ← toList_keysArray, List.head?_eq_getElem?, Array.getElem?_toList]
+
 theorem minKey?_modify [TransOrd α] [LawfulEqOrd α] {k f} (h : t.WF) :
     (t.modify k f).minKey? = t.minKey? := by
   simp_to_model [modify, minKey?] using List.minKey?_modifyKey
@@ -7262,6 +7498,11 @@ theorem minKey_eq_head_keys [TransOrd α] (h : t.WF) {he} :
     t.minKey he = t.keys.head (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) := by
   simp_to_model [minKey, keys] using List.minKey_eq_head_keys h.ordered
 
+theorem minKey_eq_getElem_keysArray [TransOrd α] (h : t.WF) {he} :
+    t.minKey he = t.keysArray[0]'(Nat.zero_lt_of_ne_zero (by simpa [size_keysArray h, isEmpty_eq_size_eq_zero h] using he)) := by
+  simp [minKey_eq_head_keys h, List.head_eq_iff_head?_eq_some, ← toList_keysArray, List.head?_eq_getElem?, Array.getElem?_toList,
+    getElem?_eq_some_getElem_iff]
+
 theorem minKey_modify [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f he} :
     (t.modify k f).minKey he = t.minKey (isEmpty_modify h ▸ he):= by
   simp_to_model [minKey, modify] using List.minKey_modifyKey
@@ -7460,6 +7701,10 @@ theorem minKey!_eq_head!_keys [TransOrd α] [Inhabited α] (h : t.WF) :
     t.minKey! = t.keys.head! := by
   simp_to_model [minKey!, keys] using List.minKey!_eq_head!_keys h.ordered
 
+theorem minKey!_eq_getElem!_keysArray [TransOrd α] [Inhabited α] (h : t.WF) :
+    t.minKey! = t.keysArray[0]! := by
+  simp [minKey!_eq_head!_keys h, ← toList_keysArray, List.head!_eq_getElem!, Array.getElem!_eq_getD]
+
 theorem minKey!_modify [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h : t.WF) : ∀ {k f},
     (t.modify k f).minKey! = t.minKey! := by
   simp_to_model [minKey!, modify] using List.minKey!_modifyKey
@@ -7677,6 +7922,10 @@ theorem minKeyD_eq_headD_keys [TransOrd α] (h : t.WF) {fallback} :
     t.minKeyD fallback = t.keys.headD fallback := by
   simp_to_model [minKeyD, keys] using List.minKeyD_eq_headD_keys h.ordered
 
+theorem minKeyD_eq_getD_keysArray [TransOrd α] (h : t.WF) {fallback} :
+    t.minKeyD fallback = t.keysArray.getD 0 fallback := by
+  simp [minKeyD_eq_headD_keys h, ← toList_keysArray, List.head?_eq_getElem?]
+
 theorem minKeyD_modify [TransOrd α] [LawfulEqOrd α] (h : t.WF) : ∀ {k f fallback},
     (t.modify k f |>.minKeyD fallback) = t.minKeyD fallback := by
   simp_to_model [minKeyD, modify] using List.minKeyD_modifyKey
@@ -7945,6 +8194,10 @@ theorem maxKey?_eq_getLast?_keys [TransOrd α] (h : t.WF) :
     t.maxKey? = t.keys.getLast? := by
   simp_to_model [maxKey?, keys] using List.maxKey?_eq_getLast?_keys _ h.ordered
 
+theorem maxKey?_eq_back?_keysArray [TransOrd α] (h : t.WF) :
+    t.maxKey? = t.keysArray.back? := by
+  simp [maxKey?_eq_getLast?_keys h, ← toList_keysArray]
+
 theorem maxKey?_modify [TransOrd α] [LawfulEqOrd α] {k f} (h : t.WF) :
     (t.modify k f).maxKey? = t.maxKey? := by
   simp_to_model [modify, maxKey?] using List.maxKey?_modifyKey
@@ -8095,6 +8348,10 @@ theorem maxKey_eq_getLast_keys [TransOrd α] (h : t.WF) {he} :
     t.maxKey he = t.keys.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) := by
   simp_to_model [maxKey, keys] using List.maxKey_eq_getLast_keys h.ordered.distinctKeys h.ordered
 
+theorem maxKey_eq_back_keysArray [TransOrd α] (h : t.WF) {he} :
+    t.maxKey he = t.keysArray.back (Nat.zero_lt_of_ne_zero (by simpa [size_keysArray h, isEmpty_eq_size_eq_zero h] using he)) := by
+  simp [maxKey_eq_getLast_keys h, ← toArray_keys, List.back_toArray]
+
 theorem maxKey_modify [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f he} :
     (t.modify k f).maxKey he = t.maxKey (isEmpty_modify h ▸ he):= by
   simp_to_model [maxKey, modify] using List.maxKey_modifyKey
@@ -8293,6 +8550,10 @@ theorem maxKey!_eq_getLast!_keys [TransOrd α] [Inhabited α] (h : t.WF) :
     t.maxKey! = t.keys.getLast! := by
   simp_to_model [maxKey!, keys] using List.maxKey!_eq_getLast!_keys h.ordered.distinctKeys h.ordered
 
+theorem maxKey!_eq_back!_keysArray [TransOrd α] [Inhabited α] (h : t.WF) :
+    t.maxKey! = t.keysArray.back! := by
+  simp [maxKey!_eq_getLast!_keys h, ← toArray_keys]
+
 theorem maxKey!_modify [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h : t.WF) : ∀ {k f},
     (t.modify k f).maxKey! = t.maxKey! := by
   simp_to_model [maxKey!, modify] using List.maxKey!_modifyKey
@@ -8510,6 +8771,10 @@ theorem maxKeyD_eq_getLastD_keys [TransOrd α] (h : t.WF) {fallback} :
     t.maxKeyD fallback = t.keys.getLastD fallback := by
   simp_to_model [maxKeyD, keys] using List.maxKeyD_eq_getLastD_keys h.ordered.distinctKeys h.ordered
 
+theorem maxKeyD_eq_getD_back?_keysArray [TransOrd α] (h : t.WF) {fallback} :
+    t.maxKeyD fallback = t.keysArray.back?.getD fallback := by
+  simp [maxKeyD_eq_getLastD_keys h, ← toList_keysArray]
+
 theorem maxKeyD_modify [TransOrd α] [LawfulEqOrd α] (h : t.WF) : ∀ {k f fallback},
     (t.modify k f |>.maxKeyD fallback) = t.maxKeyD fallback := by
   simp_to_model [maxKeyD, modify] using List.maxKeyD_modifyKey
@@ -9306,13 +9571,24 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty :=
 theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList := by
   simp_to_model [toList, Equiv]
 
+theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray := by
+  rw [equiv_iff_toList_perm, ← toArray_toList (t := t₁), ← toArray_toList (t := t₂),
+    Array.perm_iff_toList_perm]
+
 theorem Equiv.of_toList_perm : t₁.toList.Perm t₂.toList → t₁ ~m t₂ :=
   equiv_iff_toList_perm.mpr
 
+theorem Equiv.of_toArray_perm : t₁.toArray.Perm t₂.toArray → t₁ ~m t₂ :=
+  equiv_iff_toArray_perm.mpr
+
 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 equiv_iff_toArray_eq [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) :
+    t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray := by
+  simp [equiv_iff_toList_eq h₁ h₂, ← toArray_toList (t := t₁), ← toArray_toList (t := t₂)]
+
 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]
@@ -9341,12 +9617,20 @@ theorem Const.equiv_iff_toList_perm : t₁ ~m t₂ ↔ (Const.toList t₁).Perm
     have := h.map (fun (x, y) => (⟨x, y⟩ : (_ : α) × β))
     simpa only [List.map_map, Function.comp_def, List.map_id'] using this
 
+theorem Const.equiv_iff_toArray_perm : t₁ ~m t₂ ↔ (Const.toArray t₁).Perm (Const.toArray t₂) := by
+  rw [Const.equiv_iff_toList_perm, ← toArray_toList (t := t₁), ← toArray_toList (t := t₂),
+    Array.perm_iff_toList_perm]
+
 theorem Const.equiv_iff_toList_eq [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) :
     t₁ ~m t₂ ↔ Const.toList t₁ = Const.toList t₂ := by
   simp_to_model [Const.toList]
   rw [List.map_inj_right fun _ _ => congrArg fun x : α × β => (⟨x.1, x.2⟩ : (_ : α) × β)]
   exact ⟨(·.toListModel_eq h₁.ordered h₂.ordered), .mk ∘ .of_eq⟩
 
+theorem Const.equiv_iff_toArray_eq [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) :
+    t₁ ~m t₂ ↔ Const.toArray t₁ = Const.toArray t₂ := by
+  simp [Const.equiv_iff_toList_eq h₁ h₂, ← toArray_toList (t := t₁), ← toArray_toList (t := t₂)]
+
 theorem Const.equiv_iff_keys_perm {t₁ t₂ : Impl α Unit} :
     t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys := by
   simp_to_model [keys, Equiv]
@@ -9357,6 +9641,19 @@ theorem Const.equiv_iff_keys_perm {t₁ t₂ : Impl α Unit} :
     have := h.map (fun x => (⟨x, ()⟩ : (_ : α) × Unit))
     simpa only [List.map_map, Function.comp_def, List.map_id'] using this
 
+theorem Const.Equiv.of_keys_perm {t₁ t₂ : Impl α Unit} :
+    t₁.keys.Perm t₂.keys → t₁ ~m t₂ :=
+  Const.equiv_iff_keys_perm.mpr
+
+theorem Const.equiv_iff_keysArray_perm {t₁ t₂ : Impl α Unit} :
+    t₁ ~m t₂ ↔ t₁.keysArray.Perm t₂.keysArray := by
+  rw [Const.equiv_iff_keys_perm, ← toArray_keys (t := t₁), ← toArray_keys (t := t₂),
+    Array.perm_iff_toList_perm]
+
+theorem Const.Equiv.of_keysArray_perm {t₁ t₂ : Impl α Unit} :
+    t₁.keysArray.Perm t₂.keysArray → t₁ ~m t₂ :=
+  Const.equiv_iff_keysArray_perm.mpr
+
 theorem Const.equiv_iff_keys_eq {t₁ t₂ : Impl α Unit} [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) :
     t₁ ~m t₂ ↔ t₁.keys = t₂.keys := by
   simp_to_model [keys]
@@ -9364,6 +9661,10 @@ 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.equiv_iff_keysArray_eq {t₁ t₂ : Impl α Unit} [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) :
+    t₁ ~m t₂ ↔ t₁.keysArray = t₂.keysArray := by
+  simp [Const.equiv_iff_keys_eq h₁ h₂, ← toArray_keys (t := t₁), ← toArray_keys (t := t₂)]
+
 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]
@@ -9393,11 +9694,21 @@ theorem toList_filterMap {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
       t.toList.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by
   simp_to_model [filterMap, toList, Equiv]
 
+theorem toArray_filterMap {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
+    (t.filterMap f h.balanced).1.toArray =
+      t.toArray.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by
+  rw [← toArray_toList, toList_filterMap h, ← toArray_toList, List.filterMap_toArray]
+
 theorem toList_filterMap! {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
     (t.filterMap! f).toList =
       t.toList.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by
   simpa only [filterMap_eq_filterMap!] using toList_filterMap h
 
+theorem toArray_filterMap! {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
+    (t.filterMap! f).toArray =
+      t.toArray.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by
+  simpa only [filterMap_eq_filterMap!] using toArray_filterMap h
+
 theorem isEmpty_filterMap_iff [TransOrd α] [LawfulEqOrd α]
     {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
     (t.filterMap f h.balanced).1.isEmpty = true ↔
@@ -9740,11 +10051,21 @@ theorem toList_filterMap {f : α → β → Option γ} (h : t.WF) :
   simp_to_model [Const.toList, filterMap]
   simp only [List.map_filterMap, List.filterMap_map, Function.comp_def, Option.map_map]
 
+theorem toArray_filterMap {f : α → β → Option γ} (h : t.WF) :
+    Const.toArray (t.filterMap f h.balanced).1 =
+      (Const.toArray t).filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by
+  rw [← toArray_toList, toList_filterMap h, ← toArray_toList, List.filterMap_toArray]
+
 theorem toList_filterMap! {f : α → β → Option γ} (h : t.WF) :
     Const.toList (t.filterMap! f) =
       (Const.toList t).filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by
   simpa only [filterMap_eq_filterMap!] using toList_filterMap h
 
+theorem toArray_filterMap! {f : α → β → Option γ} (h : t.WF) :
+    Const.toArray (t.filterMap! f) =
+      (Const.toArray t).filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by
+  simpa only [filterMap_eq_filterMap!] using toArray_filterMap h
+
 theorem getKey?_filterMap [TransOrd α]
     {f : α → β → Option γ} {k : α} (h : t.WF) :
     (t.filterMap f h.balanced).1.getKey? k =
@@ -9808,19 +10129,36 @@ theorem toList_filter {f : (a : α) → β a → Bool} (h : t.WF) :
     (t.filter f h.balanced).1.toList = t.toList.filter (fun p => f p.1 p.2) := by
   simp_to_model [filter, toList, Equiv]
 
+theorem toArray_filter {f : (a : α) → β a → Bool} (h : t.WF) :
+    (t.filter f h.balanced).1.toArray = t.toArray.filter (fun p => f p.1 p.2) := by
+  simp_to_model [filter, toArray, Equiv]
+  simp
+
 theorem toList_filter! {f : (a : α) → β a → Bool} (h : t.WF) :
     (t.filter! f).toList = t.toList.filter (fun p => f p.1 p.2) := by
   simpa only [filter_eq_filter!] using toList_filter h
 
+theorem toArray_filter! {f : (a : α) → β a → Bool} (h : t.WF) :
+    (t.filter! f).toArray = t.toArray.filter (fun p => f p.1 p.2) := by
+  simpa only [filter_eq_filter!] using toArray_filter h
+
 theorem keys_filter_key {f : α → Bool} (h : t.WF) :
     (t.filter (fun k _ => f k) h.balanced).1.keys = t.keys.filter f := by
   simp_to_model [keys, filter]
   simp only [List.keys_eq_map, List.filter_map, Function.comp_def]
 
+theorem keysArray_filter_key {f : α → Bool} (h : t.WF) :
+    (t.filter (fun k _ => f k) h.balanced).1.keysArray = t.keysArray.filter f := by
+  rw [← toArray_keys, keys_filter_key h, ← toArray_keys, List.filter_toArray]
+
 theorem keys_filter!_key {f : α → Bool} (h : t.WF) :
     (t.filter! (fun k _ => f k)).keys = t.keys.filter f := by
   simpa only [filter_eq_filter!] using keys_filter_key h
 
+theorem keysArray_filter!_key {f : α → Bool} (h : t.WF) :
+    (t.filter! (fun k _ => f k)).keysArray = t.keysArray.filter f := by
+  simpa only [filter_eq_filter!] using keysArray_filter_key h
+
 theorem isEmpty_filter_iff [TransOrd α] [LawfulEqOrd α]
     {f : (a : α) → β a → Bool} (h : t.WF) :
     (t.filter f h.balanced).1.isEmpty = true ↔
@@ -10001,11 +10339,36 @@ theorem keys_filter [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bo
   rw [List.keys_filter h.ordered.distinctKeys]
   simp only [List.filter_map, Function.comp_def, List.unattach, List.map_map]
 
+private theorem List.unattach_filter_eq_if {p : α → Prop} {l : List { x // p x }}
+    {f : { x // p x } → Bool} :
+    open scoped Classical in
+    (l.filter f).unattach = l.unattach.filter (fun x => if h : p x then f ⟨x, h⟩ else false) := by
+  apply List.unattach_filter
+  simp +contextual
+
+private theorem Array.unattach_filter_eq_if {p : α → Prop} {xs : Array { x // p x }}
+    {f : { x // p x } → Bool} :
+    open scoped Classical in
+    (xs.filter f).unattach = xs.unattach.filter (fun x => if h : p x then f ⟨x, h⟩ else false) := by
+  apply Array.unattach_filter
+  simp +contextual
+
+theorem keysArray_filter [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF) :
+    (t.filter f h.balanced).1.keysArray =
+      (t.keysArray.attach.filter (fun ⟨x, h'⟩ => f x (t.get x (mem_of_mem_keysArray h h')))).unattach := by
+  simp only [← toArray_keys, keys_filter h, List.unattach_filter_eq_if, Array.unattach_filter_eq_if]
+  simp [← toArray_keys]
+
 theorem keys_filter! [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF) :
     (t.filter! f).keys =
       (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (t.get x (mem_of_mem_keys h h')))).unattach := by
   simpa only [filter_eq_filter!] using keys_filter h
 
+theorem keysArray_filter! [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF) :
+    (t.filter! f).keysArray =
+      (t.keysArray.attach.filter (fun ⟨x, h'⟩ => f x (t.get x (mem_of_mem_keysArray h h')))).unattach := by
+  simpa only [filter_eq_filter!] using keysArray_filter h
+
 theorem getKey?_filter [TransOrd α] [LawfulEqOrd α]
     {f : (a : α) → β a → Bool} {k : α} (h : t.WF) :
     (t.filter f h.balanced).1.getKey? k =
@@ -10259,11 +10622,21 @@ theorem toList_filter {f : α → β → Bool} (h : t.WF) :
   simp_to_model [filter, Const.toList]
   simp only [List.filter_map, Function.comp_def]
 
+theorem toArray_filter {f : α → β → Bool} (h : t.WF) :
+    Const.toArray (t.filter f h.balanced).1 =
+      (Const.toArray t).filter (fun p => f p.1 p.2) := by
+  rw [← toArray_toList, toList_filter h, ← toArray_toList, List.filter_toArray]
+
 theorem toList_filter! {f : α → β → Bool} (h : t.WF) :
     Const.toList (t.filter! f) =
       (Const.toList t).filter (fun p => f p.1 p.2) := by
   simpa only [filter_eq_filter!] using toList_filter h
 
+theorem toArray_filter! {f : α → β → Bool} (h : t.WF) :
+    Const.toArray (t.filter! f) =
+      (Const.toArray t).filter (fun p => f p.1 p.2) := by
+  simpa only [filter_eq_filter!] using toArray_filter h
+
 theorem keys_filter [TransOrd α] {f : α → β → Bool} (h : t.WF):
     (t.filter f h.balanced).1.keys =
       (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keys h h')))).unattach := by
@@ -10272,11 +10645,29 @@ theorem keys_filter [TransOrd α] {f : α → β → Bool} (h : t.WF):
   rw [List.Const.keys_filter h.ordered.distinctKeys]
   simp only [List.filter_map, Function.comp_def, List.unattach, List.map_map]
 
+theorem keysArray_filter [TransOrd α] {f : α → β → Bool} (h : t.WF):
+    (t.filter f h.balanced).1.keysArray =
+      (t.keysArray.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keysArray h h')))).unattach := by
+  simp only [← toArray_keys, keys_filter h]
+  simp only [List.unattach_filter_eq_if, Array.unattach_filter_eq_if]
+  simp only [List.unattach_attach, Array.unattach_attach, ← toArray_keys, List.mem_toArray,
+    List.size_toArray, List.filter_toArray']
+  congr; ext x
+  split <;> rename_i h'
+  all_goals
+    rw [← toList_keysArray, Array.mem_toList_iff] at h'
+    simp [h']
+
 theorem keys_filter! [TransOrd α] {f : α → β → Bool} (h : t.WF):
     (t.filter! f).keys =
       (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keys h h')))).unattach := by
   simpa only [filter_eq_filter!] using keys_filter h
 
+theorem keysArray_filter! [TransOrd α] {f : α → β → Bool} (h : t.WF):
+    (t.filter! f).keysArray =
+      (t.keysArray.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keysArray h h')))).unattach := by
+  simpa only [filter_eq_filter!] using keysArray_filter h
+
 theorem getKey?_filter [TransOrd α]
     {f : α → β → Bool} {k : α} (h : t.WF) :
     (t.filter f h.balanced).1.getKey? k =
@@ -10338,10 +10729,17 @@ theorem toList_map {f : (a : α) → β a → γ a} :
     (t.map f).toList = t.toList.map (fun p => ⟨p.1, f p.1 p.2⟩) := by
   simp_to_model [map, toList, Equiv]
 
+theorem toArray_map {f : (a : α) → β a → γ a} :
+    (t.map f).toArray = t.toArray.map (fun p => ⟨p.1, f p.1 p.2⟩) := by
+  rw [← toArray_toList, toList_map, ← toArray_toList, List.map_toArray]
+
 theorem keys_map {f : (a : α) → β a → γ a} : (t.map f).keys = t.keys := by
   simp_to_model [keys, map, Equiv]
   rw [List.keys_map]
 
+theorem keysArray_map {f : (a : α) → β a → γ a} : (t.map f).keysArray = t.keysArray := by
+  rw [← toArray_keys, keys_map, toArray_keys]
+
 theorem filterMap_equiv_map
     {f : (a : α) → β a → γ a} (h : t.WF) :
     (t.filterMap (fun k v => some (f k v)) h.balanced).1.Equiv (t.map f) := by
@@ -10483,6 +10881,10 @@ theorem toList_map {f : α → β → γ} :
   simp_to_model [map, Const.toList]
   simp only [List.map_map, Function.comp_def]
 
+theorem toArray_map {f : α → β → γ} :
+    Const.toArray (t.map f) = (Const.toArray t).map (fun p => (p.1, f p.1 p.2)) := by
+  rw [← toArray_toList, toList_map, ← toArray_toList, List.map_toArray]
+
 end Const
 
 end map

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

@@ -661,7 +661,7 @@ theorem minKey?_eq_minEntry?_map_fst {l : Impl α β} : l.minKey? = l.minEntry?.
 theorem minKey_eq_minEntry_fst {l : Impl α β} {he} : l.minKey he = (l.minEntry he).fst := by
   induction l, he using minKey.induct_unfolding <;> simp only [minEntry] <;> trivial
 
-theorem minKey!_eq_get!_minKey? [Inhabited α] {l : Impl α β} :
+theorem minKey!_eq_getElem!_minKey? [Inhabited α] {l : Impl α β} :
     l.minKey! = l.minKey?.get! := by
   induction l using minKey!.induct_unfolding <;> simp only [minKey?] <;> trivial
 

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

@@ -2296,7 +2296,7 @@ theorem minKey_eq_minKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l :
 theorem minKey!_eq_minKey! [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α]
     {l : Impl α β} (hlo : l.Ordered) :
     l.minKey! = List.minKey! l.toListModel := by
-  simp [Impl.minKey!_eq_get!_minKey?, List.minKey!_eq_get!_minKey?, minKey?_eq_minKey? hlo]
+  simp [Impl.minKey!_eq_getElem!_minKey?, List.minKey!_eq_get!_minKey?, minKey?_eq_minKey? hlo]
 
 theorem minKeyD_eq_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : Impl α β}
     (hlo : l.Ordered) {fallback} :

src/Std/Data/DTreeMap/Lemmas.lean

@@ -8,6 +8,7 @@ module
 prelude
 import Std.Data.DTreeMap.Internal.Lemmas
 public import Std.Data.DTreeMap.AdditionalOperations
+public import Init.Data.Array.Perm
 import Init.Data.List.Pairwise
 import Init.Data.Prod
 
@@ -362,14 +363,26 @@ end Const
 theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β k} :
     (t.insert k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) := Impl.toList_insert_perm t.wf
 
+theorem toArray_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β k} :
+    (t.insert k v).toArray.Perm (t.toArray.filter (¬k == ·.1) |>.push ⟨k, v⟩) :=
+  Impl.toArray_insert_perm t.wf
+
 theorem Const.toList_insert_perm {β : Type v} {t : DTreeMap α (fun _ => β) cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β} :
     (Const.toList (t.insert k v)).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) :=
   Impl.Const.toList_insert_perm t.2
 
+theorem Const.toArray_insert_perm {β : Type v} {t : DTreeMap α (fun _ => β) cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β} :
+    (Const.toArray (t.insert k v)).Perm ((Const.toArray t).filter (¬k == ·.1) |>.push ⟨k, v⟩) :=
+  Impl.Const.toArray_insert_perm t.2
+
 theorem keys_insertIfNew_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β k} :
     (t.insertIfNew k v).keys.Perm (if k ∈ t then t.keys else k :: t.keys) :=
   Impl.keys_insertIfNew_perm t.2
 
+theorem keysArray_insertIfNew_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β k} :
+    (t.insertIfNew k v).keysArray.Perm (if k ∈ t then t.keysArray else t.keysArray.push k) :=
+  Impl.keysArray_insertIfNew_perm t.2
+
 @[simp]
 theorem get_insert_self [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
     (t.insert k v).get k mem_insert_self = v :=
@@ -1094,24 +1107,47 @@ theorem length_keys [TransCmp cmp] :
     t.keys.length = t.size :=
   Impl.length_keys t.wf
 
+@[simp, grind =]
+theorem size_keysArray [TransCmp cmp] :
+    t.keysArray.size = t.size :=
+  Impl.size_keysArray t.wf
+
 @[simp, grind =]
 theorem isEmpty_keys :
     t.keys.isEmpty = t.isEmpty :=
   Impl.isEmpty_keys
 
+@[simp, grind =]
+theorem isEmpty_keysArray :
+    t.keysArray.isEmpty = t.isEmpty :=
+  Impl.isEmpty_keysArray
+
 @[simp, grind =]
 theorem contains_keys [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} :
     t.keys.contains k = t.contains k :=
   Impl.contains_keys t.wf
 
+@[simp, grind =]
+theorem contains_keysArray [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} :
+    t.keysArray.contains k = t.contains k :=
+  Impl.contains_keysArray t.wf
+
 @[simp, grind =]
 theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
     k ∈ t.keys ↔ k ∈ t :=
   Impl.mem_keys t.wf
 
+@[simp, grind =]
+theorem mem_keysArray [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
+    k ∈ t.keysArray ↔ k ∈ t :=
+  Impl.mem_keysArray t.wf
+
 theorem mem_of_mem_keys [TransCmp cmp] {k : α} (h : k ∈ t.keys) : k ∈ t :=
   Impl.mem_of_mem_keys t.wf h
 
+theorem mem_of_mem_keysArray [TransCmp cmp] {k : α} (h : k ∈ t.keysArray) : k ∈ t :=
+  Impl.mem_of_mem_keysArray t.wf h
+
 theorem distinct_keys [TransCmp cmp] :
     t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) :=
   Impl.distinct_keys t.wf
@@ -1129,34 +1165,67 @@ theorem map_fst_toList_eq_keys :
     t.toList.map Sigma.fst = t.keys :=
   Impl.map_fst_toList_eq_keys
 
+@[simp, grind _=_]
+theorem map_fst_toArray_eq_keysArray :
+    t.toArray.map Sigma.fst = t.keysArray :=
+  Impl.map_fst_toArray_eq_keysArray
+
 @[simp, grind =]
 theorem length_toList [TransCmp cmp] :
     t.toList.length = t.size :=
   Impl.length_toList t.wf
 
+@[simp, grind =]
+theorem size_toArray [TransCmp cmp] :
+    t.toArray.size = t.size :=
+  Impl.size_toArray t.wf
+
 @[simp, grind =]
 theorem isEmpty_toList :
     t.toList.isEmpty = t.isEmpty :=
   Impl.isEmpty_toList
 
+@[simp, grind =]
+theorem isEmpty_toArray :
+    t.toArray.isEmpty = t.isEmpty :=
+  Impl.isEmpty_toArray
+
 @[simp, grind =]
 theorem mem_toList_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
     ⟨k, v⟩ ∈ t.toList ↔ t.get? k = some v :=
   Impl.mem_toList_iff_get?_eq_some t.wf
 
+@[simp, grind =]
+theorem mem_toArray_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
+    ⟨k, v⟩ ∈ t.toArray ↔ t.get? k = some v :=
+  Impl.mem_toArray_iff_get?_eq_some t.wf
+
 theorem find?_toList_eq_some_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
     t.toList.find? (cmp ·.1 k == .eq) = some ⟨k, v⟩ ↔ t.get? k = some v :=
   Impl.find?_toList_eq_some_iff_get?_eq_some t.wf
 
+theorem find?_toArray_eq_some_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
+    t.toArray.find? (cmp ·.1 k == .eq) = some ⟨k, v⟩ ↔ t.get? k = some v :=
+  Impl.find?_toArray_eq_some_iff_get?_eq_some t.wf
+
 theorem find?_toList_eq_none_iff_contains_eq_false [TransCmp cmp] {k : α} :
     t.toList.find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false :=
   Impl.find?_toList_eq_none_iff_contains_eq_false t.wf
 
+theorem find?_toArray_eq_none_iff_contains_eq_false [TransCmp cmp] {k : α} :
+    t.toArray.find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false :=
+  Impl.find?_toArray_eq_none_iff_contains_eq_false t.wf
+
 @[simp]
 theorem find?_toList_eq_none_iff_not_mem [TransCmp cmp] {k : α} :
     t.toList.find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := by
   simpa only [Bool.not_eq_true, mem_iff_contains] using find?_toList_eq_none_iff_contains_eq_false
 
+@[simp]
+theorem find?_toArray_eq_none_iff_not_mem [TransCmp cmp] {k : α} :
+    t.toArray.find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t :=
+  Impl.find?_toArray_eq_none_iff_not_mem t.wf
+
 theorem distinct_keys_toList [TransCmp cmp] :
     t.toList.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
   Impl.distinct_keys_toList t.wf
@@ -1174,44 +1243,87 @@ theorem map_fst_toList_eq_keys :
     (toList t).map Prod.fst = t.keys :=
   Impl.Const.map_fst_toList_eq_keys
 
+@[simp, grind _=_]
+theorem map_fst_toArray_eq_keysArray :
+    (toArray t).map Prod.fst = t.keysArray :=
+  Impl.Const.map_fst_toArray_eq_keysArray
+
 @[simp, grind =]
 theorem length_toList :
     (toList t).length = t.size :=
   Impl.Const.length_toList t.wf
 
+@[simp, grind =]
+theorem size_toArray :
+    (toArray t).size = t.size :=
+  Impl.Const.size_toArray t.wf
+
 @[simp, grind =]
 theorem isEmpty_toList :
     (toList t).isEmpty = t.isEmpty :=
   Impl.Const.isEmpty_toList
 
+@[simp, grind =]
+theorem isEmpty_toArray :
+    (toArray t).isEmpty = t.isEmpty :=
+  Impl.Const.isEmpty_toArray
+
 @[simp, grind =]
 theorem mem_toList_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β} :
     (k, v) ∈ toList t ↔ get? t k = some v :=
   Impl.Const.mem_toList_iff_get?_eq_some t.wf
 
+@[simp, grind =]
+theorem mem_toArray_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β} :
+    (k, v) ∈ toArray t ↔ get? t k = some v :=
+  Impl.Const.mem_toArray_iff_get?_eq_some t.wf
+
 @[simp]
 theorem mem_toList_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] {k : α} {v : β} :
     (k, v) ∈ toList t ↔ t.getKey? k = some k ∧ get? t k = some v :=
   Impl.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some t.wf
 
+@[simp]
+theorem mem_toArray_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] {k : α} {v : β} :
+    (k, v) ∈ toArray t ↔ t.getKey? k = some k ∧ get? t k = some v :=
+  Impl.Const.mem_toArray_iff_getKey?_eq_some_and_get?_eq_some t.wf
+
 theorem get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList [TransCmp cmp] {k : α} {v : β} :
     get? t k = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toList t :=
   Impl.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList t.wf
 
+theorem get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray [TransCmp cmp] {k : α} {v : β} :
+    get? t k = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toArray t :=
+  Impl.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray t.wf
+
 theorem find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] {k k' : α} {v : β} :
     (toList t).find? (cmp ·.1 k == .eq) = some ⟨k', v⟩ ↔
       t.getKey? k = some k' ∧ get? t k = some v :=
   Impl.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some t.wf
 
+theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] {k k' : α} {v : β} :
+    (toArray t).find? (cmp ·.1 k == .eq) = some (k', v) ↔
+      t.getKey? k = some k' ∧ get? t k = some v :=
+  Impl.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some t.wf
+
 theorem find?_toList_eq_none_iff_contains_eq_false [TransCmp cmp] {k : α} :
     (toList t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false :=
   Impl.Const.find?_toList_eq_none_iff_contains_eq_false t.wf
 
+theorem find?_toArray_eq_none_iff_contains_eq_false [TransCmp cmp] {k : α} :
+    (toArray t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false :=
+  Impl.Const.find?_toArray_eq_none_iff_contains_eq_false t.wf
+
 @[simp]
 theorem find?_toList_eq_none_iff_not_mem [TransCmp cmp] {k : α} :
     (toList t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t :=
   Impl.Const.find?_toList_eq_none_iff_not_mem t.wf
 
+@[simp]
+theorem find?_toArray_eq_none_iff_not_mem [TransCmp cmp] {k : α} :
+    (toArray t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t :=
+  Impl.Const.find?_toArray_eq_none_iff_not_mem t.wf
+
 theorem distinct_keys_toList [TransCmp cmp] :
     (toList t).Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
   Impl.Const.distinct_keys_toList t.wf
@@ -1231,18 +1343,35 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m]
     t.foldlM f init = t.toList.foldlM (fun a b => f a b.1 b.2) init :=
   Impl.foldlM_eq_foldlM_toList
 
+theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m]
+    {f : δ → (a : α) → β a → m δ} {init : δ} :
+    t.foldlM f init = t.toArray.foldlM (fun a b => f a b.1 b.2) init :=
+  Impl.foldlM_eq_foldlM_toArray
+
 theorem foldl_eq_foldl_toList {f : δ → (a : α) → β a → δ} {init : δ} :
     t.foldl f init = t.toList.foldl (fun a b => f a b.1 b.2) init :=
   Impl.foldl_eq_foldl_toList
 
+theorem foldl_eq_foldl_toArray {f : δ → (a : α) → β a → δ} {init : δ} :
+    t.foldl f init = t.toArray.foldl (fun a b => f a b.1 b.2) init :=
+  Impl.foldl_eq_foldl_toArray
+
 theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} :
     t.foldrM f init = t.toList.foldrM (fun a b => f a.1 a.2 b) init :=
   Impl.foldrM_eq_foldrM_toList
 
+theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} :
+    t.foldrM f init = t.toArray.foldrM (fun a b => f a.1 a.2 b) init :=
+  Impl.foldrM_eq_foldrM_toArray
+
 theorem foldr_eq_foldr_toList {f : (a : α) → β a → δ → δ} {init : δ} :
     t.foldr f init = t.toList.foldr (fun a b => f a.1 a.2 b) init :=
   Impl.foldr_eq_foldr_toList
 
+theorem foldr_eq_foldr_toArray {f : (a : α) → β a → δ → δ} {init : δ} :
+    t.foldr f init = t.toArray.foldr (fun a b => f a.1 a.2 b) init :=
+  Impl.foldr_eq_foldr_toArray
+
 @[simp, grind =]
 theorem forM_eq_forM [Monad m] [LawfulMonad m] {f : (a : α) → β a → m PUnit} :
     t.forM f = ForM.forM t (fun a => f a.1 a.2) := rfl
@@ -1251,6 +1380,10 @@ theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : (a : α) × β a →
     ForM.forM t f = ForM.forM t.toList f :=
   Impl.forM_eq_forM_toList
 
+theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit} :
+    ForM.forM t f = ForM.forM t.toArray f :=
+  Impl.forM_eq_forM_toArray
+
 @[simp, grind =]
 theorem forIn_eq_forIn [Monad m] [LawfulMonad m]
     {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ} :
@@ -1261,32 +1394,63 @@ theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m]
     ForIn.forIn t init f = ForIn.forIn t.toList init f :=
   Impl.forIn_eq_forIn_toList (f := f)
 
+theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m]
+    {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ} :
+    ForIn.forIn t init f = ForIn.forIn t.toArray init f :=
+  Impl.forIn_eq_forIn_toArray (f := f)
+
 theorem foldlM_eq_foldlM_keys [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
     t.foldlM (fun d a _ => f d a) init = t.keys.foldlM f init :=
   Impl.foldlM_eq_foldlM_keys
 
+theorem foldlM_eq_foldlM_keysArray [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
+    t.foldlM (fun d a _ => f d a) init = t.keysArray.foldlM f init :=
+  Impl.foldlM_eq_foldlM_keysArray
+
 theorem foldl_eq_foldl_keys {f : δ → α → δ} {init : δ} :
     t.foldl (fun d a _ => f d a) init = t.keys.foldl f init :=
   Impl.foldl_eq_foldl_keys
 
+theorem foldl_eq_foldl_keysArray {f : δ → α → δ} {init : δ} :
+    t.foldl (fun d a _ => f d a) init = t.keysArray.foldl f init :=
+  Impl.foldl_eq_foldl_keysArray
+
 theorem foldrM_eq_foldrM_keys [Monad m] [LawfulMonad m]
     {f : α → δ → m δ} {init : δ} :
     t.foldrM (fun a _ d => f a d) init = t.keys.foldrM f init :=
   Impl.foldrM_eq_foldrM_keys
 
+theorem foldrM_eq_foldrM_keysArray [Monad m] [LawfulMonad m]
+    {f : α → δ → m δ} {init : δ} :
+    t.foldrM (fun a _ d => f a d) init = t.keysArray.foldrM f init :=
+  Impl.foldrM_eq_foldrM_keysArray
+
 theorem foldr_eq_foldr_keys {f : α → δ → δ} {init : δ} :
     t.foldr (fun a _ d => f a d) init = t.keys.foldr f init :=
   Impl.foldr_eq_foldr_keys
 
+theorem foldr_eq_foldr_keysArray {f : α → δ → δ} {init : δ} :
+    t.foldr (fun a _ d => f a d) init = t.keysArray.foldr f init :=
+  Impl.foldr_eq_foldr_keysArray
+
 theorem forM_eq_forM_keys [Monad m] [LawfulMonad m] {f : α → m PUnit} :
     ForM.forM t (fun a => f a.1) = t.keys.forM f :=
   Impl.forM_eq_forM_keys
 
+theorem forM_eq_forM_keysArray [Monad m] [LawfulMonad m] {f : α → m PUnit} :
+    ForM.forM t (fun a => f a.1) = t.keysArray.forM f :=
+  Impl.forM_eq_forM_keysArray
+
 theorem forIn_eq_forIn_keys [Monad m] [LawfulMonad m]
     {f : α → δ → m (ForInStep δ)} {init : δ} :
     ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keys init f :=
   Impl.forIn_eq_forIn_keys
 
+theorem forIn_eq_forIn_keysArray [Monad m] [LawfulMonad m]
+    {f : α → δ → m (ForInStep δ)} {init : δ} :
+    ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keysArray init f :=
+  Impl.forIn_eq_forIn_keysArray
+
 namespace Const
 
 variable {β : Type v} {t : DTreeMap α β cmp}
@@ -1296,19 +1460,37 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m]
     t.foldlM f init = (Const.toList t).foldlM (fun a b => f a b.1 b.2) init :=
   Impl.Const.foldlM_eq_foldlM_toList
 
+theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m]
+    {f : δ → α → β → m δ} {init : δ} :
+    t.foldlM f init = (Const.toArray t).foldlM (fun a b => f a b.1 b.2) init :=
+  Impl.Const.foldlM_eq_foldlM_toArray
+
 theorem foldl_eq_foldl_toList {f : δ → α → β → δ} {init : δ} :
     t.foldl f init = (Const.toList t).foldl (fun a b => f a b.1 b.2) init :=
   Impl.Const.foldl_eq_foldl_toList
 
+theorem foldl_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} :
+    t.foldl f init = (Const.toArray t).foldl (fun a b => f a b.1 b.2) init :=
+  Impl.Const.foldl_eq_foldl_toArray
+
 theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m]
     {f : α → β → δ → m δ} {init : δ} :
     t.foldrM f init = (Const.toList t).foldrM (fun a b => f a.1 a.2 b) init :=
   Impl.Const.foldrM_eq_foldrM_toList
 
+theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m]
+    {f : α → β → δ → m δ} {init : δ} :
+    t.foldrM f init = (Const.toArray t).foldrM (fun a b => f a.1 a.2 b) init :=
+  Impl.Const.foldrM_eq_foldrM_toArray
+
 theorem foldr_eq_foldr_toList {f : α → β → δ → δ} {init : δ} :
     t.foldr f init = (Const.toList t).foldr (fun a b => f a.1 a.2 b) init :=
   Impl.Const.foldr_eq_foldr_toList
 
+theorem foldr_eq_foldr_toArray {f : α → β → δ → δ} {init : δ} :
+    t.foldr f init = (Const.toArray t).foldr (fun a b => f a.1 a.2 b) init :=
+  Impl.Const.foldr_eq_foldr_toArray
+
 theorem forM_eq_forMUncurried [Monad m] [LawfulMonad m] {f : α → β → m PUnit} :
     t.forM f = forMUncurried (fun a => f a.1 a.2) t := rfl
 
@@ -1316,6 +1498,10 @@ theorem forMUncurried_eq_forM_toList [Monad m] [LawfulMonad m] {f : α × β →
     forMUncurried f t = (Const.toList t).forM f :=
   Impl.Const.forM_eq_forM_toList
 
+theorem forMUncurried_eq_forM_toArray [Monad m] [LawfulMonad m] {f : α × β → m PUnit} :
+    forMUncurried f t = (Const.toArray t).forM f :=
+  Impl.Const.forM_eq_forM_toArray
+
 theorem forIn_eq_forInUncurried [Monad m] [LawfulMonad m]
     {f : α → β → δ → m (ForInStep δ)} {init : δ} :
     t.forIn f init = forInUncurried (fun a b => f a.1 a.2 b) init t := rfl
@@ -1325,6 +1511,11 @@ theorem forInUncurried_eq_forIn_toList [Monad m] [LawfulMonad m]
     forInUncurried f init t = ForIn.forIn (Const.toList t) init f :=
   Impl.Const.forIn_eq_forIn_toList
 
+theorem forInUncurried_eq_forIn_toArray [Monad m] [LawfulMonad m]
+    {f : α × β → δ → m (ForInStep δ)} {init : δ} :
+    forInUncurried f init t = ForIn.forIn (Const.toArray t) init f :=
+  Impl.Const.forIn_eq_forIn_toArray
+
 end Const
 
 end monadic
@@ -4173,6 +4364,11 @@ theorem minKey?_insertIfNew_le_self [TransCmp cmp] {k v kmi} :
     t.minKey? = t.keys.head? :=
   Impl.minKey?_eq_head?_keys t.wf
 
+@[grind =_]
+theorem minKey?_eq_getElem?_keysArray [TransCmp cmp] :
+    t.minKey? = t.keysArray[0]? :=
+  Impl.minKey?_eq_getElem?_keysArray t.wf
+
 @[simp, grind =]
 theorem minKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
     (t.modify k f).minKey? = t.minKey? :=
@@ -4325,6 +4521,10 @@ theorem minKey_insertIfNew_le_self [TransCmp cmp] {k v} :
     t.minKey he = t.keys.head (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) :=
   Impl.minKey_eq_head_keys t.wf
 
+@[grind =_] theorem minKey_eq_getElem_keysArray [TransCmp cmp] {he} :
+    t.minKey he = t.keysArray[0]'(Nat.zero_lt_of_ne_zero (by simpa [size_keysArray, isEmpty_eq_size_eq_zero, - Array.size_eq_zero_iff] using he)) :=
+  Impl.minKey_eq_getElem_keysArray t.wf
+
 @[simp, grind =]
 theorem minKey_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
     (t.modify k f).minKey he = t.minKey (cast (congrArg (· = false) isEmpty_modify) he) :=
@@ -4473,6 +4673,10 @@ theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] {k v} :
     t.minKey! = t.keys.head! :=
   Impl.minKey!_eq_head!_keys t.wf
 
+theorem minKey!_eq_getElem!_keysArray [TransCmp cmp] [Inhabited α] :
+    t.minKey! = t.keysArray[0]! :=
+  Impl.minKey!_eq_getElem!_keysArray t.wf
+
 @[simp]
 theorem minKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f} :
     (t.modify k f).minKey! = t.minKey! :=
@@ -4614,6 +4818,10 @@ theorem minKeyD_eq_headD_keys [TransCmp cmp] {fallback} :
     t.minKeyD fallback = t.keys.headD fallback :=
   Impl.minKeyD_eq_headD_keys t.wf
 
+theorem minKeyD_eq_getD_keysArray [TransCmp cmp] {fallback} :
+    t.minKeyD fallback = t.keysArray.getD 0 fallback :=
+  Impl.minKeyD_eq_getD_keysArray t.wf
+
 @[simp, grind =]
 theorem minKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f fallback} :
     (t.modify k f |>.minKeyD fallback) = t.minKeyD fallback :=
@@ -4816,6 +5024,10 @@ theorem self_le_maxKey?_insertIfNew [TransCmp cmp] {k v kmi} :
     t.maxKey? = t.keys.getLast? :=
   Impl.maxKey?_eq_getLast?_keys t.wf
 
+@[grind =_] theorem maxKey?_eq_back?_keysArray [TransCmp cmp] :
+    t.maxKey? = t.keysArray.back? :=
+  Impl.maxKey?_eq_back?_keysArray t.wf
+
 @[simp, grind =]
 theorem maxKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
     (t.modify k f).maxKey? = t.maxKey? :=
@@ -4969,6 +5181,10 @@ theorem self_le_maxKey_insertIfNew [TransCmp cmp] {k v} :
     t.maxKey he = t.keys.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) :=
   Impl.maxKey_eq_getLast_keys t.wf
 
+@[grind =_] theorem maxKey_eq_back_keysArray [TransCmp cmp] {he} :
+    t.maxKey he = t.keysArray.back (Nat.zero_lt_of_ne_zero (by simpa [size_keysArray, isEmpty_eq_size_eq_zero, - Array.size_eq_zero_iff] using he)) :=
+  Impl.maxKey_eq_back_keysArray t.wf
+
 @[simp]
 theorem maxKey_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
     (t.modify k f).maxKey he = t.maxKey (cast (congrArg (· = false) isEmpty_modify) he) :=
@@ -5118,6 +5334,10 @@ theorem maxKey!_eq_getLast!_keys [TransCmp cmp] [Inhabited α] :
     t.maxKey! = t.keys.getLast! :=
   Impl.maxKey!_eq_getLast!_keys t.wf
 
+theorem maxKey!_eq_back!_keysArray [TransCmp cmp] [Inhabited α] :
+    t.maxKey! = t.keysArray.back! :=
+  Impl.maxKey!_eq_back!_keysArray t.wf
+
 @[simp]
 theorem maxKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f} :
     (t.modify k f).maxKey! = t.maxKey! :=
@@ -5261,6 +5481,10 @@ theorem maxKeyD_eq_getLastD_keys [TransCmp cmp] {fallback} :
     t.maxKeyD fallback = t.keys.getLastD fallback :=
   Impl.maxKeyD_eq_getLastD_keys t.wf
 
+theorem maxKeyD_eq_getD_back?_keysArray [TransCmp cmp] {fallback} :
+    t.maxKeyD fallback = t.keysArray.back?.getD fallback :=
+  Impl.maxKeyD_eq_getD_back?_keysArray t.wf
+
 @[simp]
 theorem maxKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f fallback} :
     (t.modify k f |>.maxKeyD fallback) = t.maxKeyD fallback :=
@@ -5906,13 +6130,23 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty :=
 theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList :=
   equiv_iff_equiv.trans Impl.equiv_iff_toList_perm
 
+theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray :=
+  equiv_iff_equiv.trans Impl.equiv_iff_toArray_perm
+
 theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ :=
   ⟨.of_toList_perm h⟩
 
+theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ :=
+  ⟨.of_toArray_perm h⟩
+
 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 equiv_iff_toArray_eq [TransCmp cmp] :
+    t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray :=
+  equiv_iff_equiv.trans (Impl.equiv_iff_toArray_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
@@ -5940,22 +6174,43 @@ variable {β : Type v} {t₁ t₂ : DTreeMap α β cmp}
 theorem Const.equiv_iff_toList_perm : t₁ ~m t₂ ↔ (Const.toList t₁).Perm (Const.toList t₂) :=
   equiv_iff_equiv.trans Impl.Const.equiv_iff_toList_perm
 
+theorem Const.equiv_iff_toArray_perm : t₁ ~m t₂ ↔ (Const.toArray t₁).Perm (Const.toArray t₂) :=
+  equiv_iff_equiv.trans Impl.Const.equiv_iff_toArray_perm
+
 theorem Const.equiv_iff_toList_eq [TransCmp cmp] : t₁ ~m t₂ ↔ Const.toList t₁ = Const.toList t₂ :=
   equiv_iff_equiv.trans (Impl.Const.equiv_iff_toList_eq t₁.2 t₂.2)
 
+theorem Const.equiv_iff_toArray_eq [TransCmp cmp] : t₁ ~m t₂ ↔ Const.toArray t₁ = Const.toArray t₂ :=
+  equiv_iff_equiv.trans (Impl.Const.equiv_iff_toArray_eq t₁.2 t₂.2)
+
 theorem Const.equiv_iff_keys_unit_perm {t₁ t₂ : DTreeMap α Unit cmp} : t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys :=
   equiv_iff_equiv.trans Impl.Const.equiv_iff_keys_perm
 
+theorem Const.equiv_iff_keysArray_unit_perm {t₁ t₂ : DTreeMap α Unit cmp} :
+    t₁ ~m t₂ ↔ t₁.keysArray.Perm t₂.keysArray :=
+  equiv_iff_equiv.trans Impl.Const.equiv_iff_keysArray_perm
+
 theorem Const.equiv_iff_keys_unit_eq [TransCmp cmp] {t₁ t₂ : DTreeMap α Unit cmp} :
     t₁ ~m t₂ ↔ t₁.keys = t₂.keys :=
   equiv_iff_equiv.trans (Impl.Const.equiv_iff_keys_eq t₁.2 t₂.2)
 
+theorem Const.equiv_iff_keysArray_unit_eq [TransCmp cmp] {t₁ t₂ : DTreeMap α Unit cmp} :
+    t₁ ~m t₂ ↔ t₁.keysArray = t₂.keysArray :=
+  equiv_iff_equiv.trans (Impl.Const.equiv_iff_keysArray_eq t₁.2 t₂.2)
+
 theorem Equiv.of_constToList_perm : (Const.toList t₁).Perm (Const.toList t₂) → t₁ ~m t₂ :=
   Const.equiv_iff_toList_perm.mpr
 
+theorem Equiv.of_constToArray_perm : (Const.toArray t₁).Perm (Const.toArray t₂) → t₁ ~m t₂ :=
+  Const.equiv_iff_toArray_perm.mpr
+
 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 Equiv.of_keysArray_unit_perm {t₁ t₂ : DTreeMap α Unit cmp} :
+    t₁.keysArray.Perm t₂.keysArray → t₁ ~m t₂ :=
+  Const.equiv_iff_keysArray_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
@@ -5994,6 +6249,12 @@ theorem toList_filterMap {f : (a : α) → β a → Option (γ a)} :
       t.toList.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) :=
   Impl.toList_filterMap t.wf
 
+@[simp, grind =]
+theorem toArray_filterMap {f : (a : α) → β a → Option (γ a)} :
+    (t.filterMap f).toArray =
+      t.toArray.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) :=
+  Impl.toArray_filterMap t.wf
+
 @[grind =]
 theorem isEmpty_filterMap_iff [TransCmp cmp] [LawfulEqCmp cmp]
     {f : (a : α) → β a → Option (γ a)} :
@@ -6221,6 +6482,12 @@ theorem toList_filterMap
       (Const.toList t).filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) :=
   Impl.Const.toList_filterMap t.wf
 
+theorem toArray_filterMap
+    {f : α → β → Option γ} :
+    Const.toArray (t.filterMap fun k v => f k v) =
+      (Const.toArray t).filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) :=
+  Impl.Const.toArray_filterMap t.wf
+
 @[grind =]
 theorem getKey?_filterMap [TransCmp cmp]
     {f : α → β → Option γ} {k : α} :
@@ -6260,10 +6527,19 @@ theorem toList_filter {f : (a : α) → β a → Bool} :
     (t.filter f).toList = t.toList.filter (fun p => f p.1 p.2) :=
   Impl.toList_filter t.wf
 
+@[simp, grind =]
+theorem toArray_filter {f : (a : α) → β a → Bool} :
+    (t.filter f).toArray = t.toArray.filter (fun p => f p.1 p.2) :=
+  Impl.toArray_filter t.wf
+
 theorem keys_filter_key {f : α → Bool} :
     (t.filter fun k _ => f k).keys = t.keys.filter f :=
   Impl.keys_filter_key t.wf
 
+theorem keysArray_filter_key {f : α → Bool} :
+    (t.filter fun k _ => f k).keysArray = t.keysArray.filter f :=
+  Impl.keysArray_filter_key t.wf
+
 @[grind =]
 theorem isEmpty_filter_iff [TransCmp cmp] [LawfulEqCmp cmp]
     {f : (a : α) → β a → Bool} :
@@ -6536,6 +6812,12 @@ theorem toList_filter {f : α → β → Bool} :
       (toList t).filter (fun p => f p.1 p.2) :=
   Impl.Const.toList_filter t.wf
 
+@[simp, grind =]
+theorem toArray_filter {f : α → β → Bool} :
+    toArray (t.filter f) =
+      (toArray t).filter (fun p => f p.1 p.2) :=
+  Impl.Const.toArray_filter t.wf
+
 theorem keys_filter [TransCmp cmp] {f : α → β → Bool} :
     (t.filter f).keys =
       (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keys h')))).unattach :=
@@ -6585,10 +6867,19 @@ theorem toList_map {f : (a : α) → β a → γ a} :
     (t.map f).toList = t.toList.map (fun p => ⟨p.1, f p.1 p.2⟩) :=
   Impl.toList_map
 
+@[simp, grind =]
+theorem toArray_map {f : (a : α) → β a → γ a} :
+    (t.map f).toArray = t.toArray.map (fun p => ⟨p.1, f p.1 p.2⟩) :=
+  Impl.toArray_map
+
 @[simp, grind =]
 theorem keys_map {f : (a : α) → β a → γ a} : (t.map f).keys = t.keys :=
   Impl.keys_map
 
+@[simp, grind =]
+theorem keysArray_map {f : (a : α) → β a → γ a} : (t.map f).keysArray = t.keysArray :=
+  Impl.keysArray_map
+
 theorem filterMap_equiv_map [TransCmp cmp]
     {f : (a : α) → β a → γ a} :
     (t.filterMap (fun k v => some (f k v))) ~m t.map f :=
@@ -6757,8 +7048,32 @@ theorem toList_map {f : α → β → γ} :
       (Const.toList t).map (fun p => (p.1, f p.1 p.2)) :=
   Impl.Const.toList_map
 
+@[simp, grind =]
+theorem toArray_map {f : α → β → γ} :
+    (Const.toArray (t.map f)) =
+      (Const.toArray t).map (fun p => (p.1, f p.1 p.2)) :=
+  Impl.Const.toArray_map
+
+theorem toArray_toList : (toList t).toArray = toArray t :=
+  Impl.Const.toArray_toList
+
+theorem toList_toArray : (toArray t).toList = toList t :=
+  Impl.Const.toList_toArray
+
 end Const
 
 end map
 
+theorem toArray_toList : t.toList.toArray = t.toArray :=
+  Impl.toArray_toList
+
+theorem toList_toArray : t.toArray.toList = t.toList :=
+  Impl.toList_toArray
+
+theorem toArray_keys : t.keys.toArray = t.keysArray :=
+  Impl.toArray_keys
+
+theorem toList_keysArray : t.keysArray.toList = t.keys :=
+  Impl.toList_keysArray
+
 end Std.DTreeMap

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

@@ -8,6 +8,7 @@ module
 prelude
 import Std.Data.DTreeMap.Internal.Lemmas
 public import Std.Data.DTreeMap.Raw.AdditionalOperations
+public import Init.Data.Array.Perm
 import Init.Data.List.Find
 import Init.Data.List.Pairwise
 import Init.Data.Prod
@@ -100,6 +101,18 @@ theorem isEmpty_iff_forall_not_mem [TransCmp cmp] (h : t.WF) :
     t.isEmpty = true ↔ ∀ a, ¬a ∈ t :=
   Impl.isEmpty_iff_forall_not_mem h
 
+theorem toArray_toList : t.toList.toArray = t.toArray :=
+  Impl.toArray_toList
+
+theorem toList_toArray : t.toArray.toList = t.toList :=
+  Impl.toList_toArray
+
+theorem toArray_keys : t.keys.toArray = t.keysArray :=
+  Impl.toArray_keys
+
+theorem toList_keysArray : t.keysArray.toList = t.keys :=
+  Impl.toList_keysArray
+
 @[simp]
 theorem insert_eq_insert {p : (a : α) × β a} : Insert.insert p t = t.insert p.1 p.2 :=
   rfl
@@ -286,6 +299,12 @@ namespace Const
 
 variable {β : Type v} {t : Raw α β cmp}
 
+theorem toArray_toList : (toList t).toArray = toArray t :=
+  Impl.Const.toArray_toList
+
+theorem toList_toArray : (toArray t).toList = toList t :=
+  Impl.Const.toList_toArray
+
 @[simp, grind =]
 theorem get?_emptyc [TransCmp cmp] {a : α} :
     get? (∅ : Raw α β cmp) a = none :=
@@ -357,14 +376,26 @@ theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF)
     (t.insert k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) :=
   Impl.toList_insert!_perm h
 
+theorem toArray_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insert k v).toArray.Perm (t.toArray.filter (¬k == ·.1) |>.push ⟨k, v⟩) :=
+  Impl.toArray_insert!_perm h
+
 theorem Const.toList_insert_perm {β : Type v} {t : Raw α (fun _ => β) cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β} :
     (Const.toList (t.insert k v)).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) :=
   Impl.Const.toList_insert!_perm h
 
+theorem Const.toArray_insert_perm {β : Type v} {t : Raw α (fun _ => β) cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (Const.toArray (t.insert k v)).Perm ((Const.toArray t).filter (¬k == ·.1) |>.push ⟨k, v⟩) :=
+  Impl.Const.toArray_insert!_perm h
+
 theorem keys_insertIfNew_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β k} :
     (t.insertIfNew k v).keys.Perm (if k ∈ t then t.keys else k :: t.keys) :=
   Impl.keys_insertIfNew!_perm h
 
+theorem keysArray_insertIfNew_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    (t.insertIfNew k v).keysArray.Perm (if k ∈ t then t.keysArray else t.keysArray.push k) :=
+  Impl.keysArray_insertIfNew!_perm h.out
+
 @[grind =] theorem get_insert [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {v : β k} {h₁} :
     (t.insert k v).get a h₁ =
       if h₂ : cmp k a = .eq then
@@ -1106,25 +1137,49 @@ theorem length_keys [TransCmp cmp] (h : t.WF) :
     t.keys.length = t.size :=
   Impl.length_keys h.out
 
+@[simp, grind =]
+theorem size_keysArray [TransCmp cmp] (h : t.WF) :
+    t.keysArray.size = t.size :=
+  Impl.size_keysArray h.out
+
 @[simp, grind =]
 theorem isEmpty_keys :
     t.keys.isEmpty = t.isEmpty :=
   Impl.isEmpty_keys
 
+@[simp, grind =]
+theorem isEmpty_keysArray :
+    t.keysArray.isEmpty = t.isEmpty :=
+  Impl.isEmpty_keysArray
+
 @[simp, grind =]
 theorem contains_keys [BEq α] [LawfulBEqCmp cmp] (h : t.WF) [TransCmp cmp] {k : α} :
     t.keys.contains k = t.contains k :=
   Impl.contains_keys h
 
+@[simp, grind =]
+theorem contains_keysArray [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} (h : t.WF) :
+    t.keysArray.contains k = t.contains k :=
+  Impl.contains_keysArray h.out
+
 @[simp, grind =]
 theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
     k ∈ t.keys ↔ k ∈ t :=
   Impl.mem_keys h
 
+@[simp, grind =]
+theorem mem_keysArray [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
+    k ∈ t.keysArray ↔ k ∈ t :=
+  Impl.mem_keysArray h
+
 theorem mem_of_mem_keys [TransCmp cmp] (h : t.WF) {k : α}
     (h' : k ∈ t.keys) : k ∈ t :=
   Impl.mem_of_mem_keys h h'
 
+theorem mem_of_mem_keysArray [TransCmp cmp] (h : t.WF) {k : α}
+    (h' : k ∈ t.keysArray) : k ∈ t :=
+  Impl.mem_of_mem_keysArray h h'
+
 theorem distinct_keys [TransCmp cmp] (h : t.WF) :
     t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) :=
   Impl.distinct_keys h.out
@@ -1142,34 +1197,67 @@ theorem map_fst_toList_eq_keys :
     t.toList.map Sigma.fst = t.keys :=
   Impl.map_fst_toList_eq_keys
 
+@[simp, grind _=_]
+theorem map_fst_toArray_eq_keysArray :
+    t.toArray.map Sigma.fst = t.keysArray :=
+  Impl.map_fst_toArray_eq_keysArray
+
 @[simp, grind =]
 theorem length_toList [TransCmp cmp] (h : t.WF) :
     t.toList.length = t.size :=
   Impl.length_toList h.out
 
+@[simp, grind =]
+theorem size_toArray [TransCmp cmp] (h : t.WF) :
+    t.toArray.size = t.size :=
+  Impl.size_toArray h.out
+
 @[simp, grind =]
 theorem isEmpty_toList :
     t.toList.isEmpty = t.isEmpty :=
   Impl.isEmpty_toList
 
+@[simp, grind =]
+theorem isEmpty_toArray :
+    t.toArray.isEmpty = t.isEmpty :=
+  Impl.isEmpty_toArray
+
 @[simp, grind =]
 theorem mem_toList_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β k} :
     ⟨k, v⟩ ∈ t.toList ↔ t.get? k = some v :=
   Impl.mem_toList_iff_get?_eq_some h.out
 
+@[simp, grind =]
+theorem mem_toArray_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β k} :
+    ⟨k, v⟩ ∈ t.toArray ↔ t.get? k = some v :=
+  Impl.mem_toArray_iff_get?_eq_some h.out
+
 theorem find?_toList_eq_some_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α}
     {v : β k} : t.toList.find? (cmp ·.1 k == .eq) = some ⟨k, v⟩ ↔ t.get? k = some v :=
   Impl.find?_toList_eq_some_iff_get?_eq_some h.out
 
+theorem find?_toArray_eq_some_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α}
+    {v : β k} : t.toArray.find? (cmp ·.1 k == .eq) = some ⟨k, v⟩ ↔ t.get? k = some v :=
+  Impl.find?_toArray_eq_some_iff_get?_eq_some h.out
+
 theorem find?_toList_eq_none_iff_contains_eq_false [TransCmp cmp] (h : t.WF) {k : α} :
     t.toList.find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false :=
   Impl.find?_toList_eq_none_iff_contains_eq_false h.out
 
+theorem find?_toArray_eq_none_iff_contains_eq_false [TransCmp cmp] (h : t.WF) {k : α} :
+    t.toArray.find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false :=
+  Impl.find?_toArray_eq_none_iff_contains_eq_false h.out
+
 @[simp]
 theorem find?_toList_eq_none_iff_not_mem [TransCmp cmp] (h : t.WF) {k : α} :
     t.toList.find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := by
   simpa only [Bool.not_eq_true, mem_iff_contains] using find?_toList_eq_none_iff_contains_eq_false h
 
+@[simp]
+theorem find?_toArray_eq_none_iff_not_mem [TransCmp cmp] (h : t.WF) {k : α} :
+    t.toArray.find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t :=
+  Impl.find?_toArray_eq_none_iff_not_mem h.out
+
 theorem distinct_keys_toList [TransCmp cmp] (h : t.WF) :
     t.toList.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
   Impl.distinct_keys_toList h.out
@@ -1187,45 +1275,89 @@ theorem map_fst_toList_eq_keys :
     (toList t).map Prod.fst = t.keys :=
   Impl.Const.map_fst_toList_eq_keys
 
+@[simp, grind _=_]
+theorem map_fst_toArray_eq_keysArray :
+    (toArray t).map Prod.fst = t.keysArray :=
+  Impl.Const.map_fst_toArray_eq_keysArray
+
 @[simp, grind =]
 theorem length_toList (h : t.WF) :
     (toList t).length = t.size :=
   Impl.Const.length_toList h.out
 
+@[simp, grind =]
+theorem size_toArray (h : t.WF) :
+    (toArray t).size = t.size :=
+  Impl.Const.size_toArray h.out
+
 @[simp, grind =]
 theorem isEmpty_toList :
     (toList t).isEmpty = t.isEmpty :=
   Impl.Const.isEmpty_toList
 
+@[simp, grind =]
+theorem isEmpty_toArray :
+    (toArray t).isEmpty = t.isEmpty :=
+  Impl.Const.isEmpty_toArray
+
 @[simp, grind =]
 theorem mem_toList_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β} :
     (k, v) ∈ toList t ↔ get? t k = some v :=
   Impl.Const.mem_toList_iff_get?_eq_some h
 
+@[simp, grind =]
+theorem mem_toArray_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (k, v) ∈ toArray t ↔ get? t k = some v :=
+  Impl.Const.mem_toArray_iff_get?_eq_some h
+
 @[simp]
 theorem mem_toList_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
     (k, v) ∈ toList t ↔ t.getKey? k = some k ∧ get? t k = some v :=
   Impl.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some h
 
+@[simp]
+theorem mem_toArray_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (k, v) ∈ toArray t ↔ t.getKey? k = some k ∧ get? t k = some v :=
+  Impl.Const.mem_toArray_iff_getKey?_eq_some_and_get?_eq_some h
+
 theorem get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
     get? t k = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toList t :=
   Impl.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList h
 
+theorem get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    get? t k = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toArray t :=
+  Impl.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray h
+
 theorem find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] (h : t.WF)
     {k k' : α} {v : β} :
     (toList t).find? (fun a => cmp a.1 k = .eq) = some ⟨k', v⟩ ↔
       t.getKey? k = some k' ∧ get? t k = some v :=
   Impl.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some h.out
 
+theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] (h : t.WF)
+    {k k' : α} {v : β} :
+    (toArray t).find? (fun a => cmp a.1 k = .eq) = some ⟨k', v⟩ ↔
+      t.getKey? k = some k' ∧ get? t k = some v :=
+  Impl.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some h.out
+
 theorem find?_toList_eq_none_iff_contains_eq_false [TransCmp cmp] (h : t.WF) {k : α} :
     (toList t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false :=
   Impl.Const.find?_toList_eq_none_iff_contains_eq_false h.out
 
+theorem find?_toArray_eq_none_iff_contains_eq_false [TransCmp cmp] (h : t.WF) {k : α} :
+    (toArray t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false :=
+  Impl.Const.find?_toArray_eq_none_iff_contains_eq_false h.out
+
 @[simp]
 theorem find?_toList_eq_none_iff_not_mem [TransCmp cmp] (h : t.WF) {k : α} :
     (toList t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t :=
   Impl.Const.find?_toList_eq_none_iff_not_mem h.out
 
+@[simp]
+theorem find?_toArray_eq_none_iff_not_mem [TransCmp cmp] (h : t.WF) {k : α} :
+    (toArray t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t :=
+  Impl.Const.find?_toArray_eq_none_iff_not_mem h.out
+
 theorem distinct_keys_toList [TransCmp cmp] (h : t.WF) :
     (toList t).Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
   Impl.Const.distinct_keys_toList h.out
@@ -1244,18 +1376,34 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] {f : δ → (a : α)
     t.foldlM f init = t.toList.foldlM (fun a b => f a b.1 b.2) init :=
   Impl.foldlM_eq_foldlM_toList
 
+theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ} :
+    t.foldlM f init = t.toArray.foldlM (fun a b => f a b.1 b.2) init :=
+  Impl.foldlM_eq_foldlM_toArray
+
 theorem foldl_eq_foldl_toList {f : δ → (a : α) → β a → δ} {init : δ} :
     t.foldl f init = t.toList.foldl (fun a b => f a b.1 b.2) init :=
   Impl.foldl_eq_foldl_toList
 
+theorem foldl_eq_foldl_toArray {f : δ → (a : α) → β a → δ} {init : δ} :
+    t.foldl f init = t.toArray.foldl (fun a b => f a b.1 b.2) init :=
+  Impl.foldl_eq_foldl_toArray
+
 theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} :
     t.foldrM f init = t.toList.foldrM (fun a b => f a.1 a.2 b) init :=
   Impl.foldrM_eq_foldrM_toList
 
+theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} :
+    t.foldrM f init = t.toArray.foldrM (fun a b => f a.1 a.2 b) init :=
+  Impl.foldrM_eq_foldrM_toArray
+
 theorem foldr_eq_foldr_toList {f : (a : α) → β a → δ → δ} {init : δ} :
     t.foldr f init = t.toList.foldr (fun a b => f a.1 a.2 b) init :=
   Impl.foldr_eq_foldr_toList
 
+theorem foldr_eq_foldr_toArray {f : (a : α) → β a → δ → δ} {init : δ} :
+    t.foldr f init = t.toArray.foldr (fun a b => f a.1 a.2 b) init :=
+  Impl.foldr_eq_foldr_toArray
+
 @[simp, grind =]
 theorem forM_eq_forM [Monad m] [LawfulMonad m] {f : (a : α) → β a → m PUnit} :
     t.forM f = ForM.forM t (fun a => f a.1 a.2) := rfl
@@ -1264,6 +1412,10 @@ theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : (a : α) × β a →
     ForM.forM t f = ForM.forM t.toList f :=
   Impl.forM_eq_forM_toList
 
+theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit} :
+    ForM.forM t f = ForM.forM t.toArray f :=
+  Impl.forM_eq_forM_toArray
+
 @[simp, grind =]
 theorem forIn_eq_forIn [Monad m] [LawfulMonad m]
     {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ} :
@@ -1274,31 +1426,61 @@ theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m]
     ForIn.forIn t init f = ForIn.forIn t.toList init f :=
   Impl.forIn_eq_forIn_toList (f := f)
 
+theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m]
+    {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ} :
+    ForIn.forIn t init f = ForIn.forIn t.toArray init f :=
+  Impl.forIn_eq_forIn_toArray (f := f)
+
 theorem foldlM_eq_foldlM_keys [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
     t.foldlM (fun d a _ => f d a) init = t.keys.foldlM f init :=
   Impl.foldlM_eq_foldlM_keys
 
+theorem foldlM_eq_foldlM_keysArray [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
+    t.foldlM (fun d a _ => f d a) init = t.keysArray.foldlM f init :=
+  Impl.foldlM_eq_foldlM_keysArray
+
 theorem foldl_eq_foldl_keys {f : δ → α → δ} {init : δ} :
     t.foldl (fun d a _ => f d a) init = t.keys.foldl f init :=
   Impl.foldl_eq_foldl_keys
 
+theorem foldl_eq_foldl_keysArray {f : δ → α → δ} {init : δ} :
+    t.foldl (fun d a _ => f d a) init = t.keysArray.foldl f init :=
+  Impl.foldl_eq_foldl_keysArray
+
 theorem foldrM_eq_foldrM_keys [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
     t.foldrM (fun a _ d => f a d) init = t.keys.foldrM f init :=
   Impl.foldrM_eq_foldrM_keys
 
+theorem foldrM_eq_foldrM_keysArray [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
+    t.foldrM (fun a _ d => f a d) init = t.keysArray.foldrM f init :=
+  Impl.foldrM_eq_foldrM_keysArray
+
 theorem foldr_eq_foldr_keys {f : α → δ → δ} {init : δ} :
     t.foldr (fun a _ d => f a d) init = t.keys.foldr f init :=
   Impl.foldr_eq_foldr_keys
 
+theorem foldr_eq_foldr_keysArray {f : α → δ → δ} {init : δ} :
+    t.foldr (fun a _ d => f a d) init = t.keysArray.foldr f init :=
+  Impl.foldr_eq_foldr_keysArray
+
 theorem forM_eq_forM_keys [Monad m] [LawfulMonad m] {f : α → m PUnit} :
     ForM.forM t (fun a => f a.1) = t.keys.forM f :=
   Impl.forM_eq_forM_keys
 
+theorem forM_eq_forM_keysArray [Monad m] [LawfulMonad m] {f : α → m PUnit} :
+    ForM.forM t (fun a => f a.1) = t.keysArray.forM f :=
+  Impl.forM_eq_forM_keysArray
+
 theorem forIn_eq_forIn_keys [Monad m] [LawfulMonad m]
     {f : α → δ → m (ForInStep δ)} {init : δ} :
     ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keys init f :=
   Impl.forIn_eq_forIn_keys
 
+theorem forIn_eq_forIn_keysArray [Monad m] [LawfulMonad m]
+    {f : α → δ → m (ForInStep δ)} {init : δ} :
+    ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keysArray init f :=
+  Impl.forIn_eq_forIn_keysArray
+
 namespace Const
 
 variable {β : Type v} {t : Raw α β cmp}
@@ -1307,18 +1489,34 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] {f : δ → α → β
     t.foldlM f init = (Const.toList t).foldlM (fun a b => f a b.1 b.2) init :=
   Impl.Const.foldlM_eq_foldlM_toList
 
+theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ} :
+    t.foldlM f init = (Const.toArray t).foldlM (fun a b => f a b.1 b.2) init :=
+  Impl.Const.foldlM_eq_foldlM_toArray
+
 theorem foldl_eq_foldl_toList {f : δ → α → β → δ} {init : δ} :
     t.foldl f init = (Const.toList t).foldl (fun a b => f a b.1 b.2) init :=
   Impl.Const.foldl_eq_foldl_toList
 
+theorem foldl_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} :
+    t.foldl f init = (Const.toArray t).foldl (fun a b => f a b.1 b.2) init :=
+  Impl.Const.foldl_eq_foldl_toArray
+
 theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} :
     t.foldrM f init = (Const.toList t).foldrM (fun a b => f a.1 a.2 b) init :=
   Impl.Const.foldrM_eq_foldrM_toList
 
+theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} :
+    t.foldrM f init = (Const.toArray t).foldrM (fun a b => f a.1 a.2 b) init :=
+  Impl.Const.foldrM_eq_foldrM_toArray
+
 theorem foldr_eq_foldr_toList {f : α → β → δ → δ} {init : δ} :
     t.foldr f init = (Const.toList t).foldr (fun a b => f a.1 a.2 b) init :=
   Impl.Const.foldr_eq_foldr_toList
 
+theorem foldr_eq_foldr_toArray {f : α → β → δ → δ} {init : δ} :
+    t.foldr f init = (Const.toArray t).foldr (fun a b => f a.1 a.2 b) init :=
+  Impl.Const.foldr_eq_foldr_toArray
+
 theorem forM_eq_forMUncurried [Monad m] [LawfulMonad m] {f : α → β → m PUnit} :
     t.forM f = forMUncurried (fun a => f a.1 a.2) t := rfl
 
@@ -1326,6 +1524,10 @@ theorem forMUncurried_eq_forM_toList [Monad m] [LawfulMonad m] {f : α × β →
     forMUncurried f t = (Const.toList t).forM f :=
   Impl.Const.forM_eq_forM_toList
 
+theorem forMUncurried_eq_forM_toArray [Monad m] [LawfulMonad m] {f : α × β → m PUnit} :
+    forMUncurried f t = (Const.toArray t).forM f :=
+  Impl.Const.forM_eq_forM_toArray
+
 theorem forIn_eq_forInUncurried [Monad m] [LawfulMonad m]
     {f : α → β → δ → m (ForInStep δ)} {init : δ} :
     t.forIn f init = forInUncurried (fun a b => f a.1 a.2 b) init t := rfl
@@ -1335,6 +1537,11 @@ theorem forInUncurried_eq_forIn_toList [Monad m] [LawfulMonad m]
     forInUncurried f init t = ForIn.forIn (Const.toList t) init f :=
   Impl.Const.forIn_eq_forIn_toList
 
+theorem forInUncurried_eq_forIn_toArray [Monad m] [LawfulMonad m]
+    {f : α × β → δ → m (ForInStep δ)} {init : δ} :
+    forInUncurried f init t = ForIn.forIn (Const.toArray t) init f :=
+  Impl.Const.forIn_eq_forIn_toArray
+
 end Const
 
 end monadic
@@ -4383,6 +4590,11 @@ theorem minKey?_eq_head?_keys [TransCmp cmp] (h : t.WF) :
     t.minKey? = t.keys.head? :=
   Impl.minKey?_eq_head?_keys h (instOrd := ⟨cmp⟩)
 
+@[grind =_]
+theorem minKey?_eq_getElem?_keysArray [TransCmp cmp] (h : t.WF) :
+    t.minKey? = t.keysArray[0]? :=
+  Impl.minKey?_eq_getElem?_keysArray h (instOrd := ⟨cmp⟩)
+
 @[simp, grind =]
 theorem minKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} (h : t.WF) :
     (t.modify k f).minKey? = t.minKey? :=
@@ -4532,6 +4744,11 @@ theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) :
     t.minKey! = t.keys.head! :=
   Impl.minKey!_eq_head!_keys h (instOrd := ⟨cmp⟩)
 
+@[grind =_]
+theorem minKey!_eq_getElem!_keysArray [TransCmp cmp] [Inhabited α] (h : t.WF) :
+    t.minKey! = t.keysArray[0]! :=
+  Impl.minKey!_eq_getElem!_keysArray h (instOrd := ⟨cmp⟩)
+
 @[simp]
 theorem minKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} :
     (t.modify k f).minKey! = t.minKey! :=
@@ -4678,6 +4895,10 @@ theorem minKeyD_eq_headD_keys [TransCmp cmp] (h : t.WF) {fallback} :
     t.minKeyD fallback = t.keys.headD fallback :=
   Impl.minKeyD_eq_headD_keys h (instOrd := ⟨cmp⟩)
 
+theorem minKeyD_eq_getD_keysArray [TransCmp cmp] (h : t.WF) {fallback} :
+    t.minKeyD fallback = t.keysArray.getD 0 fallback :=
+  Impl.minKeyD_eq_getD_keysArray h (instOrd := ⟨cmp⟩)
+
 @[simp, grind =]
 theorem minKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f fallback} :
     (t.modify k f |>.minKeyD fallback) = t.minKeyD fallback :=
@@ -4885,6 +5106,11 @@ theorem maxKey?_eq_getLast?_keys [TransCmp cmp] (h : t.WF) :
     t.maxKey? = t.keys.getLast? :=
   Impl.maxKey?_eq_getLast?_keys h (instOrd := ⟨cmp⟩)
 
+@[grind =_]
+theorem maxKey?_eq_back?_keysArray [TransCmp cmp] (h : t.WF) :
+    t.maxKey? = t.keysArray.back? :=
+  Impl.maxKey?_eq_back?_keysArray h (instOrd := ⟨cmp⟩)
+
 @[simp, grind =]
 theorem maxKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} (h : t.WF) :
     (t.modify k f).maxKey? = t.maxKey? :=
@@ -5032,6 +5258,11 @@ theorem maxKey!_eq_getLast!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) :
     t.maxKey! = t.keys.getLast! :=
   Impl.maxKey!_eq_getLast!_keys h (instOrd := ⟨cmp⟩)
 
+@[grind =_]
+theorem maxKey!_eq_back!_keysArray [TransCmp cmp] [Inhabited α] (h : t.WF) :
+    t.maxKey! = t.keysArray.back! :=
+  Impl.maxKey!_eq_back!_keysArray h (instOrd := ⟨cmp⟩)
+
 @[simp, grind =]
 theorem maxKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} :
     (t.modify k f).maxKey! = t.maxKey! :=
@@ -5180,6 +5411,11 @@ theorem maxKeyD_eq_getLastD_keys [TransCmp cmp] (h : t.WF) {fallback} :
     t.maxKeyD fallback = t.keys.getLastD fallback :=
   Impl.maxKeyD_eq_getLastD_keys h (instOrd := ⟨cmp⟩)
 
+@[grind =_]
+theorem maxKeyD_eq_getD_back?_keysArray [TransCmp cmp] (h : t.WF) {fallback} :
+    t.maxKeyD fallback = t.keysArray.back?.getD fallback :=
+  Impl.maxKeyD_eq_getD_back?_keysArray h (instOrd := ⟨cmp⟩)
+
 @[simp, grind =]
 theorem maxKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f fallback} :
     (t.modify k f |>.maxKeyD fallback) = t.maxKeyD fallback :=
@@ -5762,13 +5998,23 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty :=
 theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList :=
   equiv_iff.trans Impl.equiv_iff_toList_perm
 
+theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray :=
+  equiv_iff.trans Impl.equiv_iff_toArray_perm
+
 theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ :=
   ⟨.of_toList_perm h⟩
 
+theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ :=
+  ⟨.of_toArray_perm h⟩
+
 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 equiv_iff_toArray_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
+    t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray :=
+  equiv_iff.trans (Impl.equiv_iff_toArray_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
@@ -5788,24 +6034,46 @@ variable {β : Type v} {t₁ t₂ : Raw α β cmp}
 theorem Const.equiv_iff_toList_perm : t₁ ~m t₂ ↔ (Const.toList t₁).Perm (Const.toList t₂) :=
   equiv_iff.trans Impl.Const.equiv_iff_toList_perm
 
+theorem Const.equiv_iff_toArray_perm : t₁ ~m t₂ ↔ (Const.toArray t₁).Perm (Const.toArray t₂) :=
+  equiv_iff.trans Impl.Const.equiv_iff_toArray_perm
+
 theorem Const.equiv_iff_toList_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
     t₁ ~m t₂ ↔ Const.toList t₁ = Const.toList t₂ :=
   equiv_iff.trans (Impl.Const.equiv_iff_toList_eq h₁.1 h₂.1)
 
+theorem Const.equiv_iff_toArray_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
+    t₁ ~m t₂ ↔ Const.toArray t₁ = Const.toArray t₂ :=
+  equiv_iff.trans (Impl.Const.equiv_iff_toArray_eq h₁.1 h₂.1)
+
 theorem Const.equiv_iff_keys_unit_perm {t₁ t₂ : Raw α Unit cmp} :
     t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys :=
   equiv_iff.trans Impl.Const.equiv_iff_keys_perm
 
+theorem Const.equiv_iff_keysArray_unit_perm {t₁ t₂ : Raw α Unit cmp} :
+    t₁ ~m t₂ ↔ t₁.keysArray.Perm t₂.keysArray :=
+  equiv_iff.trans Impl.Const.equiv_iff_keysArray_perm
+
 theorem Const.equiv_iff_keys_unit_eq {t₁ t₂ : Raw α Unit cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
     t₁ ~m t₂ ↔ t₁.keys = t₂.keys :=
   equiv_iff.trans (Impl.Const.equiv_iff_keys_eq h₁.1 h₂.1)
 
+theorem Const.equiv_iff_keysArray_unit_eq {t₁ t₂ : Raw α Unit cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
+    t₁ ~m t₂ ↔ t₁.keysArray = t₂.keysArray :=
+  equiv_iff.trans (Impl.Const.equiv_iff_keysArray_eq h₁.1 h₂.1)
+
 theorem Equiv.of_constToList_perm : (Const.toList t₁).Perm (Const.toList t₂) → t₁ ~m t₂ :=
   Const.equiv_iff_toList_perm.mpr
 
+theorem Equiv.of_constToArray_perm : (Const.toArray t₁).Perm (Const.toArray t₂) → t₁ ~m t₂ :=
+  Const.equiv_iff_toArray_perm.mpr
+
 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 Equiv.of_keysArray_unit_perm {t₁ t₂ : Raw α Unit cmp} :
+    t₁.keysArray.Perm t₂.keysArray → t₁ ~m t₂ :=
+  Const.equiv_iff_keysArray_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
@@ -5841,6 +6109,11 @@ theorem toList_filterMap {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
       t.toList.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) :=
   Impl.toList_filterMap! h
 
+theorem toArray_filterMap {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
+    (t.filterMap f).toArray =
+      t.toArray.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) :=
+  Impl.toArray_filterMap! h
+
 @[grind =]
 theorem isEmpty_filterMap_iff [TransCmp cmp] [LawfulEqCmp cmp]
     {f : (a : α) → β a → Option (γ a)} (h : t.WF) :
@@ -6064,6 +6337,12 @@ theorem toList_filterMap
       (Const.toList t).filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) :=
   Impl.Const.toList_filterMap! h
 
+theorem toArray_filterMap
+    {f : α → β → Option γ} (h : t.WF) :
+    Const.toArray (t.filterMap f) =
+      (Const.toArray t).filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) :=
+  Impl.Const.toArray_filterMap! h
+
 @[grind =]
 theorem getKey?_filterMap [TransCmp cmp]
     {f : α → β → Option γ} {k : α} (h : t.WF) :
@@ -6108,10 +6387,18 @@ theorem toList_filter {f : (a : α) → β a → Bool} (h : t.WF) :
     (t.filter f).toList = t.toList.filter (fun p => f p.1 p.2) :=
   Impl.toList_filter! h
 
+theorem toArray_filter {f : (a : α) → β a → Bool} (h : t.WF) :
+    (t.filter f).toArray = t.toArray.filter (fun p => f p.1 p.2) :=
+  Impl.toArray_filter! h
+
 theorem keys_filter_key {f : α → Bool} (h : t.WF) :
     (t.filter fun k _ => f k).keys = t.keys.filter f :=
   Impl.keys_filter!_key h
 
+theorem keysArray_filter_key {f : α → Bool} (h : t.WF) :
+    (t.filter fun k _ => f k).keysArray = t.keysArray.filter f :=
+  Impl.keysArray_filter!_key h
+
 @[grind =]
 theorem isEmpty_filter_iff [TransCmp cmp] [LawfulEqCmp cmp]
     {f : (a : α) → β a → Bool} (h : t.WF) :
@@ -6381,6 +6668,11 @@ theorem toList_filter {f : α → β → Bool} (h : t.WF) :
       (Const.toList t).filter (fun p => f p.1 p.2) :=
   Impl.Const.toList_filter! h
 
+theorem toArray_filter {f : α → β → Bool} (h : t.WF) :
+    Const.toArray (t.filter f) =
+      (Const.toArray t).filter (fun p => f p.1 p.2) :=
+  Impl.Const.toArray_filter! h
+
 theorem keys_filter [TransCmp cmp] {f : α → β → Bool} (h : t.WF) :
     (t.filter f).keys =
       (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keys h h')))).unattach :=
@@ -6429,9 +6721,16 @@ theorem toList_map {f : (a : α) → β a → γ a} :
     (t.map f).toList = t.toList.map (fun p => ⟨p.1, f p.1 p.2⟩) :=
   Impl.toList_map
 
+theorem toArray_map {f : (a : α) → β a → γ a} :
+    (t.map f).toArray = t.toArray.map (fun p => ⟨p.1, f p.1 p.2⟩) :=
+  Impl.toArray_map
+
 theorem keys_map {f : (a : α) → β a → γ a} : (t.map f).keys = t.keys :=
   Impl.keys_map
 
+theorem keysArray_map {f : (a : α) → β a → γ a} : (t.map f).keysArray = t.keysArray :=
+  Impl.keysArray_map
+
 theorem filterMap_equiv_map [TransCmp cmp]
     {f : (a : α) → β a → γ a} (h : t.WF) :
     (t.filterMap (fun k v => some (f k v))) ~m t.map f :=
@@ -6598,6 +6897,11 @@ theorem toList_map {f : α → β → γ} :
       (Const.toList t).map (fun p => (p.1, f p.1 p.2)) :=
   Impl.Const.toList_map
 
+theorem toArray_map {f : α → β → γ} :
+    Const.toArray (t.map f) =
+      (Const.toArray t).map (fun p => (p.1, f p.1 p.2)) :=
+  Impl.Const.toArray_map
+
 end Const
 
 end map

src/Std/Data/TreeMap/Lemmas.lean

@@ -8,6 +8,7 @@ module
 prelude
 import Std.Data.DTreeMap.Lemmas
 public import Std.Data.TreeMap.AdditionalOperations
+public import Init.Data.Array.Perm
 import Init.Data.List.Pairwise
 
 @[expose] public section
@@ -297,10 +298,17 @@ theorem getElem?_congr [TransCmp cmp] {a b : α} (hab : cmp a b = .eq) :
 theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β} :
     (t.insert k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) := DTreeMap.Const.toList_insert_perm
 
+theorem toArray_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β} :
+    (t.insert k v).toArray.Perm ((t.toArray.filter (¬k == ·.1)).push ⟨k, v⟩) := DTreeMap.Const.toArray_insert_perm
+
 theorem keys_insertIfNew_perm {t : TreeMap α Unit cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} :
     (t.insertIfNew k ()).keys.Perm (if k ∈ t then t.keys else k :: t.keys) :=
   DTreeMap.keys_insertIfNew_perm
 
+theorem keysArray_insertIfNew_perm {t : TreeMap α Unit cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} :
+    (t.insertIfNew k ()).keysArray.Perm (if k ∈ t then t.keysArray else t.keysArray.push k) :=
+  DTreeMap.keysArray_insertIfNew_perm
+
 @[simp]
 theorem getElem_insert_self [TransCmp cmp] {k : α} {v : β} :
     (t.insert k v)[k]'mem_insert_self = v :=
@@ -804,24 +812,47 @@ theorem length_keys [TransCmp cmp] :
     t.keys.length = t.size :=
   DTreeMap.length_keys
 
+@[simp, grind =]
+theorem size_keysArray [TransCmp cmp] :
+    t.keysArray.size = t.size :=
+  DTreeMap.size_keysArray
+
 @[simp, grind =]
 theorem isEmpty_keys :
     t.keys.isEmpty = t.isEmpty :=
   DTreeMap.isEmpty_keys
 
+@[simp, grind =]
+theorem isEmpty_keysArray :
+    t.keysArray.isEmpty = t.isEmpty :=
+  DTreeMap.isEmpty_keysArray
+
 @[simp, grind =]
 theorem contains_keys [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} :
     t.keys.contains k = t.contains k :=
   DTreeMap.contains_keys
 
+@[simp, grind =]
+theorem contains_keysArray [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} :
+    t.keysArray.contains k = t.contains k :=
+  DTreeMap.contains_keysArray
+
 @[simp, grind =]
 theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
     k ∈ t.keys ↔ k ∈ t :=
   DTreeMap.mem_keys
 
+@[simp, grind =]
+theorem mem_keysArray [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
+    k ∈ t.keysArray ↔ k ∈ t :=
+  DTreeMap.mem_keysArray
+
 theorem mem_of_mem_keys [TransCmp cmp] {k : α} (h : k ∈ t.keys) : k ∈ t :=
   DTreeMap.mem_of_mem_keys h
 
+theorem mem_of_mem_keysArray [TransCmp cmp] {k : α} (h : k ∈ t.keysArray) : k ∈ t :=
+  DTreeMap.mem_of_mem_keysArray h
+
 theorem distinct_keys [TransCmp cmp] :
     t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) :=
   DTreeMap.distinct_keys
@@ -839,45 +870,89 @@ theorem map_fst_toList_eq_keys :
     (toList t).map Prod.fst = t.keys :=
   DTreeMap.Const.map_fst_toList_eq_keys
 
+@[simp, grind _=_]
+theorem map_fst_toArray_eq_keysArray :
+    (toArray t).map Prod.fst = t.keysArray :=
+  DTreeMap.Const.map_fst_toArray_eq_keysArray
+
 @[simp, grind =]
 theorem length_toList :
     (toList t).length = t.size :=
   DTreeMap.Const.length_toList
 
+@[simp, grind =]
+theorem size_toArray :
+    (toArray t).size = t.size :=
+  DTreeMap.Const.size_toArray
+
 @[simp, grind =]
 theorem isEmpty_toList :
     (toList t).isEmpty = t.isEmpty :=
   DTreeMap.Const.isEmpty_toList
 
+@[simp, grind =]
+theorem isEmpty_toArray :
+    (toArray t).isEmpty = t.isEmpty :=
+  DTreeMap.Const.isEmpty_toArray
+
 @[simp, grind =]
 theorem mem_toList_iff_getElem?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β} :
     (k, v) ∈ toList t ↔ t[k]? = some v :=
   DTreeMap.Const.mem_toList_iff_get?_eq_some
 
+@[simp, grind =]
+theorem mem_toArray_iff_getElem?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β} :
+    (k, v) ∈ toArray t ↔ t[k]? = some v :=
+  DTreeMap.Const.mem_toArray_iff_get?_eq_some
+
 @[simp]
 theorem mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] {k : α} {v : β} :
     (k, v) ∈ toList t ↔ t.getKey? k = some k ∧ t[k]? = some v :=
   DTreeMap.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some
 
+@[simp]
+theorem mem_toArray_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] {k : α} {v : β} :
+    (k, v) ∈ toArray t ↔ t.getKey? k = some k ∧ t[k]? = some v :=
+  DTreeMap.Const.mem_toArray_iff_getKey?_eq_some_and_get?_eq_some
+
 theorem getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList [TransCmp cmp] {k : α} {v : β} :
     t[k]? = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toList t :=
   DTreeMap.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList
 
+theorem getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray [TransCmp cmp] {k : α} {v : β} :
+    t[k]? = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toArray t :=
+  DTreeMap.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray
+
 theorem find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] {k k' : α}
     {v : β} :
     t.toList.find? (cmp ·.1 k == .eq) = some ⟨k', v⟩ ↔
       t.getKey? k = some k' ∧ t[k]? = some v :=
   DTreeMap.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some
 
+theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] {k k' : α}
+    {v : β} :
+    t.toArray.find? (cmp ·.1 k == .eq) = some (k', v) ↔
+      t.getKey? k = some k' ∧ t[k]? = some v :=
+  DTreeMap.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+
 theorem find?_toList_eq_none_iff_contains_eq_false [TransCmp cmp] {k : α} :
     (toList t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false :=
   DTreeMap.Const.find?_toList_eq_none_iff_contains_eq_false
 
+theorem find?_toArray_eq_none_iff_contains_eq_false [TransCmp cmp] {k : α} :
+    (toArray t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false :=
+  DTreeMap.Const.find?_toArray_eq_none_iff_contains_eq_false
+
 @[simp]
 theorem find?_toList_eq_none_iff_not_mem [TransCmp cmp] {k : α} :
     (toList t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t :=
   DTreeMap.Const.find?_toList_eq_none_iff_not_mem
 
+@[simp]
+theorem find?_toArray_eq_none_iff_not_mem [TransCmp cmp] {k : α} :
+    (toArray t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t :=
+  DTreeMap.Const.find?_toArray_eq_none_iff_not_mem
+
 theorem distinct_keys_toList [TransCmp cmp] :
     (toList t).Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
   DTreeMap.Const.distinct_keys_toList
@@ -894,18 +969,34 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] {f : δ → α → β
     t.foldlM f init = t.toList.foldlM (fun a b => f a b.1 b.2) init :=
   DTreeMap.Const.foldlM_eq_foldlM_toList
 
+theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ} :
+    t.foldlM f init = t.toArray.foldlM (fun a b => f a b.1 b.2) init :=
+  DTreeMap.Const.foldlM_eq_foldlM_toArray
+
 theorem foldl_eq_foldl_toList {f : δ → α → β → δ} {init : δ} :
     t.foldl f init = t.toList.foldl (fun a b => f a b.1 b.2) init :=
   DTreeMap.Const.foldl_eq_foldl_toList
 
+theorem foldl_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} :
+    t.foldl f init = t.toArray.foldl (fun a b => f a b.1 b.2) init :=
+  DTreeMap.Const.foldl_eq_foldl_toArray
+
 theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} :
     t.foldrM f init = t.toList.foldrM (fun a b => f a.1 a.2 b) init :=
   DTreeMap.Const.foldrM_eq_foldrM_toList
 
+theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} :
+    t.foldrM f init = t.toArray.foldrM (fun a b => f a.1 a.2 b) init :=
+  DTreeMap.Const.foldrM_eq_foldrM_toArray
+
 theorem foldr_eq_foldr_toList {f : α → β → δ → δ} {init : δ} :
     t.foldr f init = t.toList.foldr (fun a b => f a.1 a.2 b) init :=
   DTreeMap.Const.foldr_eq_foldr_toList
 
+theorem foldr_eq_foldr_toArray {f : α → β → δ → δ} {init : δ} :
+    t.foldr f init = t.toArray.foldr (fun a b => f a.1 a.2 b) init :=
+  DTreeMap.Const.foldr_eq_foldr_toArray
+
 @[simp, grind =]
 theorem forM_eq_forM [Monad m] [LawfulMonad m] {f : α → β → m PUnit} :
     t.forM f = ForM.forM t (fun a => f a.1 a.2) := rfl
@@ -914,6 +1005,10 @@ theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : α × β → m PUnit}
     ForM.forM t f = ForM.forM t.toList f :=
   DTreeMap.Const.forMUncurried_eq_forM_toList (f := f)
 
+theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : α × β → m PUnit} :
+    ForM.forM t f = ForM.forM t.toArray f :=
+  DTreeMap.Const.forMUncurried_eq_forM_toArray (f := f)
+
 @[simp, grind =]
 theorem forIn_eq_forIn [Monad m] [LawfulMonad m]
     {f : α → β → δ → m (ForInStep δ)} {init : δ} :
@@ -924,30 +1019,60 @@ theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m]
     ForIn.forIn t init f = ForIn.forIn t.toList init f :=
   DTreeMap.Const.forInUncurried_eq_forIn_toList
 
+theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m]
+    {f : α × β → δ → m (ForInStep δ)} {init : δ} :
+    ForIn.forIn t init f = ForIn.forIn t.toArray init f :=
+  DTreeMap.Const.forInUncurried_eq_forIn_toArray
+
 theorem foldlM_eq_foldlM_keys [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
     t.foldlM (fun d a _ => f d a) init = t.keys.foldlM f init :=
   DTreeMap.foldlM_eq_foldlM_keys
 
+theorem foldlM_eq_foldlM_keysArray [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
+    t.foldlM (fun d a _ => f d a) init = t.keysArray.foldlM f init :=
+  DTreeMap.foldlM_eq_foldlM_keysArray
+
 theorem foldl_eq_foldl_keys {f : δ → α → δ} {init : δ} :
     t.foldl (fun d a _ => f d a) init = t.keys.foldl f init :=
   DTreeMap.foldl_eq_foldl_keys
 
+theorem foldl_eq_foldl_keysArray {f : δ → α → δ} {init : δ} :
+    t.foldl (fun d a _ => f d a) init = t.keysArray.foldl f init :=
+  DTreeMap.foldl_eq_foldl_keysArray
+
 theorem foldrM_eq_foldrM_keys [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
     t.foldrM (fun a _ d => f a d) init = t.keys.foldrM f init :=
   DTreeMap.foldrM_eq_foldrM_keys
 
+theorem foldrM_eq_foldrM_keysArray [Monad m] [LawfulMonad m]
+    {f : α → δ → m δ} {init : δ} :
+    t.foldrM (fun a _ d => f a d) init = t.keysArray.foldrM f init :=
+  DTreeMap.foldrM_eq_foldrM_keysArray
+
 theorem foldr_eq_foldr_keys {f : α → δ → δ} {init : δ} :
     t.foldr (fun a _ d => f a d) init = t.keys.foldr f init :=
   DTreeMap.foldr_eq_foldr_keys
 
+theorem foldr_eq_foldr_keysArray {f : α → δ → δ} {init : δ} :
+    t.foldr (fun a _ d => f a d) init = t.keysArray.foldr f init :=
+  DTreeMap.foldr_eq_foldr_keysArray
+
 theorem forM_eq_forM_keys [Monad m] [LawfulMonad m] {f : α → m PUnit} :
     ForM.forM t (fun a => f a.1) = t.keys.forM f :=
   DTreeMap.forM_eq_forM_keys
 
+theorem forM_eq_forM_keysArray [Monad m] [LawfulMonad m] {f : α → m PUnit} :
+    ForM.forM t (fun a => f a.1) = t.keysArray.forM f :=
+  DTreeMap.forM_eq_forM_keysArray
+
 theorem forIn_eq_forIn_keys [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} :
     ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keys init f :=
   DTreeMap.forIn_eq_forIn_keys
 
+theorem forIn_eq_forIn_keysArray [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} :
+    ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keysArray init f :=
+  DTreeMap.forIn_eq_forIn_keysArray
+
 end monadic
 
 @[simp, grind =]
@@ -2901,6 +3026,10 @@ theorem minKey?_insertIfNew_le_self [TransCmp cmp] {k v kmi} :
     t.minKey? = t.keys.head? :=
   DTreeMap.minKey?_eq_head?_keys
 
+@[grind =_] theorem minKey?_eq_getElem?_keysArray [TransCmp cmp] :
+    t.minKey? = t.keysArray[0]? :=
+  DTreeMap.minKey?_eq_getElem?_keysArray
+
 theorem minKey?_modify [TransCmp cmp] {k f} :
     (t.modify k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
   DTreeMap.Const.minKey?_modify
@@ -3049,6 +3178,10 @@ theorem minKey_insertIfNew_le_self [TransCmp cmp] {k v} :
     t.minKey he = t.keys.head (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) :=
   DTreeMap.minKey_eq_head_keys
 
+theorem minKey_eq_getElem_keysArray [TransCmp cmp] {he} :
+    t.minKey he = t.keysArray[0]'(Nat.zero_lt_of_ne_zero (by simpa [size_keysArray, isEmpty_eq_size_eq_zero, - Array.size_eq_zero_iff] using he)) :=
+  DTreeMap.minKey_eq_getElem_keysArray
+
 theorem minKey_modify [TransCmp cmp] {k f he} :
     (modify t k f).minKey he =
       if cmp (t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) k = .eq then
@@ -3184,6 +3317,10 @@ theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] :
     t.minKey! = t.keys.head! :=
   DTreeMap.minKey!_eq_head!_keys
 
+theorem minKey!_eq_getElem!_keysArray [TransCmp cmp] [Inhabited α] :
+    t.minKey! = t.keysArray[0]! :=
+  DTreeMap.minKey!_eq_getElem!_keysArray
+
 theorem minKey!_modify [TransCmp cmp] [Inhabited α] {k f}
     (he : (modify t k f).isEmpty = false) :
     (modify t k f).minKey! = if cmp t.minKey! k = .eq then k else t.minKey! :=
@@ -3311,6 +3448,10 @@ theorem minKeyD_eq_headD_keys [TransCmp cmp] {fallback} :
     t.minKeyD fallback = t.keys.headD fallback :=
   DTreeMap.minKeyD_eq_headD_keys
 
+theorem minKeyD_eq_getD_keysArray [TransCmp cmp] {fallback} :
+    t.minKeyD fallback = t.keysArray.getD 0 fallback :=
+  DTreeMap.minKeyD_eq_getD_keysArray
+
 theorem minKeyD_modify [TransCmp cmp] {k f}
     (he : (modify t k f).isEmpty = false) {fallback} :
     (modify t k f |>.minKeyD fallback) =
@@ -3494,6 +3635,10 @@ theorem self_le_maxKey?_insertIfNew [TransCmp cmp] {k v kmi} :
     t.maxKey? = t.keys.getLast? :=
   DTreeMap.maxKey?_eq_getLast?_keys
 
+@[grind =_] theorem maxKey?_eq_back?_keysArray [TransCmp cmp] :
+    t.maxKey? = t.keysArray.back? :=
+  DTreeMap.maxKey?_eq_back?_keysArray
+
 @[grind =] theorem maxKey?_modify [TransCmp cmp] {k f} :
     (t.modify k f).maxKey? = t.maxKey?.map fun km => if cmp km k = .eq then k else km :=
   DTreeMap.Const.maxKey?_modify
@@ -3630,6 +3775,10 @@ theorem self_le_maxKey_insertIfNew [TransCmp cmp] {k v} :
     t.maxKey he = t.keys.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) :=
   DTreeMap.maxKey_eq_getLast_keys
 
+@[grind =_] theorem maxKey_eq_back_keysArray [TransCmp cmp] {he} :
+    t.maxKey he = t.keysArray.back (Nat.zero_lt_of_ne_zero (by simpa [size_keysArray, isEmpty_eq_size_eq_zero, - Array.size_eq_zero_iff] using he)) :=
+  DTreeMap.maxKey_eq_back_keysArray
+
 theorem maxKey_modify [TransCmp cmp] {k f he} :
     (modify t k f).maxKey he =
       if cmp (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) k = .eq then
@@ -3765,6 +3914,10 @@ theorem maxKey!_eq_getLast!_keys [TransCmp cmp] [Inhabited α] :
     t.maxKey! = t.keys.getLast! :=
   DTreeMap.maxKey!_eq_getLast!_keys
 
+theorem maxKey!_eq_back!_keysArray [TransCmp cmp] [Inhabited α] :
+    t.maxKey! = t.keysArray.back! :=
+  DTreeMap.maxKey!_eq_back!_keysArray
+
 theorem maxKey!_modify [TransCmp cmp] [Inhabited α] {k f}
     (he : (modify t k f).isEmpty = false) :
     (modify t k f).maxKey! = if cmp t.maxKey! k = .eq then k else t.maxKey! :=
@@ -3892,6 +4045,10 @@ theorem maxKeyD_eq_getLastD_keys [TransCmp cmp] {fallback} :
     t.maxKeyD fallback = t.keys.getLastD fallback :=
   DTreeMap.maxKeyD_eq_getLastD_keys
 
+theorem maxKeyD_eq_getD_back?_keysArray [TransCmp cmp] {fallback} :
+    t.maxKeyD fallback = t.keysArray.back?.getD fallback :=
+  DTreeMap.maxKeyD_eq_getD_back?_keysArray
+
 theorem maxKeyD_modify [TransCmp cmp] {k f}
     (he : (modify t k f).isEmpty = false) {fallback} :
     (modify t k f |>.maxKeyD fallback) =
@@ -4342,24 +4499,46 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty :=
 theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList :=
   equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_toList_perm
 
+theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray :=
+  equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_toArray_perm
+
 theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ :=
   ⟨.of_constToList_perm h⟩
 
+theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ :=
+  ⟨.of_constToArray_perm h⟩
+
 theorem equiv_iff_toList_eq [TransCmp cmp] :
     t₁ ~m t₂ ↔ t₁.toList = t₂.toList :=
   equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_toList_eq
 
+theorem equiv_iff_toArray_eq [TransCmp cmp] :
+    t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray :=
+  equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_toArray_eq
+
 theorem equiv_iff_keys_unit_perm {t₁ t₂ : TreeMap α Unit cmp} :
     t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys :=
   equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_keys_unit_perm
 
+theorem equiv_iff_keysArray_unit_perm {t₁ t₂ : TreeMap α Unit cmp} :
+    t₁ ~m t₂ ↔ t₁.keysArray.Perm t₂.keysArray :=
+  equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_keysArray_unit_perm
+
 theorem equiv_iff_keys_unit_eq [TransCmp cmp] {t₁ t₂ : TreeMap α Unit cmp} :
     t₁ ~m t₂ ↔ t₁.keys = t₂.keys :=
   equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_keys_unit_eq
 
+theorem equiv_iff_keysArray_unit_eq [TransCmp cmp] {t₁ t₂ : TreeMap α Unit cmp} :
+    t₁ ~m t₂ ↔ t₁.keysArray = t₂.keysArray :=
+  equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_keysArray_unit_eq
+
 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 Equiv.of_keysArray_unit_perm {t₁ t₂ : TreeMap α Unit cmp} :
+    t₁.keysArray.Perm t₂.keysArray → t₁ ~m t₂ :=
+  equiv_iff_keysArray_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
@@ -4394,6 +4573,12 @@ theorem toList_filterMap {f : (a : α) → β → Option γ} :
       t.toList.filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) :=
   DTreeMap.Const.toList_filterMap
 
+@[simp, grind =]
+theorem toArray_filterMap {f : α → β → Option γ} :
+    (t.filterMap f).toArray =
+      t.toArray.filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) :=
+  DTreeMap.Const.toArray_filterMap
+
 @[grind =]
 theorem isEmpty_filterMap_iff [TransCmp cmp]
     {f : α → β → Option γ} :
@@ -4561,10 +4746,19 @@ theorem toList_filter {f : α → β → Bool} :
     (t.filter f).toList = t.toList.filter (fun p => f p.1 p.2) :=
   DTreeMap.Const.toList_filter
 
+@[simp, grind =]
+theorem toArray_filter {f : α → β → Bool} :
+    (t.filter f).toArray = t.toArray.filter (fun p => f p.1 p.2) :=
+  DTreeMap.Const.toArray_filter
+
 theorem keys_filter_key {f : α → Bool} :
     (t.filter fun k _ => f k).keys = t.keys.filter f :=
   DTreeMap.keys_filter_key
 
+theorem keysArray_filter_key {f : α → Bool} :
+    (t.filter fun k _ => f k).keysArray = t.keysArray.filter f :=
+  DTreeMap.keysArray_filter_key
+
 @[grind =]
 theorem isEmpty_filter_iff [TransCmp cmp]
     {f : α → β → Bool} :
@@ -4748,10 +4942,19 @@ theorem toList_map {f : α → β → γ} :
     (t.map f).toList = t.toList.map (fun p => (p.1, f p.1 p.2)) :=
   DTreeMap.Const.toList_map
 
+@[simp, grind =]
+theorem toArray_map {f : α → β → γ} :
+    (t.map f).toArray = t.toArray.map (fun p => (p.1, f p.1 p.2)) :=
+  DTreeMap.Const.toArray_map
+
 @[simp, grind =]
 theorem keys_map {f : α → β → γ} : (t.map f).keys = t.keys :=
   DTreeMap.keys_map
 
+@[simp, grind =]
+theorem keysArray_map {f : α → β → γ} : (t.map f).keysArray = t.keysArray :=
+  DTreeMap.keysArray_map
+
 theorem filterMap_equiv_map [TransCmp cmp]
     {f : α → β → γ} :
     (t.filterMap (fun k v => some (f k v))) ~m t.map f :=
@@ -4891,4 +5094,16 @@ theorem getKeyD_map [TransCmp cmp]
 
 end map
 
+theorem toArray_toList : t.toList.toArray = t.toArray :=
+  DTreeMap.Const.toArray_toList
+
+theorem toList_toArray : t.toArray.toList = t.toList :=
+  DTreeMap.Const.toList_toArray
+
+theorem toArray_keys : t.keys.toArray = t.keysArray :=
+  DTreeMap.toArray_keys
+
+theorem toList_keysArray : t.keysArray.toList = t.keys :=
+  DTreeMap.toList_keysArray
+
 end Std.TreeMap

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

@@ -8,6 +8,7 @@ module
 prelude
 import Std.Data.DTreeMap.Raw.Lemmas
 public import Std.Data.TreeMap.Raw.AdditionalOperations
+public import Init.Data.Array.Perm
 import Init.Data.List.Find
 import Init.Data.List.Impl
 import Init.Data.List.Pairwise
@@ -293,10 +294,18 @@ theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF)
     (t.insert k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) :=
   DTreeMap.Raw.Const.toList_insert_perm h
 
+theorem toArray_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (t.insert k v).toArray.Perm ((t.toArray.filter (¬k == ·.1)).push ⟨k, v⟩) :=
+  DTreeMap.Raw.Const.toArray_insert_perm h
+
 theorem keys_insertIfNew_perm {t : Raw α Unit cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} :
     (t.insertIfNew k ()).keys.Perm (if k ∈ t then t.keys else k :: t.keys) :=
   DTreeMap.Raw.keys_insertIfNew_perm h
 
+theorem keysArray_insertIfNew_perm {t : Raw α Unit cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} :
+    (t.insertIfNew k ()).keysArray.Perm (if k ∈ t then t.keysArray else t.keysArray.push k) :=
+  DTreeMap.Raw.keysArray_insertIfNew_perm h
+
 @[simp]
 theorem getElem_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
     (t.insert k v)[k]'(mem_insert_self h) = v :=
@@ -806,25 +815,49 @@ theorem length_keys [TransCmp cmp] (h : t.WF) :
     t.keys.length = t.size :=
   DTreeMap.Raw.length_keys h
 
+@[simp, grind =]
+theorem size_keysArray [TransCmp cmp] (h : t.WF) :
+    t.keysArray.size = t.size :=
+  DTreeMap.Raw.size_keysArray h
+
 @[simp, grind =]
 theorem isEmpty_keys :
     t.keys.isEmpty = t.isEmpty :=
   DTreeMap.Raw.isEmpty_keys
 
+@[simp, grind =]
+theorem isEmpty_keysArray :
+    t.keysArray.isEmpty = t.isEmpty :=
+  DTreeMap.Raw.isEmpty_keysArray
+
 @[simp, grind =]
 theorem contains_keys [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
     t.keys.contains k = t.contains k :=
   DTreeMap.Raw.contains_keys h
 
+@[simp, grind =]
+theorem contains_keysArray [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
+    t.keysArray.contains k = t.contains k :=
+  DTreeMap.Raw.contains_keysArray h
+
 @[simp, grind =]
 theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
     k ∈ t.keys ↔ k ∈ t :=
   DTreeMap.Raw.mem_keys h
 
+@[simp, grind =]
+theorem mem_keysArray [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
+    k ∈ t.keysArray ↔ k ∈ t :=
+  DTreeMap.Raw.mem_keysArray h
+
 theorem mem_of_mem_keys [TransCmp cmp] (h : t.WF) {k : α} :
     k ∈ t.keys → k ∈ t :=
   DTreeMap.Raw.mem_of_mem_keys h
 
+theorem mem_of_mem_keysArray [TransCmp cmp] (h : t.WF) {k : α} :
+    k ∈ t.keysArray → k ∈ t :=
+  DTreeMap.Raw.mem_of_mem_keysArray h
+
 theorem distinct_keys [TransCmp cmp] (h : t.WF) :
     t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) :=
   DTreeMap.Raw.distinct_keys h
@@ -842,46 +875,91 @@ theorem map_fst_toList_eq_keys :
     (toList t).map Prod.fst = t.keys :=
   DTreeMap.Raw.Const.map_fst_toList_eq_keys
 
+@[simp, grind _=_]
+theorem map_fst_toArray_eq_keysArray :
+    (toArray t).map Prod.fst = t.keysArray :=
+  DTreeMap.Raw.Const.map_fst_toArray_eq_keysArray
+
 @[simp, grind =]
 theorem length_toList (h : t.WF) :
     (toList t).length = t.size :=
   DTreeMap.Raw.Const.length_toList h
 
+@[simp, grind =]
+theorem size_toArray (h : t.WF) :
+    (toArray t).size = t.size :=
+  DTreeMap.Raw.Const.size_toArray h
+
 @[simp, grind =]
 theorem isEmpty_toList :
     (toList t).isEmpty = t.isEmpty :=
   DTreeMap.Raw.Const.isEmpty_toList
 
+@[simp, grind =]
+theorem isEmpty_toArray :
+    (toArray t).isEmpty = t.isEmpty :=
+  DTreeMap.Raw.Const.isEmpty_toArray
+
 @[simp, grind =]
 theorem mem_toList_iff_getElem?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β} :
     (k, v) ∈ toList t ↔ t[k]? = some v :=
   DTreeMap.Raw.Const.mem_toList_iff_get?_eq_some h
 
+@[simp, grind =]
+theorem mem_toArray_iff_getElem?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (k, v) ∈ toArray t ↔ t[k]? = some v :=
+  DTreeMap.Raw.Const.mem_toArray_iff_get?_eq_some h
+
 @[simp]
 theorem mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
     (k, v) ∈ toList t ↔ t.getKey? k = some k ∧ t[k]? = some v :=
   DTreeMap.Raw.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some h
 
+@[simp]
+theorem mem_toArray_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] (h : t.WF) {k : α} {v : β} :
+    (k, v) ∈ toArray t ↔ t.getKey? k = some k ∧ t[k]? = some v :=
+  DTreeMap.Raw.Const.mem_toArray_iff_getKey?_eq_some_and_get?_eq_some h
+
 theorem getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList [TransCmp cmp] (h : t.WF) {k : α}
     {v : β} :
     t[k]? = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toList t :=
   DTreeMap.Raw.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList h
 
+theorem getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray [TransCmp cmp] (h : t.WF) {k : α}
+    {v : β} :
+    t[k]? = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toArray t :=
+  DTreeMap.Raw.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray h
+
 theorem find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] (h : t.WF)
     {k k' : α} {v : β} :
     t.toList.find? (cmp ·.1 k == .eq) = some ⟨k', v⟩ ↔
       t.getKey? k = some k' ∧ t[k]? = some v :=
   DTreeMap.Raw.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some h
 
+theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] (h : t.WF)
+    {k k' : α} {v : β} :
+    t.toArray.find? (cmp ·.1 k == .eq) = some ⟨k', v⟩ ↔
+      t.getKey? k = some k' ∧ t[k]? = some v :=
+  DTreeMap.Raw.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some h
+
 theorem find?_toList_eq_none_iff_contains_eq_false [TransCmp cmp] (h : t.WF) {k : α} :
     (toList t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false :=
   DTreeMap.Raw.Const.find?_toList_eq_none_iff_contains_eq_false h
 
+theorem find?_toArray_eq_none_iff_contains_eq_false [TransCmp cmp] (h : t.WF) {k : α} :
+    (toArray t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false :=
+  DTreeMap.Raw.Const.find?_toArray_eq_none_iff_contains_eq_false h
+
 @[simp]
 theorem find?_toList_eq_none_iff_not_mem [TransCmp cmp] (h : t.WF) {k : α} :
     (toList t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t :=
   DTreeMap.Raw.Const.find?_toList_eq_none_iff_not_mem h
 
+@[simp]
+theorem find?_toArray_eq_none_iff_not_mem [TransCmp cmp] (h : t.WF) {k : α} :
+    (toArray t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t :=
+  DTreeMap.Raw.Const.find?_toArray_eq_none_iff_not_mem h
+
 theorem distinct_keys_toList [TransCmp cmp] (h : t.WF) :
     (toList t).Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
   DTreeMap.Raw.Const.distinct_keys_toList h
@@ -898,18 +976,34 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] {f : δ → α → β
     t.foldlM f init = t.toList.foldlM (fun a b => f a b.1 b.2) init :=
   DTreeMap.Raw.Const.foldlM_eq_foldlM_toList
 
+theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ} :
+    t.foldlM f init = t.toArray.foldlM (fun a b => f a b.1 b.2) init :=
+  DTreeMap.Raw.Const.foldlM_eq_foldlM_toArray
+
 theorem foldl_eq_foldl_toList {f : δ → α → β → δ} {init : δ} :
     t.foldl f init = t.toList.foldl (fun a b => f a b.1 b.2) init :=
   DTreeMap.Raw.Const.foldl_eq_foldl_toList
 
+theorem foldl_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} :
+    t.foldl f init = t.toArray.foldl (fun a b => f a b.1 b.2) init :=
+  DTreeMap.Raw.Const.foldl_eq_foldl_toArray
+
 theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} :
     t.foldrM f init = t.toList.foldrM (fun a b => f a.1 a.2 b) init :=
   DTreeMap.Raw.Const.foldrM_eq_foldrM_toList
 
+theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} :
+    t.foldrM f init = t.toArray.foldrM (fun a b => f a.1 a.2 b) init :=
+  DTreeMap.Raw.Const.foldrM_eq_foldrM_toArray
+
 theorem foldr_eq_foldr_toList {f : α → β → δ → δ} {init : δ} :
     t.foldr f init = t.toList.foldr (fun a b => f a.1 a.2 b) init :=
   DTreeMap.Raw.Const.foldr_eq_foldr_toList
 
+theorem foldr_eq_foldr_toArray {f : α → β → δ → δ} {init : δ} :
+    t.foldr f init = t.toArray.foldr (fun a b => f a.1 a.2 b) init :=
+  DTreeMap.Raw.Const.foldr_eq_foldr_toArray
+
 @[simp, grind =]
 theorem forM_eq_forM [Monad m] [LawfulMonad m] {f : α → β → m PUnit} :
     t.forM f = ForM.forM t (fun a => f a.1 a.2) := rfl
@@ -918,6 +1012,10 @@ theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : α × β → m PUnit}
     ForM.forM t f = t.toList.forM f :=
   DTreeMap.Raw.Const.forMUncurried_eq_forM_toList (f := f)
 
+theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : α × β → m PUnit} :
+    ForM.forM t f = t.toArray.forM f :=
+  DTreeMap.Raw.Const.forMUncurried_eq_forM_toArray (f := f)
+
 @[simp, grind =]
 theorem forIn_eq_forIn [Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ} :
     t.forIn f init = ForIn.forIn t init (fun a d => f a.1 a.2 d) := rfl
@@ -927,31 +1025,61 @@ theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m]
     ForIn.forIn t init f = ForIn.forIn t.toList init f :=
   DTreeMap.Raw.Const.forInUncurried_eq_forIn_toList
 
+theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m]
+    {f : α × β → δ → m (ForInStep δ)} {init : δ} :
+    ForIn.forIn t init f = ForIn.forIn t.toArray init f :=
+  DTreeMap.Raw.Const.forInUncurried_eq_forIn_toArray
+
 theorem foldlM_eq_foldlM_keys [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
     t.foldlM (fun d a _ => f d a) init = t.keys.foldlM f init :=
   DTreeMap.Raw.foldlM_eq_foldlM_keys
 
+theorem foldlM_eq_foldlM_keysArray [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
+    t.foldlM (fun d a _ => f d a) init = t.keysArray.foldlM f init :=
+  DTreeMap.Raw.foldlM_eq_foldlM_keysArray
+
 theorem foldl_eq_foldl_keys {f : δ → α → δ} {init : δ} :
     t.foldl (fun d a _ => f d a) init = t.keys.foldl f init :=
   DTreeMap.Raw.foldl_eq_foldl_keys
 
+theorem foldl_eq_foldl_keysArray {f : δ → α → δ} {init : δ} :
+    t.foldl (fun d a _ => f d a) init = t.keysArray.foldl f init :=
+  DTreeMap.Raw.foldl_eq_foldl_keysArray
+
 theorem foldrM_eq_foldrM_keys [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
     t.foldrM (fun a _ d => f a d) init = t.keys.foldrM f init :=
   DTreeMap.Raw.foldrM_eq_foldrM_keys
 
+theorem foldrM_eq_foldrM_keysArray [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
+    t.foldrM (fun a _ d => f a d) init = t.keysArray.foldrM f init :=
+  DTreeMap.Raw.foldrM_eq_foldrM_keysArray
+
 theorem foldr_eq_foldr_keys {f : α → δ → δ} {init : δ} :
     t.foldr (fun a _ d => f a d) init = t.keys.foldr f init :=
   DTreeMap.Raw.foldr_eq_foldr_keys
 
+theorem foldr_eq_foldr_keysArray {f : α → δ → δ} {init : δ} :
+    t.foldr (fun a _ d => f a d) init = t.keysArray.foldr f init :=
+  DTreeMap.Raw.foldr_eq_foldr_keysArray
+
 theorem forM_eq_forM_keys [Monad m] [LawfulMonad m] {f : α → m PUnit} :
     ForM.forM t (fun a => f a.1) = t.keys.forM f :=
   DTreeMap.Raw.forM_eq_forM_keys
 
+theorem forM_eq_forM_keysArray [Monad m] [LawfulMonad m] {f : α → m PUnit} :
+    ForM.forM t (fun a => f a.1) = t.keysArray.forM f :=
+  DTreeMap.Raw.forM_eq_forM_keysArray
+
 theorem forIn_eq_forIn_keys [Monad m] [LawfulMonad m]
     {f : α → δ → m (ForInStep δ)} {init : δ} :
     ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keys init f :=
   DTreeMap.Raw.forIn_eq_forIn_keys
 
+theorem forIn_eq_forIn_keysArray [Monad m] [LawfulMonad m]
+    {f : α → δ → m (ForInStep δ)} {init : δ} :
+    ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keysArray init f :=
+  DTreeMap.Raw.forIn_eq_forIn_keysArray
+
 end monadic
 
 @[simp, grind =]
@@ -2961,6 +3089,10 @@ theorem minKey?_eq_head?_keys [TransCmp cmp] (h : t.WF) :
     t.minKey? = t.keys.head? :=
   DTreeMap.Raw.minKey?_eq_head?_keys h
 
+theorem minKey?_eq_getElem?_keysArray [TransCmp cmp] (h : t.WF) :
+    t.minKey? = t.keysArray[0]? :=
+  DTreeMap.Raw.minKey?_eq_getElem?_keysArray h
+
 @[grind =]
 theorem minKey?_modify [TransCmp cmp] (h : t.WF) {k f} :
     (t.modify k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
@@ -3102,6 +3234,10 @@ theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k
     t.minKey! = t.keys.head! :=
   DTreeMap.Raw.minKey!_eq_head!_keys h
 
+theorem minKey!_eq_getElem!_keysArray [TransCmp cmp] [Inhabited α] (h : t.WF) :
+    t.minKey! = t.keysArray[0]! :=
+  DTreeMap.Raw.minKey!_eq_getElem!_keysArray h
+
 theorem minKey!_modify [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
     (he : (modify t k f).isEmpty = false) :
     (modify t k f).minKey! = if cmp t.minKey! k = .eq then k else t.minKey! :=
@@ -3229,6 +3365,10 @@ theorem minKeyD_eq_headD_keys [TransCmp cmp] (h : t.WF) {fallback} :
     t.minKeyD fallback = t.keys.headD fallback :=
   DTreeMap.Raw.minKeyD_eq_headD_keys h
 
+theorem minKeyD_eq_getD_keysArray [TransCmp cmp] (h : t.WF) {fallback} :
+    t.minKeyD fallback = t.keysArray.getD 0 fallback :=
+  DTreeMap.Raw.minKeyD_eq_getD_keysArray h
+
 theorem minKeyD_modify [TransCmp cmp] (h : t.WF) {k f}
     (he : (modify t k f).isEmpty = false) {fallback} :
     (modify t k f |>.minKeyD fallback) =
@@ -3414,6 +3554,11 @@ theorem self_le_maxKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v kmi} :
     t.maxKey? = t.keys.getLast? :=
   DTreeMap.Raw.maxKey?_eq_getLast?_keys h
 
+@[grind =_]
+theorem maxKey?_eq_back?_keysArray [TransCmp cmp] (h : t.WF) :
+    t.maxKey? = t.keysArray.back? :=
+  DTreeMap.Raw.maxKey?_eq_back?_keysArray h
+
 theorem maxKey?_modify [TransCmp cmp] (h : t.WF) {k f} :
     (t.modify k f).maxKey? = t.maxKey?.map fun km => if cmp km k = .eq then k else km :=
   DTreeMap.Raw.Const.maxKey?_modify h
@@ -3542,6 +3687,10 @@ theorem maxKey!_eq_getLast!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) :
     t.maxKey! = t.keys.getLast! :=
   DTreeMap.Raw.maxKey!_eq_getLast!_keys h
 
+theorem maxKey!_eq_back!_keysArray [TransCmp cmp] [Inhabited α] (h : t.WF) :
+    t.maxKey! = t.keysArray.back! :=
+  DTreeMap.Raw.maxKey!_eq_back!_keysArray h
+
 theorem maxKey!_modify [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
     (he : (modify t k f).isEmpty = false) :
     (modify t k f).maxKey! = if cmp t.maxKey! k = .eq then k else t.maxKey! :=
@@ -3669,6 +3818,10 @@ theorem maxKeyD_eq_getLastD_keys [TransCmp cmp] (h : t.WF) {fallback} :
     t.maxKeyD fallback = t.keys.getLastD fallback :=
   DTreeMap.Raw.maxKeyD_eq_getLastD_keys h
 
+theorem maxKeyD_eq_getD_back?_keysArray [TransCmp cmp] (h : t.WF) {fallback} :
+    t.maxKeyD fallback = t.keysArray.back?.getD fallback :=
+  DTreeMap.Raw.maxKeyD_eq_getD_back?_keysArray h
+
 theorem maxKeyD_modify [TransCmp cmp] (h : t.WF) {k f}
     (he : (modify t k f).isEmpty = false) {fallback} :
     (modify t k f |>.maxKeyD fallback) =
@@ -4087,24 +4240,46 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty :=
 theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList :=
   equiv_iff.trans DTreeMap.Raw.Const.equiv_iff_toList_perm
 
+theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray :=
+  equiv_iff.trans DTreeMap.Raw.Const.equiv_iff_toArray_perm
+
 theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ :=
   ⟨.of_constToList_perm h⟩
 
+theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ :=
+  ⟨.of_constToArray_perm h⟩
+
 theorem equiv_iff_toList_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
     t₁ ~m t₂ ↔ t₁.toList = t₂.toList :=
   equiv_iff.trans (DTreeMap.Raw.Const.equiv_iff_toList_eq h₁.1 h₂.1)
 
+theorem equiv_iff_toArray_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
+    t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray :=
+  equiv_iff.trans (DTreeMap.Raw.Const.equiv_iff_toArray_eq h₁.1 h₂.1)
+
 theorem equiv_iff_keys_unit_perm {t₁ t₂ : Raw α Unit cmp} :
     t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys :=
   equiv_iff.trans DTreeMap.Raw.Const.equiv_iff_keys_unit_perm
 
+theorem equiv_iff_keysArray_unit_perm {t₁ t₂ : Raw α Unit cmp} :
+    t₁ ~m t₂ ↔ t₁.keysArray.Perm t₂.keysArray :=
+  equiv_iff.trans DTreeMap.Raw.Const.equiv_iff_keysArray_unit_perm
+
 theorem equiv_iff_keys_unit_eq {t₁ t₂ : Raw α Unit cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
     t₁ ~m t₂ ↔ t₁.keys = t₂.keys :=
   equiv_iff.trans (DTreeMap.Raw.Const.equiv_iff_keys_unit_eq h₁.1 h₂.1)
 
+theorem equiv_iff_keysArray_unit_eq {t₁ t₂ : Raw α Unit cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
+    t₁ ~m t₂ ↔ t₁.keysArray = t₂.keysArray :=
+  equiv_iff.trans (DTreeMap.Raw.Const.equiv_iff_keysArray_unit_eq h₁.1 h₂.1)
+
 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 Equiv.of_keysArray_unit_perm {t₁ t₂ : Raw α Unit cmp} :
+    t₁.keysArray.Perm t₂.keysArray → t₁ ~m t₂ :=
+  equiv_iff_keysArray_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
@@ -4136,6 +4311,11 @@ theorem toList_filterMap {f : α → β → Option γ} (h : t.WF) :
       (t.toList.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩))) :=
   DTreeMap.Raw.Const.toList_filterMap h
 
+theorem toArray_filterMap {f : α → β → Option γ} (h : t.WF) :
+    (t.filterMap f).toArray =
+      (t.toArray.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩))) :=
+  DTreeMap.Raw.Const.toArray_filterMap h
+
 @[grind =]
 theorem isEmpty_filterMap_iff [TransCmp cmp]
     {f : α → β → Option γ} (h : t.WF) :
@@ -4303,10 +4483,19 @@ theorem toList_filter
     (t.filter f).toList = t.toList.filter (fun p => f p.1 p.2) :=
   DTreeMap.Raw.Const.toList_filter h.out
 
+theorem toArray_filter
+    {f : (a : α) → β → Bool} (h : t.WF) :
+    (t.filter f).toArray = t.toArray.filter (fun p => f p.1 p.2) :=
+  DTreeMap.Raw.Const.toArray_filter h.out
+
 theorem keys_filter_key {f : α → Bool} (h : t.WF) :
     (t.filter fun k _ => f k).keys = t.keys.filter f :=
   DTreeMap.Raw.keys_filter_key h.out
 
+theorem keysArray_filter_key {f : α → Bool} (h : t.WF) :
+    (t.filter fun k _ => f k).keysArray = t.keysArray.filter f :=
+  DTreeMap.Raw.keysArray_filter_key h.out
+
 @[grind =]
 theorem isEmpty_filter_iff [TransCmp cmp]
     {f : α → β → Bool} (h : t.WF) :
@@ -4485,9 +4674,16 @@ theorem toList_map {f : (a : α) → β → γ} :
     (t.map f).toList = t.toList.map (fun p => ⟨p.1, f p.1 p.2⟩) :=
   DTreeMap.Raw.Const.toList_map
 
+theorem toArray_map {f : (a : α) → β → γ} :
+    (t.map f).toArray = t.toArray.map (fun p => ⟨p.1, f p.1 p.2⟩) :=
+  DTreeMap.Raw.Const.toArray_map
+
 theorem keys_map {f : α → β → γ} : (t.map f).keys = t.keys :=
   DTreeMap.Raw.keys_map
 
+theorem keysArray_map {f : α → β → γ} : (t.map f).keysArray = t.keysArray :=
+  DTreeMap.Raw.keysArray_map
+
 theorem filterMap_equiv_map [TransCmp cmp]
     {f : α → β → γ} (h : t.WF) :
     (t.filterMap (fun k v => Option.some (f k v))) ~m (t.map f) :=
@@ -4626,4 +4822,16 @@ theorem getD_map_of_getKey?_eq_some [TransCmp cmp]
 
 end map
 
+theorem toArray_toList : t.toList.toArray = t.toArray :=
+  DTreeMap.Raw.Const.toArray_toList
+
+theorem toList_toArray : t.toArray.toList = t.toList :=
+  DTreeMap.Raw.Const.toList_toArray
+
+theorem toArray_keys : t.keys.toArray = t.keysArray :=
+  DTreeMap.Raw.toArray_keys
+
+theorem toList_keysArray : t.keysArray.toList = t.keys :=
+  DTreeMap.Raw.toList_keysArray
+
 end Std.TreeMap.Raw

src/Std/Data/TreeSet/Lemmas.lean

@@ -8,6 +8,7 @@ module
 prelude
 import Std.Data.TreeMap.Lemmas
 import Std.Data.DTreeMap.Lemmas
+public import Init.Data.Array.Perm
 public import Std.Data.TreeSet.AdditionalOperations
 
 @[expose] public section
@@ -91,6 +92,12 @@ theorem isEmpty_iff_forall_not_mem [TransCmp cmp] :
     t.isEmpty = true ↔ ∀ a, ¬a ∈ t :=
   TreeMap.isEmpty_iff_forall_not_mem
 
+theorem toArray_toList : t.toList.toArray = t.toArray :=
+  TreeMap.toArray_keys
+
+theorem toList_toArray : t.toArray.toList = t.toList :=
+  TreeMap.toList_keysArray
+
 @[simp]
 theorem insert_eq_insert {p : α} : Insert.insert p t = t.insert p :=
   rfl
@@ -286,6 +293,10 @@ theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} :
     (t.insert k).toList.Perm (if k ∈ t then t.toList else k :: t.toList) :=
   DTreeMap.keys_insertIfNew_perm
 
+theorem toArray_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} :
+    (t.insert k).toArray.Perm (if k ∈ t then t.toArray else t.toArray.push k) :=
+  DTreeMap.keysArray_insertIfNew_perm
+
 @[simp, grind =] theorem get_erase [TransCmp cmp] {k a : α} {h'} :
     (t.erase k).get a h' = t.get a (mem_of_mem_erase h') :=
   TreeMap.getKey_erase
@@ -453,25 +464,49 @@ theorem length_toList [TransCmp cmp] :
     t.toList.length = t.size :=
   TreeMap.length_keys
 
+@[simp, grind =]
+theorem size_toArray [TransCmp cmp] :
+    t.toArray.size = t.size := by
+  simp [← toArray_toList, length_toList]
+
 @[simp, grind =]
 theorem isEmpty_toList :
     t.toList.isEmpty = t.isEmpty :=
   TreeMap.isEmpty_keys
 
+@[simp, grind =]
+theorem isEmpty_toArray :
+    t.toArray.isEmpty = t.isEmpty := by
+  simp [← toArray_toList, isEmpty_toList]
+
 @[simp, grind =]
 theorem contains_toList [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} :
     t.toList.contains k = t.contains k :=
   TreeMap.contains_keys
 
+@[simp, grind =]
+theorem contains_toArray [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} :
+    t.toArray.contains k = t.contains k := by
+  simp [← toArray_toList, contains_toList]
+
 @[simp, grind =]
 theorem mem_toList [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
     k ∈ t.toList ↔ k ∈ t :=
   TreeMap.mem_keys
 
+@[simp, grind =]
+theorem mem_toArray [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
+    k ∈ t.toArray ↔ k ∈ t :=
+  TreeMap.mem_keysArray
+
 theorem mem_of_mem_toList [TransCmp cmp] {k : α} :
     k ∈ t.toList → k ∈ t :=
   TreeMap.mem_of_mem_keys
 
+theorem mem_of_mem_toArray [TransCmp cmp] {k : α} :
+    k ∈ t.toArray → k ∈ t := by
+  simpa [← toArray_toList] using mem_of_mem_toList
+
 theorem distinct_toList [TransCmp cmp] :
     t.toList.Pairwise (fun a b => ¬ cmp a b = .eq) :=
   TreeMap.distinct_keys
@@ -948,18 +983,34 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] {f : δ → α → m
     t.foldlM f init = t.toList.foldlM f init :=
   TreeMap.foldlM_eq_foldlM_keys
 
+theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} :
+    t.foldlM f init = t.toArray.foldlM f init := by
+  simp [foldlM_eq_foldlM_toList, ← toArray_toList]
+
 theorem foldl_eq_foldl_toList {f : δ → α → δ} {init : δ} :
     t.foldl f init = t.toList.foldl f init :=
   TreeMap.foldl_eq_foldl_keys
 
+theorem foldl_eq_foldl_toArray {f : δ → α → δ} {init : δ} :
+    t.foldl f init = t.toArray.foldl f init := by
+  simp [foldl_eq_foldl_toList, ← toArray_toList]
+
 theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
     t.foldrM f init = t.toList.foldrM f init :=
   TreeMap.foldrM_eq_foldrM_keys
 
+theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} :
+    t.foldrM f init = t.toArray.foldrM f init := by
+  simp [foldrM_eq_foldrM_toList, ← toArray_toList]
+
 theorem foldr_eq_foldr_toList {f : α → δ → δ} {init : δ} :
     t.foldr f init = t.toList.foldr f init :=
   TreeMap.foldr_eq_foldr_keys
 
+theorem foldr_eq_foldr_toArray {f : α → δ → δ} {init : δ} :
+    t.foldr f init = t.toArray.foldr f init := by
+  simp [foldr_eq_foldr_toList, ← toArray_toList]
+
 @[simp, grind =]
 theorem forM_eq_forM [Monad m] [LawfulMonad m] {f : α → m PUnit} :
     t.forM f = ForM.forM t f := rfl
@@ -968,6 +1019,10 @@ theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : α → m PUnit} :
     ForM.forM t f = t.toList.forM f :=
   TreeMap.forM_eq_forM_keys
 
+theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : α → m PUnit} :
+    ForM.forM t f = t.toArray.forM f :=
+  TreeMap.forM_eq_forM_keysArray
+
 @[simp, grind =]
 theorem forIn_eq_forIn [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} :
     t.forIn f init = ForIn.forIn t init f := rfl
@@ -976,6 +1031,10 @@ theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m] {f : α → δ → m (Fo
     ForIn.forIn t init f = ForIn.forIn t.toList init f :=
   TreeMap.forIn_eq_forIn_keys
 
+theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} :
+    ForIn.forIn t init f = ForIn.forIn t.toArray init f := by
+  simp [forIn_eq_forIn_toList, ← toArray_toList]
+
 end monadic
 
 @[simp, grind =]
@@ -1361,6 +1420,10 @@ theorem min?_le_min?_erase [TransCmp cmp] {k km kme} :
     t.min? = t.toList.head? :=
   TreeMap.minKey?_eq_head?_keys
 
+@[grind =_] theorem min?_eq_getElem?_toArray [TransCmp cmp] :
+    t.min? = t.toArray[0]? :=
+  TreeMap.minKey?_eq_getElem?_keysArray
+
 theorem min_eq_get_min? [TransCmp cmp] {he} :
     t.min he = t.min?.get (isSome_min?_iff_isEmpty_eq_false.mpr he) :=
   TreeMap.minKey_eq_get_minKey?
@@ -1455,6 +1518,10 @@ theorem min_eq_head_toList [TransCmp cmp] {he} :
     t.min he = t.toList.head (List.isEmpty_eq_false_iff.mp <| isEmpty_toList ▸ he) :=
   TreeMap.minKey_eq_head_keys
 
+theorem min_eq_getElem_toArray [TransCmp cmp] {he} :
+   t.min he = t.toArray[0]'(Nat.zero_lt_of_ne_zero (by simpa [isEmpty_eq_size_eq_zero] using he)) :=
+  TreeMap.minKey_eq_getElem_keysArray
+
 theorem min?_eq_some_min! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
     t.min? = some t.min! :=
   TreeMap.minKey?_eq_some_minKey! he
@@ -1547,6 +1614,10 @@ theorem min!_eq_head!_toList [TransCmp cmp] [Inhabited α] :
     t.min! = t.toList.head! :=
   TreeMap.minKey!_eq_head!_keys
 
+theorem min!_eq_getElem!_toArray [TransCmp cmp] [Inhabited α] :
+    t.min! = t.toArray[0]! :=
+  TreeMap.minKey!_eq_getElem!_keysArray
+
 theorem min?_eq_some_minD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
     t.min? = some (t.minD fallback) :=
   TreeMap.minKey?_eq_some_minKeyD he
@@ -1635,6 +1706,10 @@ theorem minD_eq_headD_toList [TransCmp cmp] {fallback} :
     t.minD fallback = t.toList.headD fallback :=
   TreeMap.minKeyD_eq_headD_keys
 
+theorem minD_eq_getD_toArray [TransCmp cmp] {fallback} :
+    t.minD fallback = t.toArray.getD 0 fallback :=
+  TreeMap.minKeyD_eq_getD_keysArray
+
 end Min
 
 section Max
@@ -1769,6 +1844,10 @@ theorem max?_eq_getLast?_toList [TransCmp cmp] :
     t.max? = t.toList.getLast? :=
   TreeMap.maxKey?_eq_getLast?_keys
 
+theorem max?_eq_back?_toArray [TransCmp cmp] :
+    t.max? = t.toArray.back? := by
+  rw [max?_eq_getLast?_toList, ← Array.getLast?_toList, toList_toArray]
+
 theorem max_eq_get_max? [TransCmp cmp] {he} :
     t.max he = t.max?.get (isSome_max?_iff_isEmpty_eq_false.mpr he) :=
   TreeMap.maxKey_eq_get_maxKey?
@@ -1864,6 +1943,11 @@ theorem max_eq_getLast_toList [TransCmp cmp] {he} :
     t.max he = t.toList.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_toList ▸ he) :=
   TreeMap.maxKey_eq_getLast_keys
 
+@[grind =_]
+theorem max_eq_back_toArray [TransCmp cmp] {he} :
+    t.max he = t.toArray.back (Nat.zero_lt_of_ne_zero (by simpa [isEmpty_eq_size_eq_zero] using he)) := by
+  exact TreeMap.maxKey_eq_back_keysArray
+
 theorem max?_eq_some_max! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
     t.max? = some t.max! :=
   TreeMap.maxKey?_eq_some_maxKey! he
@@ -1957,6 +2041,11 @@ theorem max!_eq_getLast!_toList [TransCmp cmp] [Inhabited α] :
     t.max! = t.toList.getLast! :=
   TreeMap.maxKey!_eq_getLast!_keys
 
+@[grind =_]
+theorem max!_eq_back!_toArray [TransCmp cmp] [Inhabited α] :
+    t.max! = t.toArray.back! := by
+  rw [max!_eq_getLast!_toList, ← Array.getLast!_toList, toList_toArray]
+
 theorem max?_eq_some_maxD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
     t.max? = some (t.maxD fallback) :=
   TreeMap.maxKey?_eq_some_maxKeyD he
@@ -2045,6 +2134,10 @@ theorem maxD_eq_getLastD_toList [TransCmp cmp] {fallback} :
     t.maxD fallback = t.toList.getLastD fallback :=
   TreeMap.maxKeyD_eq_getLastD_keys
 
+theorem maxD_eq_getD_back?_toArray [TransCmp cmp] {fallback} :
+    t.maxD fallback = t.toArray.back?.getD fallback :=
+  TreeMap.maxKeyD_eq_getD_back?_keysArray
+
 end Max
 
 namespace Equiv
@@ -2298,6 +2391,9 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty :=
 theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList :=
   equiv_iff_equiv.trans TreeMap.equiv_iff_keys_unit_perm
 
+theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray :=
+  equiv_iff_equiv.trans TreeMap.equiv_iff_keysArray_unit_perm
+
 theorem equiv_iff_forall_mem_iff [TransCmp cmp] [LawfulEqCmp cmp] :
     t₁ ~m t₂ ↔ (∀ k, k ∈ t₁ ↔ k ∈ t₂) :=
   ⟨fun h _ => h.mem_iff, Equiv.of_forall_mem_iff⟩
@@ -2305,10 +2401,17 @@ theorem equiv_iff_forall_mem_iff [TransCmp cmp] [LawfulEqCmp cmp] :
 theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ :=
   ⟨.of_keys_unit_perm h⟩
 
+theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ :=
+  ⟨.of_keysArray_unit_perm h⟩
+
 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 equiv_iff_toArray_eq [TransCmp cmp] :
+    t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray :=
+  equiv_iff_equiv.trans TreeMap.equiv_iff_keysArray_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
@@ -2330,6 +2433,10 @@ theorem toList_filter {f : α → Bool} :
     (t.filter f).toList = t.toList.filter f :=
   TreeMap.keys_filter_key
 
+theorem toArray_filter {f : α → Bool} :
+    (t.filter f).toArray = t.toArray.filter f :=
+  TreeMap.keysArray_filter_key
+
 @[grind =] theorem isEmpty_filter_iff [TransCmp cmp]
     {f : α → Bool} :
     (t.filter f).isEmpty ↔ ∀ k h, f (t.get k h) = false :=

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

@@ -10,6 +10,7 @@ import Std.Data.TreeMap.Raw.Lemmas
 import Std.Data.DTreeMap.Raw.Lemmas
 public import Std.Data.TreeSet.Raw.Basic
 public import Init.Data.List.BasicAux
+public import Init.Data.Array.Perm
 public import Init.Data.Order.ClassesExtra
 public import Init.Data.Order.Classes
 
@@ -289,6 +290,10 @@ theorem toList_insert_perm {t : Raw α cmp} [BEq α] [TransCmp cmp] [LawfulBEqCm
     (t.insert k).toList.Perm (if k ∈ t then t.toList else k :: t.toList) :=
   TreeMap.Raw.keys_insertIfNew_perm h
 
+theorem toArray_insert_perm {t : Raw α cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} :
+    (t.insert k).toArray.Perm (if k ∈ t then t.toArray else t.toArray.push k) :=
+  TreeMap.Raw.keysArray_insertIfNew_perm h
+
 @[simp, grind =]
 theorem get_erase [TransCmp cmp] (h : t.WF) {k a : α} {h'} :
     (t.erase k).get a h' = t.get a (mem_of_mem_erase h h') :=
@@ -459,25 +464,49 @@ theorem length_toList [TransCmp cmp] (h : t.WF) :
     t.toList.length = t.size :=
   TreeMap.Raw.length_keys h
 
+@[simp, grind =]
+theorem size_toArray [TransCmp cmp] (h : t.WF) :
+    t.toArray.size = t.size :=
+  TreeMap.Raw.size_keysArray h
+
 @[simp, grind =]
 theorem isEmpty_toList :
     t.toList.isEmpty = t.isEmpty :=
   TreeMap.Raw.isEmpty_keys
 
+@[simp, grind =]
+theorem isEmpty_toArray :
+    t.toArray.isEmpty = t.isEmpty :=
+  TreeMap.Raw.isEmpty_keysArray
+
 @[simp, grind =]
 theorem contains_toList [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
     t.toList.contains k = t.contains k :=
   TreeMap.Raw.contains_keys h
 
+@[simp, grind =]
+theorem contains_toArray [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
+    t.toArray.contains k = t.contains k :=
+  TreeMap.Raw.contains_keysArray h
+
 @[simp, grind =]
 theorem mem_toList [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
     k ∈ t.toList ↔ k ∈ t :=
   TreeMap.Raw.mem_keys h
 
+@[simp, grind =]
+theorem mem_toArray [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} :
+    k ∈ t.toArray ↔ k ∈ t :=
+  TreeMap.Raw.mem_keysArray h
+
 theorem mem_of_mem_toList [TransCmp cmp] (h : t.WF) {k : α} :
     k ∈ t.toList → k ∈ t :=
   TreeMap.Raw.mem_of_mem_keys h
 
+theorem mem_of_mem_toArray [TransCmp cmp] (h : t.WF) {k : α} :
+    k ∈ t.toArray → k ∈ t :=
+  TreeMap.Raw.mem_of_mem_keysArray h
+
 theorem distinct_toList [TransCmp cmp] (h : t.WF) :
     t.toList.Pairwise (fun a b => ¬ cmp a b = .eq) :=
   TreeMap.Raw.distinct_keys h
@@ -1005,28 +1034,55 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m]
     t.foldlM f init = t.toList.foldlM f init :=
   TreeMap.Raw.foldlM_eq_foldlM_keys
 
+theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m]
+    {f : δ → α → m δ} {init : δ} :
+    t.foldlM f init = t.toArray.foldlM f init :=
+  TreeMap.Raw.foldlM_eq_foldlM_keysArray
+
 theorem foldl_eq_foldl_toList {f : δ → α → δ} {init : δ} :
     t.foldl f init = t.toList.foldl f init :=
   TreeMap.Raw.foldl_eq_foldl_keys
 
+theorem foldl_eq_foldl_toArray {f : δ → α → δ} {init : δ} :
+    t.foldl f init = t.toArray.foldl f init :=
+  TreeMap.Raw.foldl_eq_foldl_keysArray
+
 theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m]
     {f : α → δ → m δ} {init : δ} :
     t.foldrM f init = t.toList.foldrM f init :=
   TreeMap.Raw.foldrM_eq_foldrM_keys
 
+theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m]
+    {f : α → δ → m δ} {init : δ} :
+    t.foldrM f init = t.toArray.foldrM f init :=
+  TreeMap.Raw.foldrM_eq_foldrM_keysArray
+
 theorem foldr_eq_foldr_toList {f : α → δ → δ} {init : δ} :
     t.foldr f init = t.toList.foldr f init :=
   TreeMap.Raw.foldr_eq_foldr_keys
 
+theorem foldr_eq_foldr_toArray {f : α → δ → δ} {init : δ} :
+    t.foldr f init = t.toArray.foldr f init :=
+  TreeMap.Raw.foldr_eq_foldr_keysArray
+
 theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : α → m PUnit} :
     ForM.forM t f = t.toList.forM f :=
   TreeMap.Raw.forM_eq_forM_keys
 
+theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : α → m PUnit} :
+    ForM.forM t f = t.toArray.forM f :=
+  TreeMap.Raw.forM_eq_forM_keysArray
+
 theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m]
     {f : α → δ → m (ForInStep δ)} {init : δ} :
     ForIn.forIn t init f = ForIn.forIn t.toList init f :=
   TreeMap.Raw.forIn_eq_forIn_keys
 
+theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m]
+    {f : α → δ → m (ForInStep δ)} {init : δ} :
+    ForIn.forIn t init f = ForIn.forIn t.toArray init f :=
+  TreeMap.Raw.forIn_eq_forIn_keysArray
+
 end monadic
 
 @[simp, grind =]
@@ -1413,6 +1469,11 @@ theorem min?_eq_head?_toList [TransCmp cmp] (h : t.WF) :
     t.min? = t.toList.head? :=
   TreeMap.Raw.minKey?_eq_head?_keys h
 
+@[grind =_]
+theorem min?_eq_getElem?_toArray [TransCmp cmp] (h : t.WF) :
+    t.min? = t.toArray[0]? :=
+  TreeMap.Raw.minKey?_eq_getElem?_keysArray h
+
 theorem min?_eq_some_min! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
     t.min? = some t.min! :=
   TreeMap.Raw.minKey?_eq_some_minKey! h he
@@ -1498,6 +1559,11 @@ theorem min!_eq_head!_toList [TransCmp cmp] [Inhabited α] (h : t.WF) :
     t.min! = t.toList.head! :=
   TreeMap.Raw.minKey!_eq_head!_keys h
 
+@[grind =_]
+theorem min!_eq_getElem!_toArray [TransCmp cmp] [Inhabited α] (h : t.WF) :
+    t.min! = t.toArray[0]! :=
+  TreeMap.Raw.minKey!_eq_getElem!_keysArray h
+
 theorem min?_eq_some_minD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
     t.min? = some (t.minD fallback) :=
   TreeMap.Raw.minKey?_eq_some_minKeyD h he
@@ -1587,6 +1653,10 @@ theorem minD_eq_headD_toList [TransCmp cmp] (h : t.WF) {fallback} :
     t.minD fallback = t.toList.headD fallback :=
   TreeMap.Raw.minKeyD_eq_headD_keys h
 
+theorem minD_eq_getD_toArray [TransCmp cmp] (h : t.WF) {fallback} :
+    t.minD fallback = t.toArray.getD 0 fallback :=
+  TreeMap.Raw.minKeyD_eq_getD_keysArray h
+
 end Min
 
 section Max
@@ -1722,6 +1792,10 @@ theorem max?_erase_le_max? [TransCmp cmp] (h : t.WF) {k km kme} :
     t.max? = t.toList.getLast? :=
   TreeMap.Raw.maxKey?_eq_getLast?_keys h
 
+@[grind =_] theorem max?_eq_back?_toArray [TransCmp cmp] (h : t.WF) :
+    t.max? = t.toArray.back? :=
+  TreeMap.Raw.maxKey?_eq_back?_keysArray h
+
 theorem max?_eq_some_max! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
     t.max? = some t.max! :=
   TreeMap.Raw.maxKey?_eq_some_maxKey! h he
@@ -1807,6 +1881,11 @@ theorem max!_eq_getLast!_toList [TransCmp cmp] [Inhabited α] (h : t.WF) :
     t.max! = t.toList.getLast! :=
   TreeMap.Raw.maxKey!_eq_getLast!_keys h
 
+@[grind =_]
+theorem max!_eq_back!_toArray [TransCmp cmp] [Inhabited α] (h : t.WF) :
+    t.max! = t.toArray.back! :=
+  TreeMap.Raw.maxKey!_eq_back!_keysArray h
+
 theorem max?_eq_some_maxD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
     t.max? = some (t.maxD fallback) :=
   TreeMap.Raw.maxKey?_eq_some_maxKeyD h he
@@ -1896,6 +1975,11 @@ theorem maxD_eq_getLastD_toList [TransCmp cmp] (h : t.WF) {fallback} :
     t.maxD fallback = t.toList.getLastD fallback :=
   TreeMap.Raw.maxKeyD_eq_getLastD_keys h
 
+@[grind =_]
+theorem maxD_eq_getD_back?_toArray [TransCmp cmp] (h : t.WF) {fallback} :
+    t.maxD fallback = t.toArray.back?.getD fallback :=
+  TreeMap.Raw.maxKeyD_eq_getD_back?_keysArray h
+
 end Max
 
 namespace Equiv
@@ -2139,13 +2223,23 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty :=
 theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList :=
   equiv_iff.trans TreeMap.Raw.equiv_iff_keys_unit_perm
 
+theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray :=
+  equiv_iff.trans TreeMap.Raw.equiv_iff_keysArray_unit_perm
+
 theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ :=
   ⟨.of_keys_unit_perm h⟩
 
+theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ :=
+  ⟨.of_keysArray_unit_perm h⟩
+
 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 equiv_iff_toArray_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
+    t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray :=
+  equiv_iff.trans (TreeMap.Raw.equiv_iff_keysArray_unit_eq h₁.1 h₂.1)
+
 theorem equiv_iff_forall_mem_iff [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) :
     t₁ ~m t₂ ↔ (∀ k, k ∈ t₁ ↔ k ∈ t₂) :=
   ⟨fun h _ => h.mem_iff h₁ h₂, Equiv.of_forall_mem_iff h₁ h₂⟩
@@ -2169,6 +2263,10 @@ theorem toList_filter {f : α → Bool} (h : t.WF) :
     (t.filter f).toList = t.toList.filter f :=
   TreeMap.Raw.keys_filter_key h
 
+theorem toArray_filter {f : α → Bool} (h : t.WF) :
+    (t.filter f).toArray = t.toArray.filter f :=
+  TreeMap.Raw.keysArray_filter_key h
+
 @[grind =] theorem isEmpty_filter_iff [TransCmp cmp]
     {f : α → Bool} (h : t.WF) :
     (t.filter f).isEmpty ↔
@@ -2236,4 +2334,10 @@ theorem get_filter [TransCmp cmp]
 
 end filter
 
+theorem toArray_toList : t.toList.toArray = t.toArray :=
+  TreeMap.Raw.toArray_keys
+
+theorem toList_toArray : t.toArray.toList = t.toList :=
+  TreeMap.Raw.toList_keysArray
+
 end Std.TreeSet.Raw