Tree map lemmas

This file contains lemmas about Std.Data.TreeMap.Raw.Basic. Most of the lemmas require TransCmp cmp for the comparison function cmp. These proofs can be obtained from Std.Data.TreeMap.Raw.WF.

@[simp]

theorem Std.TreeMap.Raw.isEmpty_emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} : ∅.isEmpty = true

@[simp]

theorem Std.TreeMap.Raw.isEmpty_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insert k v).isEmpty = false

theorem Std.TreeMap.Raw.mem_iff_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {k : α} : k ∈ t ↔ t.contains k = true

@[simp]

theorem Std.TreeMap.Raw.contains_iff_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {k : α} : t.contains k = true ↔ k ∈ t

theorem Std.TreeMap.Raw.contains_congr {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = Ordering.eq) : t.contains k = t.contains k'

theorem Std.TreeMap.Raw.mem_congr {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} (hab : cmp k k' = Ordering.eq) : k ∈ t ↔ k' ∈ t

@[simp]

theorem Std.TreeMap.Raw.contains_emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α} : ∅.contains k = false

@[simp]

theorem Std.TreeMap.Raw.not_mem_emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α} : ¬k ∈ ∅

theorem Std.TreeMap.Raw.contains_of_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : t.isEmpty = true → t.contains a = false

theorem Std.TreeMap.Raw.not_mem_of_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : t.isEmpty = true → ¬a ∈ t

theorem Std.TreeMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.isEmpty = false ↔ ∃ (a : α), t.contains a = true

theorem Std.TreeMap.Raw.isEmpty_eq_false_iff_exists_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.isEmpty = false ↔ ∃ (a : α), a ∈ t

theorem Std.TreeMap.Raw.isEmpty_eq_false_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} (hc : t.contains a = true) : t.isEmpty = false

theorem Std.TreeMap.Raw.isEmpty_iff_forall_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.isEmpty = true ↔ ∀ (a : α), t.contains a = false

theorem Std.TreeMap.Raw.isEmpty_iff_forall_not_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.isEmpty = true ↔ ∀ (a : α), ¬a ∈ t

@[simp]

theorem Std.TreeMap.Raw.insert_eq_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {p : α × β} : Insert.insert p t = t.insert p.fst p.snd

@[simp]

theorem Std.TreeMap.Raw.singleton_eq_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {p : α × β} : {p} = ∅.insert p.fst p.snd

@[simp]

theorem Std.TreeMap.Raw.contains_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [h : TransCmp cmp] : t.WF → ∀ {k a : α} {v : β}, (t.insert k v).contains a = (cmp k a == Ordering.eq || t.contains a)

@[simp]

theorem Std.TreeMap.Raw.mem_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : a ∈ t.insert k v ↔ cmp k a = Ordering.eq ∨ a ∈ t

theorem Std.TreeMap.Raw.contains_insert_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insert k v).contains k = true

theorem Std.TreeMap.Raw.mem_insert_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : k ∈ t.insert k v

theorem Std.TreeMap.Raw.contains_of_contains_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : (t.insert k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true

theorem Std.TreeMap.Raw.mem_of_mem_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : a ∈ t.insert k v → cmp k a ≠ Ordering.eq → a ∈ t

@[simp]

theorem Std.TreeMap.Raw.size_emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} : ∅.size = 0

theorem Std.TreeMap.Raw.isEmpty_eq_size_eq_zero {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} (h : t.WF) : t.isEmpty = (t.size == 0)

theorem Std.TreeMap.Raw.size_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insert k v).size = if t.contains k = true then t.size else t.size + 1

theorem Std.TreeMap.Raw.size_le_size_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : t.size ≤ (t.insert k v).size

theorem Std.TreeMap.Raw.size_insert_le {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insert k v).size ≤ t.size + 1

@[simp]

theorem Std.TreeMap.Raw.erase_emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α} : ∅.erase k = ∅

@[simp]

theorem Std.TreeMap.Raw.isEmpty_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} : (t.erase k).isEmpty = (t.isEmpty || t.size == 1 && t.contains k)

theorem Std.TreeMap.Raw.isEmpty_eq_isEmpty_erase_and_not_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (k : α) : t.isEmpty = ((t.erase k).isEmpty && !t.contains k)

theorem Std.TreeMap.Raw.isEmpty_eq_false_of_isEmpty_erase_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) : t.isEmpty = false

@[simp]

theorem Std.TreeMap.Raw.contains_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} : (t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)

@[simp]

theorem Std.TreeMap.Raw.mem_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} : a ∈ t.erase k ↔ cmp k a ≠ Ordering.eq ∧ a ∈ t

theorem Std.TreeMap.Raw.contains_of_contains_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} : (t.erase k).contains a = true → t.contains a = true

theorem Std.TreeMap.Raw.mem_of_mem_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} : a ∈ t.erase k → a ∈ t

theorem Std.TreeMap.Raw.size_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} : (t.erase k).size = if t.contains k = true then t.size - 1 else t.size

theorem Std.TreeMap.Raw.size_erase_le {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} : (t.erase k).size ≤ t.size

theorem Std.TreeMap.Raw.size_le_size_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} : t.size ≤ (t.erase k).size + 1

@[simp]

theorem Std.TreeMap.Raw.containsThenInsert_fst {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.containsThenInsert k v).fst = t.contains k

@[simp]

theorem Std.TreeMap.Raw.containsThenInsert_snd {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.containsThenInsert k v).snd = t.insert k v

@[simp]

theorem Std.TreeMap.Raw.containsThenInsertIfNew_fst {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.containsThenInsertIfNew k v).fst = t.contains k

@[simp]

theorem Std.TreeMap.Raw.containsThenInsertIfNew_snd {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.containsThenInsertIfNew k v).snd = t.insertIfNew k v

@[simp]

theorem Std.TreeMap.Raw.get_eq_getElem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {a : α} {h : a ∈ t} : t.get a h = t[a]

@[simp]

theorem Std.TreeMap.Raw.get?_eq_getElem? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {a : α} : t.get? a = t[a]?

@[simp]

theorem Std.TreeMap.Raw.get!_eq_getElem! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [Inhabited β] {a : α} : t.get! a = t[a]!

@[simp]

theorem Std.TreeMap.Raw.getElem?_emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {a : α} : ∅[a]? = none

theorem Std.TreeMap.Raw.getElem?_of_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : t.isEmpty = true → t[a]? = none

theorem Std.TreeMap.Raw.getElem?_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a k : α} {v : β} : (t.insert k v)[a]? = if cmp k a = Ordering.eq then some v else t[a]?

@[simp]

theorem Std.TreeMap.Raw.getElem?_insert_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insert k v)[k]? = some v

theorem Std.TreeMap.Raw.contains_eq_isSome_getElem? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : t.contains a = t[a]?.isSome

@[simp]

theorem Std.TreeMap.Raw.isSome_getElem?_eq_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : t[a]?.isSome = t.contains a

theorem Std.TreeMap.Raw.mem_iff_isSome_getElem? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : a ∈ t ↔ t[a]?.isSome = true

@[simp]

theorem Std.TreeMap.Raw.isSome_getElem?_iff_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : t[a]?.isSome = true ↔ a ∈ t

theorem Std.TreeMap.Raw.getElem?_eq_none_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : t.contains a = false → t[a]? = none

theorem Std.TreeMap.Raw.getElem?_eq_none {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : ¬a ∈ t → t[a]? = none

theorem Std.TreeMap.Raw.getElem?_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} : (t.erase k)[a]? = if cmp k a = Ordering.eq then none else t[a]?

@[simp]

theorem Std.TreeMap.Raw.getElem?_erase_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} : (t.erase k)[k]? = none

theorem Std.TreeMap.Raw.getElem?_congr {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a b : α} (hab : cmp a b = Ordering.eq) : t[a]? = t[b]?

theorem Std.TreeMap.Raw.getElem_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} {h₁ : a ∈ t.insert k v} : (t.insert k v)[a] = if h₂ : cmp k a = Ordering.eq then v else t[a]

@[simp]

theorem Std.TreeMap.Raw.getElem_insert_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insert k v)[k] = v

@[simp]

theorem Std.TreeMap.Raw.getElem_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {h' : a ∈ t.erase k} : (t.erase k)[a] = t[a]

theorem Std.TreeMap.Raw.getElem?_eq_some_getElem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} {h' : a ∈ t} : t[a]? = some t[a]

theorem Std.TreeMap.Raw.getElem_congr {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a b : α} (hab : cmp a b = Ordering.eq) {h' : a ∈ t} : t[a] = t[b]

@[simp]

theorem Std.TreeMap.Raw.getElem!_emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited β] {a : α} : ∅[a]! = default

theorem Std.TreeMap.Raw.getElem!_of_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} : t.isEmpty = true → t[a]! = default

theorem Std.TreeMap.Raw.getElem!_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {k a : α} {v : β} : (t.insert k v)[a]! = if cmp k a = Ordering.eq then v else t[a]!

@[simp]

theorem Std.TreeMap.Raw.getElem!_insert_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {k : α} {v : β} : (t.insert k v)[k]! = v

theorem Std.TreeMap.Raw.getElem!_eq_default_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} : t.contains a = false → t[a]! = default

theorem Std.TreeMap.Raw.getElem!_eq_default {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} : ¬a ∈ t → t[a]! = default

theorem Std.TreeMap.Raw.getElem!_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {k a : α} : (t.erase k)[a]! = if cmp k a = Ordering.eq then default else t[a]!

@[simp]

theorem Std.TreeMap.Raw.getElem!_erase_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {k : α} : (t.erase k)[k]! = default

theorem Std.TreeMap.Raw.getElem?_eq_some_getElem!_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} : t.contains a = true → t[a]? = some t[a]!

theorem Std.TreeMap.Raw.getElem?_eq_some_getElem! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} : a ∈ t → t[a]? = some t[a]!

theorem Std.TreeMap.Raw.getElem!_eq_get!_getElem? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} : t[a]! = t[a]?.get!

@[deprecated Std.TreeMap.Raw.getElem!_eq_get!_getElem? (since := "2025-03-19")]

theorem Std.TreeMap.Raw.getElem!_eq_getElem!_getElem? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} : t[a]! = t[a]?.get!

