Tree set lemmas

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Std.TreeSet.Raw.mem_of_get_eq {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {k v : α} {w : k ∈ t} : t.get k w = v → k ∈ t

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

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

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

theorem Std.TreeSet.Raw.mem_of_mem_insert' {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {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.Raw.size_emptyc {α : Type u} {cmp : α → α → Ordering} : ∅.size = 0

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

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

theorem Std.TreeSet.Raw.get?_eq_some_iff {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k k' : α} : t.get? k = some k' ↔ ∃ (h : k ∈ t), t.get k h = k'

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

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

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

@[simp]

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

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

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

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

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

theorem Std.TreeSet.Raw.get_insert {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {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 ⋯

theorem Std.TreeSet.Raw.toList_insert_perm {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} : (t.insert k).toList.Perm (if k ∈ t then t.toList else k :: t.toList)

theorem Std.TreeSet.Raw.toArray_insert_perm {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} : (t.insert k).toArray.Perm (if k ∈ t then t.toArray else t.toArray.push k)

@[simp]

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

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

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

@[simp]

theorem Std.TreeSet.Raw.get_get? {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {a : α} {h' : (t.get? a).isSome = true} : (t.get? a).get h' = t.get a ⋯

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Std.TreeSet.Raw.size_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) : t.toArray.size = t.size

@[simp]

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

@[simp]

theorem Std.TreeSet.Raw.isEmpty_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} : t.toArray.isEmpty = t.isEmpty

@[simp]

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

@[simp]

theorem Std.TreeSet.Raw.contains_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : t.toArray.contains k = t.contains k

@[simp]

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

@[simp]

theorem Std.TreeSet.Raw.mem_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : k ∈ t.toArray ↔ k ∈ t

theorem Std.TreeSet.Raw.mem_of_mem_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} : k ∈ t.toList → k ∈ t

theorem Std.TreeSet.Raw.mem_of_mem_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} : k ∈ t.toArray → k ∈ t

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

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

@[simp]

theorem Std.TreeSet.Raw.union_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} : t₁.union t₂ = t₁ ∪ t₂

@[simp]

theorem Std.TreeSet.Raw.contains_union {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : (t₁ ∪ t₂).contains k = (t₁.contains k || t₂.contains k)

theorem Std.TreeSet.Raw.mem_union_of_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : k ∈ t₁ → k ∈ t₁ ∪ t₂

theorem Std.TreeSet.Raw.mem_union_of_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : k ∈ t₂ → k ∈ t₁ ∪ t₂

@[simp]

theorem Std.TreeSet.Raw.mem_union_iff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : k ∈ t₁ ∪ t₂ ↔ k ∈ t₁ ∨ k ∈ t₂

theorem Std.TreeSet.Raw.mem_of_mem_union_of_not_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : k ∈ t₁ ∪ t₂ → ¬k ∈ t₂ → k ∈ t₁

theorem Std.TreeSet.Raw.mem_of_mem_union_of_not_mem_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : k ∈ t₁ ∪ t₂ → ¬k ∈ t₁ → k ∈ t₂

theorem Std.TreeSet.Raw.Equiv.union_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₁.Equiv t₂) : (t₁ ∪ t₃).Equiv (t₂ ∪ t₃)

theorem Std.TreeSet.Raw.Equiv.union_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₂.Equiv t₃) : (t₁ ∪ t₂).Equiv (t₁ ∪ t₃)

theorem Std.TreeSet.Raw.Equiv.union_congr {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF) (equiv₁ : t₁.Equiv t₃) (equiv₂ : t₂.Equiv t₄) : (t₁ ∪ t₂).Equiv (t₃ ∪ t₄)

theorem Std.TreeSet.Raw.get?_union {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : (t₁ ∪ t₂).get? k = (t₂.get? k).or (t₁.get? k)

theorem Std.TreeSet.Raw.get?_union_of_not_mem_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₁) : (t₁ ∪ t₂).get? k = t₂.get? k

