Documentation

Std.Data.DTreeMap.Lemmas

Dependent tree map lemmas #

This file contains lemmas about Std.DTreeMap. Most of the lemmas require TransCmp cmp for the comparison function cmp.

@[simp]
theorem Std.DTreeMap.isEmpty_emptyc {α : Type u} {β : αType v} {cmp : ααOrdering} :
@[simp]
theorem Std.DTreeMap.isEmpty_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
theorem Std.DTreeMap.mem_iff_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {k : α} :
@[simp]
theorem Std.DTreeMap.contains_iff_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {k : α} :
theorem Std.DTreeMap.contains_congr {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k k' : α} (hab : cmp k k' = Ordering.eq) :
theorem Std.DTreeMap.mem_congr {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k k' : α} (hab : cmp k k' = Ordering.eq) :
k t k' t
@[simp]
theorem Std.DTreeMap.contains_emptyc {α : Type u} {β : αType v} {cmp : ααOrdering} {k : α} :
@[simp]
theorem Std.DTreeMap.not_mem_emptyc {α : Type u} {β : αType v} {cmp : ααOrdering} {k : α} :
theorem Std.DTreeMap.contains_of_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a : α} :
theorem Std.DTreeMap.not_mem_of_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a : α} :
t.isEmpty = true¬a t
theorem Std.DTreeMap.isEmpty_eq_false_iff_exists_contains_eq_true {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
theorem Std.DTreeMap.isEmpty_eq_false_iff_exists_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
theorem Std.DTreeMap.isEmpty_eq_false_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a : α} (hc : t.contains a = true) :
theorem Std.DTreeMap.isEmpty_iff_forall_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
t.isEmpty = true ∀ (a : α), t.contains a = false
theorem Std.DTreeMap.isEmpty_iff_forall_not_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
t.isEmpty = true ∀ (a : α), ¬a t
@[simp]
theorem Std.DTreeMap.insert_eq_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {p : (a : α) × β a} :
@[simp]
theorem Std.DTreeMap.singleton_eq_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {p : (a : α) × β a} :
@[simp]
theorem Std.DTreeMap.contains_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} :
(t.insert k v).contains a = (cmp k a == Ordering.eq || t.contains a)
@[simp]
theorem Std.DTreeMap.mem_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} :
a t.insert k v cmp k a = Ordering.eq a t
theorem Std.DTreeMap.contains_insert_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insert k v).contains k = true
theorem Std.DTreeMap.mem_insert_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
k t.insert k v
theorem Std.DTreeMap.contains_of_contains_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} :
(t.insert k v).contains a = truecmp k a Ordering.eqt.contains a = true
theorem Std.DTreeMap.mem_of_mem_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} :
a t.insert k vcmp k a Ordering.eqa t
@[simp]
theorem Std.DTreeMap.size_emptyc {α : Type u} {β : αType v} {cmp : ααOrdering} :
theorem Std.DTreeMap.isEmpty_eq_size_eq_zero {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} :
t.isEmpty = (t.size == 0)
theorem Std.DTreeMap.size_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insert k v).size = if t.contains k = true then t.size else t.size + 1
theorem Std.DTreeMap.size_le_size_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
t.size (t.insert k v).size
theorem Std.DTreeMap.size_insert_le {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insert k v).size t.size + 1
@[simp]
theorem Std.DTreeMap.erase_emptyc {α : Type u} {β : αType v} {cmp : ααOrdering} {k : α} :
@[simp]
theorem Std.DTreeMap.isEmpty_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
(t.erase k).isEmpty = (t.isEmpty || t.size == 1 && t.contains k)
theorem Std.DTreeMap.isEmpty_eq_isEmpty_erase_and_not_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (k : α) :
theorem Std.DTreeMap.isEmpty_eq_false_of_isEmpty_erase_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (he : (t.erase k).isEmpty = false) :
@[simp]
theorem Std.DTreeMap.contains_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} :
(t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)
@[simp]
theorem Std.DTreeMap.mem_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} :
a t.erase k cmp k a Ordering.eq a t
theorem Std.DTreeMap.contains_of_contains_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} :
(t.erase k).contains a = truet.contains a = true
theorem Std.DTreeMap.mem_of_mem_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} :
a t.erase ka t
theorem Std.DTreeMap.size_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
theorem Std.DTreeMap.size_erase_le {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
(t.erase k).size t.size
theorem Std.DTreeMap.size_le_size_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
t.size (t.erase k).size + 1
@[simp]
theorem Std.DTreeMap.containsThenInsert_fst {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
@[simp]
theorem Std.DTreeMap.containsThenInsert_snd {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
@[simp]
theorem Std.DTreeMap.containsThenInsertIfNew_fst {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
@[simp]
theorem Std.DTreeMap.containsThenInsertIfNew_snd {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
@[simp]
theorem Std.DTreeMap.get?_emptyc {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
theorem Std.DTreeMap.get?_of_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
t.isEmpty = truet.get? a = none
theorem Std.DTreeMap.get?_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a k : α} {v : β k} :
(t.insert k v).get? a = if h : cmp k a = Ordering.eq then some (cast v) else t.get? a
@[simp]
theorem Std.DTreeMap.get?_insert_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
(t.insert k v).get? k = some v
theorem Std.DTreeMap.contains_eq_isSome_get? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
t.contains a = (t.get? a).isSome
@[simp]
theorem Std.DTreeMap.isSome_get?_eq_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
(t.get? a).isSome = t.contains a
theorem Std.DTreeMap.mem_iff_isSome_get? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
a t (t.get? a).isSome = true
@[simp]
theorem Std.DTreeMap.isSome_get?_iff_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
(t.get? a).isSome = true a t
theorem Std.DTreeMap.get?_eq_none_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
t.contains a = falset.get? a = none
theorem Std.DTreeMap.get?_eq_none {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} :
¬a tt.get? a = none
theorem Std.DTreeMap.get?_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} :
(t.erase k).get? a = if cmp k a = Ordering.eq then none else t.get? a
@[simp]
theorem Std.DTreeMap.get?_erase_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} :
(t.erase k).get? k = none
@[simp]
theorem Std.DTreeMap.Const.get?_emptyc {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] {a : α} :
theorem Std.DTreeMap.Const.get?_of_isEmpty {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} :
t.isEmpty = trueget? t a = none
theorem Std.DTreeMap.Const.get?_insert {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a k : α} {v : β} :
get? (t.insert k v) a = if cmp k a = Ordering.eq then some v else get? t a
@[simp]
theorem Std.DTreeMap.Const.get?_insert_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {v : β} :
get? (t.insert k v) k = some v
theorem Std.DTreeMap.Const.contains_eq_isSome_get? {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} :
t.contains a = (get? t a).isSome
@[simp]
theorem Std.DTreeMap.Const.isSome_get?_eq_contains {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} :
(get? t a).isSome = t.contains a
theorem Std.DTreeMap.Const.mem_iff_isSome_get? {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} :
a t (get? t a).isSome = true
@[simp]
theorem Std.DTreeMap.Const.isSome_get?_iff_mem {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} :
(get? t a).isSome = true a t
theorem Std.DTreeMap.Const.get?_eq_none_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} :
t.contains a = falseget? t a = none
theorem Std.DTreeMap.Const.get?_eq_none {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} :
¬a tget? t a = none
theorem Std.DTreeMap.Const.get?_erase {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k a : α} :
get? (t.erase k) a = if cmp k a = Ordering.eq then none else get? t a
@[simp]
theorem Std.DTreeMap.Const.get?_erase_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} :
get? (t.erase k) k = none
theorem Std.DTreeMap.Const.get?_eq_get? {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [LawfulEqCmp cmp] [TransCmp cmp] {a : α} :
get? t a = t.get? a
theorem Std.DTreeMap.Const.get?_congr {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a b : α} (hab : cmp a b = Ordering.eq) :
get? t a = get? t b
theorem Std.DTreeMap.get_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {v : β k} {h₁ : a t.insert k v} :
(t.insert k v).get a h₁ = if h₂ : cmp k a = Ordering.eq then cast v else t.get a
@[simp]
theorem Std.DTreeMap.get_insert_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
(t.insert k v).get k = v
@[simp]
theorem Std.DTreeMap.get_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {h' : a t.erase k} :
(t.erase k).get a h' = t.get a
theorem Std.DTreeMap.get?_eq_some_get {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {h' : a t} :
t.get? a = some (t.get a h')
theorem Std.DTreeMap.Const.get_insert {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k a : α} {v : β} {h₁ : a t.insert k v} :
get (t.insert k v) a h₁ = if h₂ : cmp k a = Ordering.eq then v else get t a
@[simp]
theorem Std.DTreeMap.Const.get_insert_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {v : β} :
get (t.insert k v) k = v
@[simp]
theorem Std.DTreeMap.Const.get_erase {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k a : α} {h' : a t.erase k} :
get (t.erase k) a h' = get t a
theorem Std.DTreeMap.Const.get?_eq_some_get {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} {h : a t} :
get? t a = some (get t a h)
theorem Std.DTreeMap.Const.get_eq_get {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {h : a t} :
get t a h = t.get a h
theorem Std.DTreeMap.Const.get_congr {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a b : α} (hab : cmp a b = Ordering.eq) {h' : a t} :
get t a h' = get t b
@[simp]
theorem Std.DTreeMap.get!_emptyc {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
theorem Std.DTreeMap.get!_of_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
theorem Std.DTreeMap.get!_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} [Inhabited (β a)] {v : β k} :
(t.insert k v).get! a = if h : cmp k a = Ordering.eq then cast v else t.get! a
@[simp]
theorem Std.DTreeMap.get!_insert_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] {b : β a} :
(t.insert a b).get! a = b
theorem Std.DTreeMap.get!_eq_default_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
theorem Std.DTreeMap.get!_eq_default {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
¬a tt.get! a = default
theorem Std.DTreeMap.get!_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} [Inhabited (β a)] :
(t.erase k).get! a = if cmp k a = Ordering.eq then default else t.get! a
@[simp]
theorem Std.DTreeMap.get!_erase_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} [Inhabited (β k)] :
theorem Std.DTreeMap.get?_eq_some_get!_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
t.contains a = truet.get? a = some (t.get! a)
theorem Std.DTreeMap.get?_eq_some_get! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
a tt.get? a = some (t.get! a)
theorem Std.DTreeMap.get!_eq_get!_get? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
t.get! a = (t.get? a).get!
theorem Std.DTreeMap.get_eq_get! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] {h : a t} :
t.get a h = t.get! a
@[simp]
theorem Std.DTreeMap.Const.get!_emptyc {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] [Inhabited β] {a : α} :
theorem Std.DTreeMap.Const.get!_of_isEmpty {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {a : α} :
theorem Std.DTreeMap.Const.get!_insert {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {k a : α} {v : β} :
get! (t.insert k v) a = if cmp k a = Ordering.eq then v else get! t a
@[simp]
theorem Std.DTreeMap.Const.get!_insert_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {k : α} {v : β} :
get! (t.insert k v) k = v
theorem Std.DTreeMap.Const.get!_eq_default_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {a : α} :
theorem Std.DTreeMap.Const.get!_eq_default {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {a : α} :
¬a tget! t a = default
theorem Std.DTreeMap.Const.get!_erase {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {k a : α} :
get! (t.erase k) a = if cmp k a = Ordering.eq then default else get! t a
@[simp]
theorem Std.DTreeMap.Const.get!_erase_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {k : α} :
theorem Std.DTreeMap.Const.get?_eq_some_get!_of_contains {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {a : α} :
t.contains a = trueget? t a = some (get! t a)
theorem Std.DTreeMap.Const.get?_eq_some_get! {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {a : α} :
a tget? t a = some (get! t a)
theorem Std.DTreeMap.Const.get!_eq_get!_get? {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {a : α} :
get! t a = (get? t a).get!
theorem Std.DTreeMap.Const.get_eq_get! {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {a : α} {h : a t} :
get t a h = get! t a
theorem Std.DTreeMap.Const.get!_eq_get! {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited β] {a : α} :
get! t a = t.get! a
theorem Std.DTreeMap.Const.get!_congr {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {a b : α} (hab : cmp a b = Ordering.eq) :
get! t a = get! t b
@[simp]
theorem Std.DTreeMap.getD_emptyc {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
.getD a fallback = fallback
theorem Std.DTreeMap.getD_of_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
t.isEmpty = truet.getD a fallback = fallback
theorem Std.DTreeMap.getD_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {fallback : β a} {v : β k} :
(t.insert k v).getD a fallback = if h : cmp k a = Ordering.eq then cast v else t.getD a fallback
@[simp]
theorem Std.DTreeMap.getD_insert_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback b : β a} :
(t.insert a b).getD a fallback = b
theorem Std.DTreeMap.getD_eq_fallback_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
t.contains a = falset.getD a fallback = fallback
theorem Std.DTreeMap.getD_eq_fallback {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
¬a tt.getD a fallback = fallback
theorem Std.DTreeMap.getD_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {fallback : β a} :
(t.erase k).getD a fallback = if cmp k a = Ordering.eq then fallback else t.getD a fallback
@[simp]
theorem Std.DTreeMap.getD_erase_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {fallback : β k} :
(t.erase k).getD k fallback = fallback
theorem Std.DTreeMap.get?_eq_some_getD_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
t.contains a = truet.get? a = some (t.getD a fallback)
theorem Std.DTreeMap.get?_eq_some_getD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
a tt.get? a = some (t.getD a fallback)
theorem Std.DTreeMap.getD_eq_getD_get? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} :
t.getD a fallback = (t.get? a).getD fallback
theorem Std.DTreeMap.get_eq_getD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β a} {h : a t} :
t.get a h = t.getD a fallback
theorem Std.DTreeMap.get!_eq_getD_default {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} [Inhabited (β a)] :
t.get! a = t.getD a default
@[simp]
theorem Std.DTreeMap.Const.getD_emptyc {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] {a : α} {fallback : β} :
getD a fallback = fallback
theorem Std.DTreeMap.Const.getD_of_isEmpty {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} {fallback : β} :
t.isEmpty = truegetD t a fallback = fallback
theorem Std.DTreeMap.Const.getD_insert {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k a : α} {fallback v : β} :
getD (t.insert k v) a fallback = if cmp k a = Ordering.eq then v else getD t a fallback
@[simp]
theorem Std.DTreeMap.Const.getD_insert_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {fallback v : β} :
getD (t.insert k v) k fallback = v
theorem Std.DTreeMap.Const.getD_eq_fallback_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} {fallback : β} :
t.contains a = falsegetD t a fallback = fallback
theorem Std.DTreeMap.Const.getD_eq_fallback {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} {fallback : β} :
¬a tgetD t a fallback = fallback
theorem Std.DTreeMap.Const.getD_erase {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k a : α} {fallback : β} :
getD (t.erase k) a fallback = if cmp k a = Ordering.eq then fallback else getD t a fallback
@[simp]
theorem Std.DTreeMap.Const.getD_erase_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {fallback : β} :
getD (t.erase k) k fallback = fallback
theorem Std.DTreeMap.Const.get?_eq_some_getD_of_contains {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} {fallback : β} :
t.contains a = trueget? t a = some (getD t a fallback)
theorem Std.DTreeMap.Const.get?_eq_some_getD {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} {fallback : β} :
a tget? t a = some (getD t a fallback)
theorem Std.DTreeMap.Const.getD_eq_getD_get? {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} {fallback : β} :
getD t a fallback = (get? t a).getD fallback
theorem Std.DTreeMap.Const.get_eq_getD {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a : α} {fallback : β} {h : a t} :
get t a h = getD t a fallback
theorem Std.DTreeMap.Const.get!_eq_getD_default {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {a : α} :
get! t a = getD t a default
theorem Std.DTreeMap.Const.getD_eq_getD {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {a : α} {fallback : β} :
getD t a fallback = t.getD a fallback
theorem Std.DTreeMap.Const.getD_congr {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {a b : α} {fallback : β} (hab : cmp a b = Ordering.eq) :
getD t a fallback = getD t b fallback
@[simp]
theorem Std.DTreeMap.getKey?_emptyc {α : Type u} {β : αType v} {cmp : ααOrdering} {a : α} :
theorem Std.DTreeMap.getKey?_of_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a : α} :
theorem Std.DTreeMap.getKey?_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a k : α} {v : β k} :
(t.insert k v).getKey? a = if cmp k a = Ordering.eq then some k else t.getKey? a
@[simp]
theorem Std.DTreeMap.getKey?_insert_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insert k v).getKey? k = some k
theorem Std.DTreeMap.contains_eq_isSome_getKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a : α} :
@[simp]
theorem Std.DTreeMap.isSome_getKey?_eq_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a : α} :
theorem Std.DTreeMap.mem_iff_isSome_getKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a : α} :
@[simp]
theorem Std.DTreeMap.isSome_getKey?_iff_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a : α} :
theorem Std.DTreeMap.getKey?_eq_none_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a : α} :
theorem Std.DTreeMap.getKey?_eq_none {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a : α} :
¬a tt.getKey? a = none
theorem Std.DTreeMap.getKey?_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} :
@[simp]
theorem Std.DTreeMap.getKey?_erase_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
theorem Std.DTreeMap.compare_getKey?_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
Option.all (fun (x : α) => decide (cmp x k = Ordering.eq)) (t.getKey? k) = true
theorem Std.DTreeMap.getKey?_congr {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k k' : α} (h' : cmp k k' = Ordering.eq) :
t.getKey? k = t.getKey? k'
theorem Std.DTreeMap.getKey?_eq_some_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} (h' : t.contains k = true) :
t.getKey? k = some k
theorem Std.DTreeMap.getKey?_eq_some {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} (h' : k t) :
t.getKey? k = some k
theorem Std.DTreeMap.getKey_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} {h₁ : a t.insert k v} :
(t.insert k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq then k else t.getKey a
@[simp]
theorem Std.DTreeMap.getKey_insert_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insert k v).getKey k = k
@[simp]
theorem Std.DTreeMap.getKey_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {h' : a t.erase k} :
(t.erase k).getKey a h' = t.getKey a
theorem Std.DTreeMap.getKey?_eq_some_getKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a : α} {h' : a t} :
t.getKey? a = some (t.getKey a h')
theorem Std.DTreeMap.compare_getKey_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (h' : k t) :
cmp (t.getKey k h') k = Ordering.eq
theorem Std.DTreeMap.getKey_congr {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k₁ k₂ : α} (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ t) :
t.getKey k₁ h₁ = t.getKey k₂
@[simp]
theorem Std.DTreeMap.getKey_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} (h' : k t) :
t.getKey k h' = k
@[simp]
theorem Std.DTreeMap.getKey!_emptyc {α : Type u} {β : αType v} {cmp : ααOrdering} {a : α} [Inhabited α] :
theorem Std.DTreeMap.getKey!_of_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {a : α} :
theorem Std.DTreeMap.getKey!_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k a : α} {v : β k} :
(t.insert k v).getKey! a = if cmp k a = Ordering.eq then k else t.getKey! a
@[simp]
theorem Std.DTreeMap.getKey!_insert_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {a : α} {b : β a} :
(t.insert a b).getKey! a = a
theorem Std.DTreeMap.getKey!_eq_default_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {a : α} :
theorem Std.DTreeMap.getKey!_eq_default {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {a : α} :
¬a tt.getKey! a = default
theorem Std.DTreeMap.getKey!_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k a : α} :
@[simp]
theorem Std.DTreeMap.getKey!_erase_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} :
theorem Std.DTreeMap.getKey?_eq_some_getKey!_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {a : α} :
t.contains a = truet.getKey? a = some (t.getKey! a)
theorem Std.DTreeMap.getKey?_eq_some_getKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {a : α} :
a tt.getKey? a = some (t.getKey! a)
theorem Std.DTreeMap.getKey!_eq_get!_getKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {a : α} :
t.getKey! a = (t.getKey? a).get!
theorem Std.DTreeMap.getKey_eq_getKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {a : α} {h : a t} :
t.getKey a h = t.getKey! a
theorem Std.DTreeMap.getKey!_congr {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k k' : α} (h' : cmp k k' = Ordering.eq) :
t.getKey! k = t.getKey! k'
theorem Std.DTreeMap.getKey!_eq_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} (h' : t.contains k = true) :
t.getKey! k = k
theorem Std.DTreeMap.getKey!_eq_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} (h' : k t) :
t.getKey! k = k
@[simp]
theorem Std.DTreeMap.getKeyD_emptyc {α : Type u} {β : αType v} {cmp : ααOrdering} {a fallback : α} :
.getKeyD a fallback = fallback
theorem Std.DTreeMap.getKeyD_of_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a fallback : α} :
t.isEmpty = truet.getKeyD a fallback = fallback
theorem Std.DTreeMap.getKeyD_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a fallback : α} {v : β k} :
(t.insert k v).getKeyD a fallback = if cmp k a = Ordering.eq then k else t.getKeyD a fallback
@[simp]
theorem Std.DTreeMap.getKeyD_insert_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a fallback : α} {b : β a} :
(t.insert a b).getKeyD a fallback = a
theorem Std.DTreeMap.getKeyD_eq_fallback_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a fallback : α} :
t.contains a = falset.getKeyD a fallback = fallback
theorem Std.DTreeMap.getKeyD_eq_fallback {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a fallback : α} :
¬a tt.getKeyD a fallback = fallback
theorem Std.DTreeMap.getKeyD_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a fallback : α} :
(t.erase k).getKeyD a fallback = if cmp k a = Ordering.eq then fallback else t.getKeyD a fallback
@[simp]
theorem Std.DTreeMap.getKeyD_erase_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k fallback : α} :
(t.erase k).getKeyD k fallback = fallback
theorem Std.DTreeMap.getKey?_eq_some_getKeyD_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a fallback : α} :
t.contains a = truet.getKey? a = some (t.getKeyD a fallback)
theorem Std.DTreeMap.getKey?_eq_some_getKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a fallback : α} :
a tt.getKey? a = some (t.getKeyD a fallback)
theorem Std.DTreeMap.getKeyD_eq_getD_getKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a fallback : α} :
t.getKeyD a fallback = (t.getKey? a).getD fallback
theorem Std.DTreeMap.getKey_eq_getKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {a fallback : α} {h : a t} :
t.getKey a h = t.getKeyD a fallback
theorem Std.DTreeMap.getKey!_eq_getKeyD_default {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {a : α} :
theorem Std.DTreeMap.getKeyD_congr {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k k' fallback : α} (h' : cmp k k' = Ordering.eq) :
t.getKeyD k fallback = t.getKeyD k' fallback
theorem Std.DTreeMap.getKeyD_eq_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k fallback : α} (h' : t.contains k = true) :
t.getKeyD k fallback = k
theorem Std.DTreeMap.getKeyD_eq_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k fallback : α} (h' : k t) :
t.getKeyD k fallback = k
@[simp]
theorem Std.DTreeMap.isEmpty_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
@[simp]
theorem Std.DTreeMap.contains_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} :
(t.insertIfNew k v).contains a = (cmp k a == Ordering.eq || t.contains a)
@[simp]
theorem Std.DTreeMap.mem_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} :
a t.insertIfNew k v cmp k a = Ordering.eq a t
theorem Std.DTreeMap.contains_insertIfNew_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
theorem Std.DTreeMap.mem_insertIfNew_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
theorem Std.DTreeMap.contains_of_contains_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} :
(t.insertIfNew k v).contains a = truecmp k a Ordering.eqt.contains a = true
theorem Std.DTreeMap.mem_of_mem_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} :
a t.insertIfNew k vcmp k a Ordering.eqa t
theorem Std.DTreeMap.mem_of_mem_insertIfNew' {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} :
a t.insertIfNew k v¬(cmp k a = Ordering.eq ¬k t) → a t