theorem Std.TreeMap.Raw.getElem_eq_getElem! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} {h' : a ∈ t} : t[a] = t[a]!

theorem Std.TreeMap.Raw.getElem!_congr {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {a b : α} (hab : cmp a b = Ordering.eq) : t[a]! = t[b]!

@[simp]

theorem Std.TreeMap.Raw.getD_emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {a : α} {fallback : β} : ∅.getD a fallback = fallback

theorem Std.TreeMap.Raw.getD_of_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} : t.isEmpty = true → t.getD a fallback = fallback

theorem Std.TreeMap.Raw.getD_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {fallback v : β} : (t.insert k v).getD a fallback = if cmp k a = Ordering.eq then v else t.getD a fallback

@[simp]

theorem Std.TreeMap.Raw.getD_insert_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {fallback v : β} : (t.insert k v).getD k fallback = v

theorem Std.TreeMap.Raw.getD_eq_fallback_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} : t.contains a = false → t.getD a fallback = fallback

theorem Std.TreeMap.Raw.getD_eq_fallback {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} : ¬a ∈ t → t.getD a fallback = fallback

theorem Std.TreeMap.Raw.getD_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {fallback : β} : (t.erase k).getD a fallback = if cmp k a = Ordering.eq then fallback else t.getD a fallback

@[simp]

theorem Std.TreeMap.Raw.getD_erase_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {fallback : β} : (t.erase k).getD k fallback = fallback

theorem Std.TreeMap.Raw.getElem?_eq_some_getD_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} : t.contains a = true → t.get? a = some (t.getD a fallback)

theorem Std.TreeMap.Raw.getElem?_eq_some_getD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} : a ∈ t → t[a]? = some (t.getD a fallback)

theorem Std.TreeMap.Raw.getD_eq_getD_getElem? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} : t.getD a fallback = t[a]?.getD fallback

theorem Std.TreeMap.Raw.getElem_eq_getD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} {fallback : β} {h' : a ∈ t} : t[a] = t.getD a fallback

theorem Std.TreeMap.Raw.getElem!_eq_getD_default {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {a : α} : t[a]! = t.getD a default

theorem Std.TreeMap.Raw.getD_congr {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a b : α} {fallback : β} (hab : cmp a b = Ordering.eq) : t.getD a fallback = t.getD b fallback

@[simp]

theorem Std.TreeMap.Raw.getKey?_emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a : α} : ∅.getKey? a = none

theorem Std.TreeMap.Raw.getKey?_of_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : t.isEmpty = true → t.getKey? a = none

theorem Std.TreeMap.Raw.getKey?_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a k : α} {v : β} : (t.insert k v).getKey? a = if cmp k a = Ordering.eq then some k else t.getKey? a

@[simp]

theorem Std.TreeMap.Raw.getKey?_insert_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insert k v).getKey? k = some k

theorem Std.TreeMap.Raw.contains_eq_isSome_getKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : t.contains a = (t.getKey? a).isSome

@[simp]

theorem Std.TreeMap.Raw.isSome_getKey?_eq_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : (t.getKey? a).isSome = t.contains a

theorem Std.TreeMap.Raw.mem_iff_isSome_getKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : a ∈ t ↔ (t.getKey? a).isSome = true

@[simp]

theorem Std.TreeMap.Raw.isSome_getKey?_iff_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : (t.getKey? a).isSome = true ↔ a ∈ t

theorem Std.TreeMap.Raw.getKey?_eq_none_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : t.contains a = false → t.getKey? a = none

theorem Std.TreeMap.Raw.getKey?_eq_none {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} : ¬a ∈ t → t.getKey? a = none

theorem Std.TreeMap.Raw.getKey?_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} : (t.erase k).getKey? a = if cmp k a = Ordering.eq then none else t.getKey? a

@[simp]

theorem Std.TreeMap.Raw.getKey?_erase_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} : (t.erase k).getKey? k = none

theorem Std.TreeMap.Raw.compare_getKey?_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} : Option.all (fun (x : α) => decide (cmp x k = Ordering.eq)) (t.getKey? k) = true

theorem Std.TreeMap.Raw.getKey?_congr {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} (h' : cmp k k' = Ordering.eq) : t.getKey? k = t.getKey? k'

theorem Std.TreeMap.Raw.getKey?_eq_some_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} (h' : t.contains k = true) : t.getKey? k = some k

theorem Std.TreeMap.Raw.getKey?_eq_some {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} (h' : k ∈ t) : t.getKey? k = some k

theorem Std.TreeMap.Raw.getKey_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} {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.TreeMap.Raw.getKey_insert_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insert k v).getKey k ⋯ = k

@[simp]

theorem Std.TreeMap.Raw.getKey_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {h' : a ∈ t.erase k} : (t.erase k).getKey a h' = t.getKey a ⋯

theorem Std.TreeMap.Raw.getKey?_eq_some_getKey {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a : α} {h' : a ∈ t} : t.getKey? a = some (t.getKey a h')

theorem Std.TreeMap.Raw.compare_getKey_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (h' : k ∈ t) : cmp (t.getKey k h') k = Ordering.eq

theorem Std.TreeMap.Raw.getKey_congr {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k₁ k₂ : α} (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t) : t.getKey k₁ h₁ = t.getKey k₂ ⋯

@[simp]

theorem Std.TreeMap.Raw.getKey_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} (h' : k ∈ t) : t.getKey k h' = k

@[simp]

theorem Std.TreeMap.Raw.getKey!_emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a : α} [Inhabited α] : ∅.getKey! a = default

theorem Std.TreeMap.Raw.getKey!_of_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} : t.isEmpty = true → t.getKey! a = default

theorem Std.TreeMap.Raw.getKey!_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k a : α} {v : β} : (t.insert k v).getKey! a = if cmp k a = Ordering.eq then k else t.getKey! a

@[simp]

theorem Std.TreeMap.Raw.getKey!_insert_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} {b : β} : (t.insert a b).getKey! a = a

theorem Std.TreeMap.Raw.getKey!_eq_default_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} : t.contains a = false → t.getKey! a = default

theorem Std.TreeMap.Raw.getKey!_eq_default {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} : ¬a ∈ t → t.getKey! a = default

theorem Std.TreeMap.Raw.getKey!_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k a : α} : (t.erase k).getKey! a = if cmp k a = Ordering.eq then default else t.getKey! a

@[simp]

theorem Std.TreeMap.Raw.getKey!_erase_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} : (t.erase k).getKey! k = default

theorem Std.TreeMap.Raw.getKey?_eq_some_getKey!_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} : t.contains a = true → t.getKey? a = some (t.getKey! a)

theorem Std.TreeMap.Raw.getKey?_eq_some_getKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} : a ∈ t → t.getKey? a = some (t.getKey! a)

theorem Std.TreeMap.Raw.getKey!_eq_get!_getKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} : t.getKey! a = (t.getKey? a).get!

theorem Std.TreeMap.Raw.getKey_eq_getKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} {h' : a ∈ t} : t.getKey a h' = t.getKey! a

theorem Std.TreeMap.Raw.getKey!_congr {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k k' : α} (h' : cmp k k' = Ordering.eq) : t.getKey! k = t.getKey! k'

theorem Std.TreeMap.Raw.getKey!_eq_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k : α} (h' : t.contains k = true) : t.getKey! k = k

theorem Std.TreeMap.Raw.getKey!_eq_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k : α} (h' : k ∈ t) : t.getKey! k = k

@[simp]

theorem Std.TreeMap.Raw.getKeyD_emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a fallback : α} : ∅.getKeyD a fallback = fallback

theorem Std.TreeMap.Raw.getKeyD_of_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} : t.isEmpty = true → t.getKeyD a fallback = fallback

theorem Std.TreeMap.Raw.getKeyD_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a fallback : α} {v : β} : (t.insert k v).getKeyD a fallback = if cmp k a = Ordering.eq then k else t.getKeyD a fallback

@[simp]

theorem Std.TreeMap.Raw.getKeyD_insert_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} {b : β} : (t.insert a b).getKeyD a fallback = a

theorem Std.TreeMap.Raw.getKeyD_eq_fallback_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} : t.contains a = false → t.getKeyD a fallback = fallback

theorem Std.TreeMap.Raw.getKeyD_eq_fallback {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} : ¬a ∈ t → t.getKeyD a fallback = fallback

theorem Std.TreeMap.Raw.getKeyD_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {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.TreeMap.Raw.getKeyD_erase_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k fallback : α} : (t.erase k).getKeyD k fallback = fallback

theorem Std.TreeMap.Raw.getKey?_eq_some_getKeyD_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} : t.contains a = true → t.getKey? a = some (t.getKeyD a fallback)

theorem Std.TreeMap.Raw.getKey?_eq_some_getKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} : a ∈ t → t.getKey? a = some (t.getKeyD a fallback)

theorem Std.TreeMap.Raw.getKeyD_eq_getD_getKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} : t.getKeyD a fallback = (t.getKey? a).getD fallback

theorem Std.TreeMap.Raw.getKey_eq_getKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {a fallback : α} {h' : a ∈ t} : t.getKey a h' = t.getKeyD a fallback

theorem Std.TreeMap.Raw.getKey!_eq_getKeyD_default {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {a : α} : t.getKey! a = t.getKeyD a default

theorem Std.TreeMap.Raw.getKeyD_congr {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' fallback : α} (h' : cmp k k' = Ordering.eq) : t.getKeyD k fallback = t.getKeyD k' fallback

theorem Std.TreeMap.Raw.getKeyD_eq_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k fallback : α} (h' : t.contains k = true) : t.getKeyD k fallback = k

theorem Std.TreeMap.Raw.getKeyD_eq_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k fallback : α} (h' : k ∈ t) : t.getKeyD k fallback = k

@[simp]

theorem Std.TreeMap.Raw.isEmpty_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insertIfNew k v).isEmpty = false

@[simp]

theorem Std.TreeMap.Raw.contains_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : (t.insertIfNew k v).contains a = (cmp k a == Ordering.eq || t.contains a)

@[simp]

theorem Std.TreeMap.Raw.mem_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : a ∈ t.insertIfNew k v ↔ cmp k a = Ordering.eq ∨ a ∈ t

theorem Std.TreeMap.Raw.contains_insertIfNew_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insertIfNew k v).contains k = true

theorem Std.TreeMap.Raw.mem_insertIfNew_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : k ∈ t.insertIfNew k v

theorem Std.TreeMap.Raw.contains_of_contains_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : (t.insertIfNew k v).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true

theorem Std.TreeMap.Raw.mem_of_mem_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : a ∈ t.insertIfNew k v → cmp k a ≠ Ordering.eq → a ∈ t

theorem Std.TreeMap.Raw.mem_of_mem_insertIfNew' {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : 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.TreeMap.Raw.size_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {k : α} (h : t.WF) {v : β} : (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1

theorem Std.TreeMap.Raw.size_le_size_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : t.size ≤ (t.insertIfNew k v).size

theorem Std.TreeMap.Raw.size_insertIfNew_le {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insertIfNew k v).size ≤ t.size + 1

theorem Std.TreeMap.Raw.getElem?_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : (t.insertIfNew k v)[a]? = if cmp k a = Ordering.eq ∧ ¬k ∈ t then some v else t[a]?

theorem Std.TreeMap.Raw.getElem_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} {h₁ : a ∈ t.insertIfNew k v} : (t.insertIfNew k v)[a] = if h₂ : cmp k a = Ordering.eq ∧ ¬k ∈ t then v else t[a]

