Tree set lemmas

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

@[simp]

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

@[simp]

theorem Std.TreeSet.isEmpty_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {k : α} : (t.insert k).isEmpty = false

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

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

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

@[simp]

theorem Std.TreeSet.contains_emptyc {α : Type u} {cmp : α → α → Ordering} {k : α} : ∅.contains k = false

@[simp]

theorem Std.TreeSet.not_mem_emptyc {α : Type u} {cmp : α → α → Ordering} {k : α} : ¬k ∈ ∅

theorem Std.TreeSet.contains_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {a : α} : t.isEmpty = true → t.contains a = false

theorem Std.TreeSet.not_mem_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {a : α} : t.isEmpty = true → ¬a ∈ t

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

theorem Std.TreeSet.isEmpty_eq_false_iff_exists_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] : t.isEmpty = false ↔ ∃ (a : α), a ∈ t

theorem Std.TreeSet.isEmpty_eq_false_of_contains {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {a : α} (hc : t.contains a = true) : t.isEmpty = false

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

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

@[simp]

theorem Std.TreeSet.insert_eq_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} {p : α} : Insert.insert p t = t.insert p

@[simp]

theorem Std.TreeSet.singleton_eq_insert {α : Type u} {cmp : α → α → Ordering} {p : α} : {p} = ∅.insert p

@[simp]

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

@[simp]

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

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

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

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

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

theorem Std.TreeSet.mem_of_mem_insert' {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.size_emptyc {α : Type u} {cmp : α → α → Ordering} : ∅.size = 0

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

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

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

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

@[simp]

theorem Std.TreeSet.erase_emptyc {α : Type u} {cmp : α → α → Ordering} {k : α} : ∅.erase k = ∅

@[simp]

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

theorem Std.TreeSet.isEmpty_eq_isEmpty_erase_and_not_contains {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] (k : α) : t.isEmpty = ((t.erase k).isEmpty && !t.contains k)