This is a restatement of mem_of_mem_insertIfNew that is written to exactly match the proof obligation in the statement of get_insertIfNew.

theorem Std.DTreeMap.size_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insertIfNew k v).size = if k t then t.size else t.size + 1
theorem Std.DTreeMap.size_le_size_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
theorem Std.DTreeMap.size_insertIfNew_le {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insertIfNew k v).size t.size + 1
theorem Std.DTreeMap.get?_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {v : β k} :
(t.insertIfNew k v).get? a = if h : cmp k a = Ordering.eq ¬k t then some (cast v) else t.get? a
theorem Std.DTreeMap.get_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {v : β k} {h₁ : a t.insertIfNew k v} :
(t.insertIfNew k v).get a h₁ = if h₂ : cmp k a = Ordering.eq ¬k t then cast v else t.get a
theorem Std.DTreeMap.get!_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} [Inhabited (β a)] {v : β k} :
(t.insertIfNew k v).get! a = if h : cmp k a = Ordering.eq ¬k t then cast v else t.get! a
theorem Std.DTreeMap.getD_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} {fallback : β a} {v : β k} :
(t.insertIfNew k v).getD a fallback = if h : cmp k a = Ordering.eq ¬k t then cast v else t.getD a fallback
theorem Std.DTreeMap.Const.get?_insertIfNew {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k a : α} {v : β} :
get? (t.insertIfNew k v) a = if cmp k a = Ordering.eq ¬k t then some v else get? t a
theorem Std.DTreeMap.Const.get_insertIfNew {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k a : α} {v : β} {h₁ : a t.insertIfNew k v} :
get (t.insertIfNew k v) a h₁ = if h₂ : cmp k a = Ordering.eq ¬k t then v else get t a
theorem Std.DTreeMap.Const.get!_insertIfNew {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {k a : α} {v : β} :
get! (t.insertIfNew k v) a = if cmp k a = Ordering.eq ¬k t then v else get! t a
theorem Std.DTreeMap.Const.getD_insertIfNew {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k a : α} {fallback v : β} :
getD (t.insertIfNew k v) a fallback = if cmp k a = Ordering.eq ¬k t then v else getD t a fallback
theorem Std.DTreeMap.getKey?_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} :
theorem Std.DTreeMap.getKey_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a : α} {v : β k} {h₁ : a t.insertIfNew k v} :
(t.insertIfNew k v).getKey a h₁ = if h₂ : cmp k a = Ordering.eq ¬k t then k else t.getKey a
theorem Std.DTreeMap.getKey!_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k a : α} {v : β k} :
(t.insertIfNew k v).getKey! a = if cmp k a = Ordering.eq ¬k t then k else t.getKey! a
theorem Std.DTreeMap.getKeyD_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k a fallback : α} {v : β k} :
(t.insertIfNew k v).getKeyD a fallback = if cmp k a = Ordering.eq ¬k t then k else t.getKeyD a fallback
@[simp]
theorem Std.DTreeMap.getThenInsertIfNew?_fst {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
@[simp]
theorem Std.DTreeMap.getThenInsertIfNew?_snd {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
@[simp]
theorem Std.DTreeMap.Const.getThenInsertIfNew?_fst {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {v : β} :
@[simp]
theorem Std.DTreeMap.Const.getThenInsertIfNew?_snd {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {v : β} :
@[simp]
theorem Std.DTreeMap.length_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
@[simp]
theorem Std.DTreeMap.isEmpty_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} :
@[simp]
theorem Std.DTreeMap.contains_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} :
@[simp]
theorem Std.DTreeMap.mem_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [LawfulEqCmp cmp] [TransCmp cmp] {k : α} :
k t.keys k t
theorem Std.DTreeMap.distinct_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) t.keys
theorem Std.DTreeMap.ordered_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : α) => cmp a b = Ordering.lt) t.keys
@[simp]
theorem Std.DTreeMap.map_fst_toList_eq_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} :
@[simp]
theorem Std.DTreeMap.length_toList {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
@[simp]
theorem Std.DTreeMap.isEmpty_toList {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} :
@[simp]
theorem Std.DTreeMap.mem_toList_iff_get?_eq_some {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
k, v t.toList t.get? k = some v
theorem Std.DTreeMap.find?_toList_eq_some_iff_get?_eq_some {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} :
List.find? (fun (x : (a : α) × β a) => cmp x.fst k == Ordering.eq) t.toList = some k, v t.get? k = some v
theorem Std.DTreeMap.find?_toList_eq_none_iff_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
List.find? (fun (x : (a : α) × β a) => cmp x.fst k == Ordering.eq) t.toList = none t.contains k = false
@[simp]
theorem Std.DTreeMap.find?_toList_eq_none_iff_not_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
List.find? (fun (x : (a : α) × β a) => cmp x.fst k == Ordering.eq) t.toList = none ¬k t
theorem Std.DTreeMap.distinct_keys_toList {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) t.toList
theorem Std.DTreeMap.ordered_keys_toList {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : (a : α) × β a) => cmp a.fst b.fst = Ordering.lt) t.toList
@[simp]
theorem Std.DTreeMap.Const.map_fst_toList_eq_keys {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} :
@[simp]
theorem Std.DTreeMap.Const.length_toList {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} :
@[simp]
theorem Std.DTreeMap.Const.isEmpty_toList {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} :
@[simp]
theorem Std.DTreeMap.Const.mem_toList_iff_get?_eq_some {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β} :
(k, v) toList t get? t k = some v
@[simp]
theorem Std.DTreeMap.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {v : β} :
(k, v) toList t t.getKey? k = some k get? t k = some v
theorem Std.DTreeMap.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {v : β} :
get? t k = some v (k' : α), cmp k k' = Ordering.eq (k', v) toList t
theorem Std.DTreeMap.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k k' : α} {v : β} :
List.find? (fun (x : α × β) => cmp x.fst k == Ordering.eq) (toList t) = some (k', v) t.getKey? k = some k' get? t k = some v
theorem Std.DTreeMap.Const.find?_toList_eq_none_iff_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} :
List.find? (fun (x : α × β) => cmp x.fst k == Ordering.eq) (toList t) = none t.contains k = false
@[simp]
theorem Std.DTreeMap.Const.find?_toList_eq_none_iff_not_mem {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} :
List.find? (fun (x : α × β) => cmp x.fst k == Ordering.eq) (toList t) = none ¬k t
theorem Std.DTreeMap.Const.distinct_keys_toList {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) (toList t)
theorem Std.DTreeMap.Const.ordered_keys_toList {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] :
List.Pairwise (fun (a b : α × β) => cmp a.fst b.fst = Ordering.lt) (toList t)
theorem Std.DTreeMap.foldlM_eq_foldlM_toList {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ(a : α) → β am δ} {init : δ} :
foldlM f init t = List.foldlM (fun (a : δ) (b : (a : α) × β a) => f a b.fst b.snd) init t.toList
theorem Std.DTreeMap.foldl_eq_foldl_toList {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {δ : Type w} {f : δ(a : α) → β aδ} {init : δ} :
foldl f init t = List.foldl (fun (a : δ) (b : (a : α) × β a) => f a b.fst b.snd) init t.toList
theorem Std.DTreeMap.foldrM_eq_foldrM_toList {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β aδm δ} {init : δ} :
foldrM f init t = List.foldrM (fun (a : (a : α) × β a) (b : δ) => f a.fst a.snd b) init t.toList
theorem Std.DTreeMap.foldr_eq_foldr_toList {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {δ : Type w} {f : (a : α) → β aδδ} {init : δ} :
foldr f init t = List.foldr (fun (a : (a : α) × β a) (b : δ) => f a.fst a.snd b) init t.toList
@[simp]
theorem Std.DTreeMap.forM_eq_forM {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β am PUnit} :
forM f t = ForM.forM t fun (a : (a : α) × β a) => f a.fst a.snd
theorem Std.DTreeMap.forM_eq_forM_toList {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) × β am PUnit} :
@[simp]
theorem Std.DTreeMap.forIn_eq_forIn {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β aδm (ForInStep δ)} {init : δ} :
forIn f init t = ForIn.forIn t init fun (a : (a : α) × β a) (b : δ) => f a.fst a.snd b
theorem Std.DTreeMap.forIn_eq_forIn_toList {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) × β aδm (ForInStep δ)} {init : δ} :
ForIn.forIn t init f = ForIn.forIn t.toList init f
theorem Std.DTreeMap.foldlM_eq_foldlM_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δαm δ} {init : δ} :
foldlM (fun (d : δ) (a : α) (x : β a) => f d a) init t = List.foldlM f init t.keys
theorem Std.DTreeMap.foldl_eq_foldl_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {δ : Type w} {f : δαδ} {init : δ} :
foldl (fun (d : δ) (a : α) (x : β a) => f d a) init t = List.foldl f init t.keys
theorem Std.DTreeMap.foldrM_eq_foldrM_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : αδm δ} {init : δ} :
foldrM (fun (a : α) (x : β a) (d : δ) => f a d) init t = List.foldrM f init t.keys
theorem Std.DTreeMap.foldr_eq_foldr_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {δ : Type w} {f : αδδ} {init : δ} :
foldr (fun (a : α) (x : β a) (d : δ) => f a d) init t = List.foldr f init t.keys
theorem Std.DTreeMap.forM_eq_forM_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : αm PUnit} :
(ForM.forM t fun (a : (a : α) × β a) => f a.fst) = t.keys.forM f
theorem Std.DTreeMap.forIn_eq_forIn_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : αδm (ForInStep δ)} {init : δ} :
(ForIn.forIn t init fun (a : (a : α) × β a) (d : δ) => f a.fst d) = ForIn.forIn t.keys init f
theorem Std.DTreeMap.Const.foldlM_eq_foldlM_toList {α : Type u} {cmp : ααOrdering} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Monad m] [LawfulMonad m] {f : δαβm δ} {init : δ} :
foldlM f init t = List.foldlM (fun (a : δ) (b : α × β) => f a b.fst b.snd) init (toList t)
theorem Std.DTreeMap.Const.foldl_eq_foldl_toList {α : Type u} {cmp : ααOrdering} {δ : Type w} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {f : δαβδ} {init : δ} :
foldl f init t = List.foldl (fun (a : δ) (b : α × β) => f a b.fst b.snd) init (toList t)
theorem Std.DTreeMap.Const.foldrM_eq_foldrM_toList {α : Type u} {cmp : ααOrdering} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Monad m] [LawfulMonad m] {f : αβδm δ} {init : δ} :
foldrM f init t = List.foldrM (fun (a : α × β) (b : δ) => f a.fst a.snd b) init (toList t)
theorem Std.DTreeMap.Const.foldr_eq_foldr_toList {α : Type u} {cmp : ααOrdering} {δ : Type w} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {f : αβδδ} {init : δ} :
foldr f init t = List.foldr (fun (a : α × β) (b : δ) => f a.fst a.snd b) init (toList t)
theorem Std.DTreeMap.Const.forM_eq_forMUncurried {α : Type u} {cmp : ααOrdering} {m : Type w → Type w'} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Monad m] [LawfulMonad m] {f : αβm PUnit} :
forM f t = forMUncurried (fun (a : α × β) => f a.fst a.snd) t
theorem Std.DTreeMap.Const.forMUncurried_eq_forM_toList {α : Type u} {cmp : ααOrdering} {m : Type w → Type w'} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Monad m] [LawfulMonad m] {f : α × βm PUnit} :
@[deprecated Std.DTreeMap.Const.forMUncurried_eq_forM_toList (since := "2025-03-02")]
theorem Std.DTreeMap.Const.forM_eq_forM_toList {α : Type u} {cmp : ααOrdering} {m : Type w → Type w'} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Monad m] [LawfulMonad m] {f : αβm PUnit} :
forM f t = (toList t).forM fun (a : α × β) => f a.fst a.snd

Deprecated, use forMUncurried_eq_forM_toList together with forM_eq_forMUncurried instead.

theorem Std.DTreeMap.Const.forIn_eq_forInUncurried {α : Type u} {cmp : ααOrdering} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Monad m] [LawfulMonad m] {f : αβδm (ForInStep δ)} {init : δ} :
forIn f init t = forInUncurried (fun (a : α × β) (b : δ) => f a.fst a.snd b) init t
theorem Std.DTreeMap.Const.forInUncurried_eq_forIn_toList {α : Type u} {cmp : ααOrdering} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Monad m] [LawfulMonad m] {f : α × βδm (ForInStep δ)} {init : δ} :
forInUncurried f init t = ForIn.forIn (toList t) init f
@[deprecated Std.DTreeMap.Const.forInUncurried_eq_forIn_toList (since := "2025-03-02")]
theorem Std.DTreeMap.Const.forIn_eq_forIn_toList {α : Type u} {cmp : ααOrdering} {δ : Type w} {m : Type w → Type w'} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Monad m] [LawfulMonad m] {f : αβδm (ForInStep δ)} {init : δ} :
forIn f init t = ForIn.forIn (toList t) init fun (a : α × β) (b : δ) => f a.fst a.snd b

Deprecated, use forInUncurried_eq_forIn_toList together with forIn_eq_forInUncurried instead.

@[simp]
theorem Std.DTreeMap.insertMany_nil {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} :
@[simp]
theorem Std.DTreeMap.insertMany_list_singleton {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {k : α} {v : β k} :
theorem Std.DTreeMap.insertMany_cons {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {l : List ((a : α) × β a)} {k : α} {v : β k} :
t.insertMany (k, v :: l) = (t.insert k v).insertMany l
theorem Std.DTreeMap.insertMany_append {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} {l₁ l₂ : List ((a : α) × β a)} :
t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂
@[simp]
theorem Std.DTreeMap.contains_insertMany_list {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} :
@[simp]
theorem Std.DTreeMap.mem_insertMany_list {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} :
theorem Std.DTreeMap.mem_of_mem_insertMany_list {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} :
theorem Std.DTreeMap.get?_insertMany_list_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(t.insertMany l).get? k = t.get? k
theorem Std.DTreeMap.get?_insertMany_list_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k, v l) :
(t.insertMany l).get? k' = some (cast v)
theorem Std.DTreeMap.get_insertMany_list_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} (contains : (List.map Sigma.fst l).contains k = false) {h' : k t.insertMany l} :
(t.insertMany l).get k h' = t.get k
theorem Std.DTreeMap.get_insertMany_list_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k, v l) {h' : k' t.insertMany l} :
(t.insertMany l).get k' h' = cast v
theorem Std.DTreeMap.get!_insertMany_list_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(t.insertMany l).get! k = t.get! k
theorem Std.DTreeMap.get!_insertMany_list_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} [Inhabited (β k')] (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k, v l) :
(t.insertMany l).get! k' = cast v
theorem Std.DTreeMap.getD_insertMany_list_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(t.insertMany l).getD k fallback = t.getD k fallback
theorem Std.DTreeMap.getD_insertMany_list_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k, v l) :
(t.insertMany l).getD k' fallback = cast v
theorem Std.DTreeMap.getKey?_insertMany_list_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.getKey?_insertMany_list_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Sigma.fst l) :
theorem Std.DTreeMap.getKey_insertMany_list_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) {h' : k t.insertMany l} :
(t.insertMany l).getKey k h' = t.getKey k
theorem Std.DTreeMap.getKey_insertMany_list_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Sigma.fst l) {h' : k' t.insertMany l} :
(t.insertMany l).getKey k' h' = k
theorem Std.DTreeMap.getKey!_insertMany_list_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.getKey!_insertMany_list_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Sigma.fst l) :
(t.insertMany l).getKey! k' = k
theorem Std.DTreeMap.getKeyD_insertMany_list_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k fallback : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(t.insertMany l).getKeyD k fallback = t.getKeyD k fallback
theorem Std.DTreeMap.getKeyD_insertMany_list_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {l : List ((a : α) × β a)} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Sigma.fst l) :
(t.insertMany l).getKeyD k' fallback = k
theorem Std.DTreeMap.size_insertMany_list {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) :
(∀ (a : α), a t(List.map Sigma.fst l).contains a = false)(t.insertMany l).size = t.size + l.length
theorem Std.DTreeMap.size_le_size_insertMany_list {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {l : List ((a : α) × β a)} :
theorem Std.DTreeMap.size_insertMany_list_le {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {l : List ((a : α) × β a)} :
@[simp]
theorem Std.DTreeMap.isEmpty_insertMany_list {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {l : List ((a : α) × β a)} :
@[simp]
theorem Std.DTreeMap.Const.insertMany_nil {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} :
@[simp]
theorem Std.DTreeMap.Const.insertMany_list_singleton {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k : α} {v : β} :
theorem Std.DTreeMap.Const.insertMany_cons {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {l : List (α × β)} {k : α} {v : β} :
insertMany t ((k, v) :: l) = insertMany (t.insert k v) l
theorem Std.DTreeMap.Const.insertMany_append {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {l₁ l₂ : List (α × β)} :
insertMany t (l₁ ++ l₂) = insertMany (insertMany t l₁) l₂
@[simp]
theorem Std.DTreeMap.Const.contains_insertMany_list {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
@[simp]
theorem Std.DTreeMap.Const.mem_insertMany_list {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
theorem Std.DTreeMap.Const.mem_of_mem_insertMany_list {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
k insertMany t l(List.map Prod.fst l).contains k = falsek t
theorem Std.DTreeMap.Const.getKey?_insertMany_list_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.DTreeMap.Const.getKey?_insertMany_list_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Prod.fst l) :
theorem Std.DTreeMap.Const.getKey_insertMany_list_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k insertMany t l} :
(insertMany t l).getKey k h' = t.getKey k
theorem Std.DTreeMap.Const.getKey_insertMany_list_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Prod.fst l) {h' : k' insertMany t l} :
(insertMany t l).getKey k' h' = k
theorem Std.DTreeMap.Const.getKey!_insertMany_list_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.DTreeMap.Const.getKey!_insertMany_list_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited α] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Prod.fst l) :
(insertMany t l).getKey! k' = k
theorem Std.DTreeMap.Const.getKeyD_insertMany_list_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k fallback : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(insertMany t l).getKeyD k fallback = t.getKeyD k fallback
theorem Std.DTreeMap.Const.getKeyD_insertMany_list_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Prod.fst l) :
(insertMany t l).getKeyD k' fallback = k
theorem Std.DTreeMap.Const.size_insertMany_list {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) :
(∀ (a : α), a t(List.map Prod.fst l).contains a = false)(insertMany t l).size = t.size + l.length
theorem Std.DTreeMap.Const.size_le_size_insertMany_list {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} :
theorem Std.DTreeMap.Const.size_insertMany_list_le {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} :
@[simp]
theorem Std.DTreeMap.Const.isEmpty_insertMany_list {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} :
theorem Std.DTreeMap.Const.get?_insertMany_list_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
get? (insertMany t l) k = get? t k
theorem Std.DTreeMap.Const.get?_insertMany_list_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) l) :
get? (insertMany t l) k' = some v
theorem Std.DTreeMap.Const.get?_insertMany_list {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
get? (insertMany t l) k = (List.findSomeRev? (fun (x : α × β) => match x with | (a, b) => if cmp a k = Ordering.eq then some b else none) l).or (get? t k)
theorem Std.DTreeMap.Const.get_insertMany_list_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k insertMany t l} :
get (insertMany t l) k h' = get t k
theorem Std.DTreeMap.Const.get_insertMany_list_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) l) {h' : k' insertMany t l} :
get (insertMany t l) k' h' = v
theorem Std.DTreeMap.Const.get!_insertMany_list_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited β] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
get! (insertMany t l) k = get! t k
theorem Std.DTreeMap.Const.get!_insertMany_list_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) l) :
get! (insertMany t l) k' = v
theorem Std.DTreeMap.Const.getD_insertMany_list_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
getD (insertMany t l) k fallback = getD t k fallback
theorem Std.DTreeMap.Const.getD_insertMany_list_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v fallback : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) l) :
getD (insertMany t l) k' fallback = v
@[simp]
theorem Std.DTreeMap.Const.insertManyIfNewUnit_nil {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} :
@[simp]
theorem Std.DTreeMap.Const.insertManyIfNewUnit_list_singleton {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} {k : α} :
theorem Std.DTreeMap.Const.insertManyIfNewUnit_cons {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} {l : List α} {k : α} :
@[simp]
theorem Std.DTreeMap.Const.contains_insertManyIfNewUnit_list {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
@[simp]
theorem Std.DTreeMap.Const.mem_insertManyIfNewUnit_list {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
theorem Std.DTreeMap.Const.mem_of_mem_insertManyIfNewUnit_list {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
theorem Std.DTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
theorem Std.DTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) :
¬k tList.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) lk l(insertManyIfNewUnit t l).getKey? k' = some k
theorem Std.DTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_mem {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] {l : List α} {k : α} :
theorem Std.DTreeMap.Const.getKey_insertManyIfNewUnit_list_of_mem {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] {l : List α} {k : α} {h' : k insertManyIfNewUnit t l} (contains : k t) :
(insertManyIfNewUnit t l).getKey k h' = t.getKey k contains
theorem Std.DTreeMap.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {h' : k' insertManyIfNewUnit t l} :
¬k tList.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) lk l(insertManyIfNewUnit t l).getKey k' h' = k
theorem Std.DTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α} :
theorem Std.DTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) :
¬k tList.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) lk l(insertManyIfNewUnit t l).getKey! k' = k
theorem Std.DTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_mem {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [Inhabited α] {l : List α} {k : α} :
theorem Std.DTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k fallback : α} :
¬k tl.contains k = false(insertManyIfNewUnit t l).getKeyD k fallback = fallback
theorem Std.DTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] {l : List α} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) :
¬k tList.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) lk l(insertManyIfNewUnit t l).getKeyD k' fallback = k
theorem Std.DTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_mem {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] {l : List α} {k fallback : α} :
k t(insertManyIfNewUnit t l).getKeyD k fallback = t.getKeyD k fallback
theorem Std.DTreeMap.Const.size_insertManyIfNewUnit_list {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) :
(∀ (a : α), a tl.contains a = false)(insertManyIfNewUnit t l).size = t.size + l.length
theorem Std.DTreeMap.Const.size_le_size_insertManyIfNewUnit_list {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] {l : List α} :
theorem Std.DTreeMap.Const.size_insertManyIfNewUnit_list_le {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] {l : List α} :
@[simp]
theorem Std.DTreeMap.Const.isEmpty_insertManyIfNewUnit_list {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] {l : List α} :
@[simp]
theorem Std.DTreeMap.Const.get?_insertManyIfNewUnit_list {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
@[simp]
theorem Std.DTreeMap.Const.get_insertManyIfNewUnit_list {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} {l : List α} {k : α} {h' : k insertManyIfNewUnit t l} :
@[simp]
theorem Std.DTreeMap.Const.get!_insertManyIfNewUnit_list {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} {l : List α} {k : α} :
@[simp]
theorem Std.DTreeMap.Const.getD_insertManyIfNewUnit_list {α : Type u} {cmp : ααOrdering} {t : DTreeMap α (fun (x : α) => Unit) cmp} {l : List α} {k : α} {fallback : Unit} :
getD (insertManyIfNewUnit t l) k fallback = ()
@[simp]
theorem Std.DTreeMap.ofList_nil {α : Type u} {β : αType v} {cmp : ααOrdering} :
@[simp]
theorem Std.DTreeMap.ofList_singleton {α : Type u} {β : αType v} {cmp : ααOrdering} {k : α} {v : β k} :
ofList [k, v] cmp = .insert k v
theorem Std.DTreeMap.ofList_cons {α : Type u} {β : αType v} {cmp : ααOrdering} {k : α} {v : β k} {tl : List ((a : α) × β a)} :
ofList (k, v :: tl) cmp = (.insert k v).insertMany tl
theorem Std.DTreeMap.ofList_eq_insertMany_empty {α : Type u} {β : αType v} {cmp : ααOrdering} {l : List ((a : α) × β a)} :
@[simp]
theorem Std.DTreeMap.contains_ofList {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} :
@[simp]
theorem Std.DTreeMap.mem_ofList {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} :
theorem Std.DTreeMap.get?_ofList_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(ofList l cmp).get? k = none
theorem Std.DTreeMap.get?_ofList_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k, v l) :
(ofList l cmp).get? k' = some (cast v)
theorem Std.DTreeMap.get_ofList_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k, v l) {h : k' ofList l cmp} :
(ofList l cmp).get k' h = cast v
theorem Std.DTreeMap.get!_ofList_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(ofList l cmp).get! k = default
theorem Std.DTreeMap.get!_ofList_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} [Inhabited (β k')] (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k, v l) :
(ofList l cmp).get! k' = cast v
theorem Std.DTreeMap.getD_ofList_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(ofList l cmp).getD k fallback = fallback
theorem Std.DTreeMap.getD_ofList_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [LawfulEqCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} {fallback : β k'} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k, v l) :
(ofList l cmp).getD k' fallback = cast v
theorem Std.DTreeMap.getKey?_ofList_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(ofList l cmp).getKey? k = none
theorem Std.DTreeMap.getKey?_ofList_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Sigma.fst l) :
(ofList l cmp).getKey? k' = some k
theorem Std.DTreeMap.getKey_ofList_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Sigma.fst l) {h' : k' ofList l cmp} :
(ofList l cmp).getKey k' h' = k
theorem Std.DTreeMap.getKey!_ofList_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [Inhabited α] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
theorem Std.DTreeMap.getKey!_ofList_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [Inhabited α] {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Sigma.fst l) :
(ofList l cmp).getKey! k' = k
theorem Std.DTreeMap.getKeyD_ofList_of_contains_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k fallback : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false) :
(ofList l cmp).getKeyD k fallback = fallback
theorem Std.DTreeMap.getKeyD_ofList_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] {l : List ((a : α) × β a)} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Sigma.fst l) :
(ofList l cmp).getKeyD k' fallback = k
theorem Std.DTreeMap.size_ofList {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] {l : List ((a : α) × β a)} (distinct : List.Pairwise (fun (a b : (a : α) × β a) => ¬cmp a.fst b.fst = Ordering.eq) l) :
(ofList l cmp).size = l.length
theorem Std.DTreeMap.size_ofList_le {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] {l : List ((a : α) × β a)} :
@[simp]
theorem Std.DTreeMap.isEmpty_ofList {α : Type u} {β : αType v} {cmp : ααOrdering} [TransCmp cmp] {l : List ((a : α) × β a)} :
@[simp]
theorem Std.DTreeMap.Const.ofList_nil {α : Type u} {cmp : ααOrdering} {β : Type v} :
@[simp]
theorem Std.DTreeMap.Const.ofList_singleton {α : Type u} {cmp : ααOrdering} {β : Type v} {k : α} {v : β} :
ofList [(k, v)] cmp = .insert k v
theorem Std.DTreeMap.Const.ofList_cons {α : Type u} {cmp : ααOrdering} {β : Type v} {k : α} {v : β} {tl : List (α × β)} :
ofList ((k, v) :: tl) cmp = insertMany (.insert k v) tl
theorem Std.DTreeMap.Const.ofList_eq_insertMany_empty {α : Type u} {cmp : ααOrdering} {β : Type v} {l : List (α × β)} :
@[simp]
theorem Std.DTreeMap.Const.contains_ofList {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
@[simp]
theorem Std.DTreeMap.Const.mem_ofList {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} :
theorem Std.DTreeMap.Const.get?_ofList_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
get? (ofList l cmp) k = none
theorem Std.DTreeMap.Const.get?_ofList_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) l) :
get? (ofList l cmp) k' = some v
theorem Std.DTreeMap.Const.get_ofList_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) l) {h : k' ofList l cmp} :
get (ofList l cmp) k' h = v
theorem Std.DTreeMap.Const.get!_ofList_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} [Inhabited β] (contains_eq_false : (List.map Prod.fst l).contains k = false) :
get! (ofList l cmp) k = default
theorem Std.DTreeMap.Const.get!_ofList_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β} [Inhabited β] (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) l) :
get! (ofList l cmp) k' = v
theorem Std.DTreeMap.Const.getD_ofList_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
getD (ofList l cmp) k fallback = fallback
theorem Std.DTreeMap.Const.getD_ofList_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v fallback : β} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : (k, v) l) :
getD (ofList l cmp) k' fallback = v
theorem Std.DTreeMap.Const.getKey?_ofList_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(ofList l cmp).getKey? k = none
theorem Std.DTreeMap.Const.getKey?_ofList_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Prod.fst l) :
(ofList l cmp).getKey? k' = some k
theorem Std.DTreeMap.Const.getKey_ofList_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Prod.fst l) {h' : k' ofList l cmp} :
(ofList l cmp).getKey k' h' = k
theorem Std.DTreeMap.Const.getKey!_ofList_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
theorem Std.DTreeMap.Const.getKey!_ofList_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] [Inhabited α] {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Prod.fst l) :
(ofList l cmp).getKey! k' = k
theorem Std.DTreeMap.Const.getKeyD_ofList_of_contains_eq_false {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k fallback : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) :
(ofList l cmp).getKeyD k fallback = fallback
theorem Std.DTreeMap.Const.getKeyD_ofList_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] {l : List (α × β)} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) (mem : k List.map Prod.fst l) :
(ofList l cmp).getKeyD k' fallback = k
theorem Std.DTreeMap.Const.size_ofList {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] {l : List (α × β)} (distinct : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) l) :
(ofList l cmp).size = l.length
theorem Std.DTreeMap.Const.size_ofList_le {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] {l : List (α × β)} :
(ofList l cmp).size l.length
@[simp]
theorem Std.DTreeMap.Const.isEmpty_ofList {α : Type u} {cmp : ααOrdering} {β : Type v} [TransCmp cmp] {l : List (α × β)} :
@[simp]
theorem Std.DTreeMap.Const.unitOfList_nil {α : Type u} {cmp : ααOrdering} :
@[simp]
theorem Std.DTreeMap.Const.unitOfList_singleton {α : Type u} {cmp : ααOrdering} {k : α} :
theorem Std.DTreeMap.Const.unitOfList_cons {α : Type u} {cmp : ααOrdering} {hd : α} {tl : List α} :
@[simp]
theorem Std.DTreeMap.Const.contains_unitOfList {α : Type u} {cmp : ααOrdering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
@[simp]
theorem Std.DTreeMap.Const.mem_unitOfList {α : Type u} {cmp : ααOrdering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
theorem Std.DTreeMap.Const.getKey?_unitOfList_of_contains_eq_false {α : Type u} {cmp : ααOrdering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
theorem Std.DTreeMap.Const.getKey?_unitOfList_of_mem {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k l) :
(unitOfList l cmp).getKey? k' = some k
theorem Std.DTreeMap.Const.getKey_unitOfList_of_mem {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k l) {h' : k' unitOfList l cmp} :
(unitOfList l cmp).getKey k' h' = k
theorem Std.DTreeMap.Const.getKey!_unitOfList_of_contains_eq_false {α : Type u} {cmp : ααOrdering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) :
theorem Std.DTreeMap.Const.getKey!_unitOfList_of_mem {α : Type u} {cmp : ααOrdering} [TransCmp cmp] [Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k l) :
(unitOfList l cmp).getKey! k' = k
theorem Std.DTreeMap.Const.getKeyD_unitOfList_of_contains_eq_false {α : Type u} {cmp : ααOrdering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k fallback : α} (contains_eq_false : l.contains k = false) :
(unitOfList l cmp).getKeyD k fallback = fallback
theorem Std.DTreeMap.Const.getKeyD_unitOfList_of_mem {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {l : List α} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k l) :
(unitOfList l cmp).getKeyD k' fallback = k
theorem Std.DTreeMap.Const.size_unitOfList {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {l : List α} (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) :
theorem Std.DTreeMap.Const.size_unitOfList_le {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {l : List α} :
@[simp]
theorem Std.DTreeMap.Const.isEmpty_unitOfList {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {l : List α} :
@[simp]
theorem Std.DTreeMap.Const.get?_unitOfList {α : Type u} {cmp : ααOrdering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
@[simp]
theorem Std.DTreeMap.Const.get_unitOfList {α : Type u} {cmp : ααOrdering} {l : List α} {k : α} {h : k unitOfList l cmp} :
get (unitOfList l cmp) k h = ()
@[simp]
theorem Std.DTreeMap.Const.get!_unitOfList {α : Type u} {cmp : ααOrdering} {l : List α} {k : α} :
get! (unitOfList l cmp) k = ()
@[simp]
theorem Std.DTreeMap.Const.getD_unitOfList {α : Type u} {cmp : ααOrdering} {l : List α} {k : α} {fallback : Unit} :
getD (unitOfList l cmp) k fallback = ()
theorem Std.DTreeMap.isEmpty_alter_eq_isEmpty_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} :
(t.alter k f).isEmpty = ((t.erase k).isEmpty && (f (t.get? k)).isNone)
@[simp]
theorem Std.DTreeMap.isEmpty_alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} :
(t.alter k f).isEmpty = ((t.isEmpty || t.size == 1 && t.contains k) && (f (t.get? k)).isNone)
theorem Std.DTreeMap.contains_alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : Option (β k)Option (β k)} :
(t.alter k f).contains k' = if cmp k k' = Ordering.eq then (f (t.get? k)).isSome else t.contains k'
theorem Std.DTreeMap.mem_alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : Option (β k)Option (β k)} :
k' t.alter k f if cmp k k' = Ordering.eq then (f (t.get? k)).isSome = true else k' t
theorem Std.DTreeMap.mem_alter_of_compare_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : Option (β k)Option (β k)} (he : cmp k k' = Ordering.eq) :
k' t.alter k f (f (t.get? k)).isSome = true
@[simp]
theorem Std.DTreeMap.contains_alter_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} :
(t.alter k f).contains k = (f (t.get? k)).isSome
@[simp]
theorem Std.DTreeMap.mem_alter_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} :
k t.alter k f (f (t.get? k)).isSome = true
theorem Std.DTreeMap.contains_alter_of_not_compare_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : Option (β k)Option (β k)} (he : ¬cmp k k' = Ordering.eq) :
(t.alter k f).contains k' = t.contains k'
theorem Std.DTreeMap.mem_alter_of_not_compare_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : Option (β k)Option (β k)} (he : ¬cmp k k' = Ordering.eq) :
k' t.alter k f k' t
theorem Std.DTreeMap.size_alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} :
(t.alter k f).size = if k t (f (t.get? k)).isNone = true then t.size - 1 else if ¬k t (f (t.get? k)).isSome = true then t.size + 1 else t.size
theorem Std.DTreeMap.size_alter_eq_add_one {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} (h₁ : ¬k t) (h₂ : (f (t.get? k)).isSome = true) :
(t.alter k f).size = t.size + 1
theorem Std.DTreeMap.size_alter_eq_sub_one {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} (h₁ : k t) (h₂ : (f (t.get? k)).isNone = true) :
(t.alter k f).size = t.size - 1
theorem Std.DTreeMap.size_alter_eq_self_of_not_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} (h₁ : ¬k t) (h₂ : (f (t.get? k)).isNone = true) :
(t.alter k f).size = t.size
theorem Std.DTreeMap.size_alter_eq_self_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} (h₁ : k t) (h₂ : (f (t.get? k)).isSome = true) :
(t.alter k f).size = t.size
theorem Std.DTreeMap.size_alter_le_size {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} :
(t.alter k f).size t.size + 1
theorem Std.DTreeMap.size_le_size_alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} :
t.size - 1 (t.alter k f).size
theorem Std.DTreeMap.get?_alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : Option (β k)Option (β k)} :
(t.alter k f).get? k' = if h : cmp k k' = Ordering.eq then cast (f (t.get? k)) else t.get? k'
@[simp]
theorem Std.DTreeMap.get?_alter_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} :
(t.alter k f).get? k = f (t.get? k)
theorem Std.DTreeMap.get_alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : Option (β k)Option (β k)} {hc : k' t.alter k f} :
(t.alter k f).get k' hc = if heq : cmp k k' = Ordering.eq then cast ((f (t.get? k)).get ) else t.get k'
@[simp]
theorem Std.DTreeMap.get_alter_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} {hc : k t.alter k f} :
(t.alter k f).get k hc = (f (t.get? k)).get
theorem Std.DTreeMap.get!_alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} [Inhabited (β k')] {f : Option (β k)Option (β k)} :
(t.alter k f).get! k' = if heq : cmp k k' = Ordering.eq then (Option.map (cast ) (f (t.get? k))).get! else t.get! k'
@[simp]
theorem Std.DTreeMap.get!_alter_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} [Inhabited (β k)] {f : Option (β k)Option (β k)} :
(t.alter k f).get! k = (f (t.get? k)).get!
theorem Std.DTreeMap.getD_alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {fallback : β k'} {f : Option (β k)Option (β k)} :
(t.alter k f).getD k' fallback = if heq : cmp k k' = Ordering.eq then (Option.map (cast ) (f (t.get? k))).getD fallback else t.getD k' fallback
@[simp]
theorem Std.DTreeMap.getD_alter_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {fallback : β k} {f : Option (β k)Option (β k)} :
(t.alter k f).getD k fallback = (f (t.get? k)).getD fallback
theorem Std.DTreeMap.getKey?_alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : Option (β k)Option (β k)} :
(t.alter k f).getKey? k' = if cmp k k' = Ordering.eq then if (f (t.get? k)).isSome = true then some k else none else t.getKey? k'
theorem Std.DTreeMap.getKey?_alter_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} :
(t.alter k f).getKey? k = if (f (t.get? k)).isSome = true then some k else none
theorem Std.DTreeMap.getKey!_alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k k' : α} {f : Option (β k)Option (β k)} :
(t.alter k f).getKey! k' = if cmp k k' = Ordering.eq then if (f (t.get? k)).isSome = true then k else default else t.getKey! k'
theorem Std.DTreeMap.getKey!_alter_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} {f : Option (β k)Option (β k)} :
(t.alter k f).getKey! k = if (f (t.get? k)).isSome = true then k else default
@[deprecated Std.DTreeMap.getKey_eq (since := "2025-01-05")]
theorem Std.DTreeMap.getKey_alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k k' : α} {f : Option (β k)Option (β k)} {hc : k' t.alter k f} :
(t.alter k f).getKey k' hc = if heq : cmp k k' = Ordering.eq then k else t.getKey k'
@[simp]
theorem Std.DTreeMap.getKey_alter_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} {f : Option (β k)Option (β k)} {hc : k t.alter k f} :
(t.alter k f).getKey k hc = k
theorem Std.DTreeMap.getKeyD_alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' fallback : α} {f : Option (β k)Option (β k)} :
(t.alter k f).getKeyD k' fallback = if cmp k k' = Ordering.eq then if (f (t.get? k)).isSome = true then k else fallback else t.getKeyD k' fallback
@[simp]
theorem Std.DTreeMap.getKeyD_alter_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k fallback : α} {f : Option (β k)Option (β k)} :
(t.alter k f).getKeyD k fallback = if (f (t.get? k)).isSome = true then k else fallback
theorem Std.DTreeMap.Const.isEmpty_alter_eq_isEmpty_erase {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} :
(alter t k f).isEmpty = ((t.erase k).isEmpty && (f (get? t k)).isNone)
@[simp]
theorem Std.DTreeMap.Const.isEmpty_alter {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} :
(alter t k f).isEmpty = ((t.isEmpty || t.size == 1 && t.contains k) && (f (get? t k)).isNone)
theorem Std.DTreeMap.Const.contains_alter {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k k' : α} {f : Option βOption β} :
(alter t k f).contains k' = if cmp k k' = Ordering.eq then (f (get? t k)).isSome else t.contains k'
theorem Std.DTreeMap.Const.mem_alter {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k k' : α} {f : Option βOption β} :
k' alter t k f if cmp k k' = Ordering.eq then (f (get? t k)).isSome = true else k' t
theorem Std.DTreeMap.Const.mem_alter_of_compare_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k k' : α} {f : Option βOption β} (he : cmp k k' = Ordering.eq) :
k' alter t k f (f (get? t k)).isSome = true
@[simp]
theorem Std.DTreeMap.Const.contains_alter_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} :
(alter t k f).contains k = (f (get? t k)).isSome
@[simp]
theorem Std.DTreeMap.Const.mem_alter_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} :
k alter t k f (f (get? t k)).isSome = true
theorem Std.DTreeMap.Const.contains_alter_of_not_compare_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k k' : α} {f : Option βOption β} (he : ¬cmp k k' = Ordering.eq) :
(alter t k f).contains k' = t.contains k'
theorem Std.DTreeMap.Const.mem_alter_of_not_compare_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k k' : α} {f : Option βOption β} (he : ¬cmp k k' = Ordering.eq) :
k' alter t k f k' t
theorem Std.DTreeMap.Const.size_alter {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} :
(alter t k f).size = if k t (f (get? t k)).isNone = true then t.size - 1 else if ¬k t (f (get? t k)).isSome = true then t.size + 1 else t.size
theorem Std.DTreeMap.Const.size_alter_eq_add_one {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} (h₁ : ¬k t) (h₂ : (f (get? t k)).isSome = true) :
(alter t k f).size = t.size + 1
theorem Std.DTreeMap.Const.size_alter_eq_sub_one {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} (h₁ : k t) (h₂ : (f (get? t k)).isNone = true) :
(alter t k f).size = t.size - 1
theorem Std.DTreeMap.Const.size_alter_eq_self_of_not_mem {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} (h₁ : ¬k t) (h₂ : (f (get? t k)).isNone = true) :
(alter t k f).size = t.size
theorem Std.DTreeMap.Const.size_alter_eq_self_of_mem {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} (h₁ : k t) (h₂ : (f (get? t k)).isSome = true) :
(alter t k f).size = t.size
theorem Std.DTreeMap.Const.size_alter_le_size {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} :
(alter t k f).size t.size + 1
theorem Std.DTreeMap.Const.size_le_size_alter {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} :
t.size - 1 (alter t k f).size
theorem Std.DTreeMap.Const.get?_alter {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k k' : α} {f : Option βOption β} :
get? (alter t k f) k' = if cmp k k' = Ordering.eq then f (get? t k) else get? t k'
@[simp]
theorem Std.DTreeMap.Const.get?_alter_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} :
get? (alter t k f) k = f (get? t k)
theorem Std.DTreeMap.Const.get_alter {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k k' : α} {f : Option βOption β} {hc : k' alter t k f} :
get (alter t k f) k' hc = if heq : cmp k k' = Ordering.eq then (f (get? t k)).get else get t k'
@[simp]
theorem Std.DTreeMap.Const.get_alter_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} {hc : k alter t k f} :
get (alter t k f) k hc = (f (get? t k)).get
theorem Std.DTreeMap.Const.get!_alter {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k k' : α} [Inhabited β] {f : Option βOption β} :
get! (alter t k f) k' = if cmp k k' = Ordering.eq then (f (get? t k)).get! else get! t k'
@[simp]
theorem Std.DTreeMap.Const.get!_alter_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} [Inhabited β] {f : Option βOption β} :
get! (alter t k f) k = (f (get? t k)).get!
theorem Std.DTreeMap.Const.getD_alter {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k k' : α} {fallback : β} {f : Option βOption β} :
getD (alter t k f) k' fallback = if cmp k k' = Ordering.eq then (f (get? t k)).getD fallback else getD t k' fallback
@[simp]
theorem Std.DTreeMap.Const.getD_alter_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {fallback : β} {f : Option βOption β} :
getD (alter t k f) k fallback = (f (get? t k)).getD fallback
theorem Std.DTreeMap.Const.getKey?_alter {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k k' : α} {f : Option βOption β} :
(alter t k f).getKey? k' = if cmp k k' = Ordering.eq then if (f (get? t k)).isSome = true then some k else none else t.getKey? k'
theorem Std.DTreeMap.Const.getKey?_alter_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} :
(alter t k f).getKey? k = if (f (get? t k)).isSome = true then some k else none
theorem Std.DTreeMap.Const.getKey!_alter {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited α] {k k' : α} {f : Option βOption β} :
(alter t k f).getKey! k' = if cmp k k' = Ordering.eq then if (f (get? t k)).isSome = true then k else default else t.getKey! k'
theorem Std.DTreeMap.Const.getKey!_alter_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited α] {k : α} {f : Option βOption β} :
(alter t k f).getKey! k = if (f (get? t k)).isSome = true then k else default
theorem Std.DTreeMap.Const.getKey_alter {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited α] {k k' : α} {f : Option βOption β} {hc : k' alter t k f} :
(alter t k f).getKey k' hc = if heq : cmp k k' = Ordering.eq then k else t.getKey k'
@[simp]
theorem Std.DTreeMap.Const.getKey_alter_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited α] {k : α} {f : Option βOption β} {hc : k alter t k f} :
(alter t k f).getKey k hc = k
theorem Std.DTreeMap.Const.getKeyD_alter {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k k' fallback : α} {f : Option βOption β} :
(alter t k f).getKeyD k' fallback = if cmp k k' = Ordering.eq then if (f (get? t k)).isSome = true then k else fallback else t.getKeyD k' fallback
@[simp]
theorem Std.DTreeMap.Const.getKeyD_alter_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited α] {k fallback : α} {f : Option βOption β} :
(alter t k f).getKeyD k fallback = if (f (get? t k)).isSome = true then k else fallback
@[simp]
theorem Std.DTreeMap.isEmpty_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : β kβ k} :
theorem Std.DTreeMap.contains_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : β kβ k} :
(t.modify k f).contains k' = t.contains k'
theorem Std.DTreeMap.mem_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : β kβ k} :
k' t.modify k f k' t
theorem Std.DTreeMap.size_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : β kβ k} :
(t.modify k f).size = t.size
theorem Std.DTreeMap.get?_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : β kβ k} :
(t.modify k f).get? k' = if h : cmp k k' = Ordering.eq then cast (Option.map f (t.get? k)) else t.get? k'
@[simp]
theorem Std.DTreeMap.get?_modify_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : β kβ k} :
(t.modify k f).get? k = Option.map f (t.get? k)
theorem Std.DTreeMap.get_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : β kβ k} {hc : k' t.modify k f} :
(t.modify k f).get k' hc = if heq : cmp k k' = Ordering.eq then cast (f (t.get k )) else t.get k'
@[simp]
theorem Std.DTreeMap.get_modify_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : β kβ k} {hc : k t.modify k f} :
(t.modify k f).get k hc = f (t.get k )
theorem Std.DTreeMap.get!_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} [hi : Inhabited (β k')] {f : β kβ k} :
(t.modify k f).get! k' = if heq : cmp k k' = Ordering.eq then (Option.map (cast ) (Option.map f (t.get? k))).get! else t.get! k'
@[simp]
theorem Std.DTreeMap.get!_modify_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} [Inhabited (β k)] {f : β kβ k} :
(t.modify k f).get! k = (Option.map f (t.get? k)).get!
theorem Std.DTreeMap.getD_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {fallback : β k'} {f : β kβ k} :
(t.modify k f).getD k' fallback = if heq : cmp k k' = Ordering.eq then (Option.map (cast ) (Option.map f (t.get? k))).getD fallback else t.getD k' fallback
@[simp]
theorem Std.DTreeMap.getD_modify_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {fallback : β k} {f : β kβ k} :
(t.modify k f).getD k fallback = (Option.map f (t.get? k)).getD fallback
theorem Std.DTreeMap.getKey?_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' : α} {f : β kβ k} :
(t.modify k f).getKey? k' = if cmp k k' = Ordering.eq then if k t then some k else none else t.getKey? k'
theorem Std.DTreeMap.getKey?_modify_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : β kβ k} :
(t.modify k f).getKey? k = if k t then some k else none
theorem Std.DTreeMap.getKey!_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k k' : α} {f : β kβ k} :
(t.modify k f).getKey! k' = if cmp k k' = Ordering.eq then if k t then k else default else t.getKey! k'
theorem Std.DTreeMap.getKey!_modify_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} {f : β kβ k} :
(t.modify k f).getKey! k = if k t then k else default
theorem Std.DTreeMap.getKey_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k k' : α} {f : β kβ k} {hc : k' t.modify k f} :
(t.modify k f).getKey k' hc = if cmp k k' = Ordering.eq then k else t.getKey k'
@[simp]
theorem Std.DTreeMap.getKey_modify_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} {f : β kβ k} {hc : k t.modify k f} :
(t.modify k f).getKey k hc = k
theorem Std.DTreeMap.getKeyD_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k k' fallback : α} {f : β kβ k} :
(t.modify k f).getKeyD k' fallback = if cmp k k' = Ordering.eq then if k t then k else fallback else t.getKeyD k' fallback
theorem Std.DTreeMap.getKeyD_modify_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k fallback : α} {f : β kβ k} :
(t.modify k f).getKeyD k fallback = if k t then k else fallback
@[simp]
theorem Std.DTreeMap.Const.isEmpty_modify {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k : α} {f : ββ} :
theorem Std.DTreeMap.Const.contains_modify {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k k' : α} {f : ββ} :
(modify t k f).contains k' = t.contains k'
theorem Std.DTreeMap.Const.mem_modify {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k k' : α} {f : ββ} :
k' modify t k f k' t
theorem Std.DTreeMap.Const.size_modify {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k : α} {f : ββ} :
(modify t k f).size = t.size
theorem Std.DTreeMap.Const.get?_modify {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k k' : α} {f : ββ} :
get? (modify t k f) k' = if cmp k k' = Ordering.eq then Option.map f (get? t k) else get? t k'
@[simp]
theorem Std.DTreeMap.Const.get?_modify_self {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k : α} {f : ββ} :
get? (modify t k f) k = Option.map f (get? t k)
theorem Std.DTreeMap.Const.get_modify {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k k' : α} {f : ββ} {hc : k' modify t k f} :
get (modify t k f) k' hc = if heq : cmp k k' = Ordering.eq then f (get t k ) else get t k'
@[simp]
theorem Std.DTreeMap.Const.get_modify_self {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k : α} {f : ββ} {hc : k modify t k f} :
get (modify t k f) k hc = f (get t k )
theorem Std.DTreeMap.Const.get!_modify {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k k' : α} [hi : Inhabited β] {f : ββ} :
get! (modify t k f) k' = if cmp k k' = Ordering.eq then (Option.map f (get? t k)).get! else get! t k'
@[simp]
theorem Std.DTreeMap.Const.get!_modify_self {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k : α} [Inhabited β] {f : ββ} :
get! (modify t k f) k = (Option.map f (get? t k)).get!
theorem Std.DTreeMap.Const.getD_modify {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k k' : α} {fallback : β} {f : ββ} :
getD (modify t k f) k' fallback = if cmp k k' = Ordering.eq then (Option.map f (get? t k)).getD fallback else getD t k' fallback
@[simp]
theorem Std.DTreeMap.Const.getD_modify_self {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k : α} {fallback : β} {f : ββ} :
getD (modify t k f) k fallback = (Option.map f (get? t k)).getD fallback
theorem Std.DTreeMap.Const.getKey?_modify {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k k' : α} {f : ββ} :
(modify t k f).getKey? k' = if cmp k k' = Ordering.eq then if k t then some k else none else t.getKey? k'
theorem Std.DTreeMap.Const.getKey?_modify_self {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k : α} {f : ββ} :
(modify t k f).getKey? k = if k t then some k else none
theorem Std.DTreeMap.Const.getKey!_modify {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Inhabited α] {k k' : α} {f : ββ} :
(modify t k f).getKey! k' = if cmp k k' = Ordering.eq then if k t then k else default else t.getKey! k'
theorem Std.DTreeMap.Const.getKey!_modify_self {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Inhabited α] {k : α} {f : ββ} :
(modify t k f).getKey! k = if k t then k else default
theorem Std.DTreeMap.Const.getKey_modify {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Inhabited α] {k k' : α} {f : ββ} {hc : k' modify t k f} :
(modify t k f).getKey k' hc = if cmp k k' = Ordering.eq then k else t.getKey k'
@[simp]
theorem Std.DTreeMap.Const.getKey_modify_self {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Inhabited α] {k : α} {f : ββ} {hc : k modify t k f} :
(modify t k f).getKey k hc = k
theorem Std.DTreeMap.Const.getKeyD_modify {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} {k k' fallback : α} {f : ββ} :
(modify t k f).getKeyD k' fallback = if cmp k k' = Ordering.eq then if k t then k else fallback else t.getKeyD k' fallback
theorem Std.DTreeMap.Const.getKeyD_modify_self {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [Inhabited α] {k fallback : α} {f : ββ} :
(modify t k f).getKeyD k fallback = if k t then k else fallback
@[simp]
theorem Std.DTreeMap.minKey?_emptyc {α : Type u} {β : αType v} {cmp : ααOrdering} :
theorem Std.DTreeMap.minKey?_of_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = true) :
@[simp]
theorem Std.DTreeMap.minKey?_eq_none_iff {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
theorem Std.DTreeMap.minKey?_eq_some_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {km : α} :
t.minKey? = some km t.getKey? km = some km ∀ (k : α), k t(cmp km k).isLE = true
theorem Std.DTreeMap.minKey?_eq_some_iff_mem_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {km : α} :
t.minKey? = some km km t ∀ (k : α), k t(cmp km k).isLE = true
@[simp]
theorem Std.DTreeMap.isNone_minKey?_eq_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
@[simp]
theorem Std.DTreeMap.isSome_minKey?_eq_not_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
theorem Std.DTreeMap.isSome_minKey?_iff_isEmpty_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
theorem Std.DTreeMap.minKey?_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insert k v).minKey? = some (t.minKey?.elim k fun (k' : α) => if (cmp k k').isLE = true then k else k')
theorem Std.DTreeMap.isSome_minKey?_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
theorem Std.DTreeMap.minKey?_insert_le_minKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {km kmi : α} (hkm : t.minKey? = some km) (hkmi : (t.insert k v).minKey?.get = kmi) :
(cmp kmi km).isLE = true
theorem Std.DTreeMap.minKey?_insert_le_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {kmi : α} (hkmi : (t.insert k v).minKey?.get = kmi) :
(cmp kmi k).isLE = true
theorem Std.DTreeMap.contains_minKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {km : α} (hkm : t.minKey? = some km) :
theorem Std.DTreeMap.minKey?_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {km : α} (hkm : t.minKey? = some km) :
km t
theorem Std.DTreeMap.isSome_minKey?_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) :
theorem Std.DTreeMap.isSome_minKey?_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
k tt.minKey?.isSome = true
theorem Std.DTreeMap.minKey?_le_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k km : α} (hc : t.contains k = true) (hkm : t.minKey?.get = km) :
(cmp km k).isLE = true
theorem Std.DTreeMap.minKey?_le_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k km : α} (hc : k t) (hkm : t.minKey?.get = km) :
(cmp km k).isLE = true
theorem Std.DTreeMap.le_minKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
(∀ (k' : α), t.minKey? = some k'(cmp k k').isLE = true) ∀ (k' : α), k' t(cmp k k').isLE = true
theorem Std.DTreeMap.getKey?_minKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {km : α} (hkm : t.minKey? = some km) :
t.getKey? km = some km
theorem Std.DTreeMap.getKey_minKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {km : α} {hc : t.contains km = true} (hkm : t.minKey?.get = km) :
t.getKey km hc = km
theorem Std.DTreeMap.getKey!_minKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {km : α} (hkm : t.minKey? = some km) :
t.getKey! km = km
theorem Std.DTreeMap.getKeyD_minKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {km fallback : α} (hkm : t.minKey? = some km) :
t.getKeyD km fallback = km
@[simp]
theorem Std.DTreeMap.minKey?_bind_getKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
theorem Std.DTreeMap.minKey?_erase_eq_iff_not_compare_eq_minKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
(t.erase k).minKey? = t.minKey? ∀ {km : α}, t.minKey? = some km¬cmp k km = Ordering.eq
theorem Std.DTreeMap.minKey?_erase_eq_of_not_compare_eq_minKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hc : ∀ {km : α}, t.minKey? = some km¬cmp k km = Ordering.eq) :
theorem Std.DTreeMap.isSome_minKey?_of_isSome_minKey?_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hs : (t.erase k).minKey?.isSome = true) :
theorem Std.DTreeMap.minKey?_le_minKey?_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k km kme : α} (hkme : (t.erase k).minKey? = some kme) (hkm : t.minKey?.get = km) :
(cmp km kme).isLE = true
theorem Std.DTreeMap.minKey?_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insertIfNew k v).minKey? = some (t.minKey?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k')
theorem Std.DTreeMap.isSome_minKey?_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
theorem Std.DTreeMap.minKey?_insertIfNew_le_minKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {km kmi : α} (hkm : t.minKey? = some km) (hkmi : (t.insertIfNew k v).minKey?.get = kmi) :
(cmp kmi km).isLE = true
theorem Std.DTreeMap.minKey?_insertIfNew_le_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {kmi : α} (hkmi : (t.insertIfNew k v).minKey?.get = kmi) :
(cmp kmi k).isLE = true
theorem Std.DTreeMap.minKey?_eq_head?_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
@[simp]
theorem Std.DTreeMap.minKey?_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : β kβ k} :
theorem Std.DTreeMap.minKey?_alter_eq_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} :
(t.alter k f).minKey? = some k (f (t.get? k)).isSome = true ∀ (k' : α), k' t(cmp k k').isLE = true
theorem Std.DTreeMap.Const.minKey?_modify {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} :
(modify t k f).minKey? = Option.map (fun (km : α) => if cmp km k = Ordering.eq then k else km) t.minKey?
@[simp]
theorem Std.DTreeMap.Const.minKey?_modify_eq_minKey? {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : ββ} :
theorem Std.DTreeMap.Const.isSome_minKey?_modify {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} :
theorem Std.DTreeMap.Const.isSome_minKey?_modify_eq_isSome {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} :
theorem Std.DTreeMap.Const.compare_minKey?_modify_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} {km kmm : α} (hkm : t.minKey? = some km) (hkmm : (modify t k f).minKey?.get = kmm) :
cmp kmm km = Ordering.eq
theorem Std.DTreeMap.Const.minKey?_alter_eq_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} :
(alter t k f).minKey? = some k (f (get? t k)).isSome = true ∀ (k' : α), k' t(cmp k k').isLE = true
theorem Std.DTreeMap.minKey_eq_get_minKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} :
t.minKey he = t.minKey?.get
theorem Std.DTreeMap.minKey?_eq_some_minKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} :
t.minKey? = some (t.minKey he)
theorem Std.DTreeMap.minKey_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} {km : α} :
t.minKey he = km t.getKey? km = some km ∀ (k : α), k t(cmp km k).isLE = true
theorem Std.DTreeMap.minKey_eq_iff_mem_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {he : t.isEmpty = false} {km : α} :
t.minKey he = km km t ∀ (k : α), k t(cmp km k).isLE = true
theorem Std.DTreeMap.minKey_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insert k v).minKey = t.minKey?.elim k fun (k' : α) => if (cmp k k').isLE = true then k else k'
theorem Std.DTreeMap.minKey_insert_le_minKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {he : t.isEmpty = false} :
(cmp ((t.insert k v).minKey ) (t.minKey he)).isLE = true
theorem Std.DTreeMap.minKey_insert_le_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(cmp ((t.insert k v).minKey ) k).isLE = true
theorem Std.DTreeMap.contains_minKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} :
theorem Std.DTreeMap.minKey_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} :
t.minKey he t
theorem Std.DTreeMap.minKey_le_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) :
(cmp (t.minKey ) k).isLE = true
theorem Std.DTreeMap.minKey_le_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hc : k t) :
(cmp (t.minKey ) k).isLE = true
theorem Std.DTreeMap.le_minKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {he : t.isEmpty = false} :
(cmp k (t.minKey he)).isLE = true ∀ (k' : α), k' t(cmp k k').isLE = true
@[simp]
theorem Std.DTreeMap.getKey?_minKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} :
t.getKey? (t.minKey he) = some (t.minKey he)
@[simp]
theorem Std.DTreeMap.getKey_minKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} {hc : t.minKey he t} :
t.getKey (t.minKey he) hc = t.minKey he
@[simp]
theorem Std.DTreeMap.getKey!_minKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {he : t.isEmpty = false} :
t.getKey! (t.minKey he) = t.minKey he
@[simp]
theorem Std.DTreeMap.getKeyD_minKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} {fallback : α} :
t.getKeyD (t.minKey he) fallback = t.minKey he
@[simp]
theorem Std.DTreeMap.minKey_erase_eq_iff_not_compare_eq_minKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {he : (t.erase k).isEmpty = false} :
(t.erase k).minKey he = t.minKey ¬cmp k (t.minKey ) = Ordering.eq
theorem Std.DTreeMap.minKey_erase_eq_of_not_compare_eq_minKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {he : (t.erase k).isEmpty = false} (hc : ¬cmp k (t.minKey ) = Ordering.eq) :
(t.erase k).minKey he = t.minKey
theorem Std.DTreeMap.minKey_le_minKey_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {he : (t.erase k).isEmpty = false} :
(cmp (t.minKey ) ((t.erase k).minKey he)).isLE = true
theorem Std.DTreeMap.minKey_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insertIfNew k v).minKey = t.minKey?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'
theorem Std.DTreeMap.minKey_insertIfNew_le_minKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {he : t.isEmpty = false} :
(cmp ((t.insertIfNew k v).minKey ) (t.minKey he)).isLE = true
theorem Std.DTreeMap.minKey_insertIfNew_le_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(cmp ((t.insertIfNew k v).minKey ) k).isLE = true
theorem Std.DTreeMap.minKey_eq_head_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} :
t.minKey he = t.keys.head
@[simp]
theorem Std.DTreeMap.minKey_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : β kβ k} {he : (t.modify k f).isEmpty = false} :
(t.modify k f).minKey he = t.minKey
theorem Std.DTreeMap.minKey_alter_eq_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} {he : (t.alter k f).isEmpty = false} :
(t.alter k f).minKey he = k (f (t.get? k)).isSome = true ∀ (k' : α), k' t(cmp k k').isLE = true
theorem Std.DTreeMap.Const.minKey_modify {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} {he : (modify t k f).isEmpty = false} :
(modify t k f).minKey he = if cmp (t.minKey ) k = Ordering.eq then k else t.minKey
@[simp]
theorem Std.DTreeMap.Const.minKey_modify_eq_minKey {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : ββ} {he : (modify t k f).isEmpty = false} :
(modify t k f).minKey he = t.minKey
theorem Std.DTreeMap.Const.compare_minKey_modify_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} {he : (modify t k f).isEmpty = false} :
cmp ((modify t k f).minKey he) (t.minKey ) = Ordering.eq
@[simp]
theorem Std.DTreeMap.Const.ordCompare_minKey_modify_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : DTreeMap α (fun (x : α) => β) compare} {k : α} {f : ββ} {he : (modify t k f).isEmpty = false} :
compare ((modify t k f).minKey he) (t.minKey ) = Ordering.eq
theorem Std.DTreeMap.Const.minKey_alter_eq_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} {he : (alter t k f).isEmpty = false} :
(alter t k f).minKey he = k (f (get? t k)).isSome = true ∀ (k' : α), k' t(cmp k k').isLE = true
theorem Std.DTreeMap.minKey?_eq_some_minKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
theorem Std.DTreeMap.minKey_eq_minKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {he : t.isEmpty = false} :
theorem Std.DTreeMap.minKey!_eq_default {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = true) :
theorem Std.DTreeMap.minKey!_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {km : α} :
t.minKey! = km t.getKey? km = some km ∀ (k : α), k t(cmp km k).isLE = true
theorem Std.DTreeMap.minKey!_eq_iff_mem_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (he : t.isEmpty = false) {km : α} :
t.minKey! = km km t ∀ (k : α), k t(cmp km k).isLE = true
theorem Std.DTreeMap.minKey!_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} {v : β k} :
(t.insert k v).minKey! = t.minKey?.elim k fun (k' : α) => if (cmp k k').isLE = true then k else k'
theorem Std.DTreeMap.minKey!_insert_le_minKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k : α} {v : β k} :
(cmp (t.insert k v).minKey! t.minKey!).isLE = true
theorem Std.DTreeMap.minKey!_insert_le_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} {v : β k} :
(cmp (t.insert k v).minKey! k).isLE = true
theorem Std.DTreeMap.contains_minKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
theorem Std.DTreeMap.minKey!_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
theorem Std.DTreeMap.minKey!_le_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} (hc : t.contains k = true) :
(cmp t.minKey! k).isLE = true
theorem Std.DTreeMap.minKey!_le_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} (hc : k t) :
(cmp t.minKey! k).isLE = true
theorem Std.DTreeMap.le_minKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k : α} :
(cmp k t.minKey!).isLE = true ∀ (k' : α), k' t(cmp k k').isLE = true
theorem Std.DTreeMap.getKey?_minKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
theorem Std.DTreeMap.getKey_minKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {hc : t.minKey! t} :
@[simp]
theorem Std.DTreeMap.getKey_minKey!_eq_minKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {hc : t.minKey! t} :
t.getKey t.minKey! hc = t.minKey
theorem Std.DTreeMap.getKey!_minKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
theorem Std.DTreeMap.getKeyD_minKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {fallback : α} :
t.getKeyD t.minKey! fallback = t.minKey!
theorem Std.DTreeMap.minKey!_erase_eq_of_not_compare_minKey!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} (he : (t.erase k).isEmpty = false) (heq : ¬cmp k t.minKey! = Ordering.eq) :
theorem Std.DTreeMap.minKey!_le_minKey!_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} (he : (t.erase k).isEmpty = false) :
(cmp t.minKey! (t.erase k).minKey!).isLE = true
theorem Std.DTreeMap.minKey!_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} {v : β k} :
(t.insertIfNew k v).minKey! = t.minKey?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'
theorem Std.DTreeMap.minKey!_insertIfNew_le_minKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k : α} {v : β k} :
theorem Std.DTreeMap.minKey!_insertIfNew_le_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} {v : β k} :
(cmp (t.insertIfNew k v).minKey! k).isLE = true
theorem Std.DTreeMap.minKey!_eq_head!_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] :
@[simp]
theorem Std.DTreeMap.minKey!_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} {f : β kβ k} :
theorem Std.DTreeMap.minKey!_alter_eq_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} {f : Option (β k)Option (β k)} (he : (t.alter k f).isEmpty = false) :
(t.alter k f).minKey! = k (f (t.get? k)).isSome = true ∀ (k' : α), k' t(cmp k k').isLE = true
theorem Std.DTreeMap.Const.minKey!_modify {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited α] {k : α} {f : ββ} (he : (modify t k f).isEmpty = false) :
@[simp]
theorem Std.DTreeMap.Const.minKey!_modify_eq_minKey! {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} {f : ββ} :
theorem Std.DTreeMap.Const.compare_minKey!_modify_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited α] {k : α} {f : ββ} :
@[simp]
theorem Std.DTreeMap.Const.ordCompare_minKey!_modify_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : DTreeMap α (fun (x : α) => β) compare} [Inhabited α] {k : α} {f : ββ} :
theorem Std.DTreeMap.Const.minKey!_alter_eq_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited α] {k : α} {f : Option βOption β} (he : (alter t k f).isEmpty = false) :
(alter t k f).minKey! = k (f (get? t k)).isSome = true ∀ (k' : α), k' t(cmp k k').isLE = true
theorem Std.DTreeMap.minKey?_eq_some_minKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {fallback : α} :
t.minKey? = some (t.minKeyD fallback)
theorem Std.DTreeMap.minKeyD_eq_fallback {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = true) {fallback : α} :
t.minKeyD fallback = fallback
theorem Std.DTreeMap.minKey!_eq_minKeyD_default {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] :
theorem Std.DTreeMap.minKeyD_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {km fallback : α} :
t.minKeyD fallback = km t.getKey? km = some km ∀ (k : α), k t(cmp km k).isLE = true
theorem Std.DTreeMap.minKeyD_eq_iff_mem_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (he : t.isEmpty = false) {km fallback : α} :
t.minKeyD fallback = km km t ∀ (k : α), k t(cmp km k).isLE = true
theorem Std.DTreeMap.minKeyD_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {fallback : α} :
(t.insert k v).minKeyD fallback = t.minKey?.elim k fun (k' : α) => if (cmp k k').isLE = true then k else k'
theorem Std.DTreeMap.minKeyD_insert_le_minKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {k : α} {v : β k} {fallback : α} :
(cmp ((t.insert k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
theorem Std.DTreeMap.minKeyD_insert_le_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {fallback : α} :
(cmp ((t.insert k v).minKeyD fallback) k).isLE = true
theorem Std.DTreeMap.contains_minKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {fallback : α} :
t.contains (t.minKeyD fallback) = true
theorem Std.DTreeMap.minKeyD_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {fallback : α} :
t.minKeyD fallback t
theorem Std.DTreeMap.minKeyD_le_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) {fallback : α} :
(cmp (t.minKeyD fallback) k).isLE = true
theorem Std.DTreeMap.minKeyD_le_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hc : k t) {fallback : α} :
(cmp (t.minKeyD fallback) k).isLE = true
theorem Std.DTreeMap.le_minKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {k fallback : α} :
(cmp k (t.minKeyD fallback)).isLE = true ∀ (k' : α), k' t(cmp k k').isLE = true
theorem Std.DTreeMap.getKey?_minKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {fallback : α} :
t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback)
theorem Std.DTreeMap.getKey_minKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {fallback : α} {hc : t.minKeyD fallback t} :
t.getKey (t.minKeyD fallback) hc = t.minKeyD fallback
theorem Std.DTreeMap.getKey!_minKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {fallback : α} :
t.getKey! (t.minKeyD fallback) = t.minKeyD fallback
theorem Std.DTreeMap.getKeyD_minKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {fallback fallback' : α} :
t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback
theorem Std.DTreeMap.minKeyD_erase_eq_of_not_compare_minKeyD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k fallback : α} (he : (t.erase k).isEmpty = false) (heq : ¬cmp k (t.minKeyD fallback) = Ordering.eq) :
(t.erase k).minKeyD fallback = t.minKeyD fallback
theorem Std.DTreeMap.minKeyD_le_minKeyD_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (he : (t.erase k).isEmpty = false) {fallback : α} :
(cmp (t.minKeyD fallback) ((t.erase k).minKeyD fallback)).isLE = true
theorem Std.DTreeMap.minKeyD_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {fallback : α} :
(t.insertIfNew k v).minKeyD fallback = t.minKey?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'
theorem Std.DTreeMap.minKeyD_insertIfNew_le_minKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {k : α} {v : β k} {fallback : α} :
(cmp ((t.insertIfNew k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
theorem Std.DTreeMap.minKeyD_insertIfNew_le_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {fallback : α} :
(cmp ((t.insertIfNew k v).minKeyD fallback) k).isLE = true
theorem Std.DTreeMap.minKeyD_eq_headD_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {fallback : α} :
t.minKeyD fallback = t.keys.headD fallback
@[simp]
theorem Std.DTreeMap.minKeyD_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : β kβ k} {fallback : α} :
(t.modify k f).minKeyD fallback = t.minKeyD fallback
theorem Std.DTreeMap.minKeyD_alter_eq_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} (he : (t.alter k f).isEmpty = false) {fallback : α} :
(t.alter k f).minKeyD fallback = k (f (t.get? k)).isSome = true ∀ (k' : α), k' t(cmp k k').isLE = true
theorem Std.DTreeMap.Const.minKeyD_modify {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} (he : (modify t k f).isEmpty = false) {fallback : α} :
(modify t k f).minKeyD fallback = if cmp (t.minKeyD fallback) k = Ordering.eq then k else t.minKeyD fallback
@[simp]
theorem Std.DTreeMap.Const.minKeyD_modify_eq_minKeyD {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : ββ} {fallback : α} :
(modify t k f).minKeyD fallback = t.minKeyD fallback
theorem Std.DTreeMap.Const.compare_minKeyD_modify_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} {fallback : α} :
cmp ((modify t k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
@[simp]
theorem Std.DTreeMap.Const.ordCompare_minKeyD_modify_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : DTreeMap α (fun (x : α) => β) compare} {k : α} {f : ββ} {fallback : α} :
compare ((modify t k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
theorem Std.DTreeMap.Const.minKeyD_alter_eq_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} (he : (alter t k f).isEmpty = false) {fallback : α} :
(alter t k f).minKeyD fallback = k (f (get? t k)).isSome = true ∀ (k' : α), k' t(cmp k k').isLE = true
@[simp]
theorem Std.DTreeMap.maxKey?_emptyc {α : Type u} {β : αType v} {cmp : ααOrdering} :
theorem Std.DTreeMap.maxKey?_of_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = true) :
@[simp]
theorem Std.DTreeMap.maxKey?_eq_none_iff {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
theorem Std.DTreeMap.maxKey?_eq_some_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {km : α} :
t.maxKey? = some km t.getKey? km = some km ∀ (k : α), k t(cmp k km).isLE = true
theorem Std.DTreeMap.maxKey?_eq_some_iff_mem_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {km : α} :
t.maxKey? = some km km t ∀ (k : α), k t(cmp k km).isLE = true
@[simp]
theorem Std.DTreeMap.isNone_maxKey?_eq_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
@[simp]
theorem Std.DTreeMap.isSome_maxKey?_eq_not_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
theorem Std.DTreeMap.isSome_maxKey?_iff_isEmpty_eq_false {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
theorem Std.DTreeMap.maxKey?_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insert k v).maxKey? = some (t.maxKey?.elim k fun (k' : α) => if (cmp k' k).isLE = true then k else k')
theorem Std.DTreeMap.isSome_maxKey?_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
theorem Std.DTreeMap.maxKey?_le_maxKey?_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {km kmi : α} (hkm : t.maxKey? = some km) (hkmi : (t.insert k v).maxKey?.get = kmi) :
(cmp km kmi).isLE = true
theorem Std.DTreeMap.self_le_maxKey?_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {kmi : α} (hkmi : (t.insert k v).maxKey?.get = kmi) :
(cmp k kmi).isLE = true
theorem Std.DTreeMap.contains_maxKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {km : α} (hkm : t.maxKey? = some km) :
theorem Std.DTreeMap.maxKey?_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {km : α} (hkm : t.maxKey? = some km) :
km t
theorem Std.DTreeMap.isSome_maxKey?_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) :
theorem Std.DTreeMap.isSome_maxKey?_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
k tt.maxKey?.isSome = true
theorem Std.DTreeMap.le_maxKey?_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k km : α} (hc : t.contains k = true) (hkm : t.maxKey?.get = km) :
(cmp k km).isLE = true
theorem Std.DTreeMap.le_maxKey?_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k km : α} (hc : k t) (hkm : t.maxKey?.get = km) :
(cmp k km).isLE = true
theorem Std.DTreeMap.maxKey?_le {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
(∀ (k' : α), t.maxKey? = some k'(cmp k' k).isLE = true) ∀ (k' : α), k' t(cmp k' k).isLE = true
theorem Std.DTreeMap.getKey?_maxKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {km : α} (hkm : t.maxKey? = some km) :
t.getKey? km = some km
theorem Std.DTreeMap.getKey_maxKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {km : α} {hc : t.contains km = true} (hkm : t.maxKey?.get = km) :
t.getKey km hc = km
theorem Std.DTreeMap.getKey!_maxKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {km : α} (hkm : t.maxKey? = some km) :
t.getKey! km = km
theorem Std.DTreeMap.getKeyD_maxKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {km fallback : α} (hkm : t.maxKey? = some km) :
t.getKeyD km fallback = km
@[simp]
theorem Std.DTreeMap.maxKey?_bind_getKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
theorem Std.DTreeMap.maxKey?_erase_eq_iff_not_compare_eq_maxKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} :
(t.erase k).maxKey? = t.maxKey? ∀ {km : α}, t.maxKey? = some km¬cmp k km = Ordering.eq
theorem Std.DTreeMap.maxKey?_erase_eq_of_not_compare_eq_maxKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hc : ∀ {km : α}, t.maxKey? = some km¬cmp k km = Ordering.eq) :
theorem Std.DTreeMap.isSome_maxKey?_of_isSome_maxKey?_erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hs : (t.erase k).maxKey?.isSome = true) :
theorem Std.DTreeMap.maxKey?_erase_le_maxKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k km kme : α} (hkme : (t.erase k).maxKey? = some kme) (hkm : t.maxKey?.get = km) :
(cmp kme km).isLE = true
theorem Std.DTreeMap.maxKey?_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insertIfNew k v).maxKey? = some (t.maxKey?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k')
theorem Std.DTreeMap.isSome_maxKey?_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
theorem Std.DTreeMap.maxKey?_le_maxKey?_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {km kmi : α} (hkm : t.maxKey? = some km) (hkmi : (t.insertIfNew k v).maxKey?.get = kmi) :
(cmp km kmi).isLE = true
theorem Std.DTreeMap.self_le_maxKey?_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {kmi : α} (hkmi : (t.insertIfNew k v).maxKey?.get = kmi) :
(cmp k kmi).isLE = true
theorem Std.DTreeMap.maxKey?_eq_getLast?_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] :
@[simp]
theorem Std.DTreeMap.maxKey?_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : β kβ k} :
theorem Std.DTreeMap.maxKey?_alter_eq_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} :
(t.alter k f).maxKey? = some k (f (t.get? k)).isSome = true ∀ (k' : α), k' t(cmp k' k).isLE = true
theorem Std.DTreeMap.Const.maxKey?_modify {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} :
(modify t k f).maxKey? = Option.map (fun (km : α) => if cmp km k = Ordering.eq then k else km) t.maxKey?
@[simp]
theorem Std.DTreeMap.Const.maxKey?_modify_eq_maxKey? {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : ββ} :
theorem Std.DTreeMap.Const.isSome_maxKey?_modify {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} :
theorem Std.DTreeMap.Const.isSome_maxKey?_modify_eq_isSome {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} :
theorem Std.DTreeMap.Const.compare_maxKey?_modify_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} {km kmm : α} (hkm : t.maxKey? = some km) (hkmm : (modify t k f).maxKey?.get = kmm) :
cmp kmm km = Ordering.eq
theorem Std.DTreeMap.Const.maxKey?_alter_eq_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} :
(alter t k f).maxKey? = some k (f (get? t k)).isSome = true ∀ (k' : α), k' t(cmp k' k).isLE = true
theorem Std.DTreeMap.maxKey_eq_get_maxKey? {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} :
t.maxKey he = t.maxKey?.get
theorem Std.DTreeMap.maxKey?_eq_some_maxKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} :
t.maxKey? = some (t.maxKey he)
theorem Std.DTreeMap.maxKey_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} {km : α} :
t.maxKey he = km t.getKey? km = some km ∀ (k : α), k t(cmp k km).isLE = true
theorem Std.DTreeMap.maxKey_eq_iff_mem_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {he : t.isEmpty = false} {km : α} :
t.maxKey he = km km t ∀ (k : α), k t(cmp k km).isLE = true
theorem Std.DTreeMap.maxKey_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insert k v).maxKey = t.maxKey?.elim k fun (k' : α) => if (cmp k' k).isLE = true then k else k'
theorem Std.DTreeMap.maxKey_le_maxKey_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {he : t.isEmpty = false} :
(cmp (t.maxKey he) ((t.insert k v).maxKey )).isLE = true
theorem Std.DTreeMap.self_le_maxKey_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(cmp k ((t.insert k v).maxKey )).isLE = true
theorem Std.DTreeMap.contains_maxKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} :
theorem Std.DTreeMap.maxKey_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} :
t.maxKey he t
theorem Std.DTreeMap.le_maxKey_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) :
(cmp k (t.maxKey )).isLE = true
theorem Std.DTreeMap.le_maxKey_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hc : k t) :
(cmp k (t.maxKey )).isLE = true
theorem Std.DTreeMap.maxKey_le {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {he : t.isEmpty = false} :
(cmp (t.maxKey he) k).isLE = true ∀ (k' : α), k' t(cmp k' k).isLE = true
@[simp]
theorem Std.DTreeMap.getKey?_maxKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} :
t.getKey? (t.maxKey he) = some (t.maxKey he)
@[simp]
theorem Std.DTreeMap.getKey_maxKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} {hc : t.maxKey he t} :
t.getKey (t.maxKey he) hc = t.maxKey he
@[simp]
theorem Std.DTreeMap.getKey!_maxKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {he : t.isEmpty = false} :
t.getKey! (t.maxKey he) = t.maxKey he
@[simp]
theorem Std.DTreeMap.getKeyD_maxKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} {fallback : α} :
t.getKeyD (t.maxKey he) fallback = t.maxKey he
@[simp]
theorem Std.DTreeMap.maxKey_erase_eq_iff_not_compare_eq_maxKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {he : (t.erase k).isEmpty = false} :
(t.erase k).maxKey he = t.maxKey ¬cmp k (t.maxKey ) = Ordering.eq
theorem Std.DTreeMap.maxKey_erase_eq_of_not_compare_eq_maxKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {he : (t.erase k).isEmpty = false} (hc : ¬cmp k (t.maxKey ) = Ordering.eq) :
(t.erase k).maxKey he = t.maxKey
theorem Std.DTreeMap.maxKey_erase_le_maxKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {he : (t.erase k).isEmpty = false} :
(cmp ((t.erase k).maxKey he) (t.maxKey )).isLE = true
theorem Std.DTreeMap.maxKey_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(t.insertIfNew k v).maxKey = t.maxKey?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'
theorem Std.DTreeMap.maxKey_le_maxKey_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {he : t.isEmpty = false} :
(cmp (t.maxKey he) ((t.insertIfNew k v).maxKey )).isLE = true
theorem Std.DTreeMap.self_le_maxKey_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} :
(cmp k ((t.insertIfNew k v).maxKey )).isLE = true
theorem Std.DTreeMap.maxKey_eq_getLast_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {he : t.isEmpty = false} :
t.maxKey he = t.keys.getLast
@[simp]
theorem Std.DTreeMap.maxKey_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : β kβ k} {he : (t.modify k f).isEmpty = false} :
(t.modify k f).maxKey he = t.maxKey
theorem Std.DTreeMap.maxKey_alter_eq_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} {he : (t.alter k f).isEmpty = false} :
(t.alter k f).maxKey he = k (f (t.get? k)).isSome = true ∀ (k' : α), k' t(cmp k' k).isLE = true
theorem Std.DTreeMap.Const.maxKey_modify {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} {he : (modify t k f).isEmpty = false} :
(modify t k f).maxKey he = if cmp (t.maxKey ) k = Ordering.eq then k else t.maxKey
@[simp]
theorem Std.DTreeMap.Const.maxKey_modify_eq_maxKey {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : ββ} {he : (modify t k f).isEmpty = false} :
(modify t k f).maxKey he = t.maxKey
theorem Std.DTreeMap.Const.compare_maxKey_modify_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} {he : (modify t k f).isEmpty = false} :
cmp ((modify t k f).maxKey he) (t.maxKey ) = Ordering.eq
@[simp]
theorem Std.DTreeMap.Const.ordCompare_maxKey_modify_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : DTreeMap α (fun (x : α) => β) compare} {k : α} {f : ββ} {he : (modify t k f).isEmpty = false} :
compare ((modify t k f).maxKey he) (t.maxKey ) = Ordering.eq
theorem Std.DTreeMap.Const.maxKey_alter_eq_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} {he : (alter t k f).isEmpty = false} :
(alter t k f).maxKey he = k (f (get? t k)).isSome = true ∀ (k' : α), k' t(cmp k' k).isLE = true
theorem Std.DTreeMap.maxKey?_eq_some_maxKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
theorem Std.DTreeMap.maxKey_eq_maxKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {he : t.isEmpty = false} :
theorem Std.DTreeMap.maxKey!_eq_default {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = true) :
theorem Std.DTreeMap.maxKey!_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {km : α} :
t.maxKey! = km t.getKey? km = some km ∀ (k : α), k t(cmp k km).isLE = true
theorem Std.DTreeMap.maxKey!_eq_iff_mem_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (he : t.isEmpty = false) {km : α} :
t.maxKey! = km km t ∀ (k : α), k t(cmp k km).isLE = true
theorem Std.DTreeMap.maxKey!_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} {v : β k} :
(t.insert k v).maxKey! = t.maxKey?.elim k fun (k' : α) => if (cmp k' k).isLE = true then k else k'
theorem Std.DTreeMap.maxKey!_le_maxKey!_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k : α} {v : β k} :
(cmp t.maxKey! (t.insert k v).maxKey!).isLE = true
theorem Std.DTreeMap.self_le_maxKey!_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} {v : β k} :
(cmp k (t.insert k v).maxKey!).isLE = true
theorem Std.DTreeMap.contains_maxKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
theorem Std.DTreeMap.maxKey!_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
theorem Std.DTreeMap.le_maxKey!_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} (hc : t.contains k = true) :
(cmp k t.maxKey!).isLE = true
theorem Std.DTreeMap.le_maxKey!_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} (hc : k t) :
(cmp k t.maxKey!).isLE = true
theorem Std.DTreeMap.maxKey!_le {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k : α} :
(cmp t.maxKey! k).isLE = true ∀ (k' : α), k' t(cmp k' k).isLE = true
theorem Std.DTreeMap.getKey?_maxKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
theorem Std.DTreeMap.getKey_maxKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {hc : t.maxKey! t} :
@[simp]
theorem Std.DTreeMap.getKey_maxKey!_eq_maxKey {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {hc : t.maxKey! t} :
t.getKey t.maxKey! hc = t.maxKey
theorem Std.DTreeMap.getKey!_maxKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
theorem Std.DTreeMap.getKeyD_maxKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {fallback : α} :
t.getKeyD t.maxKey! fallback = t.maxKey!
theorem Std.DTreeMap.maxKey!_erase_eq_of_not_compare_maxKey!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} (he : (t.erase k).isEmpty = false) (heq : ¬cmp k t.maxKey! = Ordering.eq) :
theorem Std.DTreeMap.maxKey!_erase_le_maxKey! {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} (he : (t.erase k).isEmpty = false) :
(cmp (t.erase k).maxKey! t.maxKey!).isLE = true
theorem Std.DTreeMap.maxKey!_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} {v : β k} :
(t.insertIfNew k v).maxKey! = t.maxKey?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'
theorem Std.DTreeMap.maxKey!_le_maxKey!_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k : α} {v : β k} :
theorem Std.DTreeMap.self_le_maxKey!_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} {v : β k} :
(cmp k (t.insertIfNew k v).maxKey!).isLE = true
theorem Std.DTreeMap.maxKey!_eq_getLast!_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] :
@[simp]
theorem Std.DTreeMap.maxKey!_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} {f : β kβ k} :
theorem Std.DTreeMap.maxKey!_alter_eq_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} {f : Option (β k)Option (β k)} (he : (t.alter k f).isEmpty = false) :
(t.alter k f).maxKey! = k (f (t.get? k)).isSome = true ∀ (k' : α), k' t(cmp k' k).isLE = true
theorem Std.DTreeMap.Const.maxKey!_modify {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited α] {k : α} {f : ββ} (he : (modify t k f).isEmpty = false) :
@[simp]
theorem Std.DTreeMap.Const.maxKey!_modify_eq_maxKey! {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} {f : ββ} :
theorem Std.DTreeMap.Const.compare_maxKey!_modify_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited α] {k : α} {f : ββ} :
@[simp]
theorem Std.DTreeMap.Const.ordCompare_maxKey!_modify_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : DTreeMap α (fun (x : α) => β) compare} [Inhabited α] {k : α} {f : ββ} :
theorem Std.DTreeMap.Const.maxKey!_alter_eq_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited α] {k : α} {f : Option βOption β} (he : (alter t k f).isEmpty = false) :
(alter t k f).maxKey! = k (f (get? t k)).isSome = true ∀ (k' : α), k' t(cmp k' k).isLE = true
theorem Std.DTreeMap.maxKey?_eq_some_maxKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {fallback : α} :
t.maxKey? = some (t.maxKeyD fallback)
theorem Std.DTreeMap.maxKeyD_eq_fallback {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = true) {fallback : α} :
t.maxKeyD fallback = fallback
theorem Std.DTreeMap.maxKey!_eq_maxKeyD_default {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] :
theorem Std.DTreeMap.maxKeyD_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {km fallback : α} :
t.maxKeyD fallback = km t.getKey? km = some km ∀ (k : α), k t(cmp k km).isLE = true
theorem Std.DTreeMap.maxKeyD_eq_iff_mem_and_forall {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (he : t.isEmpty = false) {km fallback : α} :
t.maxKeyD fallback = km km t ∀ (k : α), k t(cmp k km).isLE = true
theorem Std.DTreeMap.maxKeyD_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {fallback : α} :
(t.insert k v).maxKeyD fallback = t.maxKey?.elim k fun (k' : α) => if (cmp k' k).isLE = true then k else k'
theorem Std.DTreeMap.maxKeyD_le_maxKeyD_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {k : α} {v : β k} {fallback : α} :
(cmp (t.maxKeyD fallback) ((t.insert k v).maxKeyD fallback)).isLE = true
theorem Std.DTreeMap.self_le_maxKeyD_insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {fallback : α} :
(cmp k ((t.insert k v).maxKeyD fallback)).isLE = true
theorem Std.DTreeMap.contains_maxKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {fallback : α} :
t.contains (t.maxKeyD fallback) = true
theorem Std.DTreeMap.maxKeyD_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {fallback : α} :
t.maxKeyD fallback t
theorem Std.DTreeMap.le_maxKeyD_of_contains {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) {fallback : α} :
(cmp k (t.maxKeyD fallback)).isLE = true
theorem Std.DTreeMap.le_maxKeyD_of_mem {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (hc : k t) {fallback : α} :
(cmp k (t.maxKeyD fallback)).isLE = true
theorem Std.DTreeMap.maxKeyD_le {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {k fallback : α} :
(cmp (t.maxKeyD fallback) k).isLE = true ∀ (k' : α), k' t(cmp k' k).isLE = true
theorem Std.DTreeMap.getKey?_maxKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {fallback : α} :
t.getKey? (t.maxKeyD fallback) = some (t.maxKeyD fallback)
theorem Std.DTreeMap.getKey_maxKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {fallback : α} {hc : t.maxKeyD fallback t} :
t.getKey (t.maxKeyD fallback) hc = t.maxKeyD fallback
theorem Std.DTreeMap.getKey!_maxKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {fallback : α} :
t.getKey! (t.maxKeyD fallback) = t.maxKeyD fallback
theorem Std.DTreeMap.getKeyD_maxKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {fallback fallback' : α} :
t.getKeyD (t.maxKeyD fallback) fallback' = t.maxKeyD fallback
theorem Std.DTreeMap.maxKeyD_erase_eq_of_not_compare_maxKeyD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k fallback : α} (he : (t.erase k).isEmpty = false) (heq : ¬cmp k (t.maxKeyD fallback) = Ordering.eq) :
(t.erase k).maxKeyD fallback = t.maxKeyD fallback
theorem Std.DTreeMap.maxKeyD_erase_le_maxKeyD {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} (he : (t.erase k).isEmpty = false) {fallback : α} :
(cmp ((t.erase k).maxKeyD fallback) (t.maxKeyD fallback)).isLE = true
theorem Std.DTreeMap.maxKeyD_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {fallback : α} :
(t.insertIfNew k v).maxKeyD fallback = t.maxKey?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'
theorem Std.DTreeMap.maxKeyD_le_maxKeyD_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] (he : t.isEmpty = false) {k : α} {v : β k} {fallback : α} :
(cmp (t.maxKeyD fallback) ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
theorem Std.DTreeMap.self_le_maxKeyD_insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {k : α} {v : β k} {fallback : α} :
(cmp k ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
theorem Std.DTreeMap.maxKeyD_eq_getLastD_keys {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] {fallback : α} :
t.maxKeyD fallback = t.keys.getLastD fallback
@[simp]
theorem Std.DTreeMap.maxKeyD_modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : β kβ k} {fallback : α} :
(t.modify k f).maxKeyD fallback = t.maxKeyD fallback
theorem Std.DTreeMap.maxKeyD_alter_eq_self {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : Option (β k)Option (β k)} (he : (t.alter k f).isEmpty = false) {fallback : α} :
(t.alter k f).maxKeyD fallback = k (f (t.get? k)).isSome = true ∀ (k' : α), k' t(cmp k' k).isLE = true
theorem Std.DTreeMap.Const.maxKeyD_modify {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} (he : (modify t k f).isEmpty = false) {fallback : α} :
(modify t k f).maxKeyD fallback = if cmp (t.maxKeyD fallback) k = Ordering.eq then k else t.maxKeyD fallback
@[simp]
theorem Std.DTreeMap.Const.maxKeyD_modify_eq_maxKeyD {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {f : ββ} {fallback : α} :
(modify t k f).maxKeyD fallback = t.maxKeyD fallback
theorem Std.DTreeMap.Const.compare_maxKeyD_modify_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : ββ} {fallback : α} :
cmp ((modify t k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
@[simp]
theorem Std.DTreeMap.Const.ordCompare_maxKeyD_modify_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : DTreeMap α (fun (x : α) => β) compare} {k : α} {f : ββ} {fallback : α} :
compare ((modify t k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
theorem Std.DTreeMap.Const.maxKeyD_alter_eq_self {α : Type u} {cmp : ααOrdering} {β : Type v} {t : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {f : Option βOption β} (he : (alter t k f).isEmpty = false) {fallback : α} :
(alter t k f).maxKeyD fallback = k (f (get? t k)).isSome = true ∀ (k' : α), k' t(cmp k' k).isLE = true
@[simp]
theorem Std.DTreeMap.Equiv.rfl {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} :
t.Equiv t
theorem Std.DTreeMap.Equiv.symm {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} :
t₁.Equiv t₂t₂.Equiv t₁
theorem Std.DTreeMap.Equiv.trans {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ t₃ : DTreeMap α β cmp} :
t₁.Equiv t₂t₂.Equiv t₃t₁.Equiv t₃
instance Std.DTreeMap.Equiv.instTrans {α : Type u} {β : αType v} {cmp : ααOrdering} :
Equations
theorem Std.DTreeMap.Equiv.comm {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} :
t₁.Equiv t₂ t₂.Equiv t₁
theorem Std.DTreeMap.Equiv.congr_left {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ t₃ : DTreeMap α β cmp} (h : t₁.Equiv t₂) :
t₁.Equiv t₃ t₂.Equiv t₃
theorem Std.DTreeMap.Equiv.congr_right {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ t₃ : DTreeMap α β cmp} (h : t₁.Equiv t₂) :
t₃.Equiv t₁ t₃.Equiv t₂
theorem Std.DTreeMap.Equiv.isEmpty_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} (h : t₁.Equiv t₂) :
t₁.isEmpty = t₂.isEmpty
theorem Std.DTreeMap.Equiv.contains_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
t₁.contains k = t₂.contains k
theorem Std.DTreeMap.Equiv.mem_iff {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
k t₁ k t₂
theorem Std.DTreeMap.Equiv.size_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} (h : t₁.Equiv t₂) :
t₁.size = t₂.size
theorem Std.DTreeMap.Equiv.get?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} (h : t₁.Equiv t₂) :
t₁.get? k = t₂.get? k
theorem Std.DTreeMap.Equiv.get_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {hk : k t₁} (h : t₁.Equiv t₂) :
t₁.get k hk = t₂.get k
theorem Std.DTreeMap.Equiv.get!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} [Inhabited (β k)] (h : t₁.Equiv t₂) :
t₁.get! k = t₂.get! k
theorem Std.DTreeMap.Equiv.getD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {fallback : β k} (h : t₁.Equiv t₂) :
t₁.getD k fallback = t₂.getD k fallback
theorem Std.DTreeMap.Equiv.getKey?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
t₁.getKey? k = t₂.getKey? k
theorem Std.DTreeMap.Equiv.getKey_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} {hk : k t₁} (h : t₁.Equiv t₂) :
t₁.getKey k hk = t₂.getKey k
theorem Std.DTreeMap.Equiv.getKey!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} (h : t₁.Equiv t₂) :
t₁.getKey! k = t₂.getKey! k
theorem Std.DTreeMap.Equiv.getKeyD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k fallback : α} (h : t₁.Equiv t₂) :
t₁.getKeyD k fallback = t₂.getKeyD k fallback
theorem Std.DTreeMap.Equiv.toList_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
t₁.toList = t₂.toList
theorem Std.DTreeMap.Equiv.toArray_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
t₁.toArray = t₂.toArray
theorem Std.DTreeMap.Equiv.keys_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
t₁.keys = t₂.keys
theorem Std.DTreeMap.Equiv.keysArray_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.foldlM_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : δ(a : α) → β am δ} {init : δ} (h : t₁.Equiv t₂) :
foldlM f init t₁ = foldlM f init t₂
theorem Std.DTreeMap.Equiv.foldl_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} {δ : Type w} [TransCmp cmp] {f : δ(a : α) → β aδ} {init : δ} (h : t₁.Equiv t₂) :
foldl f init t₁ = foldl f init t₂
theorem Std.DTreeMap.Equiv.foldrM_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : (a : α) → β aδm δ} {init : δ} (h : t₁.Equiv t₂) :
foldrM f init t₁ = foldrM f init t₂
theorem Std.DTreeMap.Equiv.foldr_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} {δ : Type w} [TransCmp cmp] {f : (a : α) → β aδδ} {init : δ} (h : t₁.Equiv t₂) :
foldr f init t₁ = foldr f init t₂
theorem Std.DTreeMap.Equiv.forIn_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {b : δ} {f : (a : α) × β aδm (ForInStep δ)} (h : t₁.Equiv t₂) :
ForIn.forIn t₁ b f = ForIn.forIn t₂ b f
theorem Std.DTreeMap.Equiv.forM_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : (a : α) × β am PUnit} (h : t₁.Equiv t₂) :
ForM.forM t₁ f = ForM.forM t₂ f
theorem Std.DTreeMap.Equiv.any_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {p : (a : α) → β aBool} (h : t₁.Equiv t₂) :
t₁.any p = t₂.any p
theorem Std.DTreeMap.Equiv.all_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {p : (a : α) → β aBool} (h : t₁.Equiv t₂) :
t₁.all p = t₂.all p
theorem Std.DTreeMap.Equiv.minKey?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
t₁.minKey? = t₂.minKey?
theorem Std.DTreeMap.Equiv.minKey_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {h' : t₁.isEmpty = false} (h : t₁.Equiv t₂) :
t₁.minKey h' = t₂.minKey
theorem Std.DTreeMap.Equiv.minKey!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (h : t₁.Equiv t₂) :
t₁.minKey! = t₂.minKey!
theorem Std.DTreeMap.Equiv.minKeyD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {fallback : α} (h : t₁.Equiv t₂) :
t₁.minKeyD fallback = t₂.minKeyD fallback
theorem Std.DTreeMap.Equiv.maxKey?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
t₁.maxKey? = t₂.maxKey?
theorem Std.DTreeMap.Equiv.maxKey_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {h' : t₁.isEmpty = false} (h : t₁.Equiv t₂) :
t₁.maxKey h' = t₂.maxKey
theorem Std.DTreeMap.Equiv.maxKey!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] (h : t₁.Equiv t₂) :
t₁.maxKey! = t₂.maxKey!
theorem Std.DTreeMap.Equiv.maxKeyD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {fallback : α} (h : t₁.Equiv t₂) :
t₁.maxKeyD fallback = t₂.maxKeyD fallback
theorem Std.DTreeMap.Equiv.minEntry?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.minEntry_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {he : t₁.isEmpty = false} (h : t₁.Equiv t₂) :
t₁.minEntry he = t₂.minEntry
theorem Std.DTreeMap.Equiv.minEntry!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited ((a : α) × β a)] (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.minEntryD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {fallback : (a : α) × β a} (h : t₁.Equiv t₂) :
t₁.minEntryD fallback = t₂.minEntryD fallback
theorem Std.DTreeMap.Equiv.maxEntry?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.maxEntry_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {he : t₁.isEmpty = false} (h : t₁.Equiv t₂) :
t₁.maxEntry he = t₂.maxEntry
theorem Std.DTreeMap.Equiv.maxEntry!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited ((a : α) × β a)] (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.maxEntryD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {fallback : (a : α) × β a} (h : t₁.Equiv t₂) :
t₁.maxEntryD fallback = t₂.maxEntryD fallback
theorem Std.DTreeMap.Equiv.entryAtIdx?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {i : Nat} (h : t₁.Equiv t₂) :
t₁.entryAtIdx? i = t₂.entryAtIdx? i
theorem Std.DTreeMap.Equiv.entryAtIdx_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {i : Nat} {h' : i < t₁.size} (h : t₁.Equiv t₂) :
t₁.entryAtIdx i h' = t₂.entryAtIdx i
theorem Std.DTreeMap.Equiv.entryAtIdx!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited ((a : α) × β a)] {i : Nat} (h : t₁.Equiv t₂) :
t₁.entryAtIdx! i = t₂.entryAtIdx! i
theorem Std.DTreeMap.Equiv.entryAtIdxD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {i : Nat} {fallback : (a : α) × β a} (h : t₁.Equiv t₂) :
t₁.entryAtIdxD i fallback = t₂.entryAtIdxD i fallback
theorem Std.DTreeMap.Equiv.keyAtIdx?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {i : Nat} (h : t₁.Equiv t₂) :
t₁.keyAtIdx? i = t₂.keyAtIdx? i
theorem Std.DTreeMap.Equiv.keyAtIdx_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {i : Nat} {h' : i < t₁.size} (h : t₁.Equiv t₂) :
t₁.keyAtIdx i h' = t₂.keyAtIdx i
theorem Std.DTreeMap.Equiv.keyAtIdx!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {i : Nat} (h : t₁.Equiv t₂) :
t₁.keyAtIdx! i = t₂.keyAtIdx! i
theorem Std.DTreeMap.Equiv.keyAtIdxD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {i : Nat} {fallback : α} (h : t₁.Equiv t₂) :
t₁.keyAtIdxD i fallback = t₂.keyAtIdxD i fallback
theorem Std.DTreeMap.Equiv.getEntryGE?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
t₁.getEntryGE? k = t₂.getEntryGE? k
theorem Std.DTreeMap.Equiv.getEntryGE_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} {h' : (a : α), a t₁ (cmp a k).isGE = true} (h : t₁.Equiv t₂) :
t₁.getEntryGE k h' = t₂.getEntryGE k
theorem Std.DTreeMap.Equiv.getEntryGE!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited ((a : α) × β a)] {k : α} (h : t₁.Equiv t₂) :
t₁.getEntryGE! k = t₂.getEntryGE! k
theorem Std.DTreeMap.Equiv.getEntryGED_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} {fallback : (a : α) × β a} (h : t₁.Equiv t₂) :
t₁.getEntryGED k fallback = t₂.getEntryGED k fallback
theorem Std.DTreeMap.Equiv.getEntryGT?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
t₁.getEntryGT? k = t₂.getEntryGT? k
theorem Std.DTreeMap.Equiv.getEntryGT_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} {h' : (a : α), a t₁ cmp a k = Ordering.gt} (h : t₁.Equiv t₂) :
t₁.getEntryGT k h' = t₂.getEntryGT k
theorem Std.DTreeMap.Equiv.getEntryGT!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited ((a : α) × β a)] {k : α} (h : t₁.Equiv t₂) :
t₁.getEntryGT! k = t₂.getEntryGT! k
theorem Std.DTreeMap.Equiv.getEntryGTD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} {fallback : (a : α) × β a} (h : t₁.Equiv t₂) :
t₁.getEntryGTD k fallback = t₂.getEntryGTD k fallback
theorem Std.DTreeMap.Equiv.getEntryLE?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
t₁.getEntryLE? k = t₂.getEntryLE? k
theorem Std.DTreeMap.Equiv.getEntryLE_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} {h' : (a : α), a t₁ (cmp a k).isLE = true} (h : t₁.Equiv t₂) :
t₁.getEntryLE k h' = t₂.getEntryLE k
theorem Std.DTreeMap.Equiv.getEntryLE!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited ((a : α) × β a)] {k : α} (h : t₁.Equiv t₂) :
t₁.getEntryLE! k = t₂.getEntryLE! k
theorem Std.DTreeMap.Equiv.getEntryLED_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} {fallback : (a : α) × β a} (h : t₁.Equiv t₂) :
t₁.getEntryLED k fallback = t₂.getEntryLED k fallback
theorem Std.DTreeMap.Equiv.getEntryLT?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
t₁.getEntryLT? k = t₂.getEntryLT? k
theorem Std.DTreeMap.Equiv.getEntryLT_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} {h' : (a : α), a t₁ cmp a k = Ordering.lt} (h : t₁.Equiv t₂) :
t₁.getEntryLT k h' = t₂.getEntryLT k
theorem Std.DTreeMap.Equiv.getEntryLT!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited ((a : α) × β a)] {k : α} (h : t₁.Equiv t₂) :
t₁.getEntryLT! k = t₂.getEntryLT! k
theorem Std.DTreeMap.Equiv.getEntryLTD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} {fallback : (a : α) × β a} (h : t₁.Equiv t₂) :
t₁.getEntryLTD k fallback = t₂.getEntryLTD k fallback
theorem Std.DTreeMap.Equiv.getKeyGE?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
t₁.getKeyGE? k = t₂.getKeyGE? k
theorem Std.DTreeMap.Equiv.getKeyGE_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} {h' : (a : α), a t₁ (cmp a k).isGE = true} (h : t₁.Equiv t₂) :
t₁.getKeyGE k h' = t₂.getKeyGE k
theorem Std.DTreeMap.Equiv.getKeyGE!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} (h : t₁.Equiv t₂) :
t₁.getKeyGE! k = t₂.getKeyGE! k
theorem Std.DTreeMap.Equiv.getKeyGED_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k fallback : α} (h : t₁.Equiv t₂) :
t₁.getKeyGED k fallback = t₂.getKeyGED k fallback
theorem Std.DTreeMap.Equiv.getKeyGT?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
t₁.getKeyGT? k = t₂.getKeyGT? k
theorem Std.DTreeMap.Equiv.getKeyGT_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} {h' : (a : α), a t₁ cmp a k = Ordering.gt} (h : t₁.Equiv t₂) :
t₁.getKeyGT k h' = t₂.getKeyGT k
theorem Std.DTreeMap.Equiv.getKeyGT!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} (h : t₁.Equiv t₂) :
t₁.getKeyGT! k = t₂.getKeyGT! k
theorem Std.DTreeMap.Equiv.getKeyGTD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k fallback : α} (h : t₁.Equiv t₂) :
t₁.getKeyGTD k fallback = t₂.getKeyGTD k fallback
theorem Std.DTreeMap.Equiv.getKeyLE?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
t₁.getKeyLE? k = t₂.getKeyLE? k
theorem Std.DTreeMap.Equiv.getKeyLE_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} {h' : (a : α), a t₁ (cmp a k).isLE = true} (h : t₁.Equiv t₂) :
t₁.getKeyLE k h' = t₂.getKeyLE k
theorem Std.DTreeMap.Equiv.getKeyLE!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} (h : t₁.Equiv t₂) :
t₁.getKeyLE! k = t₂.getKeyLE! k
theorem Std.DTreeMap.Equiv.getKeyLED_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k fallback : α} (h : t₁.Equiv t₂) :
t₁.getKeyLED k fallback = t₂.getKeyLED k fallback
theorem Std.DTreeMap.Equiv.getKeyLT?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
t₁.getKeyLT? k = t₂.getKeyLT? k
theorem Std.DTreeMap.Equiv.getKeyLT_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k : α} {h' : (a : α), a t₁ cmp a k = Ordering.lt} (h : t₁.Equiv t₂) :
t₁.getKeyLT k h' = t₂.getKeyLT k
theorem Std.DTreeMap.Equiv.getKeyLT!_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [Inhabited α] {k : α} (h : t₁.Equiv t₂) :
t₁.getKeyLT! k = t₂.getKeyLT! k
theorem Std.DTreeMap.Equiv.getKeyLTD_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] {k fallback : α} (h : t₁.Equiv t₂) :
t₁.getKeyLTD k fallback = t₂.getKeyLTD k fallback
theorem Std.DTreeMap.Equiv.insert {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) (k : α) (v : β k) :
(t₁.insert k v).Equiv (t₂.insert k v)
theorem Std.DTreeMap.Equiv.erase {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) (k : α) :
(t₁.erase k).Equiv (t₂.erase k)
theorem Std.DTreeMap.Equiv.insertIfNew {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) (k : α) (v : β k) :
(t₁.insertIfNew k v).Equiv (t₂.insertIfNew k v)
theorem Std.DTreeMap.Equiv.alter {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t₁.Equiv t₂) (k : α) (f : Option (β k)Option (β k)) :
(t₁.alter k f).Equiv (t₂.alter k f)
theorem Std.DTreeMap.Equiv.modify {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t₁.Equiv t₂) (k : α) (f : β kβ k) :
(t₁.modify k f).Equiv (t₂.modify k f)
theorem Std.DTreeMap.Equiv.filter {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} (h : t₁.Equiv t₂) (f : (a : α) → β aBool) :
theorem Std.DTreeMap.Equiv.map {α : Type u} {β : αType v} {γ : αType w} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} (h : t₁.Equiv t₂) (f : (a : α) → β aγ a) :
(DTreeMap.map f t₁).Equiv (DTreeMap.map f t₂)
theorem Std.DTreeMap.Equiv.filterMap {α : Type u} {β : αType v} {γ : αType w} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} (h : t₁.Equiv t₂) (f : (a : α) → β aOption (γ a)) :
theorem Std.DTreeMap.Equiv.insertMany_list {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) (l : List ((a : α) × β a)) :
(t₁.insertMany l).Equiv (t₂.insertMany l)
theorem Std.DTreeMap.Equiv.eraseMany_list {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] (h : t₁.Equiv t₂) (l : List α) :
(t₁.eraseMany l).Equiv (t₂.eraseMany l)
theorem Std.DTreeMap.Equiv.mergeWith {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ t₃ t₄ : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (f : (a : α) → β aβ aβ a) (h : t₁.Equiv t₂) (h' : t₃.Equiv t₄) :
(DTreeMap.mergeWith f t₁ t₃).Equiv (DTreeMap.mergeWith f t₂ t₄)
theorem Std.DTreeMap.Equiv.constGet?_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
Const.get? t₁ k = Const.get? t₂ k
theorem Std.DTreeMap.Equiv.constGet_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {hk : k t₁} (h : t₁.Equiv t₂) :
Const.get t₁ k hk = Const.get t₂ k
theorem Std.DTreeMap.Equiv.constGet!_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited β] {k : α} (h : t₁.Equiv t₂) :
Const.get! t₁ k = Const.get! t₂ k
theorem Std.DTreeMap.Equiv.constGetD_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {fallback : β} (h : t₁.Equiv t₂) :
Const.getD t₁ k fallback = Const.getD t₂ k fallback
theorem Std.DTreeMap.Equiv.constToList_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constToArray_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.values_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
t₁.values = t₂.values
theorem Std.DTreeMap.Equiv.valuesArray_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constMinEntry?_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constMinEntry_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {he : t₁.isEmpty = false} (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constMinEntry!_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited (α × β)] (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constMinEntryD_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {fallback : α × β} (h : t₁.Equiv t₂) :
Const.minEntryD t₁ fallback = Const.minEntryD t₂ fallback
theorem Std.DTreeMap.Equiv.constMaxEntry?_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constMaxEntry_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {he : t₁.isEmpty = false} (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constMaxEntry!_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited (α × β)] (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constMaxEntryD_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {fallback : α × β} (h : t₁.Equiv t₂) :
Const.maxEntryD t₁ fallback = Const.maxEntryD t₂ fallback
theorem Std.DTreeMap.Equiv.constEntryAtIdx?_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {i : Nat} (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constEntryAtIdx_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {i : Nat} {h' : i < t₁.size} (h : t₁.Equiv t₂) :
Const.entryAtIdx t₁ i h' = Const.entryAtIdx t₂ i
theorem Std.DTreeMap.Equiv.constEntryAtIdx!_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited (α × β)] {i : Nat} (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constEntryAtIdxD_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {i : Nat} {fallback : α × β} (h : t₁.Equiv t₂) :
Const.entryAtIdxD t₁ i fallback = Const.entryAtIdxD t₂ i fallback
theorem Std.DTreeMap.Equiv.constGetEntryGE?_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constGetEntryGE_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {h' : (a : α), a t₁ (cmp a k).isGE = true} (h : t₁.Equiv t₂) :
Const.getEntryGE t₁ k h' = Const.getEntryGE t₂ k
theorem Std.DTreeMap.Equiv.constGetEntryGE!_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited (α × β)] {k : α} (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constGetEntryGED_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {fallback : α × β} (h : t₁.Equiv t₂) :
Const.getEntryGED t₁ k fallback = Const.getEntryGED t₂ k fallback
theorem Std.DTreeMap.Equiv.constGetEntryGT?_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constGetEntryGT_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {h' : (a : α), a t₁ cmp a k = Ordering.gt} (h : t₁.Equiv t₂) :
Const.getEntryGT t₁ k h' = Const.getEntryGT t₂ k
theorem Std.DTreeMap.Equiv.constGetEntryGT!_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited (α × β)] {k : α} (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constGetEntryGTD_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {fallback : α × β} (h : t₁.Equiv t₂) :
Const.getEntryGTD t₁ k fallback = Const.getEntryGTD t₂ k fallback
theorem Std.DTreeMap.Equiv.constGetEntryLE?_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constGetEntryLE_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {h' : (a : α), a t₁ (cmp a k).isLE = true} (h : t₁.Equiv t₂) :
Const.getEntryLE t₁ k h' = Const.getEntryLE t₂ k
theorem Std.DTreeMap.Equiv.constGetEntryLE!_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited (α × β)] {k : α} (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constGetEntryLED_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {fallback : α × β} (h : t₁.Equiv t₂) :
Const.getEntryLED t₁ k fallback = Const.getEntryLED t₂ k fallback
theorem Std.DTreeMap.Equiv.constGetEntryLT?_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constGetEntryLT_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {h' : (a : α), a t₁ cmp a k = Ordering.lt} (h : t₁.Equiv t₂) :
Const.getEntryLT t₁ k h' = Const.getEntryLT t₂ k
theorem Std.DTreeMap.Equiv.constGetEntryLT!_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [Inhabited (α × β)] {k : α} (h : t₁.Equiv t₂) :
theorem Std.DTreeMap.Equiv.constGetEntryLTD_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] {k : α} {fallback : α × β} (h : t₁.Equiv t₂) :
Const.getEntryLTD t₁ k fallback = Const.getEntryLTD t₂ k fallback
theorem Std.DTreeMap.Equiv.constAlter {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (h : t₁.Equiv t₂) (k : α) (f : Option βOption β) :
(Const.alter t₁ k f).Equiv (Const.alter t₂ k f)
theorem Std.DTreeMap.Equiv.constModify {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (h : t₁.Equiv t₂) (k : α) (f : ββ) :
(Const.modify t₁ k f).Equiv (Const.modify t₂ k f)
theorem Std.DTreeMap.Equiv.constInsertMany_list {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (h : t₁.Equiv t₂) (l : List (α × β)) :
theorem Std.DTreeMap.Equiv.constInsertManyIfNewUnit_list {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {t₁ t₂ : DTreeMap α (fun (x : α) => Unit) cmp} (h : t₁.Equiv t₂) (l : List α) :
theorem Std.DTreeMap.Equiv.constMergeWith {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ t₃ t₄ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (f : αβββ) (h : t₁.Equiv t₂) (h' : t₃.Equiv t₄) :
(Const.mergeWith f t₁ t₃).Equiv (Const.mergeWith f t₂ t₄)
theorem Std.DTreeMap.Equiv.of_forall_get?_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : ∀ (k : α), t₁.get? k = t₂.get? k) :
t₁.Equiv t₂
theorem Std.DTreeMap.Equiv.of_forall_getKey_eq_of_forall_constGet?_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] (hk : ∀ (k : α) (hk : k t₁) (hk' : k t₂), t₁.getKey k hk = t₂.getKey k hk') (hv : ∀ (k : α), Const.get? t₁ k = Const.get? t₂ k) :
t₁.Equiv t₂
theorem Std.DTreeMap.Equiv.of_forall_constGet?_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : ∀ (k : α), Const.get? t₁ k = Const.get? t₂ k) :
t₁.Equiv t₂
theorem Std.DTreeMap.Equiv.of_forall_getKey?_unit_eq {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {t₁ t₂ : DTreeMap α (fun (x : α) => Unit) cmp} (h : ∀ (k : α), t₁.getKey? k = t₂.getKey? k) :
t₁.Equiv t₂
theorem Std.DTreeMap.Equiv.of_forall_contains_unit_eq {α : Type u} {cmp : ααOrdering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : DTreeMap α (fun (x : α) => Unit) cmp} (h : ∀ (k : α), t₁.contains k = t₂.contains k) :
t₁.Equiv t₂
theorem Std.DTreeMap.Equiv.of_forall_mem_unit_iff {α : Type u} {cmp : ααOrdering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : DTreeMap α (fun (x : α) => Unit) cmp} (h : ∀ (k : α), k t₁ k t₂) :
t₁.Equiv t₂
def Std.DTreeMap.isSetoid (α : Type u) (β : αType v) (cmp : ααOrdering := by exact compare) :
Setoid (DTreeMap α β cmp)

Implementation detail of the tree map

Equations
Instances For
    theorem Std.DTreeMap.equiv_empty_iff_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} :
    theorem Std.DTreeMap.empty_equiv_iff_isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} {t : DTreeMap α β cmp} :
    theorem Std.DTreeMap.equiv_iff_toList_perm {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} :
    t₁.Equiv t₂ t₁.toList.Perm t₂.toList
    theorem Std.DTreeMap.Equiv.of_toList_perm {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} (h : t₁.toList.Perm t₂.toList) :
    t₁.Equiv t₂
    theorem Std.DTreeMap.equiv_iff_toList_eq {α : Type u} {β : αType v} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α β cmp} [TransCmp cmp] :
    t₁.Equiv t₂ t₁.toList = t₂.toList
    theorem Std.DTreeMap.Const.equiv_iff_toList_perm {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} :
    t₁.Equiv t₂ (toList t₁).Perm (toList t₂)
    theorem Std.DTreeMap.Const.equiv_iff_toList_eq {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} [TransCmp cmp] :
    t₁.Equiv t₂ toList t₁ = toList t₂
    theorem Std.DTreeMap.Const.equiv_iff_keys_unit_perm {α : Type u} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α (fun (x : α) => Unit) cmp} :
    t₁.Equiv t₂ t₁.keys.Perm t₂.keys
    theorem Std.DTreeMap.Const.equiv_iff_keys_unit_eq {α : Type u} {cmp : ααOrdering} [TransCmp cmp] {t₁ t₂ : DTreeMap α (fun (x : α) => Unit) cmp} :
    t₁.Equiv t₂ t₁.keys = t₂.keys
    theorem Std.DTreeMap.Equiv.of_constToList_perm {α : Type u} {cmp : ααOrdering} {β : Type v} {t₁ t₂ : DTreeMap α (fun (x : α) => β) cmp} :
    (Const.toList t₁).Perm (Const.toList t₂)t₁.Equiv t₂
    theorem Std.DTreeMap.Equiv.of_keys_unit_perm {α : Type u} {cmp : ααOrdering} {t₁ t₂ : DTreeMap α (fun (x : α) => Unit) cmp} :
    t₁.keys.Perm t₂.keyst₁.Equiv t₂