theorem Std.TreeMap.Raw.getElem!_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited β] (h : t.WF) {k a : α} {v : β} : (t.insertIfNew k v)[a]! = if cmp k a = Ordering.eq ∧ ¬k ∈ t then v else t[a]!

theorem Std.TreeMap.Raw.getD_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {fallback v : β} : (t.insertIfNew k v).getD a fallback = if cmp k a = Ordering.eq ∧ ¬k ∈ t then v else t.getD a fallback

theorem Std.TreeMap.Raw.getKey?_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} : (t.insertIfNew k v).getKey? a = if cmp k a = Ordering.eq ∧ ¬k ∈ t then some k else t.getKey? a

theorem Std.TreeMap.Raw.getKey_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a : α} {v : β} {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.TreeMap.Raw.getKey!_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k a : α} {v : β} : (t.insertIfNew k v).getKey! a = if cmp k a = Ordering.eq ∧ ¬k ∈ t then k else t.getKey! a

theorem Std.TreeMap.Raw.getKeyD_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k a fallback : α} {v : β} : (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.TreeMap.Raw.getThenInsertIfNew?_fst {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.getThenInsertIfNew? k v).fst = t.get? k

@[simp]

theorem Std.TreeMap.Raw.getThenInsertIfNew?_snd {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.getThenInsertIfNew? k v).snd = t.insertIfNew k v

@[simp]

theorem Std.TreeMap.Raw.length_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.keys.length = t.size

@[simp]

theorem Std.TreeMap.Raw.isEmpty_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} : t.keys.isEmpty = t.isEmpty

@[simp]

theorem Std.TreeMap.Raw.contains_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : t.keys.contains k = t.contains k

@[simp]

theorem Std.TreeMap.Raw.mem_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : k ∈ t.keys ↔ k ∈ t

theorem Std.TreeMap.Raw.distinct_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) t.keys

theorem Std.TreeMap.Raw.ordered_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : List.Pairwise (fun (a b : α) => cmp a b = Ordering.lt) t.keys

@[simp]

theorem Std.TreeMap.Raw.map_fst_toList_eq_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} : List.map Prod.fst t.toList = t.keys

@[simp]

theorem Std.TreeMap.Raw.length_toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} (h : t.WF) : t.toList.length = t.size

@[simp]

theorem Std.TreeMap.Raw.isEmpty_toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} : t.toList.isEmpty = t.isEmpty

@[simp]

theorem Std.TreeMap.Raw.mem_toList_iff_getElem?_eq_some {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β} : (k, v) ∈ t.toList ↔ t[k]? = some v

@[simp]

theorem Std.TreeMap.Raw.mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (k, v) ∈ t.toList ↔ t.getKey? k = some k ∧ t[k]? = some v