theorem Std.TreeSet.Raw.get?_union_of_not_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₂) : (t₁ ∪ t₂).get? k = t₁.get? k

theorem Std.TreeSet.Raw.get_union_of_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂) : (t₁ ∪ t₂).get k ⋯ = t₂.get k mem

theorem Std.TreeSet.Raw.get_union_of_not_mem_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₁) {h' : k ∈ t₁ ∪ t₂} : (t₁ ∪ t₂).get k h' = t₂.get k ⋯

theorem Std.TreeSet.Raw.get_union_of_not_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₂) {h' : k ∈ t₁ ∪ t₂} : (t₁ ∪ t₂).get k h' = t₁.get k ⋯

theorem Std.TreeSet.Raw.getD_union {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k fallback : α} : (t₁ ∪ t₂).getD k fallback = t₂.getD k (t₁.getD k fallback)

theorem Std.TreeSet.Raw.getD_union_of_not_mem_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k fallback : α} (mem : ¬k ∈ t₁) : (t₁ ∪ t₂).getD k fallback = t₂.getD k fallback

theorem Std.TreeSet.Raw.getD_union_of_not_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k fallback : α} (mem : ¬k ∈ t₂) : (t₁ ∪ t₂).getD k fallback = t₁.getD k fallback

theorem Std.TreeSet.Raw.getKey!_union {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : (t₁ ∪ t₂).get! k = t₂.getD k (t₁.get! k)

theorem Std.TreeSet.Raw.getKey!_union_of_not_mem_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [Inhabited α] [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₁) : (t₁ ∪ t₂).get! k = t₂.get! k

theorem Std.TreeSet.Raw.getKey!_union_of_not_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [Inhabited α] [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₂) : (t₁ ∪ t₂).get! k = t₁.get! k

theorem Std.TreeSet.Raw.size_union_of_not_mem {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : (∀ (a : α), a ∈ t₁ → ¬a ∈ t₂) → (t₁ ∪ t₂).size = t₁.size + t₂.size

theorem Std.TreeSet.Raw.size_left_le_size_union {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁.size ≤ (t₁ ∪ t₂).size

theorem Std.TreeSet.Raw.size_right_le_size_union {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₂.size ≤ (t₁ ∪ t₂).size

theorem Std.TreeSet.Raw.size_union_le_size_add_size {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : (t₁ ∪ t₂).size ≤ t₁.size + t₂.size

@[simp]

theorem Std.TreeSet.Raw.isEmpty_union {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : (t₁ ∪ t₂).isEmpty = (t₁.isEmpty && t₂.isEmpty)

@[simp]

theorem Std.TreeSet.Raw.inter_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} : t₁.inter t₂ = t₁ ∩ t₂

@[simp]

theorem Std.TreeSet.Raw.contains_inter {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : (t₁ ∩ t₂).contains k = (t₁.contains k && t₂.contains k)

@[simp]

theorem Std.TreeSet.Raw.mem_inter_iff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : k ∈ t₁ ∩ t₂ ↔ k ∈ t₁ ∧ k ∈ t₂

theorem Std.TreeSet.Raw.not_mem_inter_of_not_mem_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₁) : ¬k ∈ t₁ ∩ t₂

theorem Std.TreeSet.Raw.not_mem_inter_of_not_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₂) : ¬k ∈ t₁ ∩ t₂

theorem Std.TreeSet.Raw.Equiv.inter_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {t₃ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₁.Equiv t₂) : (t₁ ∩ t₃).Equiv (t₂ ∩ t₃)

theorem Std.TreeSet.Raw.Equiv.inter_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {t₃ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₂.Equiv t₃) : (t₁ ∩ t₂).Equiv (t₁ ∩ t₃)

theorem Std.TreeSet.Raw.Equiv.inter_congr {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {t₃ t₄ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF) (equiv₁ : t₁.Equiv t₃) (equiv₂ : t₂.Equiv t₄) : (t₁ ∩ t₂).Equiv (t₃ ∩ t₄)

theorem Std.TreeSet.Raw.get?_inter {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : (t₁ ∩ t₂).get? k = if k ∈ t₂ then t₁.get? k else none

theorem Std.TreeSet.Raw.get?_inter_of_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂) : (t₁ ∩ t₂).get? k = t₁.get? k

theorem Std.TreeSet.Raw.get?_inter_of_not_mem_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₁) : (t₁ ∩ t₂).get? k = none

theorem Std.TreeSet.Raw.get?_inter_of_not_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₂) : (t₁ ∩ t₂).get? k = none

@[simp]

theorem Std.TreeSet.Raw.get_inter {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ ∩ t₂} : (t₁ ∩ t₂).get k h_mem = t₁.get k ⋯

theorem Std.TreeSet.Raw.getD_inter {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k fallback : α} : (t₁ ∩ t₂).getD k fallback = if k ∈ t₂ then t₁.getD k fallback else fallback

theorem Std.TreeSet.Raw.getD_inter_of_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k fallback : α} (mem : k ∈ t₂) : (t₁ ∩ t₂).getD k fallback = t₁.getD k fallback

theorem Std.TreeSet.Raw.getD_inter_of_not_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k fallback : α} (not_mem : ¬k ∈ t₂) : (t₁ ∩ t₂).getD k fallback = fallback

theorem Std.TreeSet.Raw.getD_inter_of_not_mem_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k fallback : α} (not_mem : ¬k ∈ t₁) : (t₁ ∩ t₂).getD k fallback = fallback

