Tree set lemmas

This file contains lemmas about Std.ExtTreeSet.

@[simp]

theorem Std.ExtTreeSet.isEmpty_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.isEmpty = true ↔ t = ∅

@[simp]

theorem Std.ExtTreeSet.isEmpty_eq_false_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.isEmpty = false ↔ ¬t = ∅

@[simp]

theorem Std.ExtTreeSet.isEmpty_empty {α : Type u} {cmp : α → α → Ordering} : ∅.isEmpty = true

@[simp]

theorem Std.ExtTreeSet.empty_eq {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} : ∅ = t ↔ t = ∅

@[simp]

theorem Std.ExtTreeSet.insert_ne_empty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : t.insert k ≠ ∅

theorem Std.ExtTreeSet.mem_iff_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : k ∈ t ↔ t.contains k = true

@[simp]

theorem Std.ExtTreeSet.contains_iff_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : t.contains k = true ↔ k ∈ t

theorem Std.ExtTreeSet.contains_congr {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k k' : α} (hab : cmp k k' = Ordering.eq) : t.contains k = t.contains k'

theorem Std.ExtTreeSet.mem_congr {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k k' : α} (hab : cmp k k' = Ordering.eq) : k ∈ t ↔ k' ∈ t

@[simp]

theorem Std.ExtTreeSet.contains_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {k : α} : ∅.contains k = false

@[simp]

theorem Std.ExtTreeSet.not_mem_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {k : α} : ¬k ∈ ∅

theorem Std.ExtTreeSet.eq_empty_iff_forall_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t = ∅ ↔ ∀ (a : α), t.contains a = false

theorem Std.ExtTreeSet.eq_empty_iff_forall_not_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t = ∅ ↔ ∀ (a : α), ¬a ∈ t

theorem Std.ExtTreeSet.ne_empty_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} (h : a ∈ t) : t ≠ ∅

@[simp]

theorem Std.ExtTreeSet.insert_eq_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {p : α} : Insert.insert p t = t.insert p

@[simp]

theorem Std.ExtTreeSet.singleton_eq_insert {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {p : α} : {p} = ∅.insert p

@[simp]

theorem Std.ExtTreeSet.contains_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} : (t.insert k).contains a = (cmp k a == Ordering.eq || t.contains a)

@[simp]

theorem Std.ExtTreeSet.mem_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} : a ∈ t.insert k ↔ cmp k a = Ordering.eq ∨ a ∈ t

theorem Std.ExtTreeSet.contains_insert_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.insert k).contains k = true

theorem Std.ExtTreeSet.mem_insert_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : k ∈ t.insert k

theorem Std.ExtTreeSet.contains_of_contains_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} : (t.insert k).contains a = true → cmp k a ≠ Ordering.eq → t.contains a = true

theorem Std.ExtTreeSet.mem_of_mem_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} : a ∈ t.insert k → cmp k a ≠ Ordering.eq → a ∈ t

theorem Std.ExtTreeSet.mem_of_mem_insert' {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} : a ∈ t.insert k → ¬(cmp k a = Ordering.eq ∧ ¬k ∈ t) → a ∈ t

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

@[simp]

theorem Std.ExtTreeSet.size_empty {α : Type u} {cmp : α → α → Ordering} : ∅.size = 0

theorem Std.ExtTreeSet.isEmpty_eq_size_beq_zero {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} : t.isEmpty = (t.size == 0)

theorem Std.ExtTreeSet.eq_empty_iff_size_eq_zero {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t = ∅ ↔ t.size = 0

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

theorem Std.ExtTreeSet.size_le_size_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : t.size ≤ (t.insert k).size

theorem Std.ExtTreeSet.size_insert_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.insert k).size ≤ t.size + 1

@[simp]

theorem Std.ExtTreeSet.erase_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {k : α} : ∅.erase k = ∅

@[simp]

theorem Std.ExtTreeSet.erase_eq_empty_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : t.erase k = ∅ ↔ t = ∅ ∨ t.size = 1 ∧ k ∈ t

theorem Std.ExtTreeSet.eq_empty_iff_erase_eq_empty_and_not_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (k : α) : t = ∅ ↔ t.erase k = ∅ ∧ ¬k ∈ t

theorem Std.ExtTreeSet.ne_empty_of_erase_ne_empty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (h : t.erase k ≠ ∅) : t ≠ ∅

@[simp]

theorem Std.ExtTreeSet.contains_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} : (t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)

@[simp]

theorem Std.ExtTreeSet.mem_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} : a ∈ t.erase k ↔ cmp k a ≠ Ordering.eq ∧ a ∈ t

theorem Std.ExtTreeSet.contains_of_contains_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} : (t.erase k).contains a = true → t.contains a = true

theorem Std.ExtTreeSet.mem_of_mem_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} : (t.erase k).contains a = true → t.contains a = true

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

theorem Std.ExtTreeSet.size_erase_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.erase k).size ≤ t.size

theorem Std.ExtTreeSet.size_le_size_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : t.size ≤ (t.erase k).size + 1

@[simp]

theorem Std.ExtTreeSet.get?_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a : α} : ∅.get? a = none

theorem Std.ExtTreeSet.get?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} : (t.insert k).get? a = if cmp k a = Ordering.eq ∧ ¬k ∈ t then some k else t.get? a

theorem Std.ExtTreeSet.contains_eq_isSome_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} : t.contains a = (t.get? a).isSome

@[simp]

theorem Std.ExtTreeSet.isSome_get?_eq_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} : (t.get? a).isSome = t.contains a