theorem Std.TreeMap.Raw.getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : t[k]? = some v ↔ ∃ (k' : α), cmp k k' = Ordering.eq ∧ (k', v) ∈ t.toList

theorem Std.TreeMap.Raw.find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {v : β} : List.find? (fun (x : α × β) => cmp x.fst k == Ordering.eq) t.toList = some (k', v) ↔ t.getKey? k = some k' ∧ t[k]? = some v

theorem Std.TreeMap.Raw.find?_toList_eq_none_iff_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} : List.find? (fun (x : α × β) => cmp x.fst k == Ordering.eq) t.toList = none ↔ t.contains k = false

@[simp]

theorem Std.TreeMap.Raw.find?_toList_eq_none_iff_not_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} : List.find? (fun (x : α × β) => cmp x.fst k == Ordering.eq) t.toList = none ↔ ¬k ∈ t

theorem Std.TreeMap.Raw.distinct_keys_toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : List.Pairwise (fun (a b : α × β) => ¬cmp a.fst b.fst = Ordering.eq) t.toList

theorem Std.TreeMap.Raw.ordered_keys_toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : List.Pairwise (fun (a b : α × β) => cmp a.fst b.fst = Ordering.lt) t.toList

theorem Std.TreeMap.Raw.foldlM_eq_foldlM_toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {δ : Type w} {m : Type w → Type w} [Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ} : foldlM f init t = List.foldlM (fun (a : δ) (b : α × β) => f a b.fst b.snd) init t.toList

theorem Std.TreeMap.Raw.foldl_eq_foldl_toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {δ : Type w} {f : δ → α → β → δ} {init : δ} : foldl f init t = List.foldl (fun (a : δ) (b : α × β) => f a b.fst b.snd) init t.toList

theorem Std.TreeMap.Raw.foldrM_eq_foldrM_toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {δ : Type w} {m : Type w → Type w} [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} : foldrM f init t = List.foldrM (fun (a : α × β) (b : δ) => f a.fst a.snd b) init t.toList

theorem Std.TreeMap.Raw.foldr_eq_foldr_toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {δ : Type w} {f : α → β → δ → δ} {init : δ} : foldr f init t = List.foldr (fun (a : α × β) (b : δ) => f a.fst a.snd b) init t.toList

@[simp]

theorem Std.TreeMap.Raw.forM_eq_forM {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {m : Type w → Type w} [Monad m] [LawfulMonad m] {f : α → β → m PUnit} : forM f t = ForM.forM t fun (a : α × β) => f a.fst a.snd

theorem Std.TreeMap.Raw.forM_eq_forM_toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {m : Type w → Type w} [Monad m] [LawfulMonad m] {f : α × β → m PUnit} : ForM.forM t f = t.toList.forM f

@[simp]

theorem Std.TreeMap.Raw.forIn_eq_forIn {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {δ : Type w} {m : Type w → Type w} [Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ} : forIn f init t = ForIn.forIn t init fun (a : α × β) (d : δ) => f a.fst a.snd d

theorem Std.TreeMap.Raw.forIn_eq_forIn_toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {δ : Type w} {m : Type w → Type w} [Monad m] [LawfulMonad m] {f : α × β → δ → m (ForInStep δ)} {init : δ} : ForIn.forIn t init f = ForIn.forIn t.toList init f

theorem Std.TreeMap.Raw.foldlM_eq_foldlM_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {δ : Type w} {m : Type w → Type w} [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : foldlM (fun (d : δ) (a : α) (x : β) => f d a) init t = List.foldlM f init t.keys

theorem Std.TreeMap.Raw.foldl_eq_foldl_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {δ : Type w} {f : δ → α → δ} {init : δ} : foldl (fun (d : δ) (a : α) (x : β) => f d a) init t = List.foldl f init t.keys

theorem Std.TreeMap.Raw.foldrM_eq_foldrM_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {δ : Type w} {m : Type w → Type w} [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : foldrM (fun (a : α) (x : β) (d : δ) => f a d) init t = List.foldrM f init t.keys

theorem Std.TreeMap.Raw.foldr_eq_foldr_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {δ : Type w} {f : α → δ → δ} {init : δ} : foldr (fun (a : α) (x : β) (d : δ) => f a d) init t = List.foldr f init t.keys

theorem Std.TreeMap.Raw.forM_eq_forM_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {m : Type w → Type w} [Monad m] [LawfulMonad m] {f : α → m PUnit} : (ForM.forM t fun (a : α × β) => f a.fst) = t.keys.forM f

theorem Std.TreeMap.Raw.forIn_eq_forIn_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {δ : Type w} {m : Type w → Type w} [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} : (ForIn.forIn t init fun (a : α × β) (d : δ) => f a.fst d) = ForIn.forIn t.keys init f

@[simp]

theorem Std.TreeMap.Raw.insertMany_nil {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} : t.insertMany [] = t

@[simp]

theorem Std.TreeMap.Raw.insertMany_list_singleton {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {k : α} {v : β} : t.insertMany [(k, v)] = t.insert k v

theorem Std.TreeMap.Raw.insertMany_cons {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {l : List (α × β)} {k : α} {v : β} : t.insertMany ((k, v) :: l) = (t.insert k v).insertMany l

theorem Std.TreeMap.Raw.insertMany_append {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} {l₁ l₂ : List (α × β)} : t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂

@[simp]

theorem Std.TreeMap.Raw.contains_insertMany_list {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α} : (t.insertMany l).contains k = (t.contains k || (List.map Prod.fst l).contains k)

@[simp]

theorem Std.TreeMap.Raw.mem_insertMany_list {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α} : k ∈ t.insertMany l ↔ k ∈ t ∨ (List.map Prod.fst l).contains k = true

theorem Std.TreeMap.Raw.mem_of_mem_insertMany_list {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α} : k ∈ t.insertMany l → (List.map Prod.fst l).contains k = false → k ∈ t

theorem Std.TreeMap.Raw.getKey?_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (t.insertMany l).getKey? k = t.getKey? k

theorem Std.TreeMap.Raw.getKey?_insertMany_list_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {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) : (t.insertMany l).getKey? k' = some k

theorem Std.TreeMap.Raw.getKey_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ t.insertMany l} : (t.insertMany l).getKey k h' = t.getKey k ⋯

theorem Std.TreeMap.Raw.getKey_insertMany_list_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {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' ∈ t.insertMany l} : (t.insertMany l).getKey k' h' = k

theorem Std.TreeMap.Raw.getKey!_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] (h : t.WF) {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (t.insertMany l).getKey! k = t.getKey! k

theorem Std.TreeMap.Raw.getKey!_insertMany_list_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {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) : (t.insertMany l).getKey! k' = k

theorem Std.TreeMap.Raw.getKeyD_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k fallback : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (t.insertMany l).getKeyD k fallback = t.getKeyD k fallback

theorem Std.TreeMap.Raw.getKeyD_insertMany_list_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {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) : (t.insertMany l).getKeyD k' fallback = k

theorem Std.TreeMap.Raw.size_insertMany_list {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {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) → (t.insertMany l).size = t.size + l.length

theorem Std.TreeMap.Raw.size_le_size_insertMany_list {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {l : List (α × β)} : t.size ≤ (t.insertMany l).size

theorem Std.TreeMap.Raw.size_insertMany_list_le {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {l : List (α × β)} : (t.insertMany l).size ≤ t.size + l.length

@[simp]

theorem Std.TreeMap.Raw.isEmpty_insertMany_list {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {l : List (α × β)} : (t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty)

theorem Std.TreeMap.Raw.getElem?_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (t.insertMany l)[k]? = t[k]?

theorem Std.TreeMap.Raw.getElem?_insertMany_list_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {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) : (t.insertMany l)[k']? = some v

theorem Std.TreeMap.Raw.getElem?_insertMany_list {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α} : (t.insertMany l)[k]? = (List.findSomeRev? (fun (x : α × β) => match x with | (a, b) => if cmp a k = Ordering.eq then some b else none) l).or t[k]?

theorem Std.TreeMap.Raw.getElem_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α} (contains : (List.map Prod.fst l).contains k = false) {h' : k ∈ t.insertMany l} : (t.insertMany l)[k] = t.get k ⋯

theorem Std.TreeMap.Raw.getElem_insertMany_list_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {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' ∈ t.insertMany l} : (t.insertMany l)[k'] = v

theorem Std.TreeMap.Raw.getElem_insertMany_list {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [PartialEquivBEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α} {h' : k ∈ t.insertMany l} : (t.insertMany l)[k] = match w : List.findSomeRev? (fun (x : α × β) => match x with | (a, b) => if cmp a k = Ordering.eq then some b else none) l with | some v => v | none => t[k]

theorem Std.TreeMap.Raw.getElem!_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α} [Inhabited β] (contains_eq_false : (List.map Prod.fst l).contains k = false) : (t.insertMany l)[k]! = t.get! k

theorem Std.TreeMap.Raw.getElem!_insertMany_list_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {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) : (t.insertMany l)[k']! = v

theorem Std.TreeMap.Raw.getElem!_insertMany_list {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited β] (h : t.WF) {l : List (α × β)} {k : α} : (t.insertMany l)[k]! = (List.findSomeRev? (fun (x : α × β) => match x with | (a, b) => if cmp a k = Ordering.eq then some b else none) l).getD t[k]!

theorem Std.TreeMap.Raw.getD_insertMany_list_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (t.insertMany l).getD k fallback = t.getD k fallback

theorem Std.TreeMap.Raw.getD_insertMany_list_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {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) : (t.insertMany l).getD k' fallback = v

theorem Std.TreeMap.Raw.getD_insertMany_list {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α} {fallback : β} : (t.insertMany l).getD k fallback = (List.findSomeRev? (fun (x : α × β) => match x with | (a, b) => if cmp a k = Ordering.eq then some b else none) l).getD (t.getD k fallback)

@[simp]

theorem Std.TreeMap.Raw.insertManyIfNewUnit_nil {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} : t.insertManyIfNewUnit [] = t

@[simp]

theorem Std.TreeMap.Raw.insertManyIfNewUnit_list_singleton {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} {k : α} : t.insertManyIfNewUnit [k] = t.insertIfNew k ()

theorem Std.TreeMap.Raw.insertManyIfNewUnit_cons {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} {l : List α} {k : α} : t.insertManyIfNewUnit (k :: l) = (t.insertIfNew k ()).insertManyIfNewUnit l

@[simp]

theorem Std.TreeMap.Raw.contains_insertManyIfNewUnit_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k : α} : (t.insertManyIfNewUnit l).contains k = (t.contains k || l.contains k)

@[simp]

theorem Std.TreeMap.Raw.mem_insertManyIfNewUnit_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k : α} : k ∈ t.insertManyIfNewUnit l ↔ k ∈ t ∨ l.contains k = true

theorem Std.TreeMap.Raw.mem_of_mem_insertManyIfNewUnit_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k : α} (contains_eq_false : l.contains k = false) : k ∈ t.insertManyIfNewUnit l → k ∈ t

theorem Std.TreeMap.Raw.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k : α} (not_mem : ¬k ∈ t) (contains_eq_false : l.contains k = false) : (t.insertManyIfNewUnit l).getKey? k = none

theorem Std.TreeMap.Raw.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] (h : t.WF) {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (not_mem : ¬k ∈ t) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) : (t.insertManyIfNewUnit l).getKey? k' = some k

theorem Std.TreeMap.Raw.getKey?_insertManyIfNewUnit_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] (h : t.WF) {l : List α} {k : α} (mem : k ∈ t) : (t.insertManyIfNewUnit l).getKey? k = t.getKey? k

theorem Std.TreeMap.Raw.getKey_insertManyIfNewUnit_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] (h : t.WF) {l : List α} {k : α} {h' : k ∈ t.insertManyIfNewUnit l} (contains : k ∈ t) : (t.insertManyIfNewUnit l).getKey k h' = t.getKey k contains

theorem Std.TreeMap.Raw.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] (h : t.WF) {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {h' : k' ∈ t.insertManyIfNewUnit l} (not_mem : ¬k ∈ t) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) : (t.insertManyIfNewUnit l).getKey k' h' = k

theorem Std.TreeMap.Raw.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] (h : t.WF) {l : List α} {k : α} (not_mem : ¬k ∈ t) (contains_eq_false : l.contains k = false) : (t.insertManyIfNewUnit l).getKey! k = default

theorem Std.TreeMap.Raw.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) (not_mem : ¬k ∈ t) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) : (t.insertManyIfNewUnit l).getKey! k' = k

theorem Std.TreeMap.Raw.getKey!_insertManyIfNewUnit_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {l : List α} {k : α} (mem : k ∈ t) : (t.insertManyIfNewUnit l).getKey! k = t.getKey! k

theorem Std.TreeMap.Raw.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k fallback : α} (not_mem : ¬k ∈ t) (contains_eq_false : l.contains k = false) : (t.insertManyIfNewUnit l).getKeyD k fallback = fallback

theorem Std.TreeMap.Raw.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] (h : t.WF) {l : List α} {k k' fallback : α} (k_eq : cmp k k' = Ordering.eq) (not_mem : ¬k ∈ t) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) : (t.insertManyIfNewUnit l).getKeyD k' fallback = k

theorem Std.TreeMap.Raw.getKeyD_insertManyIfNewUnit_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] (h : t.WF) {l : List α} {k fallback : α} (mem : k ∈ t) : (t.insertManyIfNewUnit l).getKeyD k fallback = t.getKeyD k fallback

theorem Std.TreeMap.Raw.size_insertManyIfNewUnit_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) : (∀ (a : α), a ∈ t → l.contains a = false) → (t.insertManyIfNewUnit l).size = t.size + l.length

theorem Std.TreeMap.Raw.size_le_size_insertManyIfNewUnit_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] (h : t.WF) {l : List α} : t.size ≤ (t.insertManyIfNewUnit l).size

theorem Std.TreeMap.Raw.size_insertManyIfNewUnit_list_le {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] (h : t.WF) {l : List α} : (t.insertManyIfNewUnit l).size ≤ t.size + l.length

@[simp]

theorem Std.TreeMap.Raw.isEmpty_insertManyIfNewUnit_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] (h : t.WF) {l : List α} : (t.insertManyIfNewUnit l).isEmpty = (t.isEmpty && l.isEmpty)

@[simp]

theorem Std.TreeMap.Raw.getElem?_insertManyIfNewUnit_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k : α} : (t.insertManyIfNewUnit l)[k]? = if k ∈ t ∨ l.contains k = true then some () else none

@[simp]

theorem Std.TreeMap.Raw.getElem_insertManyIfNewUnit_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} {l : List α} {k : α} {h' : k ∈ t.insertManyIfNewUnit l} : (t.insertManyIfNewUnit l)[k] = ()

@[simp]

theorem Std.TreeMap.Raw.getElem!_insertManyIfNewUnit_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} {l : List α} {k : α} : (t.insertManyIfNewUnit l)[k]! = ()

@[simp]

theorem Std.TreeMap.Raw.getD_insertManyIfNewUnit_list {α : Type u} {cmp : α → α → Ordering} {t : Raw α Unit cmp} {l : List α} {k : α} {fallback : Unit} : (t.insertManyIfNewUnit l).getD k fallback = ()

@[simp]

theorem Std.TreeMap.Raw.ofList_nil {α : Type u} {β : Type v} {cmp : α → α → Ordering} : ofList [] cmp = ∅

@[simp]

theorem Std.TreeMap.Raw.ofList_singleton {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α} {v : β} : ofList [(k, v)] cmp = ∅.insert k v

theorem Std.TreeMap.Raw.ofList_cons {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α} {v : β} {tl : List (α × β)} : ofList ((k, v) :: tl) cmp = (∅.insert k v).insertMany tl

@[simp]

theorem Std.TreeMap.Raw.contains_ofList {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} : (ofList l cmp).contains k = (List.map Prod.fst l).contains k

@[simp]

theorem Std.TreeMap.Raw.mem_ofList {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} : k ∈ ofList l cmp ↔ (List.map Prod.fst l).contains k = true

theorem Std.TreeMap.Raw.getElem?_ofList_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (ofList l cmp)[k]? = none

theorem Std.TreeMap.Raw.getElem?_ofList_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} [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) : (ofList l cmp)[k']? = some v

theorem Std.TreeMap.Raw.getElem_ofList_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} [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} : (ofList l cmp)[k'] = v

theorem Std.TreeMap.Raw.getElem!_ofList_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} [Inhabited β] (contains_eq_false : (List.map Prod.fst l).contains k = false) : (ofList l cmp)[k]! = default

theorem Std.TreeMap.Raw.getElem!_ofList_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} [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) : (ofList l cmp)[k']! = v

theorem Std.TreeMap.Raw.getD_ofList_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (ofList l cmp).getD k fallback = fallback

theorem Std.TreeMap.Raw.getD_ofList_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} [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) : (ofList l cmp).getD k' fallback = v