theorem Std.TreeSet.Raw.get!_inter {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : (t₁ ∩ t₂).get! k = if k ∈ t₂ then t₁.get! k else default

theorem Std.TreeSet.Raw.get!_inter_of_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [Inhabited α] [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂) : (t₁ ∩ t₂).get! k = t₁.get! k

theorem Std.TreeSet.Raw.get!_inter_of_not_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [Inhabited α] [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₂) : (t₁ ∩ t₂).get! k = default

theorem Std.TreeSet.Raw.get!_inter_of_not_mem_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [Inhabited α] [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₁) : (t₁ ∩ t₂).get! k = default

theorem Std.TreeSet.Raw.size_inter_le_size_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : (t₁ ∩ t₂).size ≤ t₁.size

theorem Std.TreeSet.Raw.size_inter_le_size_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : (t₁ ∩ t₂).size ≤ t₂.size

theorem Std.TreeSet.Raw.size_inter_eq_size_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : ∀ (a : α), a ∈ t₁ → a ∈ t₂) : (t₁ ∩ t₂).size = t₁.size

theorem Std.TreeSet.Raw.size_inter_eq_size_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : ∀ (a : α), a ∈ t₂ → a ∈ t₁) : (t₁ ∩ t₂).size = t₂.size

theorem Std.TreeSet.Raw.size_add_size_eq_size_union_add_size_inter {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁.size + t₂.size = (t₁ ∪ t₂).size + (t₁ ∩ t₂).size

@[simp]

theorem Std.TreeSet.Raw.isEmpty_inter_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.isEmpty = true) : (t₁ ∩ t₂).isEmpty = true

@[simp]

theorem Std.TreeSet.Raw.isEmpty_inter_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₂.isEmpty = true) : (t₁ ∩ t₂).isEmpty = true

theorem Std.TreeSet.Raw.isEmpty_inter_iff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : (t₁ ∩ t₂).isEmpty = true ↔ ∀ (k : α), k ∈ t₁ → ¬k ∈ t₂

theorem Std.TreeSet.Raw.isEmpty_inter_comm {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : (t₁ ∩ t₂).isEmpty = (t₂ ∩ t₁).isEmpty

theorem Std.TreeSet.Raw.Equiv.beq {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Raw α cmp} [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.Equiv m₂) : m₁.beq m₂ = true

theorem Std.TreeSet.Raw.equiv_of_beq {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : (m₁ == m₂) = true) : m₁.Equiv m₂

theorem Std.TreeSet.Raw.beq_iff_equiv {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁ == m₂) = true ↔ m₁.Equiv m₂

theorem Std.TreeSet.Raw.Equiv.beq_congr {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Raw α cmp} [TransCmp cmp] {m₃ m₄ : Raw α cmp} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁.Equiv m₃) (w₂ : m₂.Equiv m₄) : (m₁ == m₂) = (m₃ == m₄)