theorem Std.TreeSet.isEmpty_eq_false_of_isEmpty_erase_eq_false {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {k : α} (he : (t.erase k).isEmpty = false) : t.isEmpty = false

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

theorem Std.TreeSet.get?_emptyc {α : Type u} {cmp : α → α → Ordering} {a : α} : ∅.get? a = none

theorem Std.TreeSet.get?_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {a : α} : t.isEmpty = true → t.get? a = none

theorem Std.TreeSet.get?_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.contains_eq_isSome_get? {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {a : α} : t.contains a = (t.get? a).isSome

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

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

theorem Std.TreeSet.get?_erase {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.get?_erase_self {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {k : α} : (t.erase k).get? k = none

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

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

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

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

theorem Std.TreeSet.get_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.get_erase {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {k a : α} {h' : a ∈ t.erase k} : (t.erase k).get a h' = t.get a ⋯

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

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

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

@[simp]

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

@[simp]

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

theorem Std.TreeSet.get!_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} : t.isEmpty = true → t.get! a = default

theorem Std.TreeSet.get!_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.get!_eq_default_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] [Inhabited α] {a : α} : t.contains a = false → t.get! a = default

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

theorem Std.TreeSet.get!_erase {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.get!_erase_self {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] [Inhabited α] {k : α} : (t.erase k).get! k = default

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

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

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

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

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

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

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

@[simp]

theorem Std.TreeSet.getD_emptyc {α : Type u} {cmp : α → α → Ordering} {a fallback : α} : ∅.getD a fallback = fallback

theorem Std.TreeSet.getD_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {a fallback : α} : t.isEmpty = true → t.getD a fallback = fallback

theorem Std.TreeSet.getD_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.getD_eq_fallback_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {a fallback : α} : t.contains a = false → t.getD a fallback = fallback

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Std.TreeSet.isEmpty_toList {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} : t.toList.isEmpty = t.isEmpty

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

theorem Std.TreeSet.forIn_eq_forIn_toList {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

theorem Std.TreeSet.get?_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.get?_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.get?_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {l : List α} {k : α} (mem : k ∈ t) : (t.insertMany l).get? k = t.get? k

theorem Std.TreeSet.get_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.get_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.get!_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.get!_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.get!_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] [Inhabited α] {l : List α} {k : α} (mem : k ∈ t) : (t.insertMany l).get! k = t.get! k

theorem Std.TreeSet.getD_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.getD_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.getD_insertMany_list_of_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {l : List α} {k fallback : α} (mem : k ∈ t) : (t.insertMany l).getD k fallback = t.getD k fallback

theorem Std.TreeSet.size_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.size_le_size_insertMany_list {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {l : List α} : t.size ≤ (t.insertMany l).size

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem Std.TreeSet.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.TreeSet.mem_ofList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : k ∈ ofList l cmp ↔ l.contains k = true

theorem Std.TreeSet.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.TreeSet.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.TreeSet.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.TreeSet.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.TreeSet.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.TreeSet.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.TreeSet.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.TreeSet.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.TreeSet.size_ofList_le {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} : (ofList l cmp).size ≤ l.length

@[simp]

theorem Std.TreeSet.isEmpty_ofList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {l : List α} : (ofList l cmp).isEmpty = l.isEmpty

@[simp]

theorem Std.TreeSet.min?_emptyc {α : Type u} {cmp : α → α → Ordering} : ∅.min? = none

theorem Std.TreeSet.min?_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] (he : t.isEmpty = true) : t.min? = none

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem Std.TreeSet.isSome_min?_iff_isEmpty_eq_false {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] : t.min?.isSome = true ↔ t.isEmpty = false

theorem Std.TreeSet.min?_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.isSome_min?_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {k : α} : (t.insert k).min?.isSome = true

theorem Std.TreeSet.min?_insert_le_min? {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.min?_insert_le_self {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {k kmi : α} (hkmi : (t.insert k).min?.get ⋯ = kmi) : (cmp kmi k).isLE = true

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

theorem Std.TreeSet.min?_le_min?_erase {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.min?_eq_head?_toList {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] : t.min? = t.toList.head?

theorem Std.TreeSet.min_eq_get_min? {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {he : t.isEmpty = false} : t.min he = t.min?.get ⋯

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

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

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

theorem Std.TreeSet.min_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.min_insert_le_min {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {k : α} {he : t.isEmpty = false} : (cmp ((t.insert k).min ⋯) (t.min he)).isLE = true

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

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

theorem Std.TreeSet.min_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {he : t.isEmpty = false} : t.min he ∈ t

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem Std.TreeSet.min_eq_head_toList {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {he : t.isEmpty = false} : t.min he = t.toList.head ⋯

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

theorem Std.TreeSet.min_eq_min! {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] [Inhabited α] {he : t.isEmpty = false} : t.min he = t.min!

theorem Std.TreeSet.min!_eq_default {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = true) : t.min! = default

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

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

theorem Std.TreeSet.min!_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.min!_insert_le_min! {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k : α} : (cmp (t.insert k).min! t.min!).isLE = true

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

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

theorem Std.TreeSet.min!_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) : t.min! ∈ t

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

theorem Std.TreeSet.minD_eq_fallback {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] (he : t.isEmpty = true) {fallback : α} : t.minD fallback = fallback

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

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

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

theorem Std.TreeSet.minD_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.minD_insert_le_minD {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] (he : t.isEmpty = false) {k fallback : α} : (cmp ((t.insert k).minD fallback) (t.minD fallback)).isLE = true

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

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

theorem Std.TreeSet.minD_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] (he : t.isEmpty = false) {fallback : α} : t.minD fallback ∈ t

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem Std.TreeSet.max?_emptyc {α : Type u} {cmp : α → α → Ordering} : ∅.max? = none

theorem Std.TreeSet.max?_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] (he : t.isEmpty = true) : t.max? = none

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem Std.TreeSet.isSome_max?_iff_isEmpty_eq_false {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] : t.max?.isSome = true ↔ t.isEmpty = false

theorem Std.TreeSet.max?_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.isSome_max?_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {k : α} : (t.insert k).max?.isSome = true

theorem Std.TreeSet.max?_le_max?_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.self_le_max?_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {k kmi : α} (hkmi : (t.insert k).max?.get ⋯ = kmi) : (cmp k kmi).isLE = true

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

theorem Std.TreeSet.max?_erase_le_max? {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.max?_eq_getLast?_toList {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] : t.max? = t.toList.getLast?

theorem Std.TreeSet.max_eq_get_max? {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {he : t.isEmpty = false} : t.max he = t.max?.get ⋯

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

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

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

theorem Std.TreeSet.max_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.max_le_max_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {k : α} {he : t.isEmpty = false} : (cmp (t.max he) ((t.insert k).max ⋯)).isLE = true

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

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

theorem Std.TreeSet.max_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {he : t.isEmpty = false} : t.max he ∈ t

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem Std.TreeSet.max_eq_getLast_toList {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] {he : t.isEmpty = false} : t.max he = t.toList.getLast ⋯

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

theorem Std.TreeSet.max_eq_max! {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] [Inhabited α] {he : t.isEmpty = false} : t.max he = t.max!

theorem Std.TreeSet.max!_eq_default {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = true) : t.max! = default

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

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

theorem Std.TreeSet.max!_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.max!_le_max!_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k : α} : (cmp t.max! (t.insert k).max!).isLE = true

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

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

theorem Std.TreeSet.max!_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) : t.max! ∈ t

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

theorem Std.TreeSet.maxD_eq_fallback {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] (he : t.isEmpty = true) {fallback : α} : t.maxD fallback = fallback

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

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

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

theorem Std.TreeSet.maxD_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α 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.TreeSet.maxD_le_maxD_insert {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] (he : t.isEmpty = false) {k fallback : α} : (cmp (t.maxD fallback) ((t.insert k).maxD fallback)).isLE = true

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

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

theorem Std.TreeSet.maxD_mem {α : Type u} {cmp : α → α → Ordering} {t : TreeSet α cmp} [TransCmp cmp] (he : t.isEmpty = false) {fallback : α} : t.maxD fallback ∈ t

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

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

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

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

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

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

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

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

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

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