theorem Std.ExtTreeSet.mem_iff_isSome_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} : a ∈ t ↔ (t.get? a).isSome = true

@[simp]

theorem Std.ExtTreeSet.isSome_get?_iff_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} : (t.get? a).isSome = true ↔ a ∈ t

theorem Std.ExtTreeSet.get?_eq_none_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} : t.contains a = false → t.get? a = none

theorem Std.ExtTreeSet.get?_eq_none {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} : ¬a ∈ t → t.get? a = none

theorem Std.ExtTreeSet.get?_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} : (t.erase k).get? a = if cmp k a = Ordering.eq then none else t.get? a

@[simp]

theorem Std.ExtTreeSet.get?_erase_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.erase k).get? k = none

theorem Std.ExtTreeSet.compare_get?_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : Option.all (fun (x : α) => decide (cmp x k = Ordering.eq)) (t.get? k) = true

theorem Std.ExtTreeSet.get?_congr {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k k' : α} (h' : cmp k k' = Ordering.eq) : t.get? k = t.get? k'

theorem Std.ExtTreeSet.get?_eq_some_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} (h' : t.contains k = true) : t.get? k = some k

theorem Std.ExtTreeSet.get?_eq_some {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} (h' : k ∈ t) : t.get? k = some k

theorem Std.ExtTreeSet.get_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} {h₁ : a ∈ t.insert k} : (t.insert k).get a h₁ = if h₂ : cmp k a = Ordering.eq ∧ ¬k ∈ t then k else t.get a ⋯

@[simp]

theorem Std.ExtTreeSet.get_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a : α} {h' : a ∈ t.erase k} : (t.erase k).get a h' = t.get a ⋯

theorem Std.ExtTreeSet.get?_eq_some_get {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a : α} (h' : a ∈ t) : t.get? a = some (t.get a h')

theorem Std.ExtTreeSet.compare_get_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (h' : k ∈ t) : cmp (t.get k h') k = Ordering.eq

theorem Std.ExtTreeSet.get_congr {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k₁ k₂ : α} (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t) : t.get k₁ h₁ = t.get k₂ ⋯

@[simp]

theorem Std.ExtTreeSet.get_eq {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k : α} (h' : k ∈ t) : t.get k h' = k

@[simp]

theorem Std.ExtTreeSet.get!_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] {a : α} : ∅.get! a = default

theorem Std.ExtTreeSet.get!_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k a : α} : (t.insert k).get! a = if cmp k a = Ordering.eq ∧ ¬k ∈ t then k else t.get! a

theorem Std.ExtTreeSet.get!_eq_default_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} : t.contains a = false → t.get! a = default

theorem Std.ExtTreeSet.get!_eq_default {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} : ¬a ∈ t → t.get! a = default

theorem Std.ExtTreeSet.get!_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k a : α} : (t.erase k).get! a = if cmp k a = Ordering.eq then default else t.get! a

@[simp]

theorem Std.ExtTreeSet.get!_erase_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} : (t.erase k).get! k = default

theorem Std.ExtTreeSet.get?_eq_some_get!_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} : t.contains a = true → t.get? a = some (t.get! a)

theorem Std.ExtTreeSet.get?_eq_some_get! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} : a ∈ t → t.get? a = some (t.get! a)

theorem Std.ExtTreeSet.get!_eq_get!_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} : t.get! a = (t.get? a).get!

theorem Std.ExtTreeSet.get_eq_get! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} {h : a ∈ t} : t.get a h = t.get! a

theorem Std.ExtTreeSet.get!_congr {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k k' : α} (h' : cmp k k' = Ordering.eq) : t.get! k = t.get! k'

theorem Std.ExtTreeSet.get!_eq_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} (h' : t.contains k = true) : t.get! k = k

theorem Std.ExtTreeSet.get!_eq_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k : α} (h' : k ∈ t) : t.get! k = k

@[simp]

theorem Std.ExtTreeSet.getD_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {a fallback : α} : ∅.getD a fallback = fallback

theorem Std.ExtTreeSet.getD_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k a fallback : α} : (t.insert k).getD a fallback = if cmp k a = Ordering.eq ∧ ¬k ∈ t then k else t.getD a fallback

theorem Std.ExtTreeSet.getD_eq_fallback_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a fallback : α} : t.contains a = false → t.getD a fallback = fallback

theorem Std.ExtTreeSet.getD_eq_fallback {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a fallback : α} : ¬a ∈ t → t.getD a fallback = fallback

theorem Std.ExtTreeSet.getD_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.ExtTreeSet.getD_erase_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k fallback : α} : (t.erase k).getD k fallback = fallback

theorem Std.ExtTreeSet.get?_eq_some_getD_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a fallback : α} : t.contains a = true → t.get? a = some (t.getD a fallback)

theorem Std.ExtTreeSet.get?_eq_some_getD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a fallback : α} : a ∈ t → t.get? a = some (t.getD a fallback)

theorem Std.ExtTreeSet.getD_eq_getD_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a fallback : α} : t.getD a fallback = (t.get? a).getD fallback

theorem Std.ExtTreeSet.get_eq_getD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {a fallback : α} {h : a ∈ t} : t.get a h = t.getD a fallback

theorem Std.ExtTreeSet.get!_eq_getD_default {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} : t.get! a = t.getD a default

