Lemmas relating operations on well-formed size-bounded trees to operations on lists

This file contains lemmas that relate Impl.toListModel to the queries and operations on Impl. The Impl.Ordered property, being defined in terms of Impl.toListModel, is then shown to be preserved by all of the operations.

However, this file does not contain lemmas that relate operations besides Impl.toListModel to each other or themselves. Such proofs crucially build on top of the lemmas in this file and can be found in Std.Data.Internal.Lemmas.

def Std.DTreeMap.Internal.Impl.instCoeTypeForall_1 {α : Type u} : Coe (Type v) (α → Type v)

toListModel for balancing operations

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_singleL {α : Type u} {β : α → Type v} {k : α} {v : β k} {l : Impl α β} {rk : α} {rv : β rk} {rl rr : Impl α β} : (singleL k v l rk rv rl rr).toListModel = l.toListModel ++ ⟨k, v⟩ :: (rl.toListModel ++ ⟨rk, rv⟩ :: rr.toListModel)

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_singleR {α : Type u} {β : α → Type v} {k : α} {v : β k} {lk : α} {lv : β lk} {ll lr r : Impl α β} : (singleR k v lk lv ll lr r).toListModel = ll.toListModel ++ ⟨lk, lv⟩ :: lr.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_rotateL {α : Type u} {β : α → Type v} {k : α} {v : β k} {l : Impl α β} {rk : α} {rv : β rk} {rl rr : Impl α β} : (rotateL k v l rk rv rl rr).toListModel = l.toListModel ++ ⟨k, v⟩ :: (rl.toListModel ++ ⟨rk, rv⟩ :: rr.toListModel)

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_rotateR {α : Type u} {β : α → Type v} {k : α} {v : β k} {lk : α} {lv : β lk} {ll lr r : Impl α β} : (rotateR k v lk lv ll lr r).toListModel = ll.toListModel ++ ⟨lk, lv⟩ :: lr.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_balanceₘ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} : (balanceₘ k v l r).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_balance {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLErasePrecond l.size r.size ∨ BalanceLErasePrecond r.size l.size} : (balance k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_balanceL {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLPrecond l.size r.size} : (balanceL k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_balanceLErase {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLErasePrecond l.size r.size} : (balanceLErase k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_balanceR {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLPrecond r.size l.size} : (balanceR k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_balanceRErase {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLErasePrecond r.size l.size} : (balanceRErase k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_minView {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} : ⟨(minView k v l r hl hr hlr).k, (minView k v l r hl hr hlr).v⟩ :: (minView k v l r hl hr hlr).tree.impl.toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_maxView {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} : (maxView k v l r hl hr hlr).tree.impl.toListModel ++ [⟨(maxView k v l r hl hr hlr).k, (maxView k v l r hl hr hlr).v⟩] = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_glue {α : Type u} {β : α → Type v} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} {hlr : BalancedAtRoot l.size r.size} : (l.glue r hl hr hlr).toListModel = l.toListModel ++ r.toListModel

@[simp, irreducible]

theorem Std.DTreeMap.Internal.Impl.toListModel_link2 {α : Type u} {β : α → Type v} [Ord α] {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} : (l.link2 r hl hr).impl.toListModel = l.toListModel ++ r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_insertMin {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {t : Impl α β} {h : t.Balanced} : (insertMin k v t h).impl.toListModel = ⟨k, v⟩ :: t.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_insertMax {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {t : Impl α β} {h : t.Balanced} : (insertMax k v t h).impl.toListModel = t.toListModel ++ [⟨k, v⟩]

@[simp, irreducible]

theorem Std.DTreeMap.Internal.Impl.toListModel_link {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {l r : Impl α β} {hl : l.Balanced} {hr : r.Balanced} : (link k v l r hl hr).impl.toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

Verification of model functions

theorem Std.DTreeMap.Internal.Impl.toListModel_filter_gt_of_gt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.gt) (ho : (inner sz k' v' l r).Ordered) : List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) (inner sz k' v' l r).toListModel = l.toListModel ++ ⟨k', v'⟩ :: List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) r.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_filter_gt_of_eq {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.eq) (ho : (inner sz k' v' l r).Ordered) : List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) (inner sz k' v' l r).toListModel = l.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_filter_gt_of_lt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.lt) (ho : (inner sz k' v' l r).Ordered) : List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) (inner sz k' v' l r).toListModel = List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) l.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_find?_of_gt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.gt) (ho : (inner sz k' v' l r).Ordered) : List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) (inner sz k' v' l r).toListModel = List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) r.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_find?_of_eq {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.eq) (ho : (inner sz k' v' l r).Ordered) : List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) (inner sz k' v' l r).toListModel = some ⟨k', v'⟩

theorem Std.DTreeMap.Internal.Impl.toListModel_find?_of_lt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.lt) (ho : (inner sz k' v' l r).Ordered) : List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) (inner sz k' v' l r).toListModel = List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) l.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_gt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.gt) (ho : (inner sz k' v' l r).Ordered) : List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) (inner sz k' v' l r).toListModel = List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) r.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_eq {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.eq) (ho : (inner sz k' v' l r).Ordered) : List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) (inner sz k' v' l r).toListModel = r.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_lt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.lt) (ho : (inner sz k' v' l r).Ordered) : List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) (inner sz k' v' l r).toListModel = List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) l.toListModel ++ ⟨k', v'⟩ :: r.toListModel

theorem Std.DTreeMap.Internal.Impl.findCell_of_gt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.gt) (ho : (inner sz k' v' l r).Ordered) : List.findCell (inner sz k' v' l r).toListModel k = List.findCell r.toListModel k

theorem Std.DTreeMap.Internal.Impl.findCell_of_eq {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.eq) (ho : (inner sz k' v' l r).Ordered) : List.findCell (inner sz k' v' l r).toListModel k = Cell.ofEq k' v' ⋯

theorem Std.DTreeMap.Internal.Impl.findCell_of_lt {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsCut compare k] {sz : Nat} {k' : α} {v' : β k'} {l r : Impl α β} (hcmp : k k' = Ordering.lt) (ho : (inner sz k' v' l r).Ordered) : List.findCell (inner sz k' v' l r).toListModel k = List.findCell l.toListModel k

theorem Std.DTreeMap.Internal.Impl.toListModel_updateCell {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {f : Cell α β (compare k) → Cell α β (compare k)} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (updateCell k f l hlb).impl.toListModel = List.filter (fun (x : (a : α) × β a) => compare k x.fst == Ordering.gt) l.toListModel ++ (f (List.findCell l.toListModel (compare k))).inner.toList ++ List.filter (fun (x : (a : α) × β a) => compare k x.fst == Ordering.lt) l.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_eq_append {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α → Ordering) [Internal.IsStrictCut compare k] {l : Impl α β} (ho : l.Ordered) : l.toListModel = List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) l.toListModel ++ (List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) l.toListModel).toList ++ List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) l.toListModel