@[simp]

theorem Std.TreeSet.Raw.diff_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} : t₁.diff t₂ = t₁ \ t₂

@[simp]

theorem Std.TreeSet.Raw.contains_diff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k)

@[simp]

theorem Std.TreeSet.Raw.mem_diff_iff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ ¬k ∈ t₂

theorem Std.TreeSet.Raw.not_mem_diff_of_not_mem_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₁) : ¬k ∈ t₁ \ t₂

theorem Std.TreeSet.Raw.not_mem_diff_of_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂) : ¬k ∈ t₁ \ t₂

theorem Std.TreeSet.Raw.Equiv.diff_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {t₃ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₁.Equiv t₂) : (t₁ \ t₃).Equiv (t₂ \ t₃)

theorem Std.TreeSet.Raw.Equiv.diff_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {t₃ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₂.Equiv t₃) : (t₁ \ t₂).Equiv (t₁ \ t₃)

theorem Std.TreeSet.Raw.Equiv.diff_congr {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {t₃ t₄ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF) (equiv₁ : t₁.Equiv t₃) (equiv₂ : t₂.Equiv t₄) : (t₁ \ t₂).Equiv (t₃ \ t₄)

theorem Std.TreeSet.Raw.get?_diff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : (t₁ \ t₂).get? k = if k ∈ t₂ then none else t₁.get? k

theorem Std.TreeSet.Raw.get?_diff_of_not_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₂) : (t₁ \ t₂).get? k = t₁.get? k

theorem Std.TreeSet.Raw.get?_diff_of_not_mem_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₁) : (t₁ \ t₂).get? k = none

theorem Std.TreeSet.Raw.get?_diff_of_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂) : (t₁ \ t₂).get? k = none

theorem Std.TreeSet.Raw.get_diff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ \ t₂} : (t₁ \ t₂).get k h_mem = t₁.get k ⋯

theorem Std.TreeSet.Raw.getD_diff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k fallback : α} : (t₁ \ t₂).getD k fallback = if k ∈ t₂ then fallback else t₁.getD k fallback

theorem Std.TreeSet.Raw.getD_diff_of_not_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k fallback : α} (not_mem : ¬k ∈ t₂) : (t₁ \ t₂).getD k fallback = t₁.getD k fallback

theorem Std.TreeSet.Raw.getD_diff_of_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k fallback : α} (mem : k ∈ t₂) : (t₁ \ t₂).getD k fallback = fallback

theorem Std.TreeSet.Raw.getD_diff_of_not_mem_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k fallback : α} (not_mem : ¬k ∈ t₁) : (t₁ \ t₂).getD k fallback = fallback

theorem Std.TreeSet.Raw.get!_diff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : (t₁ \ t₂).get! k = if k ∈ t₂ then default else t₁.get! k

theorem Std.TreeSet.Raw.get!_diff_of_not_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [Inhabited α] [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₂) : (t₁ \ t₂).get! k = t₁.get! k

theorem Std.TreeSet.Raw.get!_diff_of_mem_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [Inhabited α] [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂) : (t₁ \ t₂).get! k = default

theorem Std.TreeSet.Raw.get!_diff_of_not_mem_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [Inhabited α] [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : ¬k ∈ t₁) : (t₁ \ t₂).get! k = default

theorem Std.TreeSet.Raw.size_diff_le_size_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : (t₁ \ t₂).size ≤ t₁.size

theorem Std.TreeSet.Raw.size_diff_eq_size_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : ∀ (a : α), a ∈ t₁ → ¬a ∈ t₂) : (t₁ \ t₂).size = t₁.size

theorem Std.TreeSet.Raw.size_diff_add_size_inter_eq_size_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size

@[simp]