theorem Std.ExtTreeSet.getD_congr {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k k' fallback : α} (h' : cmp k k' = Ordering.eq) : t.getD k fallback = t.getD k' fallback

theorem Std.ExtTreeSet.getD_eq_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k fallback : α} (h' : t.contains k = true) : t.getD k fallback = k

theorem Std.ExtTreeSet.getD_eq_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {k fallback : α} (h' : k ∈ t) : t.getD k fallback = k

@[simp]

theorem Std.ExtTreeSet.containsThenInsert_fst {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.containsThenInsert k).fst = t.contains k

@[simp]

theorem Std.ExtTreeSet.containsThenInsert_snd {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.containsThenInsert k).snd = t.insert k

@[simp]

theorem Std.ExtTreeSet.length_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.toList.length = t.size

@[simp]

theorem Std.ExtTreeSet.isEmpty_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.toList.isEmpty = t.isEmpty

@[simp]

theorem Std.ExtTreeSet.toList_eq_nil_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.toList = [] ↔ t = ∅

@[simp]

theorem Std.ExtTreeSet.contains_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} : t.toList.contains k = t.contains k

@[simp]

theorem Std.ExtTreeSet.mem_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [LawfulEqCmp cmp] [TransCmp cmp] {k : α} : k ∈ t.toList ↔ k ∈ t

theorem Std.ExtTreeSet.distinct_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) t.toList

theorem Std.ExtTreeSet.ordered_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : List.Pairwise (fun (a b : α) => cmp a b = Ordering.lt) t.toList

theorem Std.ExtTreeSet.foldlM_eq_foldlM_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : foldlM f init t = List.foldlM f init t.toList

theorem Std.ExtTreeSet.foldl_eq_foldl_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {δ : Type w} [TransCmp cmp] {f : δ → α → δ} {init : δ} : foldl f init t = List.foldl f init t.toList

theorem Std.ExtTreeSet.foldrM_eq_foldrM_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : foldrM f init t = List.foldrM f init t.toList

theorem Std.ExtTreeSet.foldr_eq_foldr_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {δ : Type w} [TransCmp cmp] {f : α → δ → δ} {init : δ} : foldr f init t = List.foldr f init t.toList

@[simp]

theorem Std.ExtTreeSet.forM_eq_forM {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → m PUnit} : forM f t = ForM.forM t f

theorem Std.ExtTreeSet.forM_eq_forM_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → m PUnit} : ForM.forM t f = t.toList.forM f

@[simp]

theorem Std.ExtTreeSet.forIn_eq_forIn {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} : forIn f init t = ForIn.forIn t init f

theorem Std.ExtTreeSet.forIn_eq_forIn_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} : ForIn.forIn t init f = ForIn.forIn t.toList init f

@[simp]

theorem Std.ExtTreeSet.insertMany_nil {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.insertMany [] = t

@[simp]

theorem Std.ExtTreeSet.insertMany_list_singleton {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : t.insertMany [k] = t.insert k

theorem Std.ExtTreeSet.insertMany_cons {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} {k : α} : t.insertMany (k :: l) = (t.insert k).insertMany l

theorem Std.ExtTreeSet.insertMany_append {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l₁ l₂ : List α} : t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂

@[simp]

theorem Std.ExtTreeSet.contains_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : (t.insertMany l).contains k = (t.contains k || l.contains k)

@[simp]

theorem Std.ExtTreeSet.mem_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : k ∈ t.insertMany l ↔ k ∈ t ∨ l.contains k = true

theorem Std.ExtTreeSet.mem_of_mem_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} (contains_eq_false : l.contains k = false) : k ∈ t.insertMany l → k ∈ t

theorem Std.ExtTreeSet.get?_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} (not_mem : ¬k ∈ t) (contains_eq_false : l.contains k = false) : (t.insertMany l).get? k = none

theorem Std.ExtTreeSet.get?_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.insertMany l).get? k' = some k

theorem Std.ExtTreeSet.get?_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} {k : α} (mem : k ∈ t) : (t.insertMany l).get? k = t.get? k

theorem Std.ExtTreeSet.get_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} {k : α} {h' : k ∈ t.insertMany l} (contains : k ∈ t) : (t.insertMany l).get k h' = t.get k contains

theorem Std.ExtTreeSet.get_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {h' : k' ∈ t.insertMany l} (not_mem : ¬k ∈ t) (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) (mem : k ∈ l) : (t.insertMany l).get k' h' = k

theorem Std.ExtTreeSet.get!_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α} (not_mem : ¬k ∈ t) (contains_eq_false : l.contains k = false) : (t.insertMany l).get! k = default

theorem Std.ExtTreeSet.get!_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {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.insertMany l).get! k' = k

theorem Std.ExtTreeSet.get!_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {l : List α} {k : α} (mem : k ∈ t) : (t.insertMany l).get! k = t.get! k

theorem Std.ExtTreeSet.getD_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k fallback : α} (not_mem : ¬k ∈ t) (contains_eq_false : l.contains k = false) : (t.insertMany l).getD k fallback = fallback

theorem Std.ExtTreeSet.getD_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {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.insertMany l).getD k' fallback = k

theorem Std.ExtTreeSet.getD_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} {k fallback : α} (mem : k ∈ t) : (t.insertMany l).getD k fallback = t.getD k fallback

theorem Std.ExtTreeSet.size_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) : (∀ (a : α), a ∈ t → l.contains a = false) → (t.insertMany l).size = t.size + l.length

theorem Std.ExtTreeSet.size_le_size_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} : t.size ≤ (t.insertMany l).size

theorem Std.ExtTreeSet.size_insertMany_list_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} : (t.insertMany l).size ≤ t.size + l.length

@[simp]

