Documentation

Std.Data.DTreeMap.Internal.Model

Model implementations of tree map functions #

General infrastructure #

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

Internal implementation detail of the tree map

Equations
    Instances For
      theorem Std.DTreeMap.Internal.Impl.contains'_compare {α : Type u} {β : αType v} [Ord α] {k : α} {l : Impl α β} :
      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 = truec.contains = true)List ((a : α) × β a)δ) :
      δ

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

      Equations
        Instances For
          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 = truec.contains = true)List ((a : α) × β a)δ) (ll : List ((a : α) × β a)) (m : Impl α β) (hm : contains' k l = truecontains' k m = true) (rr : List ((a : α) × β a)) :
          δ
          Equations
            Instances For
              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 = truec.contains = true)δ) :
              δ

              Internal implementation detail of the tree map

              Equations
                Instances For
                  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 = truec.contains = true)δ) :
                  applyCell k l f = applyPartition (compare k) l fun (x : List ((a : α) × β a)) (c : Cell α β (compare k)) (hc : contains' (compare k) l = truec.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β aList ((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 α β kList ((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β aExplorationStep α β k

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

                  Instances For
                    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
                      Instances For
                        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' = truecontains' k l = true) (f : δExplorationStep α β kδ) :
                        applyPartition.go k l' (fun (l'_1 : List ((a : α) × β a)) (c : Cell α β k) (x : contains' k l' = truec.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' = truec.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 = truec.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
                          Instances For

                            Model functions #

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

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

                            Equations
                              Instances For
                                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
                                  Instances For
                                    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
                                      Instances For
                                        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
                                          Instances For
                                            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
                                              Instances For
                                                def Std.DTreeMap.Internal.Impl.getKey?ₘ {α : Type u} {β : αType v} [Ord α] (l : Impl α β) (k : α) :

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

                                                Equations
                                                  Instances For
                                                    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
                                                      Instances For
                                                        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
                                                          Instances For
                                                            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
                                                              Instances For
                                                                def Std.DTreeMap.Internal.Impl.minEntry?ₘ' {α : Type u} {β : αType v} [Ord α] (l : Impl α β) :
                                                                Option ((a : α) × β a)

                                                                Internal implementation detail of the tree map

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

                                                                    Internal implementation detail of the tree map

                                                                    Equations
                                                                      Instances For
                                                                        def Std.DTreeMap.Internal.Impl.reverse {α : Type u} {β : αType v} :
                                                                        Impl α βImpl α β

                                                                        Internal implementation detail of the tree map

                                                                        Equations
                                                                          Instances For
                                                                            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
                                                                              Instances For
                                                                                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
                                                                                  Instances For
                                                                                    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
                                                                                      Instances For
                                                                                        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
                                                                                          Instances For
                                                                                            def Std.DTreeMap.Internal.Impl.Const.get?ₘ {α : Type u} {β : Type v} [Ord α] (l : Impl α fun (x : α) => β) (k : α) :

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

                                                                                            Equations
                                                                                              Instances For
                                                                                                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
                                                                                                  Instances For
                                                                                                    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
                                                                                                      Instances For
                                                                                                        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
                                                                                                          Instances For
                                                                                                            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
                                                                                                              Instances For

                                                                                                                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 α β) :
                                                                                                                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 α β) :
                                                                                                                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 α β) :
                                                                                                                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.some_minEntry_eq_minEntry? {α : Type u} {β : αType v} [Ord α] {l : Impl α β} {he : l.isEmpty = false} :
                                                                                                                theorem Std.DTreeMap.Internal.Impl.minEntry_eq_get_minEntry? {α : Type u} {β : αType v} [Ord α] {l : Impl α β} {he : l.isEmpty = false} :
                                                                                                                l.minEntry he = l.minEntry?.get
                                                                                                                theorem Std.DTreeMap.Internal.Impl.minKey_eq_minEntry_fst {α : Type u} {β : αType v} [Ord α] {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} [Ord α] [Inhabited α] {l : Impl α β} :
                                                                                                                theorem Std.DTreeMap.Internal.Impl.minKeyD_eq_getD_minKey? {α : Type u} {β : αType v} [Ord α] {l : Impl α β} {fallback : α} :
                                                                                                                l.minKeyD fallback = l.minKey?.getD fallback
                                                                                                                theorem Std.DTreeMap.Internal.Impl.some_maxKey_eq_maxKey? {α : Type u} {β : αType v} [Ord α] {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} [Ord α] {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} [Ord α] [Inhabited α] {l : Impl α β} :
                                                                                                                theorem Std.DTreeMap.Internal.Impl.maxKeyD_eq_getD_maxKey? {α : Type u} {β : αType v} [Ord α] {l : Impl α β} {fallback : α} :
                                                                                                                l.maxKeyD fallback = l.maxKey?.getD fallback
                                                                                                                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) :
                                                                                                                theorem Std.DTreeMap.Internal.Impl.containsThenInsert!_snd_eq_containsThenInsert_snd {α : Type u} {β : αType v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) :
                                                                                                                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) :
                                                                                                                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_containsₘ {α : Type u} {β : αType v} [Ord α] [TransOrd α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) :
                                                                                                                theorem Std.DTreeMap.Internal.Impl.containsThenInsertIfNew_snd_eq_insertIfNew {α : Type u} {β : αType v} [Ord α] (t : Impl α β) (htb : t.Balanced) (a : α) (b : β a) :
                                                                                                                theorem Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_fst_eq_containsₘ {α : Type u} {β : αType v} [Ord α] [TransOrd α] (t : Impl α β) (a : α) (b : β a) :
                                                                                                                theorem Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_snd_eq_insertIfNew! {α : Type u} {β : αType v} [Ord α] (t : Impl α β) (a : α) (b : β a) :
                                                                                                                @[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.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