theorem Std.TreeMap.Raw.getKey?_ofList_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} [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.TreeMap.Raw.getKey?_ofList_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} [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.TreeMap.Raw.getKey_ofList_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} [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.TreeMap.Raw.getKey!_ofList_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false) : (ofList l cmp).getKey! k = default

theorem Std.TreeMap.Raw.getKey!_ofList_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} [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.TreeMap.Raw.getKeyD_ofList_of_contains_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} [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.TreeMap.Raw.getKeyD_ofList_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} [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.TreeMap.Raw.size_ofList {α : Type u} {β : Type v} {cmp : α → α → Ordering} [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.TreeMap.Raw.size_ofList_le {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {l : List (α × β)} : (ofList l cmp).size ≤ l.length

theorem Std.TreeMap.Raw.isEmpty_ofList {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] {l : List (α × β)} : (ofList l cmp).isEmpty = l.isEmpty

@[simp]

theorem Std.TreeMap.Raw.unitOfList_nil {α : Type u} {cmp : α → α → Ordering} : unitOfList [] cmp = ∅

@[simp]

theorem Std.TreeMap.Raw.unitOfList_singleton {α : Type u} {cmp : α → α → Ordering} {k : α} : unitOfList [k] cmp = ∅.insertIfNew k ()

theorem Std.TreeMap.Raw.unitOfList_cons {α : Type u} {cmp : α → α → Ordering} {hd : α} {tl : List α} : unitOfList (hd :: tl) cmp = (∅.insertIfNew hd ()).insertManyIfNewUnit tl

@[simp]

theorem Std.TreeMap.Raw.contains_unitOfList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : (unitOfList l cmp).contains k = l.contains k

@[simp]

theorem Std.TreeMap.Raw.mem_unitOfList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : k ∈ unitOfList l cmp ↔ l.contains k = true

theorem Std.TreeMap.Raw.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) : (unitOfList l cmp).getKey? k = none

theorem Std.TreeMap.Raw.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.TreeMap.Raw.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.TreeMap.Raw.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) : (unitOfList l cmp).getKey! k = default

theorem Std.TreeMap.Raw.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.TreeMap.Raw.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.TreeMap.Raw.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.TreeMap.Raw.size_unitOfList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) : (unitOfList l cmp).size = l.length

theorem Std.TreeMap.Raw.size_unitOfList_le {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} : (unitOfList l cmp).size ≤ l.length

@[simp]

theorem Std.TreeMap.Raw.isEmpty_unitOfList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} : (unitOfList l cmp).isEmpty = l.isEmpty

@[simp]

theorem Std.TreeMap.Raw.getElem?_unitOfList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : (unitOfList l cmp)[k]? = if l.contains k = true then some () else none

@[simp]

theorem Std.TreeMap.Raw.getElem_unitOfList {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α} {h : k ∈ unitOfList l cmp} : (unitOfList l cmp)[k] = ()

@[simp]

theorem Std.TreeMap.Raw.getElem!_unitOfList {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α} : (unitOfList l cmp)[k]! = ()

@[simp]

theorem Std.TreeMap.Raw.getD_unitOfList {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α} {fallback : Unit} : (unitOfList l cmp).getD k fallback = ()

theorem Std.TreeMap.Raw.isEmpty_alter_eq_isEmpty_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} : (t.alter k f).isEmpty = ((t.erase k).isEmpty && (f t[k]?).isNone)

@[simp]

theorem Std.TreeMap.Raw.isEmpty_alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} : (t.alter k f).isEmpty = ((t.isEmpty || t.size == 1 && t.contains k) && (f t[k]?).isNone)

theorem Std.TreeMap.Raw.contains_alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {f : Option β → Option β} : (t.alter k f).contains k' = if cmp k k' = Ordering.eq then (f t[k]?).isSome else t.contains k'

theorem Std.TreeMap.Raw.mem_alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {f : Option β → Option β} : k' ∈ t.alter k f ↔ if cmp k k' = Ordering.eq then (f t[k]?).isSome = true else k' ∈ t

theorem Std.TreeMap.Raw.mem_alter_of_compare_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {f : Option β → Option β} (he : cmp k k' = Ordering.eq) : k' ∈ t.alter k f ↔ (f t[k]?).isSome = true

@[simp]

theorem Std.TreeMap.Raw.contains_alter_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} : (t.alter k f).contains k = (f t[k]?).isSome

@[simp]

theorem Std.TreeMap.Raw.mem_alter_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} : k ∈ t.alter k f ↔ (f t[k]?).isSome = true

theorem Std.TreeMap.Raw.contains_alter_of_not_compare_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {f : Option β → Option β} (he : ¬cmp k k' = Ordering.eq) : (t.alter k f).contains k' = t.contains k'

theorem Std.TreeMap.Raw.mem_alter_of_not_compare_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {f : Option β → Option β} (he : ¬cmp k k' = Ordering.eq) : k' ∈ t.alter k f ↔ k' ∈ t

theorem Std.TreeMap.Raw.size_alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} : (t.alter k f).size = if k ∈ t ∧ (f t[k]?).isNone = true then t.size - 1 else if ¬k ∈ t ∧ (f t[k]?).isSome = true then t.size + 1 else t.size

theorem Std.TreeMap.Raw.size_alter_eq_add_one {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} (h₁ : ¬k ∈ t) (h₂ : (f t[k]?).isSome = true) : (t.alter k f).size = t.size + 1

theorem Std.TreeMap.Raw.size_alter_eq_sub_one {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} (h₁ : k ∈ t) (h₂ : (f t[k]?).isNone = true) : (t.alter k f).size = t.size - 1

theorem Std.TreeMap.Raw.size_alter_eq_self_of_not_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} (h₁ : ¬k ∈ t) (h₂ : (f t[k]?).isNone = true) : (t.alter k f).size = t.size

theorem Std.TreeMap.Raw.size_alter_eq_self_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} (h₁ : k ∈ t) (h₂ : (f t[k]?).isSome = true) : (t.alter k f).size = t.size

theorem Std.TreeMap.Raw.size_alter_le_size {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} : (t.alter k f).size ≤ t.size + 1

theorem Std.TreeMap.Raw.size_le_size_alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} : t.size - 1 ≤ (t.alter k f).size

theorem Std.TreeMap.Raw.getElem?_alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {f : Option β → Option β} : (t.alter k f)[k']? = if cmp k k' = Ordering.eq then f t[k]? else t[k']?

@[simp]

theorem Std.TreeMap.Raw.getElem?_alter_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} : (t.alter k f)[k]? = f t[k]?

theorem Std.TreeMap.Raw.getElem_alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {f : Option β → Option β} {hc : k' ∈ t.alter k f} : (t.alter k f)[k'] = if heq : cmp k k' = Ordering.eq then (f t[k]?).get ⋯ else t[k']

@[simp]

theorem Std.TreeMap.Raw.getElem_alter_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} {hc : k ∈ t.alter k f} : (t.alter k f)[k] = (f t[k]?).get ⋯

theorem Std.TreeMap.Raw.getElem!_alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} [Inhabited β] {f : Option β → Option β} : (t.alter k f)[k']! = if cmp k k' = Ordering.eq then (f t[k]?).get! else t[k']!

@[simp]

theorem Std.TreeMap.Raw.getElem!_alter_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} [Inhabited β] {f : Option β → Option β} : (t.alter k f)[k]! = (f t[k]?).get!

theorem Std.TreeMap.Raw.getD_alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {fallback : β} {f : Option β → Option β} : (t.alter k f).getD k' fallback = if cmp k k' = Ordering.eq then (f t[k]?).getD fallback else t.getD k' fallback

@[simp]

theorem Std.TreeMap.Raw.getD_alter_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {fallback : β} {f : Option β → Option β} : (t.alter k f).getD k fallback = (f t[k]?).getD fallback

theorem Std.TreeMap.Raw.getKey?_alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {f : Option β → Option β} : (t.alter k f).getKey? k' = if cmp k k' = Ordering.eq then if (f t[k]?).isSome = true then some k else none else t.getKey? k'

theorem Std.TreeMap.Raw.getKey?_alter_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} : (t.alter k f).getKey? k = if (f t[k]?).isSome = true then some k else none

theorem Std.TreeMap.Raw.getKey!_alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k k' : α} {f : Option β → Option β} : (t.alter k f).getKey! k' = if cmp k k' = Ordering.eq then if (f t[k]?).isSome = true then k else default else t.getKey! k'

theorem Std.TreeMap.Raw.getKey!_alter_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {f : Option β → Option β} : (t.alter k f).getKey! k = if (f t[k]?).isSome = true then k else default

theorem Std.TreeMap.Raw.getKey_alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k k' : α} {f : Option β → Option β} {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.TreeMap.Raw.getKey_alter_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {f : Option β → Option β} {hc : k ∈ t.alter k f} : (t.alter k f).getKey k hc = k

theorem Std.TreeMap.Raw.getKeyD_alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' fallback : α} {f : Option β → Option β} : (t.alter k f).getKeyD k' fallback = if cmp k k' = Ordering.eq then if (f t[k]?).isSome = true then k else fallback else t.getKeyD k' fallback

@[simp]

theorem Std.TreeMap.Raw.getKeyD_alter_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k fallback : α} {f : Option β → Option β} : (t.alter k f).getKeyD k fallback = if (f t[k]?).isSome = true then k else fallback

@[simp]

theorem Std.TreeMap.Raw.isEmpty_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} : (t.modify k f).isEmpty = t.isEmpty

theorem Std.TreeMap.Raw.contains_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {f : β → β} : (t.modify k f).contains k' = t.contains k'

theorem Std.TreeMap.Raw.mem_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {f : β → β} : k' ∈ t.modify k f ↔ k' ∈ t

theorem Std.TreeMap.Raw.size_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} : (t.modify k f).size = t.size

theorem Std.TreeMap.Raw.getElem?_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {f : β → β} : (t.modify k f)[k']? = if cmp k k' = Ordering.eq then Option.map f t[k]? else t[k']?

@[simp]

theorem Std.TreeMap.Raw.getElem?_modify_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} : (t.modify k f)[k]? = Option.map f t[k]?

theorem Std.TreeMap.Raw.getElem_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {f : β → β} {hc : k' ∈ t.modify k f} : (t.modify k f)[k'] = if heq : cmp k k' = Ordering.eq then f t[k] else t[k']

@[simp]

theorem Std.TreeMap.Raw.getElem_modify_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} {hc : k ∈ t.modify k f} : (t.modify k f)[k] = f t[k]