theorem Std.ExtTreeSet.isEmpty_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} : (t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty)

@[simp]

theorem Std.ExtTreeSet.insertMany_list_eq_empty_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {l : List α} : t.insertMany l = ∅ ↔ t = ∅ ∧ l = []

@[simp]

theorem Std.ExtTreeSet.ofList_nil {α : Type u} {cmp : α → α → Ordering} : ofList [] cmp = ∅

@[simp]

theorem Std.ExtTreeSet.ofList_singleton {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {k : α} : ofList [k] cmp = ∅.insert k

theorem Std.ExtTreeSet.ofList_cons {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {hd : α} {tl : List α} : ofList (hd :: tl) cmp = (∅.insert hd).insertMany tl

theorem Std.ExtTreeSet.ofList_eq_insertMany_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} : ofList l cmp = ∅.insertMany l

@[simp]

theorem Std.ExtTreeSet.contains_ofList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : (ofList l cmp).contains k = l.contains k

@[simp]

theorem Std.ExtTreeSet.mem_ofList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : k ∈ ofList l cmp ↔ l.contains k = true

theorem Std.ExtTreeSet.get?_ofList_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} (contains_eq_false : l.contains k = false) : (ofList l cmp).get? k = none

theorem Std.ExtTreeSet.get?_ofList_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) : (ofList l cmp).get? k' = some k

theorem Std.ExtTreeSet.get_ofList_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' ∈ ofList l cmp} : (ofList l cmp).get k' h' = k

theorem Std.ExtTreeSet.get!_ofList_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α} (contains_eq_false : l.contains k = false) : (ofList l cmp).get! k = default

theorem Std.ExtTreeSet.get!_ofList_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) : (ofList l cmp).get! k' = k

theorem Std.ExtTreeSet.getD_ofList_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k fallback : α} (contains_eq_false : l.contains k = false) : (ofList l cmp).getD k fallback = fallback

theorem Std.ExtTreeSet.getD_ofList_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) : (ofList l cmp).getD k' fallback = k

theorem Std.ExtTreeSet.size_ofList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} (distinct : List.Pairwise (fun (a b : α) => ¬cmp a b = Ordering.eq) l) : (ofList l cmp).size = l.length

theorem Std.ExtTreeSet.size_ofList_le {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} : (ofList l cmp).size ≤ l.length

@[simp]

theorem Std.ExtTreeSet.ofList_eq_empty_iff {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} : ofList l cmp = ∅ ↔ l = []

@[simp]

theorem Std.ExtTreeSet.min?_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] : ∅.min? = none

@[simp]

theorem Std.ExtTreeSet.min?_eq_none_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.min? = none ↔ t = ∅

theorem Std.ExtTreeSet.min?_eq_some_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} : t.min? = some km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true

theorem Std.ExtTreeSet.min?_eq_some_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {km : α} : t.min? = some km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true

@[simp]

theorem Std.ExtTreeSet.isNone_min?_eq_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.min?.isNone = t.isEmpty

@[simp]

theorem Std.ExtTreeSet.isSome_min?_eq_not_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.min?.isSome = !t.isEmpty

theorem Std.ExtTreeSet.isSome_min?_iff_ne_empty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.min?.isSome = true ↔ t ≠ ∅

theorem Std.ExtTreeSet.min?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.insert k).min? = some (t.min?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k')

theorem Std.ExtTreeSet.isSome_min?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.insert k).min?.isSome = true

theorem Std.ExtTreeSet.min?_insert_le_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km kmi : α} (hkm : t.min? = some km) (hkmi : (t.insert k).min?.get ⋯ = kmi) : (cmp kmi km).isLE = true

theorem Std.ExtTreeSet.min?_insert_le_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k kmi : α} (hkmi : (t.insert k).min?.get ⋯ = kmi) : (cmp kmi k).isLE = true

theorem Std.ExtTreeSet.contains_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} (hkm : t.min? = some km) : t.contains km = true

theorem Std.ExtTreeSet.min?_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} (hkm : t.min? = some km) : km ∈ t

theorem Std.ExtTreeSet.isSome_min?_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) : t.min?.isSome = true

theorem Std.ExtTreeSet.isSome_min?_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : k ∈ t → t.min?.isSome = true

theorem Std.ExtTreeSet.min?_le_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km : α} (hc : t.contains k = true) (hkm : t.min?.get ⋯ = km) : (cmp km k).isLE = true

theorem Std.ExtTreeSet.min?_le_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km : α} (hc : k ∈ t) (hkm : t.min?.get ⋯ = km) : (cmp km k).isLE = true

theorem Std.ExtTreeSet.le_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (∀ (k' : α), t.min? = some k' → (cmp k k').isLE = true) ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true

theorem Std.ExtTreeSet.get?_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} (hkm : t.min? = some km) : t.get? km = some km

theorem Std.ExtTreeSet.get_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} {hc : t.contains km = true} (hkm : t.min?.get ⋯ = km) : t.get km hc = km

theorem Std.ExtTreeSet.get!_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {km : α} (hkm : t.min? = some km) : t.get! km = km

theorem Std.ExtTreeSet.getD_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km fallback : α} (hkm : t.min? = some km) : t.getD km fallback = km

@[simp]

theorem Std.ExtTreeSet.min?_bind_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.min?.bind t.get? = t.min?

theorem Std.ExtTreeSet.min?_erase_eq_iff_not_compare_eq_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.erase k).min? = t.min? ↔ ∀ {km : α}, t.min? = some km → ¬cmp k km = Ordering.eq