theorem Std.DTreeMap.Internal.Impl.ordered_updateCell {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {f : Cell α β (compare k) → Cell α β (compare k)} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (updateCell k f l hlb).impl.Ordered

Connecting the tree maps machinery to the hash map machinery

theorem Std.DTreeMap.Internal.Impl.exists_cell_of_updateCell {α : Type u} {β : α → Type v} [BEq α] [Ord α] [TransOrd α] [LawfulBEqOrd α] (l : Impl α β) (hlb : l.Balanced) (hlo : l.Ordered) (k : α) (f : Cell α β (compare k) → Cell α β (compare k)) : ∃ (l' : List ((a : α) × β a)), l.toListModel.Perm ((List.find? (fun (x : (a : α) × β a) => compare k x.fst == Ordering.eq) l.toListModel).toList ++ l') ∧ (updateCell k f l hlb).impl.toListModel.Perm ((f (List.findCell l.toListModel (compare k))).inner.toList ++ l') ∧ Internal.List.containsKey k l' = false

theorem Std.DTreeMap.Internal.Impl.Ordered.distinctKeys {α : Type u} {β : α → Type v} [BEq α] [Ord α] [LawfulBEqOrd α] {l : Impl α β} (h : l.Ordered) : Internal.List.DistinctKeys l.toListModel

theorem Std.DTreeMap.Internal.Impl.toListModel_updateCell_perm {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) {k : α} {f : Cell α β (compare k) → Cell α β (compare k)} {g : List ((a : α) × β a) → List ((a : α) × β a)} (hfg : ∀ {c : Cell α β (compare k)}, (f c).inner.toList = g c.inner.toList) (hg₁ : ∀ {l l' : List ((a : α) × β a)}, Internal.List.DistinctKeys l → l.Perm l' → (g l).Perm (g l')) (hg₂ : ∀ {l l' : List ((a : α) × β a)}, Internal.List.containsKey k l' = false → g (l ++ l') = g l ++ l') : (updateCell k f l hlb).impl.toListModel.Perm (g l.toListModel)

This is the general theorem to show that modification operations are correct.

theorem Std.DTreeMap.Internal.Impl.contains_findCell {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {l : Impl α β} (hlo : l.Ordered) (h : contains' k l = true) : (List.findCell l.toListModel k).contains = true

theorem Std.DTreeMap.Internal.Impl.applyPartition_eq {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {l : Impl α β} {f : List ((a : α) × β a) → (c : Cell α β k) → (contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ} (hlo : l.Ordered) : applyPartition k l f = f (List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) l.toListModel) (List.findCell l.toListModel k) ⋯ (List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) l.toListModel)

theorem Std.DTreeMap.Internal.Impl.containsKey_toListModel {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : Impl α β} (h : contains' (compare k) l = true) : Internal.List.containsKey k l.toListModel = true

theorem Std.DTreeMap.Internal.Impl.applyPartition_eq_apply_toListModel {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : Impl α β} (hlo : l.Ordered) {f : List ((a : α) × β a) → (c : Cell α β (compare k)) → (contains' (compare k) l = true → c.contains = true) → List ((a : α) × β a) → δ} (g : (ll : List ((a : α) × β a)) → (contains' (compare k) l = true → Internal.List.containsKey k ll = true) → δ) (h : ∀ {ll rr : List ((a : α) × β a)} {c : Cell α β (compare k)} {h₁ : contains' (compare k) l = true → c.contains = true}, List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) (ll ++ c.inner.toList ++ rr) → (∀ (p : (a : α) × β a), p ∈ ll → compare k p.fst = Ordering.gt) → (∀ (p : (a : α) × β a), p ∈ rr → compare k p.fst = Ordering.lt) → f ll c h₁ rr = g (ll ++ c.inner.toList ++ rr) ⋯) : applyPartition (compare k) l f = g l.toListModel ⋯

theorem Std.DTreeMap.Internal.Impl.applyPartition_eq_apply_toListModel' {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] [TransOrd α] {k : α → Ordering} [Internal.IsStrictCut compare k] {l : Impl α β} (hlo : l.Ordered) {f : List ((a : α) × β a) → (c : Cell α β k) → (contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ} (g : List ((a : α) × β a) → δ) (h : ∀ {ll rr : List ((a : α) × β a)} {c : Cell α β k} {h₁ : contains' k l = true → c.contains = true}, List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) (ll ++ c.inner.toList ++ rr) → (∀ (p : (a : α) × β a), p ∈ ll → k p.fst = Ordering.gt) → (∀ (p : (a : α) × β a), p ∈ rr → k p.fst = Ordering.lt) → f ll c h₁ rr = g (ll ++ c.inner.toList ++ rr)) : applyPartition k l f = g l.toListModel

theorem Std.DTreeMap.Internal.Impl.applyCell_eq_apply_toListModel {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : Impl α β} (hlo : l.Ordered) {f : (c : Cell α β (compare k)) → (contains' (compare k) l = true → c.contains = true) → δ} (g : (ll : List ((a : α) × β a)) → (contains' (compare k) l = true → Internal.List.containsKey k ll = true) → δ) (hfg : ∀ (c : Cell α β (compare k)) (hc : contains' (compare k) l = true → c.contains = true), f c hc = g c.inner.toList ⋯) (hg₁ : ∀ (l₁ l₂ : List ((a : α) × β a)) (h : contains' (compare k) l = true → Internal.List.containsKey k l₁ = true), Internal.List.DistinctKeys l₁ → ∀ (hP : l₁.Perm l₂), g l₁ h = g l₂ ⋯) (hg : ∀ (l₁ l₂ : List ((a : α) × β a)) (h : contains' (compare k) l = true → Internal.List.containsKey k (l₁ ++ l₂) = true) (h' : Internal.List.containsKey k l₂ = false), g (l₁ ++ l₂) h = g l₁ ⋯) : applyCell k l f = g l.toListModel ⋯

Verification of access operations

Equiv

theorem Std.DTreeMap.Internal.Impl.equiv_iff_toListModel_perm {α : Type u} {β : α → Type v} {t t' : Impl α β} : t.Equiv t' ↔ t.toListModel.Perm t'.toListModel

theorem Std.DTreeMap.Internal.Impl.Equiv.toListModel_eq {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] {t t' : Impl α β} (h : t.Equiv t') (htb : t.Ordered) (htb' : t'.Ordered) : t.toListModel = t'.toListModel

isEmpty

theorem Std.DTreeMap.Internal.Impl.isEmpty_eq_isEmpty {α : Type u} {β : α → Type v} {t : Impl α β} : t.isEmpty = t.toListModel.isEmpty

size

theorem Std.DTreeMap.Internal.Impl.size_eq_length {α : Type u} {β : α → Type v} (t : Impl α β) (htb : t.Balanced) : t.size = t.toListModel.length

contains

theorem Std.DTreeMap.Internal.Impl.containsₘ_eq_containsKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : Impl α β} (hlo : l.Ordered) : l.containsₘ k = Internal.List.containsKey k l.toListModel

theorem Std.DTreeMap.Internal.Impl.contains_eq_containsKey {α : Type u} {β : α → Type v} [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] {k : α} {l : Impl α β} (hlo : l.Ordered) : contains k l = Internal.List.containsKey k l.toListModel

get?

theorem Std.DTreeMap.Internal.Impl.get?ₘ_eq_getValueCast? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : t.get?ₘ k = Internal.List.getValueCast? k t.toListModel

theorem Std.DTreeMap.Internal.Impl.get?_eq_getValueCast? {α : Type u} {β : α → Type v} [instBEq : BEq α] [Ord α] [i : LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : t.get? k = Internal.List.getValueCast? k t.toListModel

get

theorem Std.DTreeMap.Internal.Impl.contains_eq_isSome_get?ₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : contains k t = (t.get?ₘ k).isSome

theorem Std.DTreeMap.Internal.Impl.getₘ_eq_getValueCast {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (h : Internal.List.containsKey k t.toListModel = true) {h' : (t.get?ₘ k).isSome = true} (hto : t.Ordered) : t.getₘ k h' = Internal.List.getValueCast k t.toListModel h

theorem Std.DTreeMap.Internal.Impl.get_eq_getValueCast {α : Type u} {β : α → Type v} [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β} {h : k ∈ t} (hto : t.Ordered) : t.get k h = Internal.List.getValueCast k t.toListModel ⋯

get!

theorem Std.DTreeMap.Internal.Impl.get!ₘ_eq_getValueCast! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α} [Inhabited (β k)] {t : Impl α β} (hto : t.Ordered) : t.get!ₘ k = Internal.List.getValueCast! k t.toListModel

theorem Std.DTreeMap.Internal.Impl.get!_eq_getValueCast! {α : Type u} {β : α → Type v} [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α} [Inhabited (β k)] {t : Impl α β} (hto : t.Ordered) : t.get! k = Internal.List.getValueCast! k t.toListModel

getD

theorem Std.DTreeMap.Internal.Impl.getDₘ_eq_getValueCastD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {fallback : β k} (hto : t.Ordered) : getDₘ k t fallback = Internal.List.getValueCastD k t.toListModel fallback

theorem Std.DTreeMap.Internal.Impl.getD_eq_getValueCastD {α : Type u} {β : α → Type v} [Ord α] [instBEq : BEq α] [LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β} {fallback : β k} (hto : t.Ordered) : t.getD k fallback = Internal.List.getValueCastD k t.toListModel fallback

getKey?

theorem Std.DTreeMap.Internal.Impl.getKey?ₘ_eq_getKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : t.getKey?ₘ k = Internal.List.getKey? k t.toListModel

theorem Std.DTreeMap.Internal.Impl.getKey?_eq_getKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : t.getKey? k = Internal.List.getKey? k t.toListModel

getKey

theorem Std.DTreeMap.Internal.Impl.contains_eq_isSome_getKey?ₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : contains k t = (t.getKey?ₘ k).isSome

theorem Std.DTreeMap.Internal.Impl.getKeyₘ_eq_getKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (h : Internal.List.containsKey k t.toListModel = true) {h' : (t.getKey?ₘ k).isSome = true} (hto : t.Ordered) : t.getKeyₘ k h' = Internal.List.getKey k t.toListModel h

theorem Std.DTreeMap.Internal.Impl.getKey_eq_getKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {h : contains k t = true} (hto : t.Ordered) : t.getKey k h = Internal.List.getKey k t.toListModel ⋯

getKey!

theorem Std.DTreeMap.Internal.Impl.getKey!ₘ_eq_getKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} [Inhabited α] {t : Impl α β} (hto : t.Ordered) : t.getKey!ₘ k = Internal.List.getKey! k t.toListModel

theorem Std.DTreeMap.Internal.Impl.getKey!_eq_getKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} [Inhabited α] {t : Impl α β} (hto : t.Ordered) : t.getKey! k = Internal.List.getKey! k t.toListModel

getKeyD

theorem Std.DTreeMap.Internal.Impl.getKeyDₘ_eq_getKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {fallback : α} (hto : t.Ordered) : getKeyDₘ k t fallback = Internal.List.getKeyD k t.toListModel fallback

theorem Std.DTreeMap.Internal.Impl.getKeyD_eq_getKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {fallback : α} (hto : t.Ordered) : t.getKeyD k fallback = Internal.List.getKeyD k t.toListModel fallback

getEntry?

theorem Std.DTreeMap.Internal.Impl.getEntry?ₘ_eq_getEntry? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : t.getEntry?ₘ k = Internal.List.getEntry? k t.toListModel

theorem Std.DTreeMap.Internal.Impl.getEntry?_eq_getEntry? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : t.getEntry? k = Internal.List.getEntry? k t.toListModel

getEntry

theorem Std.DTreeMap.Internal.Impl.contains_eq_isSome_getEntry?ₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (hto : t.Ordered) : contains k t = (t.getEntry?ₘ k).isSome

theorem Std.DTreeMap.Internal.Impl.getEntryₘ_eq_getEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (h : Internal.List.containsKey k t.toListModel = true) {h' : (t.getEntry?ₘ k).isSome = true} (hto : t.Ordered) : t.getEntryₘ k h' = Internal.List.getEntry k t.toListModel h

theorem Std.DTreeMap.Internal.Impl.getEntry_eq_getEntry {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {h : k ∈ t} (hto : t.Ordered) : t.getEntry k h = Internal.List.getEntry k t.toListModel ⋯

getEntry!

theorem Std.DTreeMap.Internal.Impl.getEntry!ₘ_eq_getEntry! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited ((a : α) × β a)] {k : α} {t : Impl α β} (hto : t.Ordered) : t.getEntry!ₘ k = Internal.List.getEntry! k t.toListModel

theorem Std.DTreeMap.Internal.Impl.getEntry!_eq_getEntry! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] [Inhabited ((a : α) × β a)] {k : α} {t : Impl α β} (hto : t.Ordered) : t.getEntry! k = Internal.List.getEntry! k t.toListModel

getEntryD

theorem Std.DTreeMap.Internal.Impl.getEntryDₘ_eq_getEntryD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {fallback : (a : α) × β a} (hto : t.Ordered) : getEntryDₘ k t fallback = Internal.List.getEntryD k fallback t.toListModel

theorem Std.DTreeMap.Internal.Impl.getEntryD_eq_getEntryD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {fallback : (a : α) × β a} (hto : t.Ordered) : t.getEntryD k fallback = Internal.List.getEntryD k fallback t.toListModel

get?

theorem Std.DTreeMap.Internal.Impl.Const.get?ₘ_eq_getValue? {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} (hto : t.Ordered) : get?ₘ t k = Internal.List.getValue? k t.toListModel

theorem Std.DTreeMap.Internal.Impl.Const.get?_eq_getValue? {α : Type u} {β : Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} (hto : t.Ordered) : get? t k = Internal.List.getValue? k t.toListModel

get

theorem Std.DTreeMap.Internal.Impl.Const.contains_eq_isSome_get?ₘ {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} (hto : t.Ordered) : contains k t = (get?ₘ t k).isSome

theorem Std.DTreeMap.Internal.Impl.Const.getₘ_eq_getValue {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} (h : Internal.List.containsKey k t.toListModel = true) {h' : (get?ₘ t k).isSome = true} (hto : t.Ordered) : getₘ t k h' = Internal.List.getValue k t.toListModel h

theorem Std.DTreeMap.Internal.Impl.Const.get_eq_getValue {α : Type u} {β : Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} {h : contains k t = true} (hto : t.Ordered) : get t k h = Internal.List.getValue k t.toListModel ⋯

get!

theorem Std.DTreeMap.Internal.Impl.Const.get!ₘ_eq_getValue! {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} [Inhabited β] {t : Impl α fun (x : α) => β} (hto : t.Ordered) : get!ₘ t k = Internal.List.getValue! k t.toListModel

theorem Std.DTreeMap.Internal.Impl.Const.get!_eq_getValue! {α : Type u} {β : Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} [Inhabited β] {t : Impl α fun (x : α) => β} (hto : t.Ordered) : get! t k = Internal.List.getValue! k t.toListModel

getD

theorem Std.DTreeMap.Internal.Impl.Const.getDₘ_eq_getValueD {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} {fallback : β} (hto : t.Ordered) : getDₘ t k fallback = Internal.List.getValueD k t.toListModel fallback

theorem Std.DTreeMap.Internal.Impl.Const.getD_eq_getValueD {α : Type u} {β : Type v} [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α fun (x : α) => β} {fallback : β} (hto : t.Ordered) : getD t k fallback = Internal.List.getValueD k t.toListModel fallback

Verification of modification operations

empty

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_empty {α : Type u} {β : α → Type v} : empty.toListModel = []

theorem Std.DTreeMap.Internal.Impl.ordered_empty {α : Type u} {β : α → Type v} [Ord α] : empty.Ordered

insertₘ

theorem Std.DTreeMap.Internal.Impl.ordered_insertₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insertₘ k v l hlb).Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_insertₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insertₘ k v l hlb).toListModel.Perm (Internal.List.insertEntry k v l.toListModel)

insert

theorem Std.DTreeMap.Internal.Impl.ordered_insert {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insert k v l hlb).impl.Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_insert {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insert k v l hlb).impl.toListModel.Perm (Internal.List.insertEntry k v l.toListModel)

insert!

theorem Std.DTreeMap.Internal.Impl.WF.insert! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.WF) : (Impl.insert! k v l).WF

theorem Std.DTreeMap.Internal.Impl.toListModel_insert! {α : Type u} {β : α → Type v} [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insert! k v l).toListModel.Perm (Internal.List.insertEntry k v l.toListModel)

eraseₘ

theorem Std.DTreeMap.Internal.Impl.ordered_eraseₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (eraseₘ k t htb).Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_eraseₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (eraseₘ k t htb).toListModel.Perm (Internal.List.eraseKey k t.toListModel)

erase

theorem Std.DTreeMap.Internal.Impl.ordered_erase {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (erase k t htb).impl.Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_erase {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (erase k t htb).impl.toListModel.Perm (Internal.List.eraseKey k t.toListModel)

erase!

theorem Std.DTreeMap.Internal.Impl.WF.erase! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {k : α} {l : Impl α β} (h : l.WF) : (Impl.erase! k l).WF

theorem Std.DTreeMap.Internal.Impl.toListModel_erase! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (erase! k l).toListModel.Perm (Internal.List.eraseKey k l.toListModel)

containsThenInsert

theorem Std.DTreeMap.Internal.Impl.size_containsThenInsert_eq_size {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) : containsThenInsert.size t = t.size

theorem Std.DTreeMap.Internal.Impl.containsThenInsert_fst_eq_containsₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] (t : Impl α β) (htb : t.Balanced) (ho : t.Ordered) (a : α) (b : β a) : (containsThenInsert a b t htb).fst = t.containsₘ a

theorem Std.DTreeMap.Internal.Impl.ordered_containsThenInsert {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (containsThenInsert k v t htb).snd.impl.Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_containsThenInsert {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (containsThenInsert k v t htb).snd.impl.toListModel.Perm (Internal.List.insertEntry k v t.toListModel)

containsThenInsert!

theorem Std.DTreeMap.Internal.Impl.WF.containsThenInsert! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {k : α} {v : β k} {t : Impl α β} (h : t.WF) : (Impl.containsThenInsert! k v t).snd.WF

theorem Std.DTreeMap.Internal.Impl.toListModel_containsThenInsert! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (containsThenInsert! k v t).snd.toListModel.Perm (Internal.List.insertEntry k v t.toListModel)

insertIfNew

theorem Std.DTreeMap.Internal.Impl.ordered_insertIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.Balanced) (ho : l.Ordered) : (insertIfNew k v l h).impl.Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_insertIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insertIfNew k v l hlb).impl.toListModel.Perm (Internal.List.insertEntryIfNew k v l.toListModel)

insertIfNew!

theorem Std.DTreeMap.Internal.Impl.ordered_insertIfNew! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.Balanced) (ho : l.Ordered) : (insertIfNew! k v l).Ordered

theorem Std.DTreeMap.Internal.Impl.WF.insertIfNew! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.WF) : (Impl.insertIfNew! k v l).WF

theorem Std.DTreeMap.Internal.Impl.toListModel_insertIfNew! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {l : Impl α β} (hlb : l.Balanced) (hlo : l.Ordered) : (insertIfNew! k v l).toListModel.Perm (Internal.List.insertEntryIfNew k v l.toListModel)

containsThenInsertIfNew

theorem Std.DTreeMap.Internal.Impl.ordered_containsThenInsertIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.Balanced) (ho : l.Ordered) : (containsThenInsertIfNew k v l h).snd.impl.Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_containsThenInsertIfNew {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} {t : Impl α β} (htb : t.Balanced) (hto : t.Ordered) : (containsThenInsertIfNew k v t htb).snd.impl.toListModel.Perm (Internal.List.insertEntryIfNew k v t.toListModel)

containsThenInsertIfNew!

theorem Std.DTreeMap.Internal.Impl.ordered_containsThenInsertIfNew! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.Balanced) (ho : l.Ordered) : (containsThenInsertIfNew! k v l).snd.Ordered

theorem Std.DTreeMap.Internal.Impl.WF.containsThenInsertIfNew! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {k : α} {v : β k} {l : Impl α β} (h : l.WF) : (Impl.containsThenInsertIfNew! k v l).snd.WF

filterMap

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Option (γ a)} : (filterMap f t h).impl.toListModel = List.filterMap (fun (x : (a : α) × β a) => Option.map (fun (x_1 : γ x.fst) => ⟨x.fst, x_1⟩) (f x.fst x.snd)) t.toListModel