theorem Std.TreeSet.Raw.isEmpty_diff_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.isEmpty = true) : (t₁ \ t₂).isEmpty = true

theorem Std.TreeSet.Raw.isEmpty_diff_iff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : (t₁ \ t₂).isEmpty = true ↔ ∀ (k : α), k ∈ t₁ → k ∈ t₂

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

theorem Std.TreeSet.Raw.foldlM_eq_foldlM_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : foldlM f init t = Array.foldlM f init t.toArray

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

theorem Std.TreeSet.Raw.foldl_eq_foldl_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {δ : Type w} {f : δ → α → δ} {init : δ} : foldl f init t = Array.foldl f init t.toArray

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

theorem Std.TreeSet.Raw.foldrM_eq_foldrM_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {δ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : foldrM f init t = Array.foldrM f init t.toArray

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

theorem Std.TreeSet.Raw.foldr_eq_foldr_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {δ : Type w} {f : α → δ → δ} {init : δ} : foldr f init t = Array.foldr f init t.toArray

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

theorem Std.TreeSet.Raw.get_insertMany_list_of_not_mem_of_mem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {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.Raw.get!_insertMany_list_of_not_mem_of_contains_eq_false {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] (h : t.WF) {l : List α} {k : α} (not_mem : ¬k ∈ t) (contains_eq_false : l.contains k = false) : (t.insertMany l).get! k = default

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Std.TreeSet.Raw.ofList_eq_insertMany_empty {α : Type u} {cmp : α → α → Ordering} {l : List α} : ofList l cmp = ∅.insertMany l

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem Std.TreeSet.Raw.min?_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Min α] [LE α] [LawfulOrderCmp cmp] [LawfulOrderMin α] [LawfulOrderLeftLeaningMin α] [LawfulEqCmp cmp] (h : t.WF) : t.toList.min? = t.min?

@[simp]

theorem Std.TreeSet.Raw.head?_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Min α] [LE α] [LawfulOrderCmp cmp] [LawfulOrderMin α] [LawfulOrderLeftLeaningMin α] [LawfulEqCmp cmp] (h : t.WF) : t.toList.head? = t.min?

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

theorem Std.TreeSet.Raw.min?_insert_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (he : t.isEmpty = true) : (t.insert k).min? = some k

theorem Std.TreeSet.Raw.min!_insert_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) {k : α} (he : t.isEmpty = true) : (t.insert k).min! = k

theorem Std.TreeSet.Raw.minD_insert_of_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {k : α} (he : t.isEmpty = true) {fallback : α} : (t.insert k).minD fallback = k

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

theorem Std.TreeSet.Raw.min?_eq_head?_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) : t.min? = t.toList.head?

theorem Std.TreeSet.Raw.min?_eq_getElem?_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) : t.min? = t.toArray[0]?

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

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

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

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

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

theorem Std.TreeSet.Raw.min!_insert_le_min! {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k : α} : (cmp (t.insert k).min! t.min!).isLE = true

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Std.TreeSet.Raw.min!_eq_getElem!_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) : t.min! = t.toArray[0]!

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Std.TreeSet.Raw.minD_eq_getD_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {fallback : α} : t.minD fallback = t.toArray.getD 0 fallback

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

theorem Std.TreeSet.Raw.max?_eq_getLast?_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) : t.max? = t.toList.getLast?

theorem Std.TreeSet.Raw.max?_eq_back?_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) : t.max? = t.toArray.back?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Std.TreeSet.Raw.max!_eq_back!_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] (h : t.WF) : t.max! = t.toArray.back!

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Std.TreeSet.Raw.maxD_eq_getD_back?_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] (h : t.WF) {fallback : α} : t.maxD fallback = t.toArray.back?.getD fallback

@[simp]

theorem Std.TreeSet.Raw.Equiv.rfl {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} : t.Equiv t

theorem Std.TreeSet.Raw.Equiv.symm {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} : t₁.Equiv t₂ → t₂.Equiv t₁