theorem Std.ExtTreeSet.min?_erase_eq_of_not_compare_eq_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : ∀ {km : α}, t.min? = some km → ¬cmp k km = Ordering.eq) : (t.erase k).min? = t.min?

theorem Std.ExtTreeSet.isSome_min?_of_isSome_min?_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hs : (t.erase k).min?.isSome = true) : t.min?.isSome = true

theorem Std.ExtTreeSet.min?_le_min?_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km kme : α} (hkme : (t.erase k).min? = some kme) (hkm : t.min?.get ⋯ = km) : (cmp km kme).isLE = true

theorem Std.ExtTreeSet.min?_eq_head?_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.min? = t.toList.head?

theorem Std.ExtTreeSet.min_eq_get_min? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} : t.min he = t.min?.get ⋯

theorem Std.ExtTreeSet.min?_eq_some_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) : t.min? = some (t.min he)

theorem Std.ExtTreeSet.min_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} {km : α} : t.min he = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true

theorem Std.ExtTreeSet.min_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {he : t ≠ ∅} {km : α} : t.min he = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true

theorem Std.ExtTreeSet.min_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.insert k).min ⋯ = t.min?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'

theorem Std.ExtTreeSet.min_insert_le_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t ≠ ∅} : (cmp ((t.insert k).min ⋯) (t.min he)).isLE = true

theorem Std.ExtTreeSet.min_insert_le_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (cmp ((t.insert k).min ⋯) k).isLE = true

theorem Std.ExtTreeSet.contains_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} : t.contains (t.min he) = true

theorem Std.ExtTreeSet.min_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} : t.min he ∈ t

theorem Std.ExtTreeSet.min_le_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) : (cmp (t.min ⋯) k).isLE = true

theorem Std.ExtTreeSet.min_le_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : k ∈ t) : (cmp (t.min ⋯) k).isLE = true

theorem Std.ExtTreeSet.le_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t ≠ ∅} : (cmp k (t.min he)).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true

@[simp]

theorem Std.ExtTreeSet.get?_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} : t.get? (t.min he) = some (t.min he)

@[simp]

theorem Std.ExtTreeSet.get_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} {hc : t.min he ∈ t} : t.get (t.min he) hc = t.min he

@[simp]

theorem Std.ExtTreeSet.get!_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {he : t ≠ ∅} : t.get! (t.min he) = t.min he

@[simp]

theorem Std.ExtTreeSet.getD_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} {fallback : α} : t.getD (t.min he) fallback = t.min he

@[simp]

theorem Std.ExtTreeSet.min_erase_eq_iff_not_compare_eq_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t.erase k ≠ ∅} : (t.erase k).min he = t.min ⋯ ↔ ¬cmp k (t.min ⋯) = Ordering.eq

theorem Std.ExtTreeSet.min_erase_eq_of_not_compare_eq_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t.erase k ≠ ∅} (hc : ¬cmp k (t.min ⋯) = Ordering.eq) : (t.erase k).min he = t.min ⋯

theorem Std.ExtTreeSet.min_le_min_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t.erase k ≠ ∅} : (cmp (t.min ⋯) ((t.erase k).min he)).isLE = true

theorem Std.ExtTreeSet.min_eq_head_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} : t.min he = t.toList.head ⋯

theorem Std.ExtTreeSet.min?_eq_some_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) : t.min? = some t.min!

theorem Std.ExtTreeSet.min_eq_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {he : t ≠ ∅} : t.min he = t.min!

theorem Std.ExtTreeSet.min!_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] : ∅.min! = default

theorem Std.ExtTreeSet.min!_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {km : α} : t.min! = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true

theorem Std.ExtTreeSet.min!_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (he : t ≠ ∅) {km : α} : t.min! = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true

theorem Std.ExtTreeSet.min!_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} : (t.insert k).min! = t.min?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'

theorem Std.ExtTreeSet.min!_insert_le_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {k : α} : (cmp (t.insert k).min! t.min!).isLE = true

theorem Std.ExtTreeSet.min!_insert_le_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} : (cmp (t.insert k).min! k).isLE = true

theorem Std.ExtTreeSet.contains_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) : t.contains t.min! = true

theorem Std.ExtTreeSet.min!_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) : t.min! ∈ t

theorem Std.ExtTreeSet.min!_le_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (hc : t.contains k = true) : (cmp t.min! k).isLE = true

theorem Std.ExtTreeSet.min!_le_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (hc : k ∈ t) : (cmp t.min! k).isLE = true

theorem Std.ExtTreeSet.le_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {k : α} : (cmp k t.min!).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true

theorem Std.ExtTreeSet.get?_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) : t.get? t.min! = some t.min!

theorem Std.ExtTreeSet.get_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {hc : t.min! ∈ t} : t.get t.min! hc = t.min!

@[simp]

theorem Std.ExtTreeSet.get_min!_eq_min {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {hc : t.min! ∈ t} : t.get t.min! hc = t.min ⋯

theorem Std.ExtTreeSet.get!_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) : t.get! t.min! = t.min!

theorem Std.ExtTreeSet.getD_min! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {fallback : α} : t.getD t.min! fallback = t.min!

theorem Std.ExtTreeSet.min!_erase_eq_of_not_compare_min!_eq {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (he : t.erase k ≠ ∅) (heq : ¬cmp k t.min! = Ordering.eq) : (t.erase k).min! = t.min!

theorem Std.ExtTreeSet.min!_le_min!_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (he : t.erase k ≠ ∅) : (cmp t.min! (t.erase k).min!).isLE = true

theorem Std.ExtTreeSet.min!_eq_head!_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] : t.min! = t.toList.head!