theorem Std.TreeMap.Raw.getElem!_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} [hi : Inhabited β] {f : β → β} : (t.modify k f)[k']! = if cmp k k' = Ordering.eq then (Option.map f t[k]?).get! else t[k']!

@[simp]

theorem Std.TreeMap.Raw.getElem!_modify_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} [Inhabited β] {f : β → β} : (t.modify k f)[k]! = (Option.map f t[k]?).get!

theorem Std.TreeMap.Raw.getD_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {fallback : β} {f : β → β} : (t.modify k f).getD k' fallback = if cmp k k' = Ordering.eq then (Option.map f t[k]?).getD fallback else t.getD k' fallback

@[simp]

theorem Std.TreeMap.Raw.getD_modify_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {fallback : β} {f : β → β} : (t.modify k f).getD k fallback = (Option.map f t[k]?).getD fallback

theorem Std.TreeMap.Raw.getKey?_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' : α} {f : β → β} : (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.TreeMap.Raw.getKey?_modify_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} : (t.modify k f).getKey? k = if k ∈ t then some k else none

theorem Std.TreeMap.Raw.getKey!_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) [Inhabited α] {k k' : α} {f : β → β} : (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.TreeMap.Raw.getKey!_modify_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) [Inhabited α] {k : α} {f : β → β} : (t.modify k f).getKey! k = if k ∈ t then k else default

theorem Std.TreeMap.Raw.getKey_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) [Inhabited α] {k k' : α} {f : β → β} {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.TreeMap.Raw.getKey_modify_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) [Inhabited α] {k : α} {f : β → β} {hc : k ∈ t.modify k f} : (t.modify k f).getKey k hc = k

theorem Std.TreeMap.Raw.getKeyD_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k k' fallback : α} {f : β → β} : (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.TreeMap.Raw.getKeyD_modify_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) [Inhabited α] {k fallback : α} {f : β → β} : (t.modify k f).getKeyD k fallback = if k ∈ t then k else fallback

@[simp]

theorem Std.TreeMap.Raw.minKey?_emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} : empty.minKey? = none

theorem Std.TreeMap.Raw.minKey?_of_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = true) : t.minKey? = none

@[simp]

theorem Std.TreeMap.Raw.minKey?_eq_none_iff {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.minKey? = none ↔ t.isEmpty = true

theorem Std.TreeMap.Raw.minKey?_eq_some_iff_getKey?_eq_self_and_forall {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {km : α} : t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true

theorem Std.TreeMap.Raw.minKey?_eq_some_iff_mem_and_forall {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {km : α} : t.minKey? = some km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true

@[simp]

theorem Std.TreeMap.Raw.isNone_minKey?_eq_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.minKey?.isNone = t.isEmpty

@[simp]

theorem Std.TreeMap.Raw.isSome_minKey?_eq_not_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.minKey?.isSome = !t.isEmpty

theorem Std.TreeMap.Raw.isSome_minKey?_iff_isEmpty_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.minKey?.isSome = true ↔ t.isEmpty = false

theorem Std.TreeMap.Raw.minKey?_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insert k v).minKey? = some (t.minKey?.elim k fun (k' : α) => if (cmp k k').isLE = true then k else k')

theorem Std.TreeMap.Raw.isSome_minKey?_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insert k v).minKey?.isSome = true

theorem Std.TreeMap.Raw.minKey?_insert_le_minKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {km kmi : α} (hkm : t.minKey? = some km) (hkmi : (t.insert k v).minKey?.get ⋯ = kmi) : (cmp kmi km).isLE = true

theorem Std.TreeMap.Raw.minKey?_insert_le_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {kmi : α} (hkmi : (t.insert k v).minKey?.get ⋯ = kmi) : (cmp kmi k).isLE = true

theorem Std.TreeMap.Raw.contains_minKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {km : α} (hkm : t.minKey? = some km) : t.contains km = true

theorem Std.TreeMap.Raw.isSome_minKey?_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : t.contains k = true) : t.minKey?.isSome = true

theorem Std.TreeMap.Raw.isSome_minKey?_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} : k ∈ t → t.minKey?.isSome = true

theorem Std.TreeMap.Raw.minKey?_le_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k km : α} (hc : t.contains k = true) (hkm : t.minKey?.get ⋯ = km) : (cmp km k).isLE = true

theorem Std.TreeMap.Raw.minKey?_le_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k km : α} (hc : k ∈ t) (hkm : t.minKey?.get ⋯ = km) : (cmp km k).isLE = true

theorem Std.TreeMap.Raw.le_minKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {k : α} (h : t.WF) : (∀ (k' : α), t.minKey? = some k' → (cmp k k').isLE = true) ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true

theorem Std.TreeMap.Raw.getKey?_minKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {km : α} (hkm : t.minKey? = some km) : t.getKey? km = some km

theorem Std.TreeMap.Raw.getKey_minKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {km : α} {hc : t.contains km = true} (hkm : t.minKey?.get ⋯ = km) : t.getKey km hc = km

theorem Std.TreeMap.Raw.getKey!_minKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {km : α} (hkm : t.minKey? = some km) : t.getKey! km = km

theorem Std.TreeMap.Raw.getKeyD_minKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {km fallback : α} (hkm : t.minKey? = some km) : t.getKeyD km fallback = km

@[simp]

theorem Std.TreeMap.Raw.minKey?_bind_getKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.minKey?.bind t.getKey? = t.minKey?

theorem Std.TreeMap.Raw.minKey?_erase_eq_iff_not_compare_eq_minKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} : (t.erase k).minKey? = t.minKey? ↔ ∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq

theorem Std.TreeMap.Raw.minKey?_erase_eq_of_not_compare_eq_minKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : ∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq) : (t.erase k).minKey? = t.minKey?

theorem Std.TreeMap.Raw.isSome_minKey?_of_isSome_minKey?_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (hs : (t.erase k).minKey?.isSome = true) : t.minKey?.isSome = true

theorem Std.TreeMap.Raw.minKey?_le_minKey?_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k km kme : α} (hkme : (t.erase k).minKey? = some kme) (hkm : t.minKey?.get ⋯ = km) : (cmp km kme).isLE = true

theorem Std.TreeMap.Raw.minKey?_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insertIfNew k v).minKey? = some (t.minKey?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k')

theorem Std.TreeMap.Raw.isSome_minKey?_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insertIfNew k v).minKey?.isSome = true

theorem Std.TreeMap.Raw.minKey?_insertIfNew_le_minKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {km kmi : α} (hkm : t.minKey? = some km) (hkmi : (t.insertIfNew k v).minKey?.get ⋯ = kmi) : (cmp kmi km).isLE = true

theorem Std.TreeMap.Raw.minKey?_insertIfNew_le_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {kmi : α} (hkmi : (t.insertIfNew k v).minKey?.get ⋯ = kmi) : (cmp kmi k).isLE = true

theorem Std.TreeMap.Raw.minKey?_eq_head?_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.minKey? = t.keys.head?

theorem Std.TreeMap.Raw.minKey?_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} : (t.modify k f).minKey? = Option.map (fun (km : α) => if cmp km k = Ordering.eq then k else km) t.minKey?

@[simp]

theorem Std.TreeMap.Raw.minKey?_modify_eq_minKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {f : β → β} : (t.modify k f).minKey? = t.minKey?

theorem Std.TreeMap.Raw.isSome_minKey?_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {k : α} {f : β → β} (h : t.WF) : (t.modify k f).minKey?.isSome = !t.isEmpty

theorem Std.TreeMap.Raw.isSome_minKey?_modify_eq_isSome {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} : (t.modify k f).minKey?.isSome = t.minKey?.isSome

theorem Std.TreeMap.Raw.compare_minKey?_modify_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} {km kmm : α} (hkm : t.minKey? = some km) (hkmm : (t.modify k f).minKey?.get ⋯ = kmm) : cmp kmm km = Ordering.eq

theorem Std.TreeMap.Raw.minKey?_alter_eq_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} : (t.alter k f).minKey? = some k ↔ (f (t.get? k)).isSome = true ∧ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true

theorem Std.TreeMap.Raw.minKey?_eq_some_minKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) : t.minKey? = some t.minKey!

theorem Std.TreeMap.Raw.minKey!_eq_default {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = true) : t.minKey! = default

theorem Std.TreeMap.Raw.minKey!_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {km : α} : t.minKey! = km ↔ t.getKey? km = some km ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true

theorem Std.TreeMap.Raw.minKey!_eq_iff_mem_and_forall {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {km : α} : t.minKey! = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true

theorem Std.TreeMap.Raw.minKey!_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {v : β} : (t.insert k v).minKey! = t.minKey?.elim k fun (k' : α) => if (cmp k k').isLE = true then k else k'

theorem Std.TreeMap.Raw.minKey!_insert_le_minKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k : α} {v : β} : (cmp (t.insert k v).minKey! t.minKey!).isLE = true

theorem Std.TreeMap.Raw.minKey!_insert_le_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {v : β} : (cmp (t.insert k v).minKey! k).isLE = true

theorem Std.TreeMap.Raw.contains_minKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) : t.contains t.minKey! = true

theorem Std.TreeMap.Raw.minKey!_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) : t.minKey! ∈ t

theorem Std.TreeMap.Raw.minKey!_le_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (hc : t.contains k = true) : (cmp t.minKey! k).isLE = true

theorem Std.TreeMap.Raw.minKey!_le_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (hc : k ∈ t) : (cmp t.minKey! k).isLE = true

theorem Std.TreeMap.Raw.le_minKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k : α} : (cmp k t.minKey!).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true

theorem Std.TreeMap.Raw.getKey?_minKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) : t.getKey? t.minKey! = some t.minKey!

theorem Std.TreeMap.Raw.getKey_minKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {hc : t.minKey! ∈ t} : t.getKey t.minKey! hc = t.minKey!

theorem Std.TreeMap.Raw.getKey!_minKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) : t.getKey! t.minKey! = t.minKey!

theorem Std.TreeMap.Raw.getKeyD_minKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback : α} : t.getKeyD t.minKey! fallback = t.minKey!

theorem Std.TreeMap.Raw.minKey!_erase_eq_of_not_compare_minKey!_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) (heq : ¬cmp k t.minKey! = Ordering.eq) : (t.erase k).minKey! = t.minKey!