theorem Std.DTreeMap.Internal.Impl.balanced_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Option (γ a)} : (filterMap f t h).impl.Balanced

theorem Std.DTreeMap.Internal.Impl.ordered_filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Option (γ a)} (ho : t.Ordered) : (filterMap f t h).impl.Ordered

filter

theorem Std.DTreeMap.Internal.Impl.filter_eq_filterMap {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Bool} : filter f t h = filterMap (fun (k : α) (v : β k) => if f k v = true then some v else none) t h

theorem Std.DTreeMap.Internal.Impl.toListModel_filter {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Bool} : (filter f t h).impl.toListModel = List.filter (fun (e : (a : α) × β a) => f e.fst e.snd) t.toListModel

theorem Std.DTreeMap.Internal.Impl.ordered_filter {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Bool} (hto : t.Ordered) : (filter f t h).impl.Ordered

alter

theorem Std.DTreeMap.Internal.Impl.toListModel_alterₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced) (hto : t.Ordered) : (alterₘ a f t htb).toListModel.Perm (Internal.List.alterKey a f t.toListModel)

theorem Std.DTreeMap.Internal.Impl.alter_eq_alterₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl = alterₘ a f t htb

theorem Std.DTreeMap.Internal.Impl.toListModel_alter {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl.toListModel.Perm (Internal.List.alterKey a f t.toListModel)

theorem Std.DTreeMap.Internal.Impl.ordered_alter {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl.Ordered

alter!

theorem Std.DTreeMap.Internal.Impl.alter_eq_alter! {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced) : (alter a f t htb).impl = alter! a f t

theorem Std.DTreeMap.Internal.Impl.toListModel_alter! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (htb : t.Balanced) (hto : t.Ordered) : (alter! a f t).toListModel.Perm (Internal.List.alterKey a f t.toListModel)

modify

theorem Std.DTreeMap.Internal.Impl.modify_eq_alter {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] {t : Impl α β} {a : α} {f : β a → β a} (htb : t.Balanced) : modify a f t = (alter a (fun (x : Option (β a)) => Option.map f x) t htb).impl

theorem Std.DTreeMap.Internal.Impl.ordered_modify {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] {t : Impl α β} {a : α} {f : β a → β a} (htb : t.Balanced) (hto : t.Ordered) : (modify a f t).Ordered

theorem Std.DTreeMap.Internal.Impl.toListModel_modify {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} {a : α} {f : β a → β a} (htb : t.Balanced) (hto : t.Ordered) : (modify a f t).toListModel.Perm (Internal.List.modifyKey a f t.toListModel)

mergeWith

theorem Std.DTreeMap.Internal.Impl.ordered_mergeWith {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] {t₁ t₂ : Impl α β} {f : (a : α) → β a → β a → β a} (htb : t₁.Balanced) (hto : t₁.Ordered) : (mergeWith f t₁ t₂ htb).impl.Ordered

foldlM

theorem Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM_toListModel {α : Type u} {β : α → Type v} {t : Impl α β} {m : Type u_1 → Type u_2} {δ : Type u_1} [Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ} : foldlM f init t = List.foldlM (fun (acc : δ) (p : (a : α) × β a) => f acc p.fst p.snd) init t.toListModel

theorem Std.DTreeMap.Internal.Impl.foldlM_toListModel_eq_foldlM {α : Type u} {β : α → Type v} {t : Impl α β} {m : Type u_1 → Type u_2} {δ : Type u_1} [Monad m] [LawfulMonad m] {f : δ → (a : α) × β a → m δ} {init : δ} : List.foldlM f init t.toListModel = foldlM (fun (acc : δ) (k : α) (v : β k) => f acc ⟨k, v⟩) init t

foldl

theorem Std.DTreeMap.Internal.Impl.foldl_eq_foldl {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type u_1} {f : δ → (a : α) → β a → δ} {init : δ} : foldl f init t = List.foldl (fun (acc : δ) (p : (a : α) × β a) => f acc p.fst p.snd) init t.toListModel

foldrM

theorem Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM {α : Type u} {β : α → Type v} {t : Impl α β} {m : Type u_1 → Type u_2} {δ : Type u_1} [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} : foldrM f init t = List.foldrM (fun (p : (a : α) × β a) (acc : δ) => f p.fst p.snd acc) init t.toListModel

foldr

theorem Std.DTreeMap.Internal.Impl.foldr_eq_foldr {α : Type u} {β : α → Type v} {t : Impl α β} {δ : Type u_1} {f : (a : α) → β a → δ → δ} {init : δ} : foldr f init t = List.foldr (fun (p : (a : α) × β a) (acc : δ) => f p.fst p.snd acc) init t.toListModel

toList

theorem Std.DTreeMap.Internal.Impl.toList_eq_toListModel {α : Type u} {β : α → Type v} {t : Impl α β} : t.toList = t.toListModel

toArray

theorem Std.DTreeMap.Internal.Impl.toArray_eq_toArray {α : Type u} {β : α → Type v} {t : Impl α β} : t.toArray = t.toListModel.toArray

keys

theorem Std.DTreeMap.Internal.Impl.keys_eq_keys {α : Type u} {β : α → Type v} {t : Impl α β} : t.keys = Internal.List.keys t.toListModel

keysArray

theorem Std.DTreeMap.Internal.Impl.keysArray_eq_toArray_keys {α : Type u} {β : α → Type v} {t : Impl α β} : t.keysArray = (Internal.List.keys t.toListModel).toArray

values

theorem Std.DTreeMap.Internal.Impl.values_eq_map_snd {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} : t.values = List.map (fun (x : (_ : α) × β) => x.snd) t.toListModel

valuesArray

theorem Std.DTreeMap.Internal.Impl.valuesArray_eq_toArray_map {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} : t.valuesArray = (List.map (fun (x : (_ : α) × β) => x.snd) t.toListModel).toArray

forM

theorem Std.DTreeMap.Internal.Impl.forM_eq_forM {α : Type u} {β : α → Type v} {t : Impl α β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → m PUnit} : forM f t = t.toListModel.forM fun (a : (a : α) × β a) => f a.fst a.snd

forIn

theorem Std.DTreeMap.Internal.Impl.forInStep_eq_foldlM {α : Type u} {β : α → Type v} {δ : Type w} {t : Impl α β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ} : forInStep f init t = foldlM (fun (x : ForInStep δ) => match (motive := ForInStep δ → (a : α) → β a → m (ForInStep δ)) x with | ForInStep.yield d => fun (k : α) (v : β k) => f k v d | ForInStep.done d => fun (x : α) (x_1 : β x) => pure (ForInStep.done d)) (ForInStep.yield init) t

theorem Std.DTreeMap.Internal.Impl.forIn_eq_forIn_toListModel {α : Type u} {β : α → Type v} {δ : Type w} {t : Impl α β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ} : forIn f init t = ForIn.forIn t.toListModel init fun (a : (a : α) × β a) (d : δ) => f a.fst a.snd d

getThenInsertIfNew?!

theorem Std.DTreeMap.Internal.Impl.Const.WF.getThenInsertIfNew?! {α : Type u} {β : Type v} [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α} {v : β} {t : Impl α fun (x : α) => β} (h : t.WF) : (Const.getThenInsertIfNew?! t k v).snd.WF

alter

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_alterₘ {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (htb : t.Balanced) (hto : t.Ordered) : (alterₘ a f t htb).toListModel.Perm (Internal.List.Const.alterKey a f t.toListModel)

theorem Std.DTreeMap.Internal.Impl.Const.alter_eq_alterₘ {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl = alterₘ a f t htb

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_alter {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl.toListModel.Perm (Internal.List.Const.alterKey a f t.toListModel)

theorem Std.DTreeMap.Internal.Impl.Const.ordered_alter {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (htb : t.Balanced) (hto : t.Ordered) : (alter a f t htb).impl.Ordered

alter!

theorem Std.DTreeMap.Internal.Impl.Const.alter_eq_alter! {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (htb : t.Balanced) : (alter a f t htb).impl = alter! a f t

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_alter! {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (htb : t.Balanced) (hto : t.Ordered) : (alter! a f t).toListModel.Perm (Internal.List.Const.alterKey a f t.toListModel)

modify

theorem Std.DTreeMap.Internal.Impl.Const.modify_eq_alter {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : β → β} (htb : t.Balanced) : modify a f t = (alter a (fun (x : Option β) => Option.map f x) t htb).impl

theorem Std.DTreeMap.Internal.Impl.Const.ordered_modify {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : β → β} (htb : t.Balanced) (hto : t.Ordered) : (modify a f t).Ordered

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_modify {α : Type u} {β : Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α fun (x : α) => β} {a : α} {f : β → β} (htb : t.Balanced) (hto : t.Ordered) : (modify a f t).toListModel.Perm (Internal.List.Const.modifyKey a f t.toListModel)

mergeWith

theorem Std.DTreeMap.Internal.Impl.Const.ordered_mergeWith {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t₁ t₂ : Impl α fun (x : α) => β} {f : α → β → β → β} (htb : t₁.Balanced) (hto : t₁.Ordered) : (mergeWith f t₁ t₂ htb).impl.Ordered

toList

theorem Std.DTreeMap.Internal.Impl.Const.toList_eq_toListModel_map {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} : toList t = List.map (fun (e : (_ : α) × β) => (e.fst, e.snd)) t.toListModel

toArray

theorem Std.DTreeMap.Internal.Impl.Const.toArray_eq_toArray_map {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} : toArray t = (List.map (fun (e : (_ : α) × β) => (e.fst, e.snd)) t.toListModel).toArray

interSmallerFn

theorem Std.DTreeMap.Internal.Impl.WF.interSmallerFn {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] [BEq α] (m₁ m₂ : Impl α β) (hm₂ : m₂.WF) (k : α) : (m₁.interSmallerFn ⟨m₂, ⋯⟩ k).val.WF

theorem Std.DTreeMap.Internal.Impl.ordered_inter {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {l₁ l₂ : Impl α β} (hlb : l₁.Balanced) (hlo : l₁.Ordered) : (l₁.inter l₂ hlb).Ordered

Deducing that well-formed trees are ordered

theorem Std.DTreeMap.Internal.Impl.WF.ordered {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {l : Impl α β} (h : l.WF) : l.Ordered

Deducing that additional operations are well-formed

inductive Std.DTreeMap.Internal.Impl.SameKeys {α : Type u} {β : α → Type v} {β' : α → Type u_1} : Impl α β → Impl α β' → Prop

Internal implementation detail of the tree map

• leaf {α : Type u} {β : α → Type v} {β' : α → Type u_1} : Impl.leaf.SameKeys Impl.leaf

  Internal implementation detail of the tree map

• inner {α : Type u} {β : α → Type v} {β' : α → Type u_1} (sz : Nat) (k : α) (v : β k) (v' : β' k) (r : Impl α β) (r' : Impl α β') (l : Impl α β) (l' : Impl α β') : r.SameKeys r' → l.SameKeys l' → (Impl.inner sz k v l r).SameKeys (Impl.inner sz k v' l' r')

  Internal implementation detail of the tree map

theorem Std.DTreeMap.Internal.Impl.SameKeys.ordered_iff_pairwise_keys {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} : t.Ordered ↔ List.Pairwise (fun (x1 x2 : α) => compare x1 x2 = Ordering.lt) (List.map (fun (x : (a : α) × β a) => x.fst) t.toListModel)

theorem Std.DTreeMap.Internal.Impl.SameKeys.symm {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Impl α β} {t' : Impl α β'} (hs : t.SameKeys t') : t'.SameKeys t

theorem Std.DTreeMap.Internal.Impl.SameKeys.keys_eq {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Impl α β} {t' : Impl α β'} (h : t.SameKeys t') : List.map (fun (x : (a : α) × β a) => x.fst) t.toListModel = List.map (fun (x : (a : α) × β' a) => x.fst) t'.toListModel

theorem Std.DTreeMap.Internal.Impl.SameKeys.size_eq {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Impl α β} {t' : Impl α β'} (h : t.SameKeys t') : t.size = t'.size

theorem Std.DTreeMap.Internal.Impl.SameKeys.ordered {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Impl α β} {t' : Impl α β'} (hs : t.SameKeys t') (h : t.Ordered) : t'.Ordered

theorem Std.DTreeMap.Internal.Impl.SameKeys.balanced {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Impl α β} {t' : Impl α β'} (hs : t.SameKeys t') (h : t.Balanced) : t'.Balanced

theorem Std.DTreeMap.Internal.Impl.SameKeys.wf {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Impl α β} {t' : Impl α β'} (hs : t.SameKeys t') (h : t.WF) : t'.WF

getThenInsertIfNew?!

theorem Std.DTreeMap.Internal.Impl.WF.getThenInsertIfNew?! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k} {t : Impl α β} (h : t.WF) : (t.getThenInsertIfNew?! k v).snd.WF

theorem Std.DTreeMap.Internal.Impl.WF.constGetThenInsertIfNew?! {α : Type u} {β : Type v} {x✝ : Ord α} [TransOrd α] {k : α} {v : β} {t : Impl α fun (x : α) => β} (h : t.WF) : (Const.getThenInsertIfNew?! t k v).snd.WF

eraseMany!

theorem Std.DTreeMap.Internal.Impl.WF.eraseMany! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {ρ : Type u_1} [ForIn Id ρ α] {l : ρ} {t : Impl α β} (h : t.WF) : (t.eraseMany! l).val.WF

eraseManyEntries

theorem Std.DTreeMap.Internal.Impl.eraseManyEntries!_eq_foldl {α : Type u} {β : α → Type v} {x✝ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} : (t.eraseManyEntries! l).val = List.foldl (fun (acc : Impl α β) (x : (a : α) × β a) => match x with | ⟨k, snd⟩ => erase! k acc) t l

theorem Std.DTreeMap.Internal.Impl.eraseManyEntries_eq_foldl {α : Type u} {β : α → Type v} {x✝ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} (h : t.Balanced) : (t.eraseManyEntries l h).val = List.foldl (fun (acc : Impl α β) (x : (a : α) × β a) => match x with | ⟨k, snd⟩ => erase! k acc) t l

theorem Std.DTreeMap.Internal.Impl.eraseManyEntries_impl_eq_foldl {α : Type u} {β : α → Type v} {x✝ : Ord α} {t₁ : Impl α β} (h₁ : t₁.Balanced) {t₂ : Impl α β} : (t₁.eraseManyEntries t₂ h₁).val = foldl (fun (acc : Impl α β) (k : α) (x : β k) => erase! k acc) t₁ t₂

theorem Std.DTreeMap.Internal.Impl.eraseManyEntries!_impl_eq_foldl {α : Type u} {β : α → Type v} {x✝ : Ord α} {t₁ t₂ : Impl α β} : (t₁.eraseManyEntries! t₂).val = foldl (fun (acc : Impl α β) (k : α) (x : β k) => erase! k acc) t₁ t₂

theorem Std.DTreeMap.Internal.Impl.eraseManyEntries_impl_eq_eraseManyEntries! {α : Type u} {β : α → Type v} {x✝ : Ord α} {t₁ t₂ : Impl α β} (h : t₁.Balanced) : (t₁.eraseManyEntries t₂ h).val = (t₁.eraseManyEntries! t₂).val

theorem Std.DTreeMap.Internal.Impl.eraseManyEntries_impl_perm_eraseList {α : Type u} {β : α → Type v} {x✝ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] {t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} : (t₁.eraseManyEntries t₂ ⋯).val.toListModel.Perm (Internal.List.eraseList t₁.toListModel (List.map (fun (x : (a : α) × β a) => x.fst) t₂.toListModel))

theorem Std.DTreeMap.Internal.Impl.toListModel_eraseManyEntries_impl {α : Type u} {β : α → Type v} {x✝ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] {t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} : (t₁.eraseManyEntries t₂ ⋯).val.toListModel.Perm (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst t₂.toListModel).contains p.fst) t₁.toListModel)

theorem Std.DTreeMap.Internal.Impl.toListModel_eraseManyEntries!_impl {α : Type u} {β : α → Type v} {x✝ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] {t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} : (t₁.eraseManyEntries! t₂).val.toListModel.Perm (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst t₂.toListModel).contains p.fst) t₁.toListModel)

theorem Std.DTreeMap.Internal.Impl.WF.eraseManyEntries! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {ρ : Type u_1} [ForIn Id ρ ((a : α) × β a)] {l : ρ} {t : Impl α β} (h : t.WF) : (t.eraseManyEntries! l).val.WF

insertMany

theorem Std.DTreeMap.Internal.Impl.insertMany!_eq_foldl {α : Type u} {β : α → Type v} {x✝ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} : (t.insertMany! l).val = List.foldl (fun (acc : Impl α β) (x : (a : α) × β a) => match x with | ⟨k, v⟩ => insert! k v acc) t l

theorem Std.DTreeMap.Internal.Impl.insertMany_eq_foldl {α : Type u} {β : α → Type v} {x✝ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} (h : t.Balanced) : (t.insertMany l h).val = List.foldl (fun (acc : Impl α β) (x : (a : α) × β a) => match x with | ⟨k, v⟩ => insert! k v acc) t l

theorem Std.DTreeMap.Internal.Impl.insertMany_eq_foldl_impl {α : Type u} {β : α → Type v} {x✝ : Ord α} {t₁ : Impl α β} (h₁ : t₁.Balanced) {t₂ : Impl α β} : (t₁.insertMany t₂ h₁).val = foldl (fun (acc : Impl α β) (k : α) (v : β k) => insert! k v acc) t₁ t₂

theorem Std.DTreeMap.Internal.Impl.insertMany!_eq_foldl_impl {α : Type u} {β : α → Type v} {x✝ : Ord α} {t₁ t₂ : Impl α β} : (t₁.insertMany! t₂).val = foldl (fun (acc : Impl α β) (k : α) (v : β k) => insert! k v acc) t₁ t₂

theorem Std.DTreeMap.Internal.Impl.insertManyIfNew_eq_foldl {α : Type u} {β : α → Type v} {x✝ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} (h : t.Balanced) : (t.insertManyIfNew l h).val = List.foldl (fun (acc : Impl α β) (x : (a : α) × β a) => match x with | ⟨k, v⟩ => insertIfNew! k v acc) t l

theorem Std.DTreeMap.Internal.Impl.insertManyIfNew!_eq_foldl {α : Type u} {β : α → Type v} {x✝ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} : (t.insertManyIfNew! l).val = List.foldl (fun (acc : Impl α β) (x : (a : α) × β a) => match x with | ⟨k, v⟩ => insertIfNew! k v acc) t l

theorem Std.DTreeMap.Internal.Impl.insertManyIfNew_eq_foldl_impl {α : Type u} {β : α → Type v} {x✝ : Ord α} {t₁ : Impl α β} (h₁ : t₁.Balanced) {t₂ : Impl α β} : (t₁.insertManyIfNew t₂ h₁).val = foldl (fun (acc : Impl α β) (k : α) (v : β k) => insertIfNew! k v acc) t₁ t₂

theorem Std.DTreeMap.Internal.Impl.insertManyIfNew!_eq_foldl_impl {α : Type u} {β : α → Type v} {x✝ : Ord α} {t₁ t₂ : Impl α β} : (t₁.insertManyIfNew! t₂).val = foldl (fun (acc : Impl α β) (k : α) (v : β k) => insertIfNew! k v acc) t₁ t₂

theorem Std.DTreeMap.Internal.Impl.insertMany_eq_insertMany! {α : Type u} {β : α → Type v} {x✝ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} (h : t.Balanced) : (t.insertMany l h).val = (t.insertMany! l).val

theorem Std.DTreeMap.Internal.Impl.insertMany_eq_insertMany!_impl {α : Type u} {β : α → Type v} {x✝ : Ord α} {t₁ t₂ : Impl α β} (h : t₁.Balanced) : (t₁.insertMany t₂ h).val = (t₁.insertMany! t₂).val

theorem Std.DTreeMap.Internal.Impl.insertManyIfNew_eq_insertManyIfNew! {α : Type u} {β : α → Type v} {x✝ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} (h : t.Balanced) : (t.insertMany l h).val = (t.insertMany! l).val

theorem Std.DTreeMap.Internal.Impl.insertManyIfNew_eq_insertManyIfNew!_impl {α : Type u} {β : α → Type v} {x✝ : Ord α} {t₁ t₂ : Impl α β} (h : t₁.Balanced) : (t₁.insertManyIfNew t₂ h).val = (t₁.insertManyIfNew! t₂).val

theorem Std.DTreeMap.Internal.Impl.toListModel_insertMany_list {α : Type u} {β : α → Type v} {x✝ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] {l : List ((a : α) × β a)} {t : Impl α β} (h : t.WF) : (t.insertMany l ⋯).val.toListModel.Perm (Internal.List.insertList t.toListModel l)

theorem Std.DTreeMap.Internal.Impl.toListModel_insertMany_impl {α : Type u} {β : α → Type v} {x✝ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] {t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} : (t₁.insertMany t₂ ⋯).val.toListModel.Perm (Internal.List.insertList t₁.toListModel t₂.toListModel)

theorem Std.DTreeMap.Internal.Impl.toListModel_insertManyIfNew_impl {α : Type u} {β : α → Type v} {x✝ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] {t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} : (t₁.insertManyIfNew t₂ ⋯).val.toListModel.Perm (Internal.List.insertListIfNew t₁.toListModel t₂.toListModel)

theorem Std.DTreeMap.Internal.Impl.toListModel_insertManyIfNew_list {α : Type u} {β : α → Type v} {x✝ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] {l : List ((a : α) × β a)} {t : Impl α β} (h : t.WF) : (t.insertManyIfNew l ⋯).val.toListModel.Perm (Internal.List.insertListIfNew t.toListModel l)

theorem Std.DTreeMap.Internal.Impl.toListModel_union_list {α : Type u} {β : α → Type v} {x✝ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] {t₁ t₂ : Impl α β} (h₁ : t₁.WF) (h₂ : t₂.WF) : (t₁.union t₂ ⋯ ⋯).toListModel.Perm (Internal.List.insertList t₁.toListModel t₂.toListModel)

theorem Std.DTreeMap.Internal.Impl.union_eq_union! {α : Type u} {β : α → Type v} [Ord α] {t₁ t₂ : Impl α β} (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁.union t₂ ⋯ ⋯ = t₁.union! t₂

theorem Std.DTreeMap.Internal.Impl.toListModel_insertMany!_list {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {t : Impl α β} (h : t.WF) : (t.insertMany! l).val.toListModel.Perm (Internal.List.insertList t.toListModel l)

theorem Std.DTreeMap.Internal.Impl.WF.insertMany! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {ρ : Type u_1} [ForIn Id ρ ((a : α) × β a)] {l : ρ} {t : Impl α β} (h : t.WF) : (t.insertMany! l).val.WF

theorem Std.DTreeMap.Internal.Impl.WF.insertManyIfNew! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {ρ : Type u_1} [ForIn Id ρ ((a : α) × β a)] {l : ρ} {t : Impl α β} (h : t.WF) : (t.insertManyIfNew! l).val.WF

theorem Std.DTreeMap.Internal.Impl.WF.union! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} (h₂ : t₂.WF) : (t₁.union! t₂).WF

theorem Std.DTreeMap.Internal.Impl.all_eq_all_toListModel {α : Type u} {β : α → Type v} {p : (a : α) → β a → Bool} {m : Impl α β} : m.all p = m.toListModel.all fun (x : (a : α) × β a) => p x.fst x.snd

theorem Std.DTreeMap.Internal.Impl.beq_eq_beqModel {α : Type u} {β : α → Type v} {x✝ : Ord α} [BEq α] [TransOrd α] [LawfulBEq α] [LawfulBEqOrd α] [(k : α) → BEq (β k)] {m₁ m₂ : Impl α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁.beq m₂ = Internal.List.beqModel m₁.toListModel m₂.toListModel

theorem Std.DTreeMap.Internal.Impl.Const.beq_eq_beqModel {α : Type u} {β : Type v} {x✝ : Ord α} [BEq α] [TransOrd α] [LawfulBEqOrd α] [BEq β] {m₁ m₂ : Impl α fun (x : α) => β} (h₁ : m₁.WF) (h₂ : m₂.WF) : beq m₁ m₂ = Internal.List.Const.beqModel m₁.toListModel m₂.toListModel

theorem Std.DTreeMap.Internal.Impl.WF.constInsertMany! {α : Type u} {β : Type v} {x✝ : Ord α} [TransOrd α] {ρ : Type u_1} [ForIn Id ρ (α × β)] {l : ρ} {t : Impl α fun (x : α) => β} (h : t.WF) : (Const.insertMany! t l).val.WF

theorem Std.DTreeMap.Internal.Impl.WF.constInsertManyIfNewUnit! {α : Type u} {x✝ : Ord α} [TransOrd α] {ρ : Type u_1} [ForIn Id ρ α] {l : ρ} {t : Impl α fun (x : α) => Unit} (h : t.WF) : (Const.insertManyIfNewUnit! t l).val.WF

insertMany

theorem Std.DTreeMap.Internal.Impl.Const.insertMany!_eq_foldl {α : Type u} {β : Type v} {x✝ : Ord α} {l : List (α × β)} {t : Impl α fun (x : α) => β} : (insertMany! t l).val = List.foldl (fun (acc : Impl α fun (x : α) => β) (x : α × β) => match x with | (k, v) => insert! k v acc) t l

theorem Std.DTreeMap.Internal.Impl.Const.insertMany_eq_foldl {α : Type u} {β : Type v} {x✝ : Ord α} {l : List (α × β)} {t : Impl α fun (x : α) => β} (h : t.Balanced) : (insertMany t l h).val = List.foldl (fun (acc : Impl α fun (x : α) => β) (x : α × β) => match x with | (k, v) => insert! k v acc) t l

theorem Std.DTreeMap.Internal.Impl.Const.insertMany_eq_insertMany! {α : Type u} {β : Type v} {x✝ : Ord α} {l : List (α × β)} {t : Impl α fun (x : α) => β} (h : t.Balanced) : (insertMany t l h).val = (insertMany! t l).val

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_insertMany_list {α : Type u} {β : Type v} {x✝ : Ord α} [BEq α] [TransOrd α] [LawfulBEqOrd α] {l : List (α × β)} {t : Impl α fun (x : α) => β} (h : t.WF) : (insertMany t l ⋯).val.toListModel.Perm (Internal.List.insertListConst t.toListModel l)

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_insertMany!_list {α : Type u} {β : Type v} {x✝ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] {l : List (α × β)} {t : Impl α fun (x : α) => β} (h : t.WF) : (insertMany! t l).val.toListModel.Perm (Internal.List.insertListConst t.toListModel l)

theorem Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_eq_foldl {α : Type u} {x✝ : Ord α} {l : List α} {t : Impl α fun (x : α) => Unit} (h : t.Balanced) : (insertManyIfNewUnit t l h).val = List.foldl (fun (acc : Impl α fun (x : α) => Unit) (k : α) => insertIfNew! k () acc) t l

theorem Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit!_eq_foldl {α : Type u} {x✝ : Ord α} {l : List α} {t : Impl α fun (x : α) => Unit} : (insertManyIfNewUnit! t l).val = List.foldl (fun (acc : Impl α fun (x : α) => Unit) (k : α) => insertIfNew! k () acc) t l

theorem Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit_eq_insertManyIfNewUnit! {α : Type u} {x✝ : Ord α} {l : List α} {t : Impl α fun (x : α) => Unit} (h : t.Balanced) : (insertManyIfNewUnit t l h).val = (insertManyIfNewUnit! t l).val

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_insertManyIfNewUnit_list {α : Type u} {x✝ : Ord α} [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {l : List α} {t : Impl α fun (x : α) => Unit} (h : t.WF) : (insertManyIfNewUnit t l ⋯).val.toListModel.Perm (Internal.List.insertListIfNewUnit t.toListModel l)

theorem Std.DTreeMap.Internal.Impl.Const.toListModel_insertManyIfNewUnit!_list {α : Type u} {x✝ : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List α} {t : Impl α fun (x : α) => Unit} (h : t.WF) : (insertManyIfNewUnit! t l).val.toListModel.Perm (Internal.List.insertListIfNewUnit t.toListModel l)

alter!

theorem Std.DTreeMap.Internal.Impl.WF.alter! {α : Type u} {β : α → Type v} {x✝ : Ord α} [LawfulEqOrd α] {t : Impl α β} {a : α} {f : Option (β a) → Option (β a)} (h : t.WF) : (Impl.alter! a f t).WF

theorem Std.DTreeMap.Internal.Impl.WF.constAlter! {α : Type u} {x✝ : Ord α} {β : Type v} {t : Impl α fun (x : α) => β} {a : α} {f : Option β → Option β} (h : t.WF) : (Const.alter! a f t).WF

mergeWith!

theorem Std.DTreeMap.Internal.Impl.mergeWith_eq_mergeWith! {α : Type u} {β : α → Type v} {x✝ : Ord α} [LawfulEqOrd α] {mergeFn : (a : α) → β a → β a → β a} {t₁ t₂ : Impl α β} (h : t₁.Balanced) : (mergeWith mergeFn t₁ t₂ h).impl = mergeWith! mergeFn t₁ t₂

theorem Std.DTreeMap.Internal.Impl.WF.mergeWith! {α : Type u} {β : α → Type v} {x✝ : Ord α} [LawfulEqOrd α] {mergeFn : (a : α) → β a → β a → β a} {t₁ t₂ : Impl α β} (h : t₁.WF) : (Impl.mergeWith! mergeFn t₁ t₂).WF

theorem Std.DTreeMap.Internal.Impl.Const.mergeWith_eq_mergeWith! {α : Type u} {β : Type v} {x✝ : Ord α} {mergeFn : α → β → β → β} {t₁ t₂ : Impl α fun (x : α) => β} (h : t₁.Balanced) : (mergeWith mergeFn t₁ t₂ h).impl = mergeWith! mergeFn t₁ t₂

theorem Std.DTreeMap.Internal.Impl.WF.constMergeWith! {α : Type u} {β : Type v} {x✝ : Ord α} {mergeFn : α → β → β → β} {t₁ t₂ : Impl α fun (x : α) => β} (h : t₁.WF) : (Const.mergeWith! mergeFn t₁ t₂).WF

filterMap

theorem Std.DTreeMap.Internal.Impl.WF.filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Option (γ a)} (hwf : t.WF) : (Impl.filterMap f t h).impl.WF

filterMap!

theorem Std.DTreeMap.Internal.Impl.filterMap_eq_filterMap! {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Option (γ a)} : (filterMap f t h).impl = filterMap! f t

theorem Std.DTreeMap.Internal.Impl.WF.filterMap! {α : Type u} {β : α → Type v} {γ : α → Type w} {x✝ : Ord α} {t : Impl α β} {f : (a : α) → β a → Option (γ a)} (h : t.WF) : (Impl.filterMap! f t).WF

filter!

theorem Std.DTreeMap.Internal.Impl.filter_eq_filter! {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {h : t.Balanced} {f : (a : α) → β a → Bool} : (filter f t h).impl = filter! f t

theorem Std.DTreeMap.Internal.Impl.WF.filter! {α : Type u} {β : α → Type v} {x✝ : Ord α} {t : Impl α β} {f : (a : α) → β a → Bool} (h : t.WF) : (Impl.filter! f t).WF

theorem Std.DTreeMap.Internal.Impl.toListModel_interSmallerFn {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α] (m sofar : Impl α β) (h₁ : m.WF) (h₂ : sofar.WF) (l : List ((a : α) × β a)) (k : α) (hml : sofar.toListModel.Perm l) : (m.interSmallerFn ⟨sofar, ⋯⟩ k).val.toListModel.Perm (Internal.List.interSmallerFn m.toListModel l k)

diff

theorem Std.DTreeMap.Internal.Impl.toListModel_diff {α : Type u} {β : α → Type v} {x✝ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] {t₁ t₂ : Impl α β} (h₁ : t₁.WF) (h₂ : t₂.WF) : (t₁.diff t₂ ⋯).toListModel.Perm (List.filter (fun (p : (a : α) × β a) => !(List.map Sigma.fst t₂.toListModel).contains p.fst) t₁.toListModel)

theorem Std.DTreeMap.Internal.Impl.diff_eq_diff! {α : Type u} {β : α → Type v} [Ord α] {t₁ t₂ : Impl α β} (h₁ : t₁.WF) : t₁.diff t₂ ⋯ = t₁.diff! t₂

theorem Std.DTreeMap.Internal.Impl.WF.diff! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} : (t₁.diff! t₂).WF

interSmaller

theorem Std.DTreeMap.Internal.Impl.toListModel_interSmaller {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α] (m₁ m₂ : Impl α β) (hm₁ : m₁.WF) : (m₁.interSmaller m₂).toListModel.Perm (Internal.List.interSmaller m₁.toListModel m₂.toListModel)

inter

theorem Std.DTreeMap.Internal.Impl.toListModel_inter {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α] (m₁ m₂ : Impl α β) (hm₁ : m₁.WF) (hm₂ : m₂.WF) : (m₁.inter m₂ ⋯).toListModel.Perm (List.filter (fun (p : (a : α) × β a) => Internal.List.containsKey p.fst m₂.toListModel) m₁.toListModel)

inter!

theorem Std.DTreeMap.Internal.Impl.inter_eq_inter! {α : Type u} {β : α → Type v} [Ord α] {l₁ l₂ : Impl α β} {h : l₁.Balanced} : l₁.inter l₂ h = l₁.inter! l₂

theorem Std.DTreeMap.Internal.Impl.toListModel_inter! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α] (m₁ m₂ : Impl α β) (hm₁ : m₁.WF) (hm₂ : m₂.WF) : (m₁.inter! m₂).toListModel.Perm (List.filter (fun (p : (a : α) × β a) => Internal.List.containsKey p.fst m₂.toListModel) m₁.toListModel)

theorem Std.DTreeMap.Internal.Impl.WF.inter! {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {m₁ m₂ : Impl α β} (wh₁ : m₁.WF) : (m₁.inter! m₂).WF

map

theorem Std.DTreeMap.Internal.Impl.toListModel_map {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {f : (a : α) → β a → γ a} : (map f t).toListModel = List.map (fun (x : (a : α) × β a) => ⟨x.fst, f x.fst x.snd⟩) t.toListModel

theorem Std.DTreeMap.Internal.Impl.sameKeys_map {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {f : (a : α) → β a → γ a} : (map f t).SameKeys t

@[simp]

theorem Std.DTreeMap.Internal.Impl.size_map {α : Type u} {β : α → Type v} {γ : α → Type w} {instOrd : Ord α} {t : Impl α β} {f : (a : α) → β a → γ a} : (map f t).size = t.size

theorem Std.DTreeMap.Internal.Impl.WF.map {α : Type u} {β : α → Type v} {γ : α → Type w} [Ord α] {t : Impl α β} {f : (a : α) → β a → γ a} (h : t.WF) : (Impl.map f t).WF

minEntry?

theorem Std.DTreeMap.Internal.Impl.minEntry?ₘ_eq_minEntry? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {l : Impl α β} (hlo : l.Ordered) : l.minEntry?ₘ = Internal.List.minEntry? l.toListModel

theorem Std.DTreeMap.Internal.Impl.minEntry?_eq_minEntry? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {l : Impl α β} (hlo : l.Ordered) : l.minEntry? = Internal.List.minEntry? l.toListModel

theorem Std.DTreeMap.Internal.Impl.minKey?_eq_minKey? {α : Type u} {β : α → Type v} {x✝ : Ord α} [TransOrd α] {l : Impl α β} (hlo : l.Ordered) : l.minKey? = Internal.List.minKey? l.toListModel

theorem Std.DTreeMap.Internal.Impl.minKey_eq_minKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : Impl α β} (hlo : l.Ordered) {he : l.isEmpty = false} : l.minKey he = Internal.List.minKey l.toListModel ⋯

theorem Std.DTreeMap.Internal.Impl.minKey!_eq_minKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α] {l : Impl α β} (hlo : l.Ordered) : l.minKey! = Internal.List.minKey! l.toListModel

theorem Std.DTreeMap.Internal.Impl.minKeyD_eq_minKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : Impl α β} (hlo : l.Ordered) {fallback : α} : l.minKeyD fallback = Internal.List.minKeyD l.toListModel fallback

theorem Std.DTreeMap.Internal.Impl.toListModel_reverse {α : Type u} {β : α → Type v} {l : Impl α β} : l.reverse.toListModel = l.toListModel.reverse

theorem Std.DTreeMap.Internal.Impl.Ordered.reverse {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} (h : t.Ordered) : t.reverse.Ordered

theorem Std.DTreeMap.Internal.Impl.maxEntry?_eq_minEntry? {α : Type u} {β : α → Type v} [o : Ord α] [to : TransOrd α] {t : Impl α β} (hlo : t.Ordered) : t.maxEntry? = Internal.List.minEntry? t.toListModel

theorem Std.DTreeMap.Internal.Impl.maxKey?_eq_maxKey? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} (hlo : t.Ordered) : t.maxKey? = Internal.List.maxKey? t.toListModel

theorem Std.DTreeMap.Internal.Impl.maxKey_eq_maxKey {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} (hlo : t.Ordered) {he : t.isEmpty = false} : t.maxKey he = Internal.List.maxKey t.toListModel ⋯

theorem Std.DTreeMap.Internal.Impl.maxKey!_eq_maxKey! {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} (hlo : t.Ordered) : t.maxKey! = Internal.List.maxKey! t.toListModel

theorem Std.DTreeMap.Internal.Impl.maxKeyD_eq_maxKeyD {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {t : Impl α β} (hlo : t.Ordered) {fallback : α} : t.maxKeyD fallback = Internal.List.maxKeyD t.toListModel fallback

entryAtIdx? / keyAtIdx?

theorem Std.DTreeMap.Internal.Impl.entryAtIdx?_eq_getElem? {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} : t.entryAtIdx? i = t.toListModel[i]?

theorem Std.DTreeMap.Internal.Impl.entryAtIdx_eq_getElem {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} {h : i < t.size} : t.entryAtIdx htb i h = t.toListModel[i]

theorem Std.DTreeMap.Internal.Impl.entryAtIdx!_eq_getElem! {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} [Inhabited ((a : α) × β a)] : t.entryAtIdx! i = t.toListModel[i]!

theorem Std.DTreeMap.Internal.Impl.entryAtIdxD_eq_getD {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} {fallback : (a : α) × β a} : t.entryAtIdxD i fallback = t.toListModel.getD i fallback

theorem Std.DTreeMap.Internal.Impl.keyAtIdx?_eq_getElem? {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} : t.keyAtIdx? i = Option.map (fun (x : (a : α) × β a) => x.fst) t.toListModel[i]?

theorem Std.DTreeMap.Internal.Impl.keyAtIdx_eq_getElem_fst {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} {h : i < t.size} : t.keyAtIdx htb i h = t.toListModel[i].fst

theorem Std.DTreeMap.Internal.Impl.keyAtIdx!_eq_get!_map_getElem? {α : Type u} {β : α → Type v} [Inhabited α] {t : Impl α β} (htb : t.Balanced) {i : Nat} : t.keyAtIdx! i = (Option.map (fun (x : (a : α) × β a) => x.fst) t.toListModel[i]?).get!

theorem Std.DTreeMap.Internal.Impl.keyAtIdxD_eq_getD_map_getElem? {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} {fallback : α} : t.keyAtIdxD i fallback = (Option.map (fun (x : (a : α) × β a) => x.fst) t.toListModel[i]?).getD fallback

theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdx?_eq_getElem? {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} (htb : t.Balanced) {i : Nat} : entryAtIdx? t i = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) t.toListModel[i]?

theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdx_eq_getElem {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} (htb : t.Balanced) {i : Nat} {h : i < t.size} : entryAtIdx t htb i h = (t.toListModel[i].fst, t.toListModel[i].snd)

theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdx!_eq_get!_map_getElem? {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} (htb : t.Balanced) {i : Nat} [Inhabited (α × β)] : entryAtIdx! t i = (Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) t.toListModel[i]?).get!

theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdxD_eq_getD_map_getElem? {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} (htb : t.Balanced) {i : Nat} {fallback : α × β} : entryAtIdxD t i fallback = (Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) t.toListModel[i]?).getD fallback

getEntryLE? / getKeyLE? / ...

theorem Std.DTreeMap.Internal.Impl.getEntryGE?_eq_find? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Ordered) {k : α} : getEntryGE? k t = List.find? (fun (e : (a : α) × β a) => (compare e.fst k).isGE) t.toListModel

theorem Std.DTreeMap.Internal.Impl.getEntryGT?_eq_find? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Ordered) {k : α} : getEntryGT? k t = List.find? (fun (e : (a : α) × β a) => (compare e.fst k).isGT) t.toListModel

theorem Std.DTreeMap.Internal.Impl.getEntryLE?_eq_findRev? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Ordered) {k : α} : getEntryLE? k t = List.findRev? (fun (e : (a : α) × β a) => (compare e.fst k).isLE) t.toListModel

theorem Std.DTreeMap.Internal.Impl.getEntryLT?_eq_findRev? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Impl α β} (hto : t.Ordered) {k : α} : getEntryLT? k t = List.findRev? (fun (e : (a : α) × β a) => (compare e.fst k).isLT) t.toListModel