theorem Std.ExtTreeSet.min?_eq_some_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} : t.min? = some (t.minD fallback)

theorem Std.ExtTreeSet.minD_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {fallback : α} : ∅.minD fallback = fallback

theorem Std.ExtTreeSet.min!_eq_minD_default {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] : t.min! = t.minD default

theorem Std.ExtTreeSet.minD_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {km fallback : α} : t.minD fallback = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true

theorem Std.ExtTreeSet.minD_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (he : t ≠ ∅) {km fallback : α} : t.minD fallback = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp km k).isLE = true

theorem Std.ExtTreeSet.minD_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k fallback : α} : (t.insert k).minD fallback = t.min?.elim k fun (k' : α) => if cmp k k' = Ordering.lt then k else k'

theorem Std.ExtTreeSet.minD_insert_le_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {k fallback : α} : (cmp ((t.insert k).minD fallback) (t.minD fallback)).isLE = true

theorem Std.ExtTreeSet.minD_insert_le_self {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k fallback : α} : (cmp ((t.insert k).minD fallback) k).isLE = true

theorem Std.ExtTreeSet.contains_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} : t.contains (t.minD fallback) = true

theorem Std.ExtTreeSet.minD_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} : t.minD fallback ∈ t

theorem Std.ExtTreeSet.minD_le_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) {fallback : α} : (cmp (t.minD fallback) k).isLE = true

theorem Std.ExtTreeSet.minD_le_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : k ∈ t) {fallback : α} : (cmp (t.minD fallback) k).isLE = true

theorem Std.ExtTreeSet.le_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {k fallback : α} : (cmp k (t.minD fallback)).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k k').isLE = true

theorem Std.ExtTreeSet.get?_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} : t.get? (t.minD fallback) = some (t.minD fallback)

theorem Std.ExtTreeSet.get_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {fallback : α} {hc : t.minD fallback ∈ t} : t.get (t.minD fallback) hc = t.minD fallback

theorem Std.ExtTreeSet.get!_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {fallback : α} : t.get! (t.minD fallback) = t.minD fallback

theorem Std.ExtTreeSet.getD_minD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback fallback' : α} : t.getD (t.minD fallback) fallback' = t.minD fallback

theorem Std.ExtTreeSet.minD_erase_eq_of_not_compare_minD_eq {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k fallback : α} (he : t.erase k ≠ ∅) (heq : ¬cmp k (t.minD fallback) = Ordering.eq) : (t.erase k).minD fallback = t.minD fallback

theorem Std.ExtTreeSet.minD_le_minD_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (he : t.erase k ≠ ∅) {fallback : α} : (cmp (t.minD fallback) ((t.erase k).minD fallback)).isLE = true

theorem Std.ExtTreeSet.minD_eq_headD_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {fallback : α} : t.minD fallback = t.toList.headD fallback

@[simp]

theorem Std.ExtTreeSet.max?_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] : ∅.max? = none

@[simp]

theorem Std.ExtTreeSet.max?_eq_none_iff {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.max? = none ↔ t = ∅

theorem Std.ExtTreeSet.max?_eq_some_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} : t.max? = some km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true

theorem Std.ExtTreeSet.max?_eq_some_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {km : α} : t.max? = some km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true

@[simp]

theorem Std.ExtTreeSet.isNone_max?_eq_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.max?.isNone = t.isEmpty

@[simp]

theorem Std.ExtTreeSet.isSome_max?_eq_not_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.max?.isSome = !t.isEmpty

theorem Std.ExtTreeSet.isSome_max?_iff_ne_empty {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.max?.isSome = true ↔ t ≠ ∅

theorem Std.ExtTreeSet.max?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.insert k).max? = some (t.max?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k')

theorem Std.ExtTreeSet.isSome_max?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.insert k).max?.isSome = true

theorem Std.ExtTreeSet.max?_le_max?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km kmi : α} (hkm : t.max? = some km) (hkmi : (t.insert k).max?.get ⋯ = kmi) : (cmp km kmi).isLE = true

theorem Std.ExtTreeSet.self_le_max?_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k kmi : α} (hkmi : (t.insert k).max?.get ⋯ = kmi) : (cmp k kmi).isLE = true

theorem Std.ExtTreeSet.contains_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} (hkm : t.max? = some km) : t.contains km = true

theorem Std.ExtTreeSet.max?_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} (hkm : t.max? = some km) : km ∈ t

theorem Std.ExtTreeSet.isSome_max?_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) : t.max?.isSome = true

theorem Std.ExtTreeSet.isSome_max?_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : k ∈ t → t.max?.isSome = true

theorem Std.ExtTreeSet.le_max?_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km : α} (hc : t.contains k = true) (hkm : t.max?.get ⋯ = km) : (cmp k km).isLE = true

theorem Std.ExtTreeSet.le_max?_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km : α} (hc : k ∈ t) (hkm : t.max?.get ⋯ = km) : (cmp k km).isLE = true

theorem Std.ExtTreeSet.max?_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (∀ (k' : α), t.max? = some k' → (cmp k' k).isLE = true) ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true

theorem Std.ExtTreeSet.get?_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} (hkm : t.max? = some km) : t.get? km = some km

theorem Std.ExtTreeSet.get_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km : α} {hc : t.contains km = true} (hkm : t.max?.get ⋯ = km) : t.get km hc = km

theorem Std.ExtTreeSet.get!_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {km : α} (hkm : t.max? = some km) : t.get! km = km

theorem Std.ExtTreeSet.getD_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {km fallback : α} (hkm : t.max? = some km) : t.getD km fallback = km

@[simp]

theorem Std.ExtTreeSet.max?_bind_get? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.max?.bind t.get? = t.max?

theorem Std.ExtTreeSet.max?_erase_eq_iff_not_compare_eq_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.erase k).max? = t.max? ↔ ∀ {km : α}, t.max? = some km → ¬cmp k km = Ordering.eq