theorem Std.TreeMap.Raw.minKey!_le_minKey!_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) : (cmp t.minKey! (t.erase k).minKey!).isLE = true

theorem Std.TreeMap.Raw.minKey!_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {v : β} : (t.insertIfNew k v).minKey! = t.minKey?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'

theorem Std.TreeMap.Raw.minKey!_insertIfNew_le_minKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k : α} {v : β} : (cmp (t.insertIfNew k v).minKey! t.minKey!).isLE = true

theorem Std.TreeMap.Raw.minKey!_insertIfNew_le_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {v : β} : (cmp (t.insertIfNew k v).minKey! k).isLE = true

theorem Std.TreeMap.Raw.minKey!_eq_head!_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) : t.minKey! = t.keys.head!

theorem Std.TreeMap.Raw.minKey!_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {f : β → β} (he : (t.modify k f).isEmpty = false) : (t.modify k f).minKey! = if cmp t.minKey! k = Ordering.eq then k else t.minKey!

@[simp]

theorem Std.TreeMap.Raw.minKey!_modify_eq_minKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k : α} {f : β → β} : (t.modify k f).minKey! = t.minKey!

theorem Std.TreeMap.Raw.compare_minKey!_modify_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {f : β → β} : cmp (t.modify k f).minKey! t.minKey! = Ordering.eq

@[simp]

theorem Std.TreeMap.Raw.ordCompare_minKey!_modify_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Raw α β compare} [Inhabited α] (h : t.WF) {k : α} {f : β → β} : compare (t.modify k f).minKey! t.minKey! = Ordering.eq

theorem Std.TreeMap.Raw.minKey!_alter_eq_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {f : Option β → Option β} (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.TreeMap.Raw.minKey?_eq_some_minKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} : t.minKey? = some (t.minKeyD fallback)

theorem Std.TreeMap.Raw.minKeyD_eq_fallback {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = true) {fallback : α} : t.minKeyD fallback = fallback

theorem Std.TreeMap.Raw.minKey!_eq_minKeyD_default {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) : t.minKey! = t.minKeyD default

theorem Std.TreeMap.Raw.minKeyD_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (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.TreeMap.Raw.minKeyD_eq_iff_mem_and_forall {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) (he : t.isEmpty = false) {km fallback : α} : t.minKeyD fallback = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true

theorem Std.TreeMap.Raw.minKeyD_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {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.TreeMap.Raw.minKeyD_insert_le_minKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {k : α} {v : β} {fallback : α} : (cmp ((t.insert k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true

theorem Std.TreeMap.Raw.minKeyD_insert_le_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {fallback : α} : (cmp ((t.insert k v).minKeyD fallback) k).isLE = true

theorem Std.TreeMap.Raw.contains_minKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} : t.contains (t.minKeyD fallback) = true

theorem Std.TreeMap.Raw.minKeyD_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} : t.minKeyD fallback ∈ t

theorem Std.TreeMap.Raw.minKeyD_le_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : t.contains k = true) {fallback : α} : (cmp (t.minKeyD fallback) k).isLE = true

theorem Std.TreeMap.Raw.minKeyD_le_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : k ∈ t) {fallback : α} : (cmp (t.minKeyD fallback) k).isLE = true

theorem Std.TreeMap.Raw.le_minKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {k fallback : α} : (cmp k (t.minKeyD fallback)).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true

theorem Std.TreeMap.Raw.getKey?_minKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} : t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback)

theorem Std.TreeMap.Raw.getKey_minKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {fallback : α} {hc : t.minKeyD fallback ∈ t} : t.getKey (t.minKeyD fallback) hc = t.minKeyD fallback

theorem Std.TreeMap.Raw.getKey!_minKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback : α} : t.getKey! (t.minKeyD fallback) = t.minKeyD fallback

theorem Std.TreeMap.Raw.getKeyD_minKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback fallback' : α} : t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback

theorem Std.TreeMap.Raw.minKeyD_erase_eq_of_not_compare_minKeyD_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {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.TreeMap.Raw.minKeyD_le_minKeyD_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) {fallback : α} : (cmp (t.minKeyD fallback) ((t.erase k).minKeyD fallback)).isLE = true

theorem Std.TreeMap.Raw.minKeyD_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {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.TreeMap.Raw.minKeyD_insertIfNew_le_minKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {k : α} {v : β} {fallback : α} : (cmp ((t.insertIfNew k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true

theorem Std.TreeMap.Raw.minKeyD_insertIfNew_le_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {fallback : α} : (cmp ((t.insertIfNew k v).minKeyD fallback) k).isLE = true

theorem Std.TreeMap.Raw.minKeyD_eq_headD_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {fallback : α} : t.minKeyD fallback = t.keys.headD fallback

theorem Std.TreeMap.Raw.minKeyD_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} (he : (t.modify k f).isEmpty = false) {fallback : α} : (t.modify k f).minKeyD fallback = if cmp (t.minKeyD fallback) k = Ordering.eq then k else t.minKeyD fallback

@[simp]

theorem Std.TreeMap.Raw.minKeyD_modify_eq_minKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {f : β → β} {fallback : α} : (t.modify k f).minKeyD fallback = t.minKeyD fallback

theorem Std.TreeMap.Raw.compare_minKeyD_modify_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} {fallback : α} : cmp ((t.modify k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq

@[simp]

theorem Std.TreeMap.Raw.ordCompare_minKeyD_modify_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Raw α β compare} (h : t.WF) {k : α} {f : β → β} {fallback : α} : compare ((t.modify k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq

theorem Std.TreeMap.Raw.minKeyD_alter_eq_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} (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

@[simp]

theorem Std.TreeMap.Raw.maxKey?_emptyc {α : Type u} {β : Type v} {cmp : α → α → Ordering} : empty.maxKey? = none

theorem Std.TreeMap.Raw.maxKey?_of_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = true) : t.maxKey? = none

@[simp]

theorem Std.TreeMap.Raw.maxKey?_eq_none_iff {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.maxKey? = none ↔ t.isEmpty = true

theorem Std.TreeMap.Raw.maxKey?_eq_some_iff_getKey?_eq_self_and_forall {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {km : α} : t.maxKey? = some km ↔ t.getKey? km = some km ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true

theorem Std.TreeMap.Raw.maxKey?_eq_some_iff_mem_and_forall {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {km : α} : t.maxKey? = some km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true

@[simp]

theorem Std.TreeMap.Raw.isNone_maxKey?_eq_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.maxKey?.isNone = t.isEmpty

@[simp]

theorem Std.TreeMap.Raw.isSome_maxKey?_eq_not_isEmpty {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.maxKey?.isSome = !t.isEmpty

theorem Std.TreeMap.Raw.isSome_maxKey?_iff_isEmpty_eq_false {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.maxKey?.isSome = true ↔ t.isEmpty = false

theorem Std.TreeMap.Raw.maxKey?_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insert k v).maxKey? = some (t.maxKey?.elim k fun (k' : α) => if (cmp k' k).isLE = true then k else k')

theorem Std.TreeMap.Raw.isSome_maxKey?_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insert k v).maxKey?.isSome = true

theorem Std.TreeMap.Raw.maxKey?_le_maxKey?_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {km kmi : α} (hkm : t.maxKey? = some km) (hkmi : (t.insert k v).maxKey?.get ⋯ = kmi) : (cmp km kmi).isLE = true

theorem Std.TreeMap.Raw.self_le_maxKey?_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {kmi : α} (hkmi : (t.insert k v).maxKey?.get ⋯ = kmi) : (cmp k kmi).isLE = true

theorem Std.TreeMap.Raw.contains_maxKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {km : α} (hkm : t.maxKey? = some km) : t.contains km = true

theorem Std.TreeMap.Raw.isSome_maxKey?_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : t.contains k = true) : t.maxKey?.isSome = true

theorem Std.TreeMap.Raw.isSome_maxKey?_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} : k ∈ t → t.maxKey?.isSome = true

theorem Std.TreeMap.Raw.le_maxKey?_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k km : α} (hc : t.contains k = true) (hkm : t.maxKey?.get ⋯ = km) : (cmp k km).isLE = true

theorem Std.TreeMap.Raw.le_maxKey?_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k km : α} (hc : k ∈ t) (hkm : t.maxKey?.get ⋯ = km) : (cmp k km).isLE = true

theorem Std.TreeMap.Raw.maxKey?_le {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {k : α} (h : t.WF) : (∀ (k' : α), t.maxKey? = some k' → (cmp k' k).isLE = true) ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true

theorem Std.TreeMap.Raw.getKey?_maxKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {km : α} (hkm : t.maxKey? = some km) : t.getKey? km = some km

theorem Std.TreeMap.Raw.getKey_maxKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {km : α} {hc : t.contains km = true} (hkm : t.maxKey?.get ⋯ = km) : t.getKey km hc = km

theorem Std.TreeMap.Raw.getKey!_maxKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {km : α} (hkm : t.maxKey? = some km) : t.getKey! km = km

theorem Std.TreeMap.Raw.getKeyD_maxKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {km fallback : α} (hkm : t.maxKey? = some km) : t.getKeyD km fallback = km

@[simp]

theorem Std.TreeMap.Raw.maxKey?_bind_getKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.maxKey?.bind t.getKey? = t.maxKey?

theorem Std.TreeMap.Raw.maxKey?_erase_eq_iff_not_compare_eq_maxKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} : (t.erase k).maxKey? = t.maxKey? ↔ ∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq

theorem Std.TreeMap.Raw.maxKey?_erase_eq_of_not_compare_eq_maxKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : ∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq) : (t.erase k).maxKey? = t.maxKey?

theorem Std.TreeMap.Raw.isSome_maxKey?_of_isSome_maxKey?_erase {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (hs : (t.erase k).maxKey?.isSome = true) : t.maxKey?.isSome = true

theorem Std.TreeMap.Raw.maxKey?_erase_le_maxKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k km kme : α} (hkme : (t.erase k).maxKey? = some kme) (hkm : t.maxKey?.get ⋯ = km) : (cmp kme km).isLE = true

theorem Std.TreeMap.Raw.maxKey?_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insertIfNew k v).maxKey? = some (t.maxKey?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k')

theorem Std.TreeMap.Raw.isSome_maxKey?_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insertIfNew k v).maxKey?.isSome = true

theorem Std.TreeMap.Raw.maxKey?_le_maxKey?_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {km kmi : α} (hkm : t.maxKey? = some km) (hkmi : (t.insertIfNew k v).maxKey?.get ⋯ = kmi) : (cmp km kmi).isLE = true

theorem Std.TreeMap.Raw.self_le_maxKey?_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {kmi : α} (hkmi : (t.insertIfNew k v).maxKey?.get ⋯ = kmi) : (cmp k kmi).isLE = true

theorem Std.TreeMap.Raw.maxKey?_eq_getLast?_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) : t.maxKey? = t.keys.getLast?

theorem Std.TreeMap.Raw.maxKey?_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} : (t.modify k f).maxKey? = Option.map (fun (km : α) => if cmp km k = Ordering.eq then k else km) t.maxKey?

@[simp]

theorem Std.TreeMap.Raw.maxKey?_modify_eq_maxKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {f : β → β} : (t.modify k f).maxKey? = t.maxKey?

theorem Std.TreeMap.Raw.isSome_maxKey?_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] {k : α} {f : β → β} (h : t.WF) : (t.modify k f).maxKey?.isSome = !t.isEmpty

theorem Std.TreeMap.Raw.isSome_maxKey?_modify_eq_isSome {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} : (t.modify k f).maxKey?.isSome = t.maxKey?.isSome

theorem Std.TreeMap.Raw.compare_maxKey?_modify_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} {km kmm : α} (hkm : t.maxKey? = some km) (hkmm : (t.modify k f).maxKey?.get ⋯ = kmm) : cmp kmm km = Ordering.eq

theorem Std.TreeMap.Raw.maxKey?_alter_eq_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} : (t.alter k f).maxKey? = some k ↔ (f (t.get? k)).isSome = true ∧ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true

