Model implementations of tree map functions

General infrastructure

def Std.DTreeMap.Internal.Impl.contains' {α : Type u} {β : α → Type v} [Ord α] (k : α → Ordering) (l : Impl α β) : Bool

Internal implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.contains' k Std.DTreeMap.Internal.Impl.leaf = false

theorem Std.DTreeMap.Internal.Impl.contains'_compare {α : Type u} {β : α → Type v} [Ord α] {k : α} {l : Impl α β} : contains' (compare k) l = contains k l

def Std.DTreeMap.Internal.Impl.applyPartition {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] (k : α → Ordering) (l : Impl α β) (f : List ((a : α) × β a) → (c : Cell α β k) → (contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ) : δ

General tree-traversal function. Internal implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.applyPartition k l f = Std.DTreeMap.Internal.Impl.applyPartition.go k l f [] l ⋯ []

def Std.DTreeMap.Internal.Impl.applyPartition.go {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] (k : α → Ordering) (l : Impl α β) (f : List ((a : α) × β a) → (c : Cell α β k) → (contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ) (ll : List ((a : α) × β a)) (m : Impl α β) (hm : contains' k l = true → contains' k m = true) (rr : List ((a : α) × β a)) : δ

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.applyPartition.go k l f ll Std.DTreeMap.Internal.Impl.leaf hm_2 rr = f ll Std.DTreeMap.Internal.Cell.empty ⋯ rr

def Std.DTreeMap.Internal.Impl.applyCell {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] (k : α) (l : Impl α β) (f : (c : Cell α β (compare k)) → (contains' (compare k) l = true → c.contains = true) → δ) : δ

Internal implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.applyCell k Std.DTreeMap.Internal.Impl.leaf f_2 = f_2 Std.DTreeMap.Internal.Cell.empty Std.DTreeMap.Internal.Impl.applyCell._proof_1

theorem Std.DTreeMap.Internal.Impl.applyCell_eq_applyPartition {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] (k : α) (l : Impl α β) (f : (c : Cell α β (compare k)) → (contains' (compare k) l = true → c.contains = true) → δ) : applyCell k l f = applyPartition (compare k) l fun (x : List ((a : α) × β a)) (c : Cell α β (compare k)) (hc : contains' (compare k) l = true → c.contains = true) (x : List ((a : α) × β a)) => f c hc

Internal implementation detail of the tree map

inductive Std.DTreeMap.Internal.Impl.ExplorationStep (α : Type u) (β : α → Type v) [Ord α] (k : α → Ordering) : Type (max u v)

Data structure used by the general tree-traversal function explore. Internal implementation detail of the tree map

• lt {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} (a : α) : k a = Ordering.lt → β a → List ((a : α) × β a) → ExplorationStep α β k

  Needle was less than key at this node: return key-value pair and unexplored right subtree, recursion will continue in left subtree.

• eq {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} : List ((a : α) × β a) → Cell α β k → List ((a : α) × β a) → ExplorationStep α β k

  Needle was equal to key at this node: return key-value pair and both unexplored subtrees, recursion will terminate.

• gt {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} : List ((a : α) × β a) → (a : α) → k a = Ordering.gt → β a → ExplorationStep α β k

  Needle was larger than key at this node: return key-value pair and unexplored left subtree, recursion will containue in right subtree.

def Std.DTreeMap.Internal.Impl.explore {α : Type u} {β : α → Type v} {γ : Type w} [Ord α] (k : α → Ordering) (init : γ) (inner : γ → ExplorationStep α β k → γ) (l : Impl α β) : γ

General tree-traversal function. Internal implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.explore k init inner Std.DTreeMap.Internal.Impl.leaf = inner init (Std.DTreeMap.Internal.Impl.ExplorationStep.eq [] Std.DTreeMap.Internal.Cell.empty [])

theorem Std.DTreeMap.Internal.Impl.applyPartition.go.match_1.congr {α : Sort u} {o o' : Ordering} {lt : o = Ordering.lt → α} {eq : o = Ordering.eq → α} {gt : o = Ordering.gt → α} {lt' : o' = Ordering.lt → α} {eq' : o' = Ordering.eq → α} {gt' : o' = Ordering.gt → α} (ho : o = o') (hlt : ∀ (h : o' = Ordering.lt), lt ⋯ = lt' h) (heq : ∀ (h : o' = Ordering.eq), eq ⋯ = eq' h) (hgt : ∀ (h : o' = Ordering.gt), gt ⋯ = gt' h) : (match h : o with | Ordering.lt => lt h | Ordering.eq => eq h | Ordering.gt => gt h) = match h : o' with | Ordering.lt => lt' h | Ordering.eq => eq' h | Ordering.gt => gt' h

theorem Std.DTreeMap.Internal.Impl.entryAtIdx.match_1.congr {α : Sort u} {o o' : Ordering} {lt : o = Ordering.lt → α} {eq : o = Ordering.eq → α} {gt : o = Ordering.gt → α} {lt' : o' = Ordering.lt → α} {eq' : o' = Ordering.eq → α} {gt' : o' = Ordering.gt → α} (ho : o = o') (hlt : ∀ (h : o' = Ordering.lt), lt ⋯ = lt' h) (heq : ∀ (h : o' = Ordering.eq), eq ⋯ = eq' h) (hgt : ∀ (h : o' = Ordering.gt), gt ⋯ = gt' h) : (match h : o with | Ordering.lt => lt h | Ordering.eq => eq h | Ordering.gt => gt h) = match h : o' with | Ordering.lt => lt' h | Ordering.eq => eq' h | Ordering.gt => gt' h

theorem Std.DTreeMap.Internal.Impl.getEntryLE.match_1.congr {α : Sort u} {o o' : Ordering} {lt : o = Ordering.lt → α} {eq : o = Ordering.eq → α} {gt : o = Ordering.gt → α} {lt' : o' = Ordering.lt → α} {eq' : o' = Ordering.eq → α} {gt' : o' = Ordering.gt → α} (ho : o = o') (hlt : ∀ (h : o' = Ordering.lt), lt ⋯ = lt' h) (heq : ∀ (h : o' = Ordering.eq), eq ⋯ = eq' h) (hgt : ∀ (h : o' = Ordering.gt), gt ⋯ = gt' h) : (match hkky : o with | Ordering.gt => gt hkky | Ordering.eq => eq hkky | Ordering.lt => lt hkky) = match hkky : o' with | Ordering.gt => gt' hkky | Ordering.eq => eq' hkky | Ordering.lt => lt' hkky

theorem Std.DTreeMap.Internal.Impl.get?.match_1.congr {α : Sort u} {o o' : Ordering} {lt : o = Ordering.lt → α} {eq : o = Ordering.eq → α} {gt : o = Ordering.gt → α} {lt' : o' = Ordering.lt → α} {eq' : o' = Ordering.eq → α} {gt' : o' = Ordering.gt → α} (ho : o = o') (hlt : ∀ (h : o' = Ordering.lt), lt ⋯ = lt' h) (heq : ∀ (h : o' = Ordering.eq), eq ⋯ = eq' h) (hgt : ∀ (h : o' = Ordering.gt), gt ⋯ = gt' h) : (match h : o with | Ordering.lt => lt h | Ordering.gt => gt h | Ordering.eq => eq h) = match h : o' with | Ordering.lt => lt' h | Ordering.gt => gt' h | Ordering.eq => eq' h

theorem Std.DTreeMap.Internal.Impl.tree_split_ind_no_gen {α : Type u} {β : α → Type v} [Ord α] (k : α → Ordering) {motive : Impl α β → Prop} (leaf : motive leaf) (lt : ∀ (n : Nat) (ky : α) (y : β ky) (l r : Impl α β), k ky = Ordering.lt → motive l → motive (inner n ky y l r)) (eq : ∀ (n : Nat) (ky : α) (y : β ky) (l r : Impl α β), k ky = Ordering.eq → motive l → motive r → motive (inner n ky y l r)) (gt : ∀ (n : Nat) (ky : α) (y : β ky) (l r : Impl α β), k ky = Ordering.gt → motive r → motive (inner n ky y l r)) (t : Impl α β) : motive t

Induction principle on Impl with an additional case split on k ky for Impl.inner _ ky _ _ _ without generalization.

theorem Std.DTreeMap.Internal.Impl.tree_split_ind {α : Type u} {β : α → Type v} {γ : Sort w} [Ord α] (k : α → Ordering) {motive : Impl α β → γ → Prop} (leaf : ∀ (x : γ), motive leaf x) (lt : ∀ (n : Nat) (ky : α) (y : β ky) (l r : Impl α β), k ky = Ordering.lt → (∀ (x : γ), motive l x) → ∀ (x : γ), motive (inner n ky y l r) x) (eq : ∀ (n : Nat) (ky : α) (y : β ky) (l r : Impl α β), k ky = Ordering.eq → (∀ (x : γ), motive l x) → (∀ (x : γ), motive r x) → ∀ (x : γ), motive (inner n ky y l r) x) (gt : ∀ (n : Nat) (ky : α) (y : β ky) (l r : Impl α β), k ky = Ordering.gt → (∀ (x : γ), motive r x) → ∀ (x : γ), motive (inner n ky y l r) x) (t : Impl α β) (x : γ) : motive t x

Induction principle on Impl with an additional case split on k ky for Impl.inner _ ky _ _ _ and a generalization built in for convenience.

theorem Std.DTreeMap.Internal.Impl.applyPartition_go_step {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] {k : α → Ordering} {init : δ} (l₁ l₂ : List ((a : α) × β a)) (l l' : Impl α β) (h : contains' k l' = true → contains' k l = true) (f : δ → ExplorationStep α β k → δ) : applyPartition.go k l' (fun (l'_1 : List ((a : α) × β a)) (c : Cell α β k) (x : contains' k l' = true → c.contains = true) (r' : List ((a : α) × β a)) => f init (ExplorationStep.eq l'_1 c r')) l₁ l h l₂ = applyPartition.go k l' (fun (l'_1 : List ((a : α) × β a)) (c : Cell α β k) (x : contains' k l' = true → c.contains = true) (r' : List ((a : α) × β a)) => f init (ExplorationStep.eq (l₁ ++ l'_1) c (r' ++ l₂))) [] l h []

theorem Std.DTreeMap.Internal.Impl.explore_eq_applyPartition {α : Type u} {β : α → Type v} {δ : Type w} [Ord α] {k : α → Ordering} (init : δ) (l : Impl α β) (f : δ → ExplorationStep α β k → δ) (hfr : ∀ {k_1 : α} {hk : k k_1 = Ordering.lt} {v : β k_1} {ll : List ((a : α) × β a)} {c : Cell α β k} {rr r : List ((a : α) × β a)} {init : δ}, f (f init (ExplorationStep.lt k_1 hk v r)) (ExplorationStep.eq ll c rr) = f init (ExplorationStep.eq ll c (rr ++ ⟨k_1, v⟩ :: r))) (hfl : ∀ {k_1 : α} {hk : k k_1 = Ordering.gt} {v : β k_1} {ll : List ((a : α) × β a)} {c : Cell α β k} {rr l : List ((a : α) × β a)} {init : δ}, f (f init (ExplorationStep.gt l k_1 hk v)) (ExplorationStep.eq ll c rr) = f init (ExplorationStep.eq (l ++ ⟨k_1, v⟩ :: ll) c rr)) : explore k init f l = applyPartition k l fun (l_1 : List ((a : α) × β a)) (c : Cell α β k) (x : contains' k l = true → c.contains = true) (r : List ((a : α) × β a)) => f init (ExplorationStep.eq l_1 c r)

noncomputable def Std.DTreeMap.Internal.Impl.updateCell {α : Type u} {β : α → Type v} [Ord α] (k : α) (f : Cell α β (compare k) → Cell α β (compare k)) (l : Impl α β) (hl : l.Balanced) : SizedBalancedTree α β (l.size - 1) (l.size + 1)

General "update the mapping for a given key" function. Internal implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.

Model functions

def Std.DTreeMap.Internal.Impl.containsₘ {α : Type u} {β : α → Type v} [Ord α] (l : Impl α β) (k : α) : Bool

Model implementation of the contains function. Internal implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.get?ₘ {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (l : Impl α β) (k : α) : Option (β k)

Model implementation of the get? function. Internal implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.getₘ {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (l : Impl α β) (k : α) (h : (l.get?ₘ k).isSome = true) : β k

Model implementation of the get function. Internal implementation detail of the tree map

Equations

• l.getₘ k h = (l.get?ₘ k).get h

def Std.DTreeMap.Internal.Impl.get!ₘ {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (l : Impl α β) (k : α) [Inhabited (β k)] : β k

Model implementation of the get! function. Internal implementation detail of the tree map

Equations

• l.get!ₘ k = (l.get?ₘ k).get!

def Std.DTreeMap.Internal.Impl.getDₘ {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) (fallback : β k) : β k

Model implementation of the getD function. Internal implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getDₘ k l fallback = (l.get?ₘ k).getD fallback

def Std.DTreeMap.Internal.Impl.getKey?ₘ {α : Type u} {β : α → Type v} [Ord α] (l : Impl α β) (k : α) : Option α

Model implementation of the getKey? function. Internal implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.getKeyₘ {α : Type u} {β : α → Type v} [Ord α] (l : Impl α β) (k : α) (h : (l.getKey?ₘ k).isSome = true) : α

Model implementation of the getKey function. Internal implementation detail of the tree map

Equations

• l.getKeyₘ k h = (l.getKey?ₘ k).get h

def Std.DTreeMap.Internal.Impl.getKey!ₘ {α : Type u} {β : α → Type v} [Ord α] (l : Impl α β) (k : α) [Inhabited α] : α

Model implementation of the getKey! function. Internal implementation detail of the tree map

Equations

• l.getKey!ₘ k = (l.getKey?ₘ k).get!

def Std.DTreeMap.Internal.Impl.getKeyDₘ {α : Type u} {β : α → Type v} [Ord α] (k : α) (l : Impl α β) (fallback : α) : α

Model implementation of the getKeyD function. Internal implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getKeyDₘ k l fallback = (l.getKey?ₘ k).getD fallback

def Std.DTreeMap.Internal.Impl.minEntry?ₘ' {α : Type u} {β : α → Type v} [Ord α] (l : Impl α β) : Option ((a : α) × β a)

Internal implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.minEntry?ₘ {α : Type u} {β : α → Type v} [Ord α] (l : Impl α β) : Option ((a : α) × β a)

Internal implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.reverse {α : Type u} {β : α → Type v} : Impl α β → Impl α β

Internal implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.reverse = Std.DTreeMap.Internal.Impl.leaf
• (Std.DTreeMap.Internal.Impl.inner size k' v l_1 r).reverse = Std.DTreeMap.Internal.Impl.inner size k' v r.reverse l_1.reverse

noncomputable def Std.DTreeMap.Internal.Impl.insertₘ {α : Type u} {β : α → Type v} [Ord α] (k : α) (v : β k) (l : Impl α β) (h : l.Balanced) : Impl α β

Model implementation of the insert function. Internal implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.insertₘ k v l h = (Std.DTreeMap.Internal.Impl.updateCell k (fun (x : Std.DTreeMap.Internal.Cell α β (compare k)) => Std.DTreeMap.Internal.Cell.of k v) l h).impl

noncomputable def Std.DTreeMap.Internal.Impl.eraseₘ {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) (h : t.Balanced) : Impl α β

Model implementation of the erase function. Internal implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.eraseₘ k t h = (Std.DTreeMap.Internal.Impl.updateCell k (fun (x : Std.DTreeMap.Internal.Cell α β (compare k)) => Std.DTreeMap.Internal.Cell.empty) t h).impl

noncomputable def Std.DTreeMap.Internal.Impl.insertIfNewₘ {α : Type u} {β : α → Type v} [Ord α] (k : α) (v : β k) (l : Impl α β) (h : l.Balanced) : Impl α β

Model implementation of the insertIfNew function. Internal implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Std.DTreeMap.Internal.Impl.alterₘ {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (f : Option (β k) → Option (β k)) (t : Impl α β) (h : t.Balanced) : Impl α β

Model implementation of the alter function. Internal implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.alterₘ k f t h = (Std.DTreeMap.Internal.Impl.updateCell k (fun (x : Std.DTreeMap.Internal.Cell α β (compare k)) => Std.DTreeMap.Internal.Cell.alter f x) t h).impl

def Std.DTreeMap.Internal.Impl.Const.get?ₘ {α : Type u} {β : Type v} [Ord α] (l : Impl α fun (x : α) => β) (k : α) : Option β

Model implementation of the get? function. Internal implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.Const.getₘ {α : Type u} {β : Type v} [Ord α] (l : Impl α fun (x : α) => β) (k : α) (h : (get?ₘ l k).isSome = true) : β

Model implementation of the get function. Internal implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getₘ l k h = (Std.DTreeMap.Internal.Impl.Const.get?ₘ l k).get h

def Std.DTreeMap.Internal.Impl.Const.get!ₘ {α : Type u} {β : Type v} [Ord α] (l : Impl α fun (x : α) => β) (k : α) [Inhabited β] : β

Model implementation of the get! function. Internal implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.get!ₘ l k = (Std.DTreeMap.Internal.Impl.Const.get?ₘ l k).get!

def Std.DTreeMap.Internal.Impl.Const.getDₘ {α : Type u} {β : Type v} [Ord α] (l : Impl α fun (x : α) => β) (k : α) (fallback : β) : β

Model implementation of the getD function. Internal implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getDₘ l k fallback = (Std.DTreeMap.Internal.Impl.Const.get?ₘ l k).getD fallback

noncomputable def Std.DTreeMap.Internal.Impl.Const.alterₘ {α : Type u} {β : Type v} [Ord α] [OrientedOrd α] (k : α) (f : Option β → Option β) (t : Impl α fun (x : α) => β) (h : t.Balanced) : Impl α fun (x : α) => β

Model implementation of the alter function. Internal implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.alterₘ k f t h = (Std.DTreeMap.Internal.Impl.updateCell k (Std.DTreeMap.Internal.Cell.Const.alter f) t h).impl

Helper theorems for reasoning with key-value pairs

theorem Std.DTreeMap.Internal.Impl.balanceL!_pair_congr {α : Type u} {β : α → Type v} {k : α} {v : β k} {k' : α} {v' : β k'} (h : ⟨k, v⟩ = ⟨k', v'⟩) {l l' r r' : Impl α β} (hl : l = l') (hr : r = r') : balanceL! k v l r = balanceL! k' v' l' r'

theorem Std.DTreeMap.Internal.Impl.balanceR!_pair_congr {α : Type u} {β : α → Type v} {k : α} {v : β k} {k' : α} {v' : β k'} (h : ⟨k, v⟩ = ⟨k', v'⟩) {l l' r r' : Impl α β} (hl : l = l') (hr : r = r') : balanceR! k v l r = balanceR! k' v' l' r'

Equivalence of function to model functions

theorem Std.DTreeMap.Internal.Impl.contains_eq_containsₘ {α : Type u} {β : α → Type v} [Ord α] (k : α) (l : Impl α β) : contains k l = l.containsₘ k

theorem Std.DTreeMap.Internal.Impl.get?_eq_get?ₘ {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) : l.get? k = l.get?ₘ k

theorem Std.DTreeMap.Internal.Impl.get_eq_get? {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) {h : k ∈ l} : some (l.get k h) = l.get? k

theorem Std.DTreeMap.Internal.Impl.get_eq_getₘ {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) {h : k ∈ l} (h' : (l.get?ₘ k).isSome = true) : l.get k h = l.getₘ k h'

theorem Std.DTreeMap.Internal.Impl.get!_eq_get!ₘ {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) [Inhabited (β k)] (l : Impl α β) : l.get! k = l.get!ₘ k

theorem Std.DTreeMap.Internal.Impl.getD_eq_getDₘ {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] (k : α) (l : Impl α β) (fallback : β k) : l.getD k fallback = getDₘ k l fallback

theorem Std.DTreeMap.Internal.Impl.getKey?_eq_getKey?ₘ {α : Type u} {β : α → Type v} [Ord α] (k : α) (l : Impl α β) : l.getKey? k = l.getKey?ₘ k

theorem Std.DTreeMap.Internal.Impl.getKey_eq_getKey? {α : Type u} {β : α → Type v} [Ord α] (k : α) (l : Impl α β) {h : contains k l = true} : some (l.getKey k h) = l.getKey? k

theorem Std.DTreeMap.Internal.Impl.getKey_eq_getKeyₘ {α : Type u} {β : α → Type v} [Ord α] (k : α) (l : Impl α β) {h : contains k l = true} (h' : (l.getKey?ₘ k).isSome = true) : l.getKey k h = l.getKeyₘ k h'

theorem Std.DTreeMap.Internal.Impl.getKey!_eq_getKey!ₘ {α : Type u} {β : α → Type v} [Ord α] (k : α) [Inhabited α] (l : Impl α β) : l.getKey! k = l.getKey!ₘ k

theorem Std.DTreeMap.Internal.Impl.getKeyD_eq_getKeyDₘ {α : Type u} {β : α → Type v} [Ord α] (k : α) (l : Impl α β) (fallback : α) : l.getKeyD k fallback = getKeyDₘ k l fallback

theorem Std.DTreeMap.Internal.Impl.minEntry?_eq_minEntry?ₘ' {α : Type u} {β : α → Type v} [Ord α] {l : Impl α β} : l.minEntry? = l.minEntry?ₘ'

theorem Std.DTreeMap.Internal.Impl.minEntry?ₘ'_eq_minEntry?ₘ {α : Type u} {β : α → Type v} [Ord α] {l : Impl α β} : l.minEntry?ₘ' = l.minEntry?ₘ

theorem Std.DTreeMap.Internal.Impl.minEntry?_eq_minEntry?ₘ {α : Type u} {β : α → Type v} [Ord α] {l : Impl α β} : l.minEntry? = l.minEntry?ₘ

theorem Std.DTreeMap.Internal.Impl.minEntry!_eq_get!_minEntry? {α : Type u} {β : α → Type v} [Inhabited ((a : α) × β a)] {l : Impl α β} : l.minEntry! = l.minEntry?.get!

theorem Std.DTreeMap.Internal.Impl.minEntryD_eq_getD_minEntry? {α : Type u} {β : α → Type v} {l : Impl α β} {fallback : (a : α) × β a} : l.minEntryD fallback = l.minEntry?.getD fallback

theorem Std.DTreeMap.Internal.Impl.some_minEntry_eq_minEntry? {α : Type u} {β : α → Type v} {l : Impl α β} {he : l.isEmpty = false} : some (l.minEntry he) = l.minEntry?

theorem Std.DTreeMap.Internal.Impl.minEntry_eq_get_minEntry? {α : Type u} {β : α → Type v} {l : Impl α β} {he : l.isEmpty = false} : l.minEntry he = l.minEntry?.get ⋯

theorem Std.DTreeMap.Internal.Impl.maxEntry?_eq_minEntry?_reverse {α : Type u} {β : α → Type v} {l : Impl α β} : l.maxEntry? = l.reverse.minEntry?

theorem Std.DTreeMap.Internal.Impl.maxEntry!_eq_get!_maxEntry? {α : Type u} {β : α → Type v} [Inhabited ((a : α) × β a)] {l : Impl α β} : l.maxEntry! = l.maxEntry?.get!

theorem Std.DTreeMap.Internal.Impl.maxEntryD_eq_getD_maxEntry? {α : Type u} {β : α → Type v} {l : Impl α β} {fallback : (a : α) × β a} : l.maxEntryD fallback = l.maxEntry?.getD fallback

theorem Std.DTreeMap.Internal.Impl.some_maxEntry_eq_maxEntry? {α : Type u} {β : α → Type v} {l : Impl α β} {he : l.isEmpty = false} : some (l.maxEntry he) = l.maxEntry?

theorem Std.DTreeMap.Internal.Impl.minKey?_eq_minEntry?_map_fst {α : Type u} {β : α → Type v} {l : Impl α β} : l.minKey? = Option.map Sigma.fst l.minEntry?

theorem Std.DTreeMap.Internal.Impl.minKey_eq_minEntry_fst {α : Type u} {β : α → Type v} {l : Impl α β} {he : l.isEmpty = false} : l.minKey he = (l.minEntry he).fst

theorem Std.DTreeMap.Internal.Impl.minKey!_eq_get!_minKey? {α : Type u} {β : α → Type v} [Inhabited α] {l : Impl α β} : l.minKey! = l.minKey?.get!

theorem Std.DTreeMap.Internal.Impl.minKeyD_eq_getD_minKey? {α : Type u} {β : α → Type v} {l : Impl α β} {fallback : α} : l.minKeyD fallback = l.minKey?.getD fallback

theorem Std.DTreeMap.Internal.Impl.maxKey?_eq_minKey?_reverse {α : Type u} {β : α → Type v} {l : Impl α β} : l.maxKey? = l.reverse.minKey?

theorem Std.DTreeMap.Internal.Impl.some_maxKey_eq_maxKey? {α : Type u} {β : α → Type v} {l : Impl α β} {he : l.isEmpty = false} : some (l.maxKey he) = l.maxKey?

theorem Std.DTreeMap.Internal.Impl.maxKey_eq_get_maxKey? {α : Type u} {β : α → Type v} {l : Impl α β} {he : l.isEmpty = false} : l.maxKey he = l.maxKey?.get ⋯

theorem Std.DTreeMap.Internal.Impl.maxKey!_eq_get!_maxKey? {α : Type u} {β : α → Type v} [Inhabited α] {l : Impl α β} : l.maxKey! = l.maxKey?.get!

theorem Std.DTreeMap.Internal.Impl.maxKeyD_eq_getD_maxKey? {α : Type u} {β : α → Type v} {l : Impl α β} {fallback : α} : l.maxKeyD fallback = l.maxKey?.getD fallback

theorem Std.DTreeMap.Internal.Impl.Const.minEntry?_eq_minEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} : minEntry? l = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l.minEntry?

theorem Std.DTreeMap.Internal.Impl.Const.minEntry!_eq_get!_minEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} [Inhabited (α × β)] : minEntry! l = (minEntry? l).get!

theorem Std.DTreeMap.Internal.Impl.Const.minEntryD_eq_getD_minEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} {fallback : α × β} : minEntryD l fallback = (minEntry? l).getD fallback

theorem Std.DTreeMap.Internal.Impl.Const.some_minEntry_eq_minEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} {he : l.isEmpty = false} : some (minEntry l he) = minEntry? l

theorem Std.DTreeMap.Internal.Impl.Const.maxEntry?_eq_maxEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} : maxEntry? l = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) l.maxEntry?

theorem Std.DTreeMap.Internal.Impl.Const.maxEntry!_eq_get!_maxEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} [Inhabited (α × β)] : maxEntry! l = (maxEntry? l).get!

theorem Std.DTreeMap.Internal.Impl.Const.maxEntryD_eq_getD_maxEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} {fallback : α × β} : maxEntryD l fallback = (maxEntry? l).getD fallback

theorem Std.DTreeMap.Internal.Impl.Const.some_maxEntry_eq_maxEntry? {α : Type u} {β : Type v} [Ord α] {l : Impl α fun (x : α) => β} {he : l.isEmpty = false} : some (maxEntry l he) = maxEntry? l

theorem Std.DTreeMap.Internal.Impl.balanceL_eq_balance {α : 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 = balance k v l r hlb hrb ⋯

theorem Std.DTreeMap.Internal.Impl.balanceR_eq_balance {α : 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 = balance k v l r hlb hrb ⋯

theorem Std.DTreeMap.Internal.Impl.balanceLErase_eq_balance {α : 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 = balance k v l r hlb hrb ⋯

theorem Std.DTreeMap.Internal.Impl.balanceRErase_eq_balance {α : 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 = balance k v l r hlb hrb ⋯

theorem Std.DTreeMap.Internal.Impl.balanceL_eq_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 = balanceL! k v l r

theorem Std.DTreeMap.Internal.Impl.balanceR_eq_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 = balanceR! k v l r

theorem Std.DTreeMap.Internal.Impl.minView_k_eq_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).k

theorem Std.DTreeMap.Internal.Impl.minView_kv_eq_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).k, (minView! k v l r).v⟩

theorem Std.DTreeMap.Internal.Impl.minView_tree_impl_eq_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).tree.impl = (minView! k v l r).tree

theorem Std.DTreeMap.Internal.Impl.maxView_k_eq_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).k = (maxView! k v l r).k

theorem Std.DTreeMap.Internal.Impl.maxView_kv_eq_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).k, (maxView k v l r hl hr hlr).v⟩ = ⟨(maxView! k v l r).k, (maxView! k v l r).v⟩

theorem Std.DTreeMap.Internal.Impl.maxView_tree_impl_eq_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 = (maxView! k v l r).tree

theorem Std.DTreeMap.Internal.Impl.glue_eq_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 = l.glue! r

theorem Std.DTreeMap.Internal.Impl.insert_eq_insert! {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {l : Impl α β} {h : l.Balanced} : (insert k v l h).impl = insert! k v l

theorem Std.DTreeMap.Internal.Impl.insert_eq_insertₘ {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {l : Impl α β} {h : l.Balanced} : (insert k v l h).impl = insertₘ k v l h

theorem Std.DTreeMap.Internal.Impl.insert!_eq_insertₘ {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {l : Impl α β} (h : l.Balanced) : insert! k v l = insertₘ k v l h

theorem Std.DTreeMap.Internal.Impl.erase_eq_erase! {α : Type u} {β : α → Type v} [Ord α] {k : α} {t : Impl α β} {h : t.Balanced} : (erase k t h).impl = erase! k t

theorem Std.DTreeMap.Internal.Impl.erase_eq_eraseₘ {α : Type u} {β : α → Type v} [Ord α] {k : α} {t : Impl α β} {h : t.Balanced} : (erase k t h).impl = eraseₘ k t h

theorem Std.DTreeMap.Internal.Impl.erase!_eq_eraseₘ {α : Type u} {β : α → Type v} [Ord α] {k : α} {t : Impl α β} (h : t.Balanced) : erase! k t = eraseₘ k t h

theorem Std.DTreeMap.Internal.Impl.containsThenInsert!_fst_eq_containsThenInsert_fst {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (containsThenInsert! a b t).fst = (containsThenInsert a b t htb).fst

theorem Std.DTreeMap.Internal.Impl.containsThenInsert!_snd_eq_containsThenInsert_snd {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (containsThenInsert! a b t).snd = (containsThenInsert a b t htb).snd.impl

theorem Std.DTreeMap.Internal.Impl.containsThenInsert_snd_eq_insertₘ {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (containsThenInsert a b t htb).snd.impl = insertₘ a b t htb

theorem Std.DTreeMap.Internal.Impl.containsThenInsert!_snd_eq_insertₘ {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (containsThenInsert! a b t).snd = insertₘ a b t htb

theorem Std.DTreeMap.Internal.Impl.insertIfNew_eq_insertIfNew! {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {l : Impl α β} {h : l.Balanced} : (insertIfNew k v l h).impl = insertIfNew! k v l

theorem Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_fst_eq_containsThenInsertIfNew_fst {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (containsThenInsertIfNew! a b t).fst = (containsThenInsertIfNew a b t htb).fst

theorem Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_snd_eq_containsThenInsertIfNew_snd {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (containsThenInsertIfNew! a b t).snd = (containsThenInsertIfNew a b t htb).snd.impl

theorem Std.DTreeMap.Internal.Impl.containsThenInsertIfNew_fst_eq_containsₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (containsThenInsertIfNew a b t htb).fst = t.containsₘ a

theorem Std.DTreeMap.Internal.Impl.containsThenInsertIfNew_snd_eq_insertIfNew {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (containsThenInsertIfNew a b t htb).snd = insertIfNew a b t htb

theorem Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_fst_eq_containsₘ {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (a : α) (b : β a) : (containsThenInsertIfNew! a b t).fst = t.containsₘ a

theorem Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_snd_eq_insertIfNew! {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (a : α) (b : β a) : (containsThenInsertIfNew! a b t).snd = insertIfNew! a b t

@[irreducible]

theorem Std.DTreeMap.Internal.Impl.insertMin_eq_insertMin! {α : Type u} {β : α → Type v} [Ord α] {a : α} {b : β a} {t : Impl α β} (htb : t.Balanced) : (insertMin a b t htb).impl = insertMin! a b t

@[irreducible]

theorem Std.DTreeMap.Internal.Impl.insertMax_eq_insertMax! {α : Type u} {β : α → Type v} [Ord α] {a : α} {b : β a} {t : Impl α β} (htb : t.Balanced) : (insertMax a b t htb).impl = insertMax! a b t

theorem Std.DTreeMap.Internal.Impl.link_eq_link! {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) : (link k v l r hlb hrb).impl = link! k v l r

theorem Std.DTreeMap.Internal.Impl.link2_eq_link2! {α : Type u} {β : α → Type v} [Ord α] {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) : (l.link2 r hlb hrb).impl = l.link2! r

theorem Std.DTreeMap.Internal.Impl.Const.get?_eq_get?ₘ {α : Type u} {β : Type v} [Ord α] (k : α) (l : Impl α fun (x : α) => β) : get? l k = get?ₘ l k

theorem Std.DTreeMap.Internal.Impl.Const.get_eq_get? {α : Type u} {β : Type v} [Ord α] (k : α) (l : Impl α fun (x : α) => β) {h : contains k l = true} : some (get l k h) = get? l k

theorem Std.DTreeMap.Internal.Impl.Const.get_eq_getₘ {α : Type u} {β : Type v} [Ord α] (k : α) (l : Impl α fun (x : α) => β) {h : contains k l = true} (h' : (get?ₘ l k).isSome = true) : get l k h = getₘ l k h'

theorem Std.DTreeMap.Internal.Impl.Const.get!_eq_get!ₘ {α : Type u} {β : Type v} [Ord α] (k : α) [Inhabited β] (l : Impl α fun (x : α) => β) : get! l k = get!ₘ l k

theorem Std.DTreeMap.Internal.Impl.Const.getD_eq_getDₘ {α : Type u} {β : Type v} [Ord α] (k : α) (l : Impl α fun (x : α) => β) (fallback : β) : getD l k fallback = getDₘ l k fallback

theorem Std.DTreeMap.Internal.Impl.entryAtIdx?_eq_some_entryAtIdx {α : Type u} {β : α → Type v} {t : Impl α β} (htb : t.Balanced) {i : Nat} (h : i < t.size) : t.entryAtIdx? i = some (t.entryAtIdx htb i h)

theorem Std.DTreeMap.Internal.Impl.entryAtIdx!_eq_get!_entryAtIdx? {α : Type u} {β : α → Type v} {t : Impl α β} {i : Nat} [Inhabited ((a : α) × β a)] : t.entryAtIdx! i = (t.entryAtIdx? i).get!

theorem Std.DTreeMap.Internal.Impl.entryAtIdxD_eq_getD_entryAtIdx? {α : Type u} {β : α → Type v} {t : Impl α β} {i : Nat} {fallback : (a : α) × β a} : t.entryAtIdxD i fallback = (t.entryAtIdx? i).getD fallback

theorem Std.DTreeMap.Internal.Impl.keyAtIdx?_eq_entryAtIdx? {α : Type u} {β : α → Type v} {t : Impl α β} {i : Nat} : t.keyAtIdx? i = Option.map (fun (x : (a : α) × β a) => x.fst) (t.entryAtIdx? i)

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

theorem Std.DTreeMap.Internal.Impl.keyAtIdx!_eq_get!_keyAtIdx? {α : Type u} {β : α → Type v} [Inhabited α] {t : Impl α β} {i : Nat} : t.keyAtIdx! i = (t.keyAtIdx? i).get!

theorem Std.DTreeMap.Internal.Impl.keyAtIdxD_eq_getD_keyAtIdx? {α : Type u} {β : α → Type v} {t : Impl α β} {i : Nat} {fallback : α} : t.keyAtIdxD i fallback = (t.keyAtIdx? i).getD fallback

def Std.DTreeMap.Internal.Impl.getEntryGE?ₘ {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) : Option ((a : α) × β a)

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.getEntryGE?ₘ' {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) : Option ((a : α) × β a)

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.

theorem Std.DTreeMap.Internal.Impl.getEntryGE?_eq_getEntryGE?ₘ' {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) : getEntryGE? k t = getEntryGE?ₘ' k t

theorem Std.DTreeMap.Internal.Impl.getEntryGE?_eq_getEntryGE?ₘ {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) : getEntryGE? k t = getEntryGE?ₘ k t

def Std.DTreeMap.Internal.Impl.getEntryGT?ₘ {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) : Option ((a : α) × β a)

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.

def Std.DTreeMap.Internal.Impl.getEntryGT?ₘ' {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) : Option ((a : α) × β a)

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.

theorem Std.DTreeMap.Internal.Impl.getEntryGT?_eq_getEntryGT?ₘ' {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) : getEntryGT? k t = getEntryGT?ₘ' k t

theorem Std.DTreeMap.Internal.Impl.getEntryGT?_eq_getEntryGT?ₘ {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) : getEntryGT? k t = getEntryGT?ₘ k t

theorem Std.DTreeMap.Internal.Impl.getEntryLT?_eq_getEntryGT?_reverse {α : Type u} {β : α → Type v} [o : Ord α] [TransOrd α] {t : Impl α β} {k : α} : getEntryLT? k t = getEntryGT? k t.reverse

theorem Std.DTreeMap.Internal.Impl.getEntryLE?_eq_getEntryGE?_reverse {α : Type u} {β : α → Type v} [o : Ord α] [TransOrd α] {t : Impl α β} {k : α} : getEntryLE? k t = getEntryGE? k t.reverse

theorem Std.DTreeMap.Internal.Impl.getEntryGE!_eq_get!_getEntryGE? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} [Inhabited ((a : α) × β a)] : getEntryGE! k t = (getEntryGE? k t).get!

theorem Std.DTreeMap.Internal.Impl.getEntryGT!_eq_get!_getEntryGT? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} [Inhabited ((a : α) × β a)] : getEntryGT! k t = (getEntryGT? k t).get!

theorem Std.DTreeMap.Internal.Impl.getEntryLE!_eq_get!_getEntryLE? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} [Inhabited ((a : α) × β a)] : getEntryLE! k t = (getEntryLE? k t).get!

theorem Std.DTreeMap.Internal.Impl.getEntryLT!_eq_get!_getEntryLT? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} [Inhabited ((a : α) × β a)] : getEntryLT! k t = (getEntryLT? k t).get!

theorem Std.DTreeMap.Internal.Impl.getEntryGED_eq_getD_getEntryGE? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} {fallback : (a : α) × β a} : getEntryGED k t fallback = (getEntryGE? k t).getD fallback

theorem Std.DTreeMap.Internal.Impl.getEntryGTD_eq_getD_getEntryGT? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} {fallback : (a : α) × β a} : getEntryGTD k t fallback = (getEntryGT? k t).getD fallback

theorem Std.DTreeMap.Internal.Impl.getEntryLED_eq_getD_getEntryLE? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} {fallback : (a : α) × β a} : getEntryLED k t fallback = (getEntryLE? k t).getD fallback

theorem Std.DTreeMap.Internal.Impl.getEntryLTD_eq_getD_getEntryLT? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} {fallback : (a : α) × β a} : getEntryLTD k t fallback = (getEntryLT? k t).getD fallback

theorem Std.DTreeMap.Internal.Impl.getEntryGE?.eq_go {α : Type u} {β : α → Type v} [Ord α] (k : α) (x : Option ((a : α) × β a)) (t : Impl α β) : (getEntryGE? k t).or x = go k x t

theorem Std.DTreeMap.Internal.Impl.getEntryGT?.eq_go {α : Type u} {β : α → Type v} [Ord α] (k : α) (x : Option ((a : α) × β a)) (t : Impl α β) : (getEntryGT? k t).or x = go k x t

theorem Std.DTreeMap.Internal.Impl.getEntryLE?.eq_go {α : Type u} {β : α → Type v} [Ord α] (k : α) (x : Option ((a : α) × β a)) (t : Impl α β) : (getEntryLE? k t).or x = go k x t

theorem Std.DTreeMap.Internal.Impl.getEntryLT?.eq_go {α : Type u} {β : α → Type v} [Ord α] (k : α) (x : Option ((a : α) × β a)) (t : Impl α β) : (getEntryLT? k t).or x = go k x t

theorem Std.DTreeMap.Internal.Impl.some_getEntryGE_eq_getEntryGE? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) {ho : t.Ordered} {he : ∃ (a : α), a ∈ t ∧ (compare a k).isGE = true} : some (getEntryGE k t ho he) = getEntryGE? k t

theorem Std.DTreeMap.Internal.Impl.some_getEntryGT_eq_getEntryGT? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) {ho : t.Ordered} {he : ∃ (a : α), a ∈ t ∧ compare a k = Ordering.gt} : some (getEntryGT k t ho he) = getEntryGT? k t

theorem Std.DTreeMap.Internal.Impl.some_getEntryLE_eq_getEntryLE? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) {ho : t.Ordered} {he : ∃ (a : α), a ∈ t ∧ (compare a k).isLE = true} : some (getEntryLE k t ho he) = getEntryLE? k t

theorem Std.DTreeMap.Internal.Impl.some_getEntryLT_eq_getEntryLT? {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) {ho : t.Ordered} {he : ∃ (a : α), a ∈ t ∧ compare a k = Ordering.lt} : some (getEntryLT k t ho he) = getEntryLT? k t

theorem Std.DTreeMap.Internal.Impl.getKeyGE?_eq_getEntryGE? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} : getKeyGE? k t = Option.map (fun (x : (a : α) × β a) => x.fst) (getEntryGE? k t)

theorem Std.DTreeMap.Internal.Impl.getKeyGT?_eq_getEntryGT? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} : getKeyGT? k t = Option.map (fun (x : (a : α) × β a) => x.fst) (getEntryGT? k t)

theorem Std.DTreeMap.Internal.Impl.getKeyLE?_eq_getEntryLE? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} : getKeyLE? k t = Option.map (fun (x : (a : α) × β a) => x.fst) (getEntryLE? k t)

theorem Std.DTreeMap.Internal.Impl.getKeyLT?_eq_getEntryLT? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} : getKeyLT? k t = Option.map (fun (x : (a : α) × β a) => x.fst) (getEntryLT? k t)

theorem Std.DTreeMap.Internal.Impl.getKeyGE!_eq_get!_getKeyGE? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} [Inhabited α] : getKeyGE! k t = (getKeyGE? k t).get!

theorem Std.DTreeMap.Internal.Impl.getKeyGT!_eq_get!_getKeyGT? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} [Inhabited α] : getKeyGT! k t = (getKeyGT? k t).get!

theorem Std.DTreeMap.Internal.Impl.getKeyLE!_eq_get!_getKeyLE? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} [Inhabited α] : getKeyLE! k t = (getKeyLE? k t).get!

theorem Std.DTreeMap.Internal.Impl.getKeyLT!_eq_get!_getKeyLT? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k : α} [Inhabited α] : getKeyLT! k t = (getKeyLT? k t).get!

theorem Std.DTreeMap.Internal.Impl.getKeyGED_eq_getD_getKeyGE? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k fallback : α} : getKeyGED k t fallback = (getKeyGE? k t).getD fallback

theorem Std.DTreeMap.Internal.Impl.getKeyGTD_eq_getD_getKeyGT? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k fallback : α} : getKeyGTD k t fallback = (getKeyGT? k t).getD fallback

theorem Std.DTreeMap.Internal.Impl.getKeyLED_eq_getD_getKeyLE? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k fallback : α} : getKeyLED k t fallback = (getKeyLE? k t).getD fallback

theorem Std.DTreeMap.Internal.Impl.getKeyLTD_eq_getD_getKeyLT? {α : Type u} {β : α → Type v} [Ord α] {t : Impl α β} {k fallback : α} : getKeyLTD k t fallback = (getKeyLT? k t).getD fallback

theorem Std.DTreeMap.Internal.Impl.getKeyGE_eq_getEntryGE {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Impl α β} {k : α} {hto : t.Ordered} {he : ∃ (a : α), a ∈ t ∧ (compare a k).isGE = true} : getKeyGE k t hto he = (getEntryGE k t hto he).fst

theorem Std.DTreeMap.Internal.Impl.getKeyGT_eq_getEntryGT {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Impl α β} {k : α} {hto : t.Ordered} {he : ∃ (a : α), a ∈ t ∧ compare a k = Ordering.gt} : getKeyGT k t hto he = (getEntryGT k t hto he).fst

theorem Std.DTreeMap.Internal.Impl.getKeyLE_eq_getEntryLE {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Impl α β} {k : α} {hto : t.Ordered} {he : ∃ (a : α), a ∈ t ∧ (compare a k).isLE = true} : getKeyLE k t hto he = (getEntryLE k t hto he).fst

theorem Std.DTreeMap.Internal.Impl.getKeyLT_eq_getEntryLT {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] {t : Impl α β} {k : α} {hto : t.Ordered} {he : ∃ (a : α), a ∈ t ∧ compare a k = Ordering.lt} : getKeyLT k t hto he = (getEntryLT k t hto he).fst

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

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

theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdx!_eq_get!_entryAtIdx? {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} {i : Nat} [Inhabited (α × β)] : entryAtIdx! t i = (entryAtIdx? t i).get!

theorem Std.DTreeMap.Internal.Impl.Const.entryAtIdxD_eq_getD_entryAtIdx? {α : Type u} {β : Type v} {t : Impl α fun (x : α) => β} {i : Nat} {fallback : α × β} : entryAtIdxD t i fallback = (entryAtIdx? t i).getD fallback

theorem Std.DTreeMap.Internal.Impl.Const.getEntryGE?_eq_map {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} : getEntryGE? k t = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) (Impl.getEntryGE? k t)

theorem Std.DTreeMap.Internal.Impl.Const.getEntryGT?_eq_map {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} : getEntryGT? k t = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) (Impl.getEntryGT? k t)

theorem Std.DTreeMap.Internal.Impl.Const.getEntryLE?_eq_map {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} : getEntryLE? k t = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) (Impl.getEntryLE? k t)

theorem Std.DTreeMap.Internal.Impl.Const.getEntryLT?_eq_map {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} : getEntryLT? k t = Option.map (fun (x : (_ : α) × β) => (x.fst, x.snd)) (Impl.getEntryLT? k t)

theorem Std.DTreeMap.Internal.Impl.Const.getEntryGE!_eq_get!_getEntryGE? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} [Inhabited (α × β)] : getEntryGE! k t = (getEntryGE? k t).get!

theorem Std.DTreeMap.Internal.Impl.Const.getEntryGT!_eq_get!_getEntryGT? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} [Inhabited (α × β)] : getEntryGT! k t = (getEntryGT? k t).get!

theorem Std.DTreeMap.Internal.Impl.Const.getEntryLE!_eq_get!_getEntryLE? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} [Inhabited (α × β)] : getEntryLE! k t = (getEntryLE? k t).get!

theorem Std.DTreeMap.Internal.Impl.Const.getEntryLT!_eq_get!_getEntryLT? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} [Inhabited (α × β)] : getEntryLT! k t = (getEntryLT? k t).get!

theorem Std.DTreeMap.Internal.Impl.Const.getEntryGED_eq_getD_getEntryGE? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} {fallback : α × β} : getEntryGED k t fallback = (getEntryGE? k t).getD fallback

theorem Std.DTreeMap.Internal.Impl.Const.getEntryGTD_eq_getD_getEntryGT? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} {fallback : α × β} : getEntryGTD k t fallback = (getEntryGT? k t).getD fallback

theorem Std.DTreeMap.Internal.Impl.Const.getEntryLED_eq_getD_getEntryLE? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} {fallback : α × β} : getEntryLED k t fallback = (getEntryLE? k t).getD fallback