theorem Std.ExtTreeSet.max?_erase_eq_of_not_compare_eq_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : ∀ {km : α}, t.max? = some km → ¬cmp k km = Ordering.eq) : (t.erase k).max? = t.max?

theorem Std.ExtTreeSet.isSome_max?_of_isSome_max?_erase {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hs : (t.erase k).max?.isSome = true) : t.max?.isSome = true

theorem Std.ExtTreeSet.max?_erase_le_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k km kme : α} (hkme : (t.erase k).max? = some kme) (hkm : t.max?.get ⋯ = km) : (cmp kme km).isLE = true

theorem Std.ExtTreeSet.max?_eq_getLast?_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] : t.max? = t.toList.getLast?

theorem Std.ExtTreeSet.max_eq_get_max? {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} : t.max he = t.max?.get ⋯

theorem Std.ExtTreeSet.max?_eq_some_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) : t.max? = some (t.max he)

theorem Std.ExtTreeSet.max_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} {km : α} : t.max he = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true

theorem Std.ExtTreeSet.max_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] {he : t ≠ ∅} {km : α} : t.max he = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true

theorem Std.ExtTreeSet.max_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (t.insert k).max ⋯ = t.max?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'

theorem Std.ExtTreeSet.max_le_max_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t ≠ ∅} : (cmp (t.max he) ((t.insert k).max ⋯)).isLE = true

theorem Std.ExtTreeSet.self_le_max_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} : (cmp k ((t.insert k).max ⋯)).isLE = true

theorem Std.ExtTreeSet.contains_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} : t.contains (t.max he) = true

theorem Std.ExtTreeSet.max_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} : t.max he ∈ t

theorem Std.ExtTreeSet.le_max_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) : (cmp k (t.max ⋯)).isLE = true

theorem Std.ExtTreeSet.le_max_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : k ∈ t) : (cmp k (t.max ⋯)).isLE = true

theorem Std.ExtTreeSet.max_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t ≠ ∅} : (cmp (t.max he) k).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true

@[simp]

theorem Std.ExtTreeSet.get?_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} : t.get? (t.max he) = some (t.max he)

@[simp]

theorem Std.ExtTreeSet.get_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} {hc : t.max he ∈ t} : t.get (t.max he) hc = t.max he

@[simp]

theorem Std.ExtTreeSet.get!_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {he : t ≠ ∅} : t.get! (t.max he) = t.max he

@[simp]

theorem Std.ExtTreeSet.getD_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} {fallback : α} : t.getD (t.max he) fallback = t.max he

@[simp]

theorem Std.ExtTreeSet.max_erase_eq_iff_not_compare_eq_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t.erase k ≠ ∅} : (t.erase k).max he = t.max ⋯ ↔ ¬cmp k (t.max ⋯) = Ordering.eq

theorem Std.ExtTreeSet.max_erase_eq_of_not_compare_eq_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t.erase k ≠ ∅} (hc : ¬cmp k (t.max ⋯) = Ordering.eq) : (t.erase k).max he = t.max ⋯

theorem Std.ExtTreeSet.max_erase_le_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} {he : t.erase k ≠ ∅} : (cmp ((t.erase k).max he) (t.max ⋯)).isLE = true

theorem Std.ExtTreeSet.max_eq_getLast_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {he : t ≠ ∅} : t.max he = t.toList.getLast ⋯

theorem Std.ExtTreeSet.max?_eq_some_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) : t.max? = some t.max!

theorem Std.ExtTreeSet.max_eq_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {he : t ≠ ∅} : t.max he = t.max!

theorem Std.ExtTreeSet.max!_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] : ∅.max! = default

theorem Std.ExtTreeSet.max!_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {km : α} : t.max! = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true

theorem Std.ExtTreeSet.max!_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (he : t ≠ ∅) {km : α} : t.max! = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true

theorem Std.ExtTreeSet.max!_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} : (t.insert k).max! = t.max?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'

theorem Std.ExtTreeSet.max!_le_max!_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {k : α} : (cmp t.max! (t.insert k).max!).isLE = true

theorem Std.ExtTreeSet.self_le_max!_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} : (cmp k (t.insert k).max!).isLE = true

theorem Std.ExtTreeSet.contains_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) : t.contains t.max! = true

theorem Std.ExtTreeSet.max!_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) : t.max! ∈ t

theorem Std.ExtTreeSet.le_max!_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (hc : t.contains k = true) : (cmp k t.max!).isLE = true

theorem Std.ExtTreeSet.le_max!_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (hc : k ∈ t) : (cmp k t.max!).isLE = true

theorem Std.ExtTreeSet.max!_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {k : α} : (cmp t.max! k).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true

theorem Std.ExtTreeSet.get?_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) : t.get? t.max! = some t.max!

theorem Std.ExtTreeSet.get_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {hc : t.max! ∈ t} : t.get t.max! hc = t.max!

@[simp]

theorem Std.ExtTreeSet.get_max!_eq_max {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {hc : t.max! ∈ t} : t.get t.max! hc = t.max ⋯

theorem Std.ExtTreeSet.get!_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) : t.get! t.max! = t.max!