theorem Std.TreeSet.Raw.Equiv.trans {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Raw α cmp} : t₁.Equiv t₂ → t₂.Equiv t₃ → t₁.Equiv t₃

@[instance_reducible]

instance Std.TreeSet.Raw.Equiv.instTrans {α : Type u} {cmp : α → α → Ordering} : Trans Equiv Equiv Equiv

Equations

• Std.TreeSet.Raw.Equiv.instTrans = { trans := ⋯ }

theorem Std.TreeSet.Raw.Equiv.comm {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} : t₁.Equiv t₂ ↔ t₂.Equiv t₁

theorem Std.TreeSet.Raw.Equiv.congr_left {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Raw α cmp} (h : t₁.Equiv t₂) : t₁.Equiv t₃ ↔ t₂.Equiv t₃

theorem Std.TreeSet.Raw.Equiv.congr_right {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Raw α cmp} (h : t₁.Equiv t₂) : t₃.Equiv t₁ ↔ t₃.Equiv t₂

theorem Std.TreeSet.Raw.Equiv.isEmpty_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} (h : t₁.Equiv t₂) : t₁.isEmpty = t₂.isEmpty

theorem Std.TreeSet.Raw.Equiv.contains_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.contains k = t₂.contains k

theorem Std.TreeSet.Raw.Equiv.mem_iff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : k ∈ t₁ ↔ k ∈ t₂

theorem Std.TreeSet.Raw.Equiv.size_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.size = t₂.size

theorem Std.TreeSet.Raw.Equiv.get?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.get? k = t₂.get? k

theorem Std.TreeSet.Raw.Equiv.getKey_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} {hk : k ∈ t₁} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.get k hk = t₂.get k ⋯

theorem Std.TreeSet.Raw.Equiv.getKey!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.get! k = t₂.get! k

theorem Std.TreeSet.Raw.Equiv.getKeyD_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.getD k fallback = t₂.getD k fallback

theorem Std.TreeSet.Raw.Equiv.toList_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.toList = t₂.toList

theorem Std.TreeSet.Raw.Equiv.toArray_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.toArray = t₂.toArray

theorem Std.TreeSet.Raw.Equiv.foldlM_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : foldlM f init t₁ = foldlM f init t₂

theorem Std.TreeSet.Raw.Equiv.foldl_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} {δ : Type w} [TransCmp cmp] {f : δ → α → δ} {init : δ} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : foldl f init t₁ = foldl f init t₂

theorem Std.TreeSet.Raw.Equiv.foldrM_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : foldrM f init t₁ = foldrM f init t₂

theorem Std.TreeSet.Raw.Equiv.foldr_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} {δ : Type w} [TransCmp cmp] {f : α → δ → δ} {init : δ} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : foldr f init t₁ = foldr f init t₂

theorem Std.TreeSet.Raw.Equiv.forIn_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} {δ : Type w} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {b : δ} {f : α → δ → m (ForInStep δ)} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : ForIn.forIn t₁ b f = ForIn.forIn t₂ b f

theorem Std.TreeSet.Raw.Equiv.forM_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} {m : Type w → Type w'} [TransCmp cmp] [Monad m] [LawfulMonad m] {f : α → m PUnit} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : ForM.forM t₁ f = ForM.forM t₂ f

theorem Std.TreeSet.Raw.Equiv.any_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {p : α → Bool} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.any p = t₂.any p

theorem Std.TreeSet.Raw.Equiv.all_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {p : α → Bool} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.all p = t₂.all p

theorem Std.TreeSet.Raw.Equiv.min?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.min? = t₂.min?

theorem Std.TreeSet.Raw.Equiv.min!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.min! = t₂.min!

theorem Std.TreeSet.Raw.Equiv.minD_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.minD fallback = t₂.minD fallback

theorem Std.TreeSet.Raw.Equiv.max?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.max? = t₂.max?

theorem Std.TreeSet.Raw.Equiv.max!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.max! = t₂.max!

theorem Std.TreeSet.Raw.Equiv.maxD_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.maxD fallback = t₂.maxD fallback

theorem Std.TreeSet.Raw.Equiv.atIdx?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {i : Nat} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.atIdx? i = t₂.atIdx? i

theorem Std.TreeSet.Raw.Equiv.atIdx!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] {i : Nat} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.atIdx! i = t₂.atIdx! i