theorem Std.DTreeMap.Internal.Impl.Const.getEntryLTD_eq_getD_getEntryLT? {α : Type u} {β : Type v} [Ord α] {t : Impl α fun (x : α) => β} {k : α} {fallback : α × β} : getEntryLTD k t fallback = (getEntryLT? k t).getD fallback

theorem Std.DTreeMap.Internal.Impl.Const.getEntryGE_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} (hto : t.Ordered) {k : α} (he : ∃ (a : α), a ∈ t ∧ (compare a k).isGE = true) : getEntryGE k t hto he = ((Impl.getEntryGE k t hto he).fst, (Impl.getEntryGE k t hto he).snd)

theorem Std.DTreeMap.Internal.Impl.Const.getEntryGT_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} (hto : t.Ordered) {k : α} (he : ∃ (a : α), a ∈ t ∧ compare a k = Ordering.gt) : getEntryGT k t hto he = ((Impl.getEntryGT k t hto he).fst, (Impl.getEntryGT k t hto he).snd)

theorem Std.DTreeMap.Internal.Impl.Const.getEntryLE_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} (hto : t.Ordered) {k : α} (he : ∃ (a : α), a ∈ t ∧ (compare a k).isLE = true) : getEntryLE k t hto he = ((Impl.getEntryLE k t hto he).fst, (Impl.getEntryLE k t hto he).snd)

theorem Std.DTreeMap.Internal.Impl.Const.getEntryLT_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Impl α fun (x : α) => β} (hto : t.Ordered) {k : α} (he : ∃ (a : α), a ∈ t ∧ compare a k = Ordering.lt) : getEntryLT k t hto he = ((Impl.getEntryLT k t hto he).fst, (Impl.getEntryLT k t hto he).snd)