theorem Std.ExtTreeSet.getD_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {fallback : α} : t.getD t.max! fallback = t.max!

theorem Std.ExtTreeSet.max!_erase_eq_of_not_compare_max!_eq {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (he : t.erase k ≠ ∅) (heq : ¬cmp k t.max! = Ordering.eq) : (t.erase k).max! = t.max!

theorem Std.ExtTreeSet.max!_erase_le_max! {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} (he : t.erase k ≠ ∅) : (cmp (t.erase k).max! t.max!).isLE = true

theorem Std.ExtTreeSet.max!_eq_getLast!_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] : t.max! = t.toList.getLast!

theorem Std.ExtTreeSet.max?_eq_some_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} : t.max? = some (t.maxD fallback)

theorem Std.ExtTreeSet.maxD_empty {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {fallback : α} : ∅.maxD fallback = fallback

theorem Std.ExtTreeSet.max!_eq_maxD_default {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] : t.max! = t.maxD default

theorem Std.ExtTreeSet.maxD_eq_iff_get?_eq_self_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {km fallback : α} : t.maxD fallback = km ↔ t.get? km = some km ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true

theorem Std.ExtTreeSet.maxD_eq_iff_mem_and_forall {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (he : t ≠ ∅) {km fallback : α} : t.maxD fallback = km ↔ km ∈ t ∧ ∀ (k : α), k ∈ t → (cmp k km).isLE = true

theorem Std.ExtTreeSet.maxD_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k fallback : α} : (t.insert k).maxD fallback = t.max?.elim k fun (k' : α) => if cmp k' k = Ordering.lt then k else k'

theorem Std.ExtTreeSet.maxD_le_maxD_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {k fallback : α} : (cmp (t.maxD fallback) ((t.insert k).maxD fallback)).isLE = true

theorem Std.ExtTreeSet.self_le_maxD_insert {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k fallback : α} : (cmp k ((t.insert k).maxD fallback)).isLE = true

theorem Std.ExtTreeSet.contains_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} : t.contains (t.maxD fallback) = true

theorem Std.ExtTreeSet.maxD_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} : t.maxD fallback ∈ t

theorem Std.ExtTreeSet.le_maxD_of_contains {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : t.contains k = true) {fallback : α} : (cmp k (t.maxD fallback)).isLE = true

theorem Std.ExtTreeSet.le_maxD_of_mem {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (hc : k ∈ t) {fallback : α} : (cmp k (t.maxD fallback)).isLE = true

theorem Std.ExtTreeSet.maxD_le {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {k fallback : α} : (cmp (t.maxD fallback) k).isLE = true ↔ ∀ (k' : α), k' ∈ t → (cmp k' k).isLE = true

theorem Std.ExtTreeSet.get?_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback : α} : t.get? (t.maxD fallback) = some (t.maxD fallback)

theorem Std.ExtTreeSet.get_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {fallback : α} {hc : t.maxD fallback ∈ t} : t.get (t.maxD fallback) hc = t.maxD fallback

theorem Std.ExtTreeSet.get!_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t ≠ ∅) {fallback : α} : t.get! (t.maxD fallback) = t.maxD fallback

theorem Std.ExtTreeSet.getD_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] (he : t ≠ ∅) {fallback fallback' : α} : t.getD (t.maxD fallback) fallback' = t.maxD fallback

theorem Std.ExtTreeSet.maxD_erase_eq_of_not_compare_maxD_eq {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k fallback : α} (he : t.erase k ≠ ∅) (heq : ¬cmp k (t.maxD fallback) = Ordering.eq) : (t.erase k).maxD fallback = t.maxD fallback

theorem Std.ExtTreeSet.maxD_erase_le_maxD {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {k : α} (he : t.erase k ≠ ∅) {fallback : α} : (cmp ((t.erase k).maxD fallback) (t.maxD fallback)).isLE = true

theorem Std.ExtTreeSet.maxD_eq_getLastD_toList {α : Type u} {cmp : α → α → Ordering} {t : ExtTreeSet α cmp} [TransCmp cmp] {fallback : α} : t.maxD fallback = t.toList.getLastD fallback

theorem Std.ExtTreeSet.ext_get? {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {t₁ t₂ : ExtTreeSet α cmp} (h : ∀ (k : α), t₁.get? k = t₂.get? k) : t₁ = t₂

theorem Std.ExtTreeSet.ext_get?_iff {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {t₁ t₂ : ExtTreeSet α cmp} : t₁ = t₂ ↔ ∀ (k : α), t₁.get? k = t₂.get? k

theorem Std.ExtTreeSet.ext_contains {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : ExtTreeSet α cmp} (h : ∀ (k : α), t₁.contains k = t₂.contains k) : t₁ = t₂

theorem Std.ExtTreeSet.ext_mem {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : ExtTreeSet α cmp} (h : ∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) : t₁ = t₂

theorem Std.ExtTreeSet.ext_mem_iff {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] {t₁ t₂ : ExtTreeSet α cmp} : t₁ = t₂ ↔ ∀ (k : α), k ∈ t₁ ↔ k ∈ t₂

theorem Std.ExtTreeSet.ext_toList {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : ExtTreeSet α cmp} [TransCmp cmp] (h : t₁.toList.Perm t₂.toList) : t₁ = t₂

theorem Std.ExtTreeSet.toList_inj {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : ExtTreeSet α cmp} [TransCmp cmp] : t₁.toList = t₂.toList ↔ t₁ = t₂