theorem Std.TreeSet.Raw.Equiv.atIdxD_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {i : Nat} {fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.atIdxD i fallback = t₂.atIdxD i fallback

theorem Std.TreeSet.Raw.Equiv.getGE?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.getGE? k = t₂.getGE? k

theorem Std.TreeSet.Raw.Equiv.getGE!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.getGE! k = t₂.getGE! k

theorem Std.TreeSet.Raw.Equiv.getGED_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.getGED k fallback = t₂.getGED k fallback

theorem Std.TreeSet.Raw.Equiv.getGT?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.getGT? k = t₂.getGT? k

theorem Std.TreeSet.Raw.Equiv.getGT!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.getGT! k = t₂.getGT! k

theorem Std.TreeSet.Raw.Equiv.getGTD_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.getGTD k fallback = t₂.getGTD k fallback

theorem Std.TreeSet.Raw.Equiv.getLE?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.getLE? k = t₂.getLE? k

theorem Std.TreeSet.Raw.Equiv.getLE!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.getLE! k = t₂.getLE! k

theorem Std.TreeSet.Raw.Equiv.getLED_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.getLED k fallback = t₂.getLED k fallback

theorem Std.TreeSet.Raw.Equiv.getLT?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.getLT? k = t₂.getLT? k

theorem Std.TreeSet.Raw.Equiv.getLT!_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [Inhabited α] {k : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.getLT! k = t₂.getLT! k

theorem Std.TreeSet.Raw.Equiv.getLTD_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] {k fallback : α} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) : t₁.getLTD k fallback = t₂.getLTD k fallback

theorem Std.TreeSet.Raw.Equiv.insert {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) (k : α) : (t₁.insert k).Equiv (t₂.insert k)

theorem Std.TreeSet.Raw.Equiv.erase {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) (k : α) : (t₁.erase k).Equiv (t₂.erase k)

theorem Std.TreeSet.Raw.Equiv.filter {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) (f : α → Bool) : (Raw.filter f t₁).Equiv (Raw.filter f t₂)

theorem Std.TreeSet.Raw.Equiv.insertMany_list {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) (l : List α) : (t₁.insertMany l).Equiv (t₂.insertMany l)

theorem Std.TreeSet.Raw.Equiv.eraseMany_list {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) (l : List α) : (t₁.eraseMany l).Equiv (t₂.eraseMany l)

theorem Std.TreeSet.Raw.Equiv.merge {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF) (h : t₁.Equiv t₂) (h' : t₃.Equiv t₄) : (t₁.merge t₃).Equiv (t₂.merge t₄)

theorem Std.TreeSet.Raw.Equiv.of_forall_get?_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : ∀ (k : α), t₁.get? k = t₂.get? k) : t₁.Equiv t₂

theorem Std.TreeSet.Raw.Equiv.of_forall_contains_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : ∀ (k : α), t₁.contains k = t₂.contains k) : t₁.Equiv t₂

theorem Std.TreeSet.Raw.Equiv.of_forall_mem_iff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : ∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) : t₁.Equiv t₂

theorem Std.TreeSet.Raw.equiv_empty_iff_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} : t.Equiv empty ↔ t.isEmpty = true