theorem Std.TreeMap.Raw.maxKey?_eq_some_maxKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) : t.maxKey? = some t.maxKey!

theorem Std.TreeMap.Raw.maxKey!_eq_default {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = true) : t.maxKey! = default

theorem Std.TreeMap.Raw.maxKey!_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {km : α} : t.maxKey! = km ↔ t.getKey? km = some km ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true

theorem Std.TreeMap.Raw.maxKey!_eq_iff_mem_and_forall {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {km : α} : t.maxKey! = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true

theorem Std.TreeMap.Raw.maxKey!_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {v : β} : (t.insert k v).maxKey! = t.maxKey?.elim k fun (k' : α) => if (cmp k' k).isLE = true then k else k'

theorem Std.TreeMap.Raw.maxKey!_le_maxKey!_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k : α} {v : β} : (cmp t.maxKey! (t.insert k v).maxKey!).isLE = true

theorem Std.TreeMap.Raw.self_le_maxKey!_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {v : β} : (cmp k (t.insert k v).maxKey!).isLE = true

theorem Std.TreeMap.Raw.contains_maxKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) : t.contains t.maxKey! = true

theorem Std.TreeMap.Raw.maxKey!_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) : t.maxKey! ∈ t

theorem Std.TreeMap.Raw.le_maxKey!_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (hc : t.contains k = true) : (cmp k t.maxKey!).isLE = true

theorem Std.TreeMap.Raw.le_maxKey!_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (hc : k ∈ t) : (cmp k t.maxKey!).isLE = true

theorem Std.TreeMap.Raw.maxKey!_le {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k : α} : (cmp t.maxKey! k).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true

theorem Std.TreeMap.Raw.getKey?_maxKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) : t.getKey? t.maxKey! = some t.maxKey!

theorem Std.TreeMap.Raw.getKey_maxKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {hc : t.maxKey! ∈ t} : t.getKey t.maxKey! hc = t.maxKey!

theorem Std.TreeMap.Raw.getKey!_maxKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) : t.getKey! t.maxKey! = t.maxKey!

theorem Std.TreeMap.Raw.getKeyD_maxKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback : α} : t.getKeyD t.maxKey! fallback = t.maxKey!

theorem Std.TreeMap.Raw.maxKey!_erase_eq_of_not_compare_maxKey!_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) (heq : ¬cmp k t.maxKey! = Ordering.eq) : (t.erase k).maxKey! = t.maxKey!

theorem Std.TreeMap.Raw.maxKey!_erase_le_maxKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) : (cmp (t.erase k).maxKey! t.maxKey!).isLE = true

theorem Std.TreeMap.Raw.maxKey!_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {v : β} : (t.insertIfNew k v).maxKey! = t.maxKey?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'

theorem Std.TreeMap.Raw.maxKey!_le_maxKey!_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k : α} {v : β} : (cmp t.maxKey! (t.insertIfNew k v).maxKey!).isLE = true

theorem Std.TreeMap.Raw.self_le_maxKey!_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {v : β} : (cmp k (t.insertIfNew k v).maxKey!).isLE = true

theorem Std.TreeMap.Raw.maxKey!_eq_getLast!_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) : t.maxKey! = t.keys.getLast!

theorem Std.TreeMap.Raw.maxKey!_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {f : β → β} (he : (t.modify k f).isEmpty = false) : (t.modify k f).maxKey! = if cmp t.maxKey! k = Ordering.eq then k else t.maxKey!

@[simp]

theorem Std.TreeMap.Raw.maxKey!_modify_eq_maxKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k : α} {f : β → β} : (t.modify k f).maxKey! = t.maxKey!

theorem Std.TreeMap.Raw.compare_maxKey!_modify_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {f : β → β} : cmp (t.modify k f).maxKey! t.maxKey! = Ordering.eq

@[simp]

theorem Std.TreeMap.Raw.ordCompare_maxKey!_modify_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Raw α β compare} [Inhabited α] (h : t.WF) {k : α} {f : β → β} : compare (t.modify k f).maxKey! t.maxKey! = Ordering.eq

theorem Std.TreeMap.Raw.maxKey!_alter_eq_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} {f : Option β → Option β} (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.TreeMap.Raw.maxKey?_eq_some_maxKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} : t.maxKey? = some (t.maxKeyD fallback)

theorem Std.TreeMap.Raw.maxKeyD_eq_fallback {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = true) {fallback : α} : t.maxKeyD fallback = fallback

theorem Std.TreeMap.Raw.maxKey!_eq_maxKeyD_default {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) : t.maxKey! = t.maxKeyD default

theorem Std.TreeMap.Raw.maxKeyD_eq_iff_getKey?_eq_self_and_forall {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (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.TreeMap.Raw.maxKeyD_eq_iff_mem_and_forall {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) (he : t.isEmpty = false) {km fallback : α} : t.maxKeyD fallback = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true

theorem Std.TreeMap.Raw.maxKeyD_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {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.TreeMap.Raw.maxKeyD_le_maxKeyD_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {k : α} {v : β} {fallback : α} : (cmp (t.maxKeyD fallback) ((t.insert k v).maxKeyD fallback)).isLE = true

theorem Std.TreeMap.Raw.self_le_maxKeyD_insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {fallback : α} : (cmp k ((t.insert k v).maxKeyD fallback)).isLE = true

theorem Std.TreeMap.Raw.contains_maxKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} : t.contains (t.maxKeyD fallback) = true

theorem Std.TreeMap.Raw.maxKeyD_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} : t.maxKeyD fallback ∈ t

theorem Std.TreeMap.Raw.le_maxKeyD_of_contains {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : t.contains k = true) {fallback : α} : (cmp k (t.maxKeyD fallback)).isLE = true

theorem Std.TreeMap.Raw.le_maxKeyD_of_mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (hc : k ∈ t) {fallback : α} : (cmp k (t.maxKeyD fallback)).isLE = true

theorem Std.TreeMap.Raw.maxKeyD_le {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {k fallback : α} : (cmp (t.maxKeyD fallback) k).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true

theorem Std.TreeMap.Raw.getKey?_maxKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback : α} : t.getKey? (t.maxKeyD fallback) = some (t.maxKeyD fallback)

theorem Std.TreeMap.Raw.getKey_maxKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {fallback : α} {hc : t.maxKeyD fallback ∈ t} : t.getKey (t.maxKeyD fallback) hc = t.maxKeyD fallback

theorem Std.TreeMap.Raw.getKey!_maxKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback : α} : t.getKey! (t.maxKeyD fallback) = t.maxKeyD fallback

theorem Std.TreeMap.Raw.getKeyD_maxKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback fallback' : α} : t.getKeyD (t.maxKeyD fallback) fallback' = t.maxKeyD fallback

theorem Std.TreeMap.Raw.maxKeyD_erase_eq_of_not_compare_maxKeyD_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {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.TreeMap.Raw.maxKeyD_erase_le_maxKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} (he : (t.erase k).isEmpty = false) {fallback : α} : (cmp ((t.erase k).maxKeyD fallback) (t.maxKeyD fallback)).isLE = true

theorem Std.TreeMap.Raw.maxKeyD_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {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.TreeMap.Raw.maxKeyD_le_maxKeyD_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {k : α} {v : β} {fallback : α} : (cmp (t.maxKeyD fallback) ((t.insertIfNew k v).maxKeyD fallback)).isLE = true

theorem Std.TreeMap.Raw.self_le_maxKeyD_insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {v : β} {fallback : α} : (cmp k ((t.insertIfNew k v).maxKeyD fallback)).isLE = true

theorem Std.TreeMap.Raw.maxKeyD_eq_getLastD_keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {fallback : α} : t.maxKeyD fallback = t.keys.getLastD fallback

theorem Std.TreeMap.Raw.maxKeyD_modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} (he : (t.modify k f).isEmpty = false) {fallback : α} : (t.modify k f).maxKeyD fallback = if cmp (t.maxKeyD fallback) k = Ordering.eq then k else t.maxKeyD fallback

@[simp]

theorem Std.TreeMap.Raw.maxKeyD_modify_eq_maxKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {f : β → β} {fallback : α} : (t.modify k f).maxKeyD fallback = t.maxKeyD fallback

theorem Std.TreeMap.Raw.compare_maxKeyD_modify_eq {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : β → β} {fallback : α} : cmp ((t.modify k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq

@[simp]

theorem Std.TreeMap.Raw.ordCompare_maxKeyD_modify_eq {α : Type u} {β : Type v} [Ord α] [TransOrd α] {t : Raw α β compare} (h : t.WF) {k : α} {f : β → β} {fallback : α} : compare ((t.modify k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq

theorem Std.TreeMap.Raw.maxKeyD_alter_eq_self {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} [TransCmp cmp] (h : t.WF) {k : α} {f : Option β → Option β} (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