theorem Std.TreeSet.Raw.inter_equiv_empty_comm {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : (t₁ ∩ t₂).Equiv ∅ ↔ (t₂ ∩ t₁).Equiv ∅

theorem Std.TreeSet.Raw.empty_equiv_iff_isEmpty {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} : empty.Equiv t ↔ t.isEmpty = true

theorem Std.TreeSet.Raw.equiv_iff_toList_perm {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} : t₁.Equiv t₂ ↔ t₁.toList.Perm t₂.toList

theorem Std.TreeSet.Raw.equiv_iff_toArray_perm {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} : t₁.Equiv t₂ ↔ t₁.toArray.Perm t₂.toArray

theorem Std.TreeSet.Raw.Equiv.of_toList_perm {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} (h : t₁.toList.Perm t₂.toList) : t₁.Equiv t₂

theorem Std.TreeSet.Raw.Equiv.of_toArray_perm {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} (h : t₁.toArray.Perm t₂.toArray) : t₁.Equiv t₂

theorem Std.TreeSet.Raw.equiv_iff_toList_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁.Equiv t₂ ↔ t₁.toList = t₂.toList

theorem Std.TreeSet.Raw.equiv_iff_toArray_eq {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁.Equiv t₂ ↔ t₁.toArray = t₂.toArray

theorem Std.TreeSet.Raw.equiv_iff_forall_mem_iff {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Raw α cmp} [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁.Equiv t₂ ↔ ∀ (k : α), k ∈ t₁ ↔ k ∈ t₂

theorem Std.TreeSet.Raw.insertMany_list_equiv_foldl {α : Type u} {cmp : α → α → Ordering} {t₁ : Raw α cmp} {l : List α} : (t₁.insertMany l).Equiv (List.foldl (fun (acc : Raw α cmp) (a : α) => acc.insert a) t₁ l)

theorem Std.TreeSet.Raw.ofList_equiv_foldl {α : Type u} {cmp : α → α → Ordering} {l : List α} : (ofList l cmp).Equiv (List.foldl (fun (acc : Raw α cmp) (a : α) => acc.insert a) ∅ l)

theorem Std.TreeSet.Raw.toList_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {f : α → Bool} (h : t.WF) : (filter f t).toList = List.filter f t.toList

theorem Std.TreeSet.Raw.toArray_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {f : α → Bool} (h : t.WF) : (filter f t).toArray = Array.filter f t.toArray

theorem Std.TreeSet.Raw.isEmpty_filter_iff {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} (h : t.WF) : (filter f t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = false

theorem Std.TreeSet.Raw.isEmpty_filter_eq_false_iff {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} (h : t.WF) : (filter f t).isEmpty = false ↔ ∃ (k : α), ∃ (h : k ∈ t), f (t.get k h) = true

@[simp]

theorem Std.TreeSet.Raw.mem_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} {k : α} (h : t.WF) : k ∈ filter f t ↔ ∃ (h' : k ∈ t), f (t.get k h') = true

theorem Std.TreeSet.Raw.mem_of_mem_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} {k : α} (h : t.WF) : k ∈ filter f t → k ∈ t

theorem Std.TreeSet.Raw.size_filter_le_size {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} (h : t.WF) : (filter f t).size ≤ t.size

theorem Std.TreeSet.Raw.size_filter_eq_size_iff {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} (h : t.WF) : (filter f t).size = t.size ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = true

theorem Std.TreeSet.Raw.filter_equiv_self_iff {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} (h : t.WF) : (filter f t).Equiv t ↔ ∀ (a : α) (h : a ∈ t), f (t.get a h) = true

@[simp]

theorem Std.TreeSet.Raw.get?_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} {k : α} (h : t.WF) : (filter f t).get? k = Option.filter f (t.get? k)

@[simp]

theorem Std.TreeSet.Raw.get_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} {k : α} {h' : k ∈ filter f t} (h : t.WF) : (filter f t).get k h' = t.get k ⋯

theorem Std.TreeSet.Raw.get!_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] [Inhabited α] {f : α → Bool} {k : α} (h : t.WF) : (filter f t).get! k = (Option.filter f (t.get? k)).get!

theorem Std.TreeSet.Raw.getD_filter {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} [TransCmp cmp] {f : α → Bool} {k fallback : α} (h : t.WF) : (filter f t).getD k fallback = (Option.filter f (t.get? k)).getD fallback

theorem Std.TreeSet.Raw.toArray_toList {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} : t.toList.toArray = t.toArray

theorem Std.TreeSet.Raw.toList_toArray {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} : t.toArray.toList = t.toList