Documentation

Batteries.Data.RBMap.Lemmas

Additional lemmas for Red-black trees #

@[simp, irreducible]
theorem Batteries.RBNode.min?_reverse {α : Type u_1} (t : Batteries.RBNode α) :
t.reverse.min? = t.max?
@[simp]
theorem Batteries.RBNode.max?_reverse {α : Type u_1} (t : Batteries.RBNode α) :
t.reverse.max? = t.min?
@[simp]
theorem Batteries.RBNode.mem_nil {α : Type u_1} {x : α} :
¬x Batteries.RBNode.nil
@[simp]
theorem Batteries.RBNode.mem_node {α : Type u_1} {y : α} {c : Batteries.RBColor} {a : Batteries.RBNode α} {x : α} {b : Batteries.RBNode α} :
y Batteries.RBNode.node c a x b y = x y a y b
theorem Batteries.RBNode.All_def {α : Type u_1} {p : αProp} {t : Batteries.RBNode α} :
Batteries.RBNode.All p t ∀ (x : α), x tp x
theorem Batteries.RBNode.Any_def {α : Type u_1} {p : αProp} {t : Batteries.RBNode α} :
Batteries.RBNode.Any p t ∃ (x : α), x t p x
theorem Batteries.RBNode.memP_def :
∀ {α : Type u_1} {cut : αOrdering} {t : Batteries.RBNode α}, Batteries.RBNode.MemP cut t ∃ (x : α), x t cut x = Ordering.eq
theorem Batteries.RBNode.mem_def :
∀ {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Batteries.RBNode α}, Batteries.RBNode.Mem cmp x t ∃ (y : α), y t cmp x y = Ordering.eq
theorem Batteries.RBNode.mem_congr {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} [Batteries.TransCmp cmp] {t : Batteries.RBNode α} (h : cmp x y = Ordering.eq) :
theorem Batteries.RBNode.isOrdered_iff' {α : Type u_1} {cmp : ααOrdering} {L : Option α} {R : Option α} [Batteries.TransCmp cmp] {t : Batteries.RBNode α} :
Batteries.RBNode.isOrdered cmp t L R = true (∀ (a : α), a LBatteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp a x) t) (∀ (a : α), a RBatteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp x a) t) (∀ (a : α), a L∀ (b : α), b RBatteries.RBNode.cmpLT cmp a b) Batteries.RBNode.Ordered cmp t
class Batteries.RBNode.IsCut {α : Sort u_1} (cmp : ααOrdering) (cut : αOrdering) :

A cut is like a homomorphism of orderings: it is a monotonic predicate with respect to cmp, but it can make things that are distinguished by cmp equal. This is sufficient for find? to locate an element on which cut returns .eq, but there may be other elements, not returned by find?, on which cut also returns .eq.

Instances
    theorem Batteries.RBNode.IsCut.le_lt_trans {α : Sort u_1} {cmp : ααOrdering} {cut : αOrdering} [self : Batteries.RBNode.IsCut cmp cut] {x : α} {y : α} [Batteries.TransCmp cmp] :
    cmp x y Ordering.gtcut x = Ordering.ltcut y = Ordering.lt

    The set {x | cut x = .lt} is downward-closed.

    theorem Batteries.RBNode.IsCut.le_gt_trans {α : Sort u_1} {cmp : ααOrdering} {cut : αOrdering} [self : Batteries.RBNode.IsCut cmp cut] {x : α} {y : α} [Batteries.TransCmp cmp] :
    cmp x y Ordering.gtcut y = Ordering.gtcut x = Ordering.gt

    The set {x | cut x = .gt} is upward-closed.

    theorem Batteries.RBNode.IsCut.lt_trans :
    ∀ {α : Sort u_1} {cmp : ααOrdering} {cut : αOrdering} {x y : α} [inst : Batteries.RBNode.IsCut cmp cut] [inst : Batteries.TransCmp cmp], cmp x y = Ordering.ltcut x = Ordering.ltcut y = Ordering.lt
    theorem Batteries.RBNode.IsCut.gt_trans :
    ∀ {α : Sort u_1} {cmp : ααOrdering} {cut : αOrdering} {x y : α} [inst : Batteries.RBNode.IsCut cmp cut] [inst : Batteries.TransCmp cmp], cmp x y = Ordering.ltcut y = Ordering.gtcut x = Ordering.gt
    theorem Batteries.RBNode.IsCut.congr :
    ∀ {α : Sort u_1} {cmp : ααOrdering} {cut : αOrdering} {x y : α} [inst : Batteries.RBNode.IsCut cmp cut] [inst : Batteries.TransCmp cmp], cmp x y = Ordering.eqcut x = cut y
    instance Batteries.RBNode.instIsCutFlipOrderingSwap {α : Sort u_1} (cmp : ααOrdering) (cut : αOrdering) [Batteries.RBNode.IsCut cmp cut] :
    Batteries.RBNode.IsCut (flip cmp) fun (x : α) => (cut x).swap
    Equations
    • =
    class Batteries.RBNode.IsStrictCut {α : Sort u_1} (cmp : ααOrdering) (cut : αOrdering) extends Batteries.RBNode.IsCut :

    IsStrictCut upgrades the IsCut property to ensure that at most one element of the tree can match the cut, and hence find? will return the unique such element if one exists.

    Instances
      theorem Batteries.RBNode.IsStrictCut.exact {α : Sort u_1} {cmp : ααOrdering} {cut : αOrdering} [self : Batteries.RBNode.IsStrictCut cmp cut] {x : α} {y : α} [Batteries.TransCmp cmp] :
      cut x = Ordering.eqcmp x y = cut y

      If cut = x, then cut and x have compare the same with respect to other elements.

      instance Batteries.RBNode.instIsStrictCut {α : Sort u_1} (cmp : ααOrdering) (a : α) :

      A "representable cut" is one generated by cmp a for some a. This is always a valid cut.

      Equations
      • =
      instance Batteries.RBNode.instIsStrictCutFlipOrderingSwap {α : Sort u_1} (cmp : ααOrdering) (cut : αOrdering) [Batteries.RBNode.IsStrictCut cmp cut] :
      Batteries.RBNode.IsStrictCut (flip cmp) fun (x : α) => (cut x).swap
      Equations
      • =
      theorem Batteries.RBNode.foldr_cons {α : Type u_1} (t : Batteries.RBNode α) (l : List α) :
      Batteries.RBNode.foldr (fun (x1 : α) (x2 : List α) => x1 :: x2) t l = t.toList ++ l
      @[simp]
      theorem Batteries.RBNode.toList_nil {α : Type u_1} :
      Batteries.RBNode.nil.toList = []
      @[simp]
      theorem Batteries.RBNode.toList_node {α : Type u_1} {c : Batteries.RBColor} {a : Batteries.RBNode α} {x : α} {b : Batteries.RBNode α} :
      (Batteries.RBNode.node c a x b).toList = a.toList ++ x :: b.toList
      @[simp]
      theorem Batteries.RBNode.toList_reverse {α : Type u_1} (t : Batteries.RBNode α) :
      t.reverse.toList = t.toList.reverse
      @[simp]
      theorem Batteries.RBNode.mem_toList {α : Type u_1} {x : α} {t : Batteries.RBNode α} :
      x t.toList x t
      @[simp]
      theorem Batteries.RBNode.mem_reverse {α : Type u_1} {a : α} {t : Batteries.RBNode α} :
      a t.reverse a t
      theorem Batteries.RBNode.min?_eq_toList_head? {α : Type u_1} {t : Batteries.RBNode α} :
      t.min? = t.toList.head?
      theorem Batteries.RBNode.max?_eq_toList_getLast? {α : Type u_1} {t : Batteries.RBNode α} :
      t.max? = t.toList.getLast?
      theorem Batteries.RBNode.foldr_eq_foldr_toList {α : Type u_1} :
      ∀ {α_1 : Type u_2} {f : αα_1α_1} {init : α_1} {t : Batteries.RBNode α}, Batteries.RBNode.foldr f t init = List.foldr f init t.toList
      theorem Batteries.RBNode.foldl_eq_foldl_toList {α : Type u_1} :
      ∀ {α_1 : Type u_2} {f : α_1αα_1} {init : α_1} {t : Batteries.RBNode α}, Batteries.RBNode.foldl f init t = List.foldl f init t.toList
      theorem Batteries.RBNode.foldl_reverse {α : Type u_1} {β : Type u_2} {t : Batteries.RBNode α} {f : βαβ} {init : β} :
      theorem Batteries.RBNode.foldr_reverse {α : Type u_1} {β : Type u_2} {t : Batteries.RBNode α} {f : αββ} {init : β} :
      theorem Batteries.RBNode.forM_eq_forM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {f : αm PUnit} [Monad m] [LawfulMonad m] {t : Batteries.RBNode α} :
      Batteries.RBNode.forM f t = t.toList.forM f
      theorem Batteries.RBNode.foldlM_eq_foldlM_toList {m : Type u_1 → Type u_2} {α : Type u_3} :
      ∀ {a : Type u_1} {f : aαm a} {init : a} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Batteries.RBNode α}, Batteries.RBNode.foldlM f init t = List.foldlM f init t.toList
      theorem Batteries.RBNode.forIn_visit_eq_bindList {m : Type u_1 → Type u_2} {α : Type u_3} :
      ∀ {α_1 : Type u_1} {f : αα_1m (ForInStep α_1)} {init : α_1} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Batteries.RBNode α}, Batteries.RBNode.forIn.visit f t init = ForInStep.bindList f t.toList (ForInStep.yield init)
      theorem Batteries.RBNode.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} :
      ∀ {α_1 : Type u_1} {init : α_1} {f : αα_1m (ForInStep α_1)} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Batteries.RBNode α}, forIn t init f = forIn t.toList init f
      theorem Batteries.RBNode.Stream.foldr_cons {α : Type u_1} (t : Batteries.RBNode.Stream α) (l : List α) :
      Batteries.RBNode.Stream.foldr (fun (x1 : α) (x2 : List α) => x1 :: x2) t l = t.toList ++ l
      @[simp]
      theorem Batteries.RBNode.Stream.toList_nil {α : Type u_1} :
      Batteries.RBNode.Stream.nil.toList = []
      @[simp]
      theorem Batteries.RBNode.Stream.toList_cons {α : Type u_1} {x : α} {r : Batteries.RBNode α} {s : Batteries.RBNode.Stream α} :
      (Batteries.RBNode.Stream.cons x r s).toList = x :: r.toList ++ s.toList
      theorem Batteries.RBNode.Stream.foldr_eq_foldr_toList {α : Type u_1} :
      ∀ {α_1 : Type u_2} {f : αα_1α_1} {init : α_1} {s : Batteries.RBNode.Stream α}, Batteries.RBNode.Stream.foldr f s init = List.foldr f init s.toList
      theorem Batteries.RBNode.Stream.foldl_eq_foldl_toList {α : Type u_1} :
      ∀ {α_1 : Type u_2} {f : α_1αα_1} {init : α_1} {t : Batteries.RBNode.Stream α}, Batteries.RBNode.Stream.foldl f init t = List.foldl f init t.toList
      theorem Batteries.RBNode.Stream.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} :
      ∀ {α_1 : Type u_1} {init : α_1} {f : αα_1m (ForInStep α_1)} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Batteries.RBNode α}, forIn t init f = forIn t.toList init f
      theorem Batteries.RBNode.toStream_toList' {α : Type u_1} {t : Batteries.RBNode α} {s : Batteries.RBNode.Stream α} :
      (t.toStream s).toList = t.toList ++ s.toList
      @[simp]
      theorem Batteries.RBNode.toStream_toList {α : Type u_1} {t : Batteries.RBNode α} :
      t.toStream.toList = t.toList
      theorem Batteries.RBNode.Stream.next?_toList {α : Type u_1} {s : Batteries.RBNode.Stream α} :
      Option.map (fun (x : α × Batteries.RBNode.Stream α) => match x with | (a, b) => (a, b.toList)) s.next? = s.toList.next?
      theorem Batteries.RBNode.min?_mem {α : Type u_1} {a : α} {t : Batteries.RBNode α} (h : t.min? = some a) :
      a t
      theorem Batteries.RBNode.Ordered.min?_le {α : Type u_1} {cmp : ααOrdering} {a : α} {t : Batteries.RBNode α} [Batteries.TransCmp cmp] (ht : Batteries.RBNode.Ordered cmp t) (h : t.min? = some a) (x : α) (hx : x t) :
      theorem Batteries.RBNode.max?_mem {α : Type u_1} {a : α} {t : Batteries.RBNode α} (h : t.max? = some a) :
      a t
      theorem Batteries.RBNode.Ordered.le_max? {α : Type u_1} {cmp : ααOrdering} {a : α} {t : Batteries.RBNode α} [Batteries.TransCmp cmp] (ht : Batteries.RBNode.Ordered cmp t) (h : t.max? = some a) (x : α) (hx : x t) :
      @[simp]
      theorem Batteries.RBNode.setBlack_toList {α : Type u_1} {t : Batteries.RBNode α} :
      t.setBlack.toList = t.toList
      @[simp]
      theorem Batteries.RBNode.setRed_toList {α : Type u_1} {t : Batteries.RBNode α} :
      t.setRed.toList = t.toList
      @[simp]
      theorem Batteries.RBNode.balance1_toList {α : Type u_1} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} :
      (l.balance1 v r).toList = l.toList ++ v :: r.toList
      @[simp]
      theorem Batteries.RBNode.balance2_toList {α : Type u_1} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} :
      (l.balance2 v r).toList = l.toList ++ v :: r.toList
      @[simp]
      theorem Batteries.RBNode.balLeft_toList {α : Type u_1} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} :
      (l.balLeft v r).toList = l.toList ++ v :: r.toList
      @[simp]
      theorem Batteries.RBNode.balRight_toList {α : Type u_1} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} :
      (l.balRight v r).toList = l.toList ++ v :: r.toList
      theorem Batteries.RBNode.size_eq {α : Type u_1} {t : Batteries.RBNode α} :
      t.size = t.toList.length
      @[simp]
      theorem Batteries.RBNode.reverse_size {α : Type u_1} (t : Batteries.RBNode α) :
      t.reverse.size = t.size
      @[simp]
      theorem Batteries.RBNode.Any_reverse {α : Type u_1} {p : αProp} {t : Batteries.RBNode α} :
      @[simp]
      theorem Batteries.RBNode.memP_reverse {α : Type u_1} {cut : αOrdering} {t : Batteries.RBNode α} :
      Batteries.RBNode.MemP cut t.reverse Batteries.RBNode.MemP (fun (x : α) => (cut x).swap) t
      theorem Batteries.RBNode.Mem_reverse {α : Type u_1} {cmp : ααOrdering} {x : α} [Batteries.OrientedCmp cmp] {t : Batteries.RBNode α} :
      theorem Batteries.RBNode.find?_some_eq_eq {α : Type u_1} {cut : αOrdering} {x : α} {t : Batteries.RBNode α} :
      theorem Batteries.RBNode.find?_some_mem {α : Type u_1} {cut : αOrdering} {x : α} {t : Batteries.RBNode α} :
      theorem Batteries.RBNode.find?_some_memP {α : Type u_1} {cut : αOrdering} {x : α} {t : Batteries.RBNode α} (h : x Batteries.RBNode.find? cut t) :
      theorem Batteries.RBNode.Ordered.memP_iff_find? {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBNode α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] (ht : Batteries.RBNode.Ordered cmp t) :
      theorem Batteries.RBNode.Ordered.unique {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBNode α} {x : α} {y : α} [Batteries.TransCmp cmp] (ht : Batteries.RBNode.Ordered cmp t) (hx : x t) (hy : y t) (e : cmp x y = Ordering.eq) :
      x = y
      theorem Batteries.RBNode.Ordered.find?_some {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBNode α} {x : α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsStrictCut cmp cut] (ht : Batteries.RBNode.Ordered cmp t) :
      @[simp]
      theorem Batteries.RBNode.find?_reverse {α : Type u_1} (t : Batteries.RBNode α) (cut : αOrdering) :
      Batteries.RBNode.find? cut t.reverse = Batteries.RBNode.find? (fun (x : α) => (cut x).swap) t

      Auxiliary definition for zoom_ins: set the root of the tree to v, creating a node if necessary.

      Equations
      Instances For

        Auxiliary definition for zoom_ins: set the root of the tree to v, creating a node if necessary.

        Equations
        Instances For
          @[simp]
          theorem Batteries.RBNode.upperBound?_reverse {α : Type u_1} (t : Batteries.RBNode α) (cut : αOrdering) (ub : Option α) :
          Batteries.RBNode.upperBound? cut t.reverse ub = Batteries.RBNode.lowerBound? (fun (x : α) => (cut x).swap) t ub
          @[simp]
          theorem Batteries.RBNode.lowerBound?_reverse {α : Type u_1} (t : Batteries.RBNode α) (cut : αOrdering) (lb : Option α) :
          Batteries.RBNode.lowerBound? cut t.reverse lb = Batteries.RBNode.upperBound? (fun (x : α) => (cut x).swap) t lb
          theorem Batteries.RBNode.upperBound?_eq_find? {α : Type u_1} {x : α} {t : Batteries.RBNode α} {cut : αOrdering} (ub : Option α) (H : Batteries.RBNode.find? cut t = some x) :
          theorem Batteries.RBNode.lowerBound?_eq_find? {α : Type u_1} {x : α} {t : Batteries.RBNode α} {cut : αOrdering} (lb : Option α) (H : Batteries.RBNode.find? cut t = some x) :
          theorem Batteries.RBNode.upperBound?_ge' {α : Type u_1} {ub : Option α} {cut : αOrdering} {x : α} {t : Batteries.RBNode α} (H : ∀ {x : α}, x ubcut x Ordering.gt) :

          The value x returned by upperBound? is greater or equal to the cut.

          theorem Batteries.RBNode.upperBound?_ge {α : Type u_1} {cut : αOrdering} {x : α} {t : Batteries.RBNode α} :

          The value x returned by upperBound? is greater or equal to the cut.

          theorem Batteries.RBNode.lowerBound?_le' {α : Type u_1} {lb : Option α} {cut : αOrdering} {x : α} {t : Batteries.RBNode α} (H : ∀ {x : α}, x lbcut x Ordering.lt) :

          The value x returned by lowerBound? is less or equal to the cut.

          theorem Batteries.RBNode.lowerBound?_le {α : Type u_1} {cut : αOrdering} {x : α} {t : Batteries.RBNode α} :

          The value x returned by lowerBound? is less or equal to the cut.

          theorem Batteries.RBNode.All.upperBound?_ub {α : Type u_1} {p : αProp} {ub : Option α} {cut : αOrdering} {x : α} {t : Batteries.RBNode α} (hp : Batteries.RBNode.All p t) (H : ∀ {x : α}, ub = some xp x) :
          theorem Batteries.RBNode.All.upperBound? {α : Type u_1} {p : αProp} {cut : αOrdering} {x : α} {t : Batteries.RBNode α} (hp : Batteries.RBNode.All p t) :
          theorem Batteries.RBNode.All.lowerBound?_lb {α : Type u_1} {p : αProp} {lb : Option α} {cut : αOrdering} {x : α} {t : Batteries.RBNode α} (hp : Batteries.RBNode.All p t) (H : ∀ {x : α}, lb = some xp x) :
          theorem Batteries.RBNode.All.lowerBound? {α : Type u_1} {p : αProp} {cut : αOrdering} {x : α} {t : Batteries.RBNode α} (hp : Batteries.RBNode.All p t) :
          theorem Batteries.RBNode.upperBound?_mem_ub {α : Type u_1} {cut : αOrdering} {ub : Option α} {x : α} {t : Batteries.RBNode α} (h : Batteries.RBNode.upperBound? cut t ub = some x) :
          x t ub = some x
          theorem Batteries.RBNode.upperBound?_mem {α : Type u_1} {cut : αOrdering} {x : α} {t : Batteries.RBNode α} (h : Batteries.RBNode.upperBound? cut t = some x) :
          x t
          theorem Batteries.RBNode.lowerBound?_mem_lb {α : Type u_1} {cut : αOrdering} {lb : Option α} {x : α} {t : Batteries.RBNode α} (h : Batteries.RBNode.lowerBound? cut t lb = some x) :
          x t lb = some x
          theorem Batteries.RBNode.lowerBound?_mem {α : Type u_1} {cut : αOrdering} {x : α} {t : Batteries.RBNode α} (h : Batteries.RBNode.lowerBound? cut t = some x) :
          x t
          theorem Batteries.RBNode.upperBound?_of_some {α : Type u_1} {cut : αOrdering} {y : α} {t : Batteries.RBNode α} :
          ∃ (x : α), Batteries.RBNode.upperBound? cut t (some y) = some x
          theorem Batteries.RBNode.lowerBound?_of_some {α : Type u_1} {cut : αOrdering} {y : α} {t : Batteries.RBNode α} :
          ∃ (x : α), Batteries.RBNode.lowerBound? cut t (some y) = some x
          theorem Batteries.RBNode.Ordered.upperBound?_exists {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBNode α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] (h : Batteries.RBNode.Ordered cmp t) :
          (∃ (x : α), Batteries.RBNode.upperBound? cut t = some x) ∃ (x : α), x t cut x Ordering.gt
          theorem Batteries.RBNode.Ordered.lowerBound?_exists {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBNode α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] (h : Batteries.RBNode.Ordered cmp t) :
          (∃ (x : α), Batteries.RBNode.lowerBound? cut t = some x) ∃ (x : α), x t cut x Ordering.lt
          theorem Batteries.RBNode.Ordered.upperBound?_least_ub {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBNode α} {ub : Option α} {x : α} {y : α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] (h : Batteries.RBNode.Ordered cmp t) (hub : ∀ {x : α}, ub = some xBatteries.RBNode.All (fun (x_1 : α) => Batteries.RBNode.cmpLT cmp x_1 x) t) :
          Batteries.RBNode.upperBound? cut t ub = some xy tcut x = Ordering.ltcmp y x = Ordering.ltcut y = Ordering.gt
          theorem Batteries.RBNode.Ordered.lowerBound?_greatest_lb {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBNode α} {lb : Option α} {x : α} {y : α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] (h : Batteries.RBNode.Ordered cmp t) (hlb : ∀ {x : α}, lb = some xBatteries.RBNode.All (fun (x_1 : α) => Batteries.RBNode.cmpLT cmp x x_1) t) :
          Batteries.RBNode.lowerBound? cut t lb = some xy tcut x = Ordering.gtcmp x y = Ordering.ltcut y = Ordering.lt
          theorem Batteries.RBNode.Ordered.upperBound?_least {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBNode α} {x : α} {y : α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] (ht : Batteries.RBNode.Ordered cmp t) (H : Batteries.RBNode.upperBound? cut t = some x) (hy : y t) (xy : cmp y x = Ordering.lt) (hx : cut x = Ordering.lt) :

          A statement of the least-ness of the result of upperBound?. If x is the return value of upperBound? and it is strictly greater than the cut, then any other y < x in the tree is in fact strictly less than the cut (so there is no exact match, and nothing closer to the cut).

          theorem Batteries.RBNode.Ordered.lowerBound?_greatest {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBNode α} {x : α} {y : α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] (ht : Batteries.RBNode.Ordered cmp t) (H : Batteries.RBNode.lowerBound? cut t = some x) (hy : y t) (xy : cmp x y = Ordering.lt) (hx : cut x = Ordering.gt) :

          A statement of the greatest-ness of the result of lowerBound?. If x is the return value of lowerBound? and it is strictly less than the cut, then any other y > x in the tree is in fact strictly greater than the cut (so there is no exact match, and nothing closer to the cut).

          theorem Batteries.RBNode.Ordered.lowerBound?_lt {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBNode α} {x : α} {y : α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsStrictCut cmp cut] (ht : Batteries.RBNode.Ordered cmp t) (H : Batteries.RBNode.lowerBound? cut t = some x) (hy : y t) :
          cmp x y = Ordering.lt cut y = Ordering.lt

          A stronger version of lowerBound?_greatest that holds when the cut is strict.

          theorem Batteries.RBNode.Ordered.lt_upperBound? {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBNode α} {x : α} {y : α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsStrictCut cmp cut] (ht : Batteries.RBNode.Ordered cmp t) (H : Batteries.RBNode.upperBound? cut t = some x) (hy : y t) :
          cmp y x = Ordering.lt cut y = Ordering.gt

          A stronger version of upperBound?_least that holds when the cut is strict.

          The list of elements to the left of the hole. (This function is intended for specification purposes only.)

          Equations
          Instances For

            The list of elements to the right of the hole. (This function is intended for specification purposes only.)

            Equations
            Instances For
              @[reducible, inline]
              abbrev Batteries.RBNode.Path.withList {α : Type u_1} (p : Batteries.RBNode.Path α) (l : List α) :
              List α

              Wraps a list of elements with the left and right elements of the path.

              Equations
              • p.withList l = p.listL ++ l ++ p.listR
              Instances For
                theorem Batteries.RBNode.Path.rootOrdered_iff {α : Type u_1} {cmp : ααOrdering} {v : α} {p : Batteries.RBNode.Path α} (hp : Batteries.RBNode.Path.Ordered cmp p) :
                Batteries.RBNode.Path.RootOrdered cmp p v (∀ (a : α), a p.listLBatteries.RBNode.cmpLT cmp a v) ∀ (a : α), a p.listRBatteries.RBNode.cmpLT cmp v a
                theorem Batteries.RBNode.Path.ordered_iff {α : Type u_1} {cmp : ααOrdering} {p : Batteries.RBNode.Path α} :
                Batteries.RBNode.Path.Ordered cmp p List.Pairwise (Batteries.RBNode.cmpLT cmp) p.listL List.Pairwise (Batteries.RBNode.cmpLT cmp) p.listR ∀ (x : α), x p.listL∀ (y : α), y p.listRBatteries.RBNode.cmpLT cmp x y
                theorem Batteries.RBNode.Path.zoom_zoomed₁ :
                ∀ {α : Type u_1} {cut : αOrdering} {t : Batteries.RBNode α} {path : Batteries.RBNode.Path α} {t' : Batteries.RBNode α} {path' : Batteries.RBNode.Path α}, Batteries.RBNode.zoom cut t path = (t', path')Batteries.RBNode.OnRoot (fun (x : α) => cut x = Ordering.eq) t'
                @[simp]
                theorem Batteries.RBNode.Path.fill_toList {α : Type u_1} {t : Batteries.RBNode α} {p : Batteries.RBNode.Path α} :
                (p.fill t).toList = p.withList t.toList
                theorem Batteries.RBNode.zoom_toList {α : Type u_1} {cut : αOrdering} {t' : Batteries.RBNode α} {p' : Batteries.RBNode.Path α} {t : Batteries.RBNode α} (eq : Batteries.RBNode.zoom cut t = (t', p')) :
                p'.withList t'.toList = t.toList
                @[simp]
                theorem Batteries.RBNode.Path.ins_toList {α : Type u_1} {t : Batteries.RBNode α} {p : Batteries.RBNode.Path α} :
                (p.ins t).toList = p.withList t.toList
                @[simp]
                theorem Batteries.RBNode.Path.insertNew_toList {α : Type u_1} {v : α} {p : Batteries.RBNode.Path α} :
                (p.insertNew v).toList = p.withList [v]
                theorem Batteries.RBNode.Path.insert_toList {α : Type u_1} {t : Batteries.RBNode α} {v : α} {p : Batteries.RBNode.Path α} :
                (p.insert t v).toList = p.withList (Batteries.RBNode.setRoot v t).toList
                theorem Batteries.RBNode.Path.Balanced.insert {α : Type u_1} {c₀ : Batteries.RBColor} {n₀ : Nat} {c : Batteries.RBColor} {n : Nat} {t : Batteries.RBNode α} {v : α} {path : Batteries.RBNode.Path α} (hp : Batteries.RBNode.Path.Balanced c₀ n₀ path c n) :
                t.Balanced c n∃ (c : Batteries.RBColor), ∃ (n : Nat), (path.insert t v).Balanced c n
                @[irreducible]
                theorem Batteries.RBNode.Path.zoom_ins {α : Type u_1} {v : α} {path : Batteries.RBNode.Path α} {t' : Batteries.RBNode α} {path' : Batteries.RBNode.Path α} {t : Batteries.RBNode α} {cmp : ααOrdering} :
                Batteries.RBNode.zoom (cmp v) t path = (t', path')path.ins (Batteries.RBNode.ins cmp v t) = path'.ins (Batteries.RBNode.setRoot v t')
                theorem Batteries.RBNode.Path.insertNew_eq_insert :
                ∀ {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBNode α} {path : Batteries.RBNode.Path α} {v : α}, Batteries.RBNode.zoom (cmp v) t = (Batteries.RBNode.nil, path)path.insertNew v = (Batteries.RBNode.insert cmp t v).setBlack
                theorem Batteries.RBNode.Path.ins_eq_fill {α : Type u_1} {c₀ : Batteries.RBColor} {n₀ : Nat} {c : Batteries.RBColor} {n : Nat} {path : Batteries.RBNode.Path α} {t : Batteries.RBNode α} :
                Batteries.RBNode.Path.Balanced c₀ n₀ path c nt.Balanced c npath.ins t = (path.fill t).setBlack
                theorem Batteries.RBNode.Path.zoom_insert {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {cmp : ααOrdering} {t' : Batteries.RBNode α} {v : α} {path : Batteries.RBNode.Path α} {t : Batteries.RBNode α} (ht : t.Balanced c n) (H : Batteries.RBNode.zoom (cmp v) t = (t', path)) :
                (path.insert t' v).setBlack = (Batteries.RBNode.insert cmp t v).setBlack
                @[irreducible]
                theorem Batteries.RBNode.Path.zoom_del {α : Type u_1} {cut : αOrdering} {path : Batteries.RBNode.Path α} {t' : Batteries.RBNode α} {path' : Batteries.RBNode.Path α} {t : Batteries.RBNode α} :
                Batteries.RBNode.zoom cut t path = (t', path')path.del (Batteries.RBNode.del cut t) (match t with | Batteries.RBNode.node c l v r => c | x => Batteries.RBColor.red) = path'.del t'.delRoot (match t' with | Batteries.RBNode.node c l v r => c | x => Batteries.RBColor.red)
                def Batteries.RBNode.Path.AllL {α : Type u_1} (p : αProp) :

                Asserts that p holds on all elements to the left of the hole.

                Equations
                Instances For
                  def Batteries.RBNode.Path.AllR {α : Type u_1} (p : αProp) :

                  Asserts that p holds on all elements to the right of the hole.

                  Equations
                  Instances For
                    theorem Batteries.RBNode.insert_toList_zoom {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {cmp : ααOrdering} {t' : Batteries.RBNode α} {p : Batteries.RBNode.Path α} {v : α} {t : Batteries.RBNode α} (ht : t.Balanced c n) (e : Batteries.RBNode.zoom (cmp v) t = (t', p)) :
                    (Batteries.RBNode.insert cmp t v).toList = p.withList (Batteries.RBNode.setRoot v t').toList
                    theorem Batteries.RBNode.insert_toList_zoom_nil {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {cmp : ααOrdering} {p : Batteries.RBNode.Path α} {v : α} {t : Batteries.RBNode α} (ht : t.Balanced c n) (e : Batteries.RBNode.zoom (cmp v) t = (Batteries.RBNode.nil, p)) :
                    (Batteries.RBNode.insert cmp t v).toList = p.withList [v]
                    theorem Batteries.RBNode.exists_insert_toList_zoom_nil {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {cmp : ααOrdering} {p : Batteries.RBNode.Path α} {v : α} {t : Batteries.RBNode α} (ht : t.Balanced c n) (e : Batteries.RBNode.zoom (cmp v) t = (Batteries.RBNode.nil, p)) :
                    ∃ (L : List α), ∃ (R : List α), t.toList = L ++ R (Batteries.RBNode.insert cmp t v).toList = L ++ v :: R
                    theorem Batteries.RBNode.insert_toList_zoom_node {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {cmp : ααOrdering} {c' : Batteries.RBColor} {l : Batteries.RBNode α} {v' : α} {r : Batteries.RBNode α} {p : Batteries.RBNode.Path α} {v : α} {t : Batteries.RBNode α} (ht : t.Balanced c n) (e : Batteries.RBNode.zoom (cmp v) t = (Batteries.RBNode.node c' l v' r, p)) :
                    (Batteries.RBNode.insert cmp t v).toList = p.withList (Batteries.RBNode.node c l v r).toList
                    theorem Batteries.RBNode.exists_insert_toList_zoom_node {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {cmp : ααOrdering} {c' : Batteries.RBColor} {l : Batteries.RBNode α} {v' : α} {r : Batteries.RBNode α} {p : Batteries.RBNode.Path α} {v : α} {t : Batteries.RBNode α} (ht : t.Balanced c n) (e : Batteries.RBNode.zoom (cmp v) t = (Batteries.RBNode.node c' l v' r, p)) :
                    ∃ (L : List α), ∃ (R : List α), t.toList = L ++ v' :: R (Batteries.RBNode.insert cmp t v).toList = L ++ v :: R
                    theorem Batteries.RBNode.mem_insert_self {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {cmp : ααOrdering} {v : α} {t : Batteries.RBNode α} (ht : t.Balanced c n) :
                    theorem Batteries.RBNode.mem_insert_of_mem {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {v' : α} {cmp : ααOrdering} {v : α} {t : Batteries.RBNode α} (ht : t.Balanced c n) (h : v' t) :
                    theorem Batteries.RBNode.exists_find?_insert_self {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {c : Batteries.RBColor} {n : Nat} {v : α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] {t : Batteries.RBNode α} (ht : t.Balanced c n) (ht₂ : Batteries.RBNode.Ordered cmp t) (hv : cut v = Ordering.eq) :
                    theorem Batteries.RBNode.find?_insert_self {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {c : Batteries.RBColor} {n : Nat} {v : α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsStrictCut cmp cut] {t : Batteries.RBNode α} (ht : t.Balanced c n) (ht₂ : Batteries.RBNode.Ordered cmp t) (hv : cut v = Ordering.eq) :
                    theorem Batteries.RBNode.mem_insert {α : Type u_1} {cmp : ααOrdering} {c : Batteries.RBColor} {n : Nat} {v : α} {v' : α} [Batteries.TransCmp cmp] {t : Batteries.RBNode α} (ht : t.Balanced c n) (ht₂ : Batteries.RBNode.Ordered cmp t) :
                    @[simp]
                    theorem Batteries.RBSet.val_toList {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBSet α cmp} :
                    t.val.toList = t.toList
                    @[simp]
                    theorem Batteries.RBSet.mkRBSet_eq {α : Type u_1} {cmp : ααOrdering} :
                    @[simp]
                    theorem Batteries.RBSet.empty_eq {α : Type u_1} {cmp : ααOrdering} :
                    Batteries.RBSet.empty =
                    @[simp]
                    theorem Batteries.RBSet.default_eq {α : Type u_1} {cmp : ααOrdering} :
                    default =
                    @[simp]
                    theorem Batteries.RBSet.empty_toList {α : Type u_1} {cmp : ααOrdering} :
                    .toList = []
                    @[simp]
                    theorem Batteries.RBSet.single_toList {α : Type u_1} {cmp : ααOrdering} {a : α} :
                    (Batteries.RBSet.single a).toList = [a]
                    theorem Batteries.RBSet.mem_toList {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Batteries.RBSet α cmp} :
                    x t.toList x t.val
                    theorem Batteries.RBSet.mem_congr {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} [Batteries.TransCmp cmp] {t : Batteries.RBSet α cmp} (h : cmp x y = Ordering.eq) :
                    x t y t
                    theorem Batteries.RBSet.mem_iff_mem_toList {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Batteries.RBSet α cmp} :
                    x t ∃ (y : α), y t.toList cmp x y = Ordering.eq
                    theorem Batteries.RBSet.mem_of_mem_toList {α : Type u_1} {cmp : ααOrdering} {x : α} [Batteries.OrientedCmp cmp] {t : Batteries.RBSet α cmp} (h : x t.toList) :
                    x t
                    theorem Batteries.RBSet.foldl_eq_foldl_toList {α : Type u_1} {cmp : ααOrdering} :
                    ∀ {α_1 : Type u_2} {f : α_1αα_1} {init : α_1} {t : Batteries.RBSet α cmp}, Batteries.RBSet.foldl f init t = List.foldl f init t.toList
                    theorem Batteries.RBSet.foldr_eq_foldr_toList {α : Type u_1} {cmp : ααOrdering} :
                    ∀ {α_1 : Type u_2} {f : αα_1α_1} {init : α_1} {t : Batteries.RBSet α cmp}, Batteries.RBSet.foldr f init t = List.foldr f init t.toList
                    theorem Batteries.RBSet.foldlM_eq_foldlM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : ααOrdering} :
                    ∀ {a : Type u_1} {f : aαm a} {init : a} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Batteries.RBSet α cmp}, Batteries.RBSet.foldlM f init t = List.foldlM f init t.toList
                    theorem Batteries.RBSet.forM_eq_forM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : ααOrdering} {f : αm PUnit} [Monad m] [LawfulMonad m] {t : Batteries.RBSet α cmp} :
                    Batteries.RBSet.forM f t = t.toList.forM f
                    theorem Batteries.RBSet.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : ααOrdering} :
                    ∀ {α_1 : Type u_1} {init : α_1} {f : αα_1m (ForInStep α_1)} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Batteries.RBSet α cmp}, forIn t init f = forIn t.toList init f
                    theorem Batteries.RBSet.toStream_eq {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBSet α cmp} :
                    toStream t = t.val.toStream
                    @[simp]
                    theorem Batteries.RBSet.toStream_toList {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBSet α cmp} :
                    (toStream t).toList = t.toList
                    theorem Batteries.RBSet.isEmpty_iff_toList_eq_nil {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBSet α cmp} :
                    t.isEmpty = true t.toList = []
                    theorem Batteries.RBSet.toList_sorted {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBSet α cmp} :
                    theorem Batteries.RBSet.findP?_some_eq_eq {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {y : α} {t : Batteries.RBSet α cmp} :
                    t.findP? cut = some ycut y = Ordering.eq
                    theorem Batteries.RBSet.find?_some_eq_eq {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {t : Batteries.RBSet α cmp} :
                    t.find? x = some ycmp x y = Ordering.eq
                    theorem Batteries.RBSet.findP?_some_mem_toList {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {y : α} {t : Batteries.RBSet α cmp} (h : t.findP? cut = some y) :
                    y t.toList
                    theorem Batteries.RBSet.find?_some_mem_toList {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {t : Batteries.RBSet α cmp} (h : t.find? x = some y) :
                    y t.toList
                    theorem Batteries.RBSet.findP?_some_memP {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {y : α} {t : Batteries.RBSet α cmp} (h : t.findP? cut = some y) :
                    theorem Batteries.RBSet.find?_some_mem {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {t : Batteries.RBSet α cmp} (h : t.find? x = some y) :
                    x t
                    theorem Batteries.RBSet.mem_toList_unique {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} [Batteries.TransCmp cmp] {t : Batteries.RBSet α cmp} (hx : x t.toList) (hy : y t.toList) (e : cmp x y = Ordering.eq) :
                    x = y
                    theorem Batteries.RBSet.findP?_some {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {y : α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsStrictCut cmp cut] {t : Batteries.RBSet α cmp} :
                    t.findP? cut = some y y t.toList cut y = Ordering.eq
                    theorem Batteries.RBSet.find?_some {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} [Batteries.TransCmp cmp] {t : Batteries.RBSet α cmp} :
                    t.find? x = some y y t.toList cmp x y = Ordering.eq
                    theorem Batteries.RBSet.memP_iff_findP? {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] {t : Batteries.RBSet α cmp} :
                    Batteries.RBSet.MemP cut t ∃ (y : α), t.findP? cut = some y
                    theorem Batteries.RBSet.mem_iff_find? {α : Type u_1} {cmp : ααOrdering} {x : α} [Batteries.TransCmp cmp] {t : Batteries.RBSet α cmp} :
                    x t ∃ (y : α), t.find? x = some y
                    @[simp]
                    theorem Batteries.RBSet.contains_iff {α : Type u_1} {cmp : ααOrdering} {x : α} [Batteries.TransCmp cmp] {t : Batteries.RBSet α cmp} :
                    t.contains x = true x t
                    instance Batteries.RBSet.instDecidableMemOfTransCmp {α : Type u_1} {cmp : ααOrdering} {x : α} [Batteries.TransCmp cmp] {t : Batteries.RBSet α cmp} :
                    Equations
                    theorem Batteries.RBSet.size_eq {α : Type u_1} {cmp : ααOrdering} (t : Batteries.RBSet α cmp) :
                    t.size = t.toList.length
                    theorem Batteries.RBSet.mem_toList_insert_self {α : Type u_1} {cmp : ααOrdering} (v : α) (t : Batteries.RBSet α cmp) :
                    v (t.insert v).toList
                    theorem Batteries.RBSet.mem_insert_self {α : Type u_1} {cmp : ααOrdering} [Batteries.OrientedCmp cmp] (v : α) (t : Batteries.RBSet α cmp) :
                    v t.insert v
                    theorem Batteries.RBSet.mem_insert_of_eq {α : Type u_1} {cmp : ααOrdering} {v : α} {v' : α} [Batteries.TransCmp cmp] (t : Batteries.RBSet α cmp) (h : cmp v v' = Ordering.eq) :
                    v' t.insert v
                    theorem Batteries.RBSet.mem_toList_insert_of_mem {α : Type u_1} {cmp : ααOrdering} {v' : α} (v : α) {t : Batteries.RBSet α cmp} (h : v' t.toList) :
                    v' (t.insert v).toList cmp v v' = Ordering.eq
                    theorem Batteries.RBSet.mem_insert_of_mem_toList {α : Type u_1} {cmp : ααOrdering} {v' : α} [Batteries.OrientedCmp cmp] (v : α) {t : Batteries.RBSet α cmp} (h : v' t.toList) :
                    v' t.insert v
                    theorem Batteries.RBSet.mem_insert_of_mem {α : Type u_1} {cmp : ααOrdering} {v' : α} [Batteries.TransCmp cmp] (v : α) {t : Batteries.RBSet α cmp} (h : v' t) :
                    v' t.insert v
                    theorem Batteries.RBSet.mem_toList_insert {α : Type u_1} {cmp : ααOrdering} {v : α} {v' : α} [Batteries.TransCmp cmp] {t : Batteries.RBSet α cmp} :
                    v' (t.insert v).toList v' t.toList t.find? v some v' v' = v
                    theorem Batteries.RBSet.mem_insert {α : Type u_1} {cmp : ααOrdering} {v : α} {v' : α} [Batteries.TransCmp cmp] {t : Batteries.RBSet α cmp} :
                    v' t.insert v v' t cmp v v' = Ordering.eq
                    theorem Batteries.RBSet.find?_congr {α : Type u_1} {cmp : ααOrdering} {v₁ : α} {v₂ : α} [Batteries.TransCmp cmp] (t : Batteries.RBSet α cmp) (h : cmp v₁ v₂ = Ordering.eq) :
                    t.find? v₁ = t.find? v₂
                    theorem Batteries.RBSet.findP?_insert_of_eq {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {v : α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsStrictCut cmp cut] (t : Batteries.RBSet α cmp) (h : cut v = Ordering.eq) :
                    (t.insert v).findP? cut = some v
                    theorem Batteries.RBSet.find?_insert_of_eq {α : Type u_1} {cmp : ααOrdering} {v' : α} {v : α} [Batteries.TransCmp cmp] (t : Batteries.RBSet α cmp) (h : cmp v' v = Ordering.eq) :
                    (t.insert v).find? v' = some v
                    theorem Batteries.RBSet.findP?_insert_of_ne {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {v : α} [Batteries.TransCmp cmp] [Batteries.RBNode.IsStrictCut cmp cut] (t : Batteries.RBSet α cmp) (h : cut v Ordering.eq) :
                    (t.insert v).findP? cut = t.findP? cut
                    theorem Batteries.RBSet.find?_insert_of_ne {α : Type u_1} {cmp : ααOrdering} {v' : α} {v : α} [Batteries.TransCmp cmp] (t : Batteries.RBSet α cmp) (h : cmp v' v Ordering.eq) :
                    (t.insert v).find? v' = t.find? v'
                    theorem Batteries.RBSet.findP?_insert {α : Type u_1} {cmp : ααOrdering} [Batteries.TransCmp cmp] (t : Batteries.RBSet α cmp) (v : α) (cut : αOrdering) [Batteries.RBNode.IsStrictCut cmp cut] :
                    (t.insert v).findP? cut = if cut v = Ordering.eq then some v else t.findP? cut
                    theorem Batteries.RBSet.find?_insert {α : Type u_1} {cmp : ααOrdering} [Batteries.TransCmp cmp] (t : Batteries.RBSet α cmp) (v : α) (v' : α) :
                    (t.insert v).find? v' = if cmp v' v = Ordering.eq then some v else t.find? v'
                    theorem Batteries.RBSet.upperBoundP?_eq_findP? {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Batteries.RBSet α cmp} {cut : αOrdering} (H : t.findP? cut = some x) :
                    t.upperBoundP? cut = some x
                    theorem Batteries.RBSet.lowerBoundP?_eq_findP? {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Batteries.RBSet α cmp} {cut : αOrdering} (H : t.findP? cut = some x) :
                    t.lowerBoundP? cut = some x
                    theorem Batteries.RBSet.upperBound?_eq_find? {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {t : Batteries.RBSet α cmp} (H : t.find? x = some y) :
                    t.upperBound? x = some y
                    theorem Batteries.RBSet.lowerBound?_eq_find? {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {t : Batteries.RBSet α cmp} (H : t.find? x = some y) :
                    t.lowerBound? x = some y
                    theorem Batteries.RBSet.upperBoundP?_ge {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {x : α} {t : Batteries.RBSet α cmp} :
                    t.upperBoundP? cut = some xcut x Ordering.gt

                    The value x returned by upperBoundP? is greater or equal to the cut.

                    theorem Batteries.RBSet.upperBound?_ge {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {t : Batteries.RBSet α cmp} :
                    t.upperBound? x = some ycmp x y Ordering.gt

                    The value y returned by upperBound? x is greater or equal to x.

                    theorem Batteries.RBSet.lowerBoundP?_le {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {x : α} {t : Batteries.RBSet α cmp} :
                    t.lowerBoundP? cut = some xcut x Ordering.lt

                    The value x returned by lowerBoundP? is less or equal to the cut.

                    theorem Batteries.RBSet.lowerBound?_le {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {t : Batteries.RBSet α cmp} :
                    t.lowerBound? x = some ycmp x y Ordering.lt

                    The value y returned by lowerBound? x is less or equal to x.

                    theorem Batteries.RBSet.upperBoundP?_mem_toList {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {x : α} {t : Batteries.RBSet α cmp} (h : t.upperBoundP? cut = some x) :
                    x t.toList
                    theorem Batteries.RBSet.upperBound?_mem_toList {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {t : Batteries.RBSet α cmp} (h : t.upperBound? x = some y) :
                    y t.toList
                    theorem Batteries.RBSet.lowerBoundP?_mem_toList {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {x : α} {t : Batteries.RBSet α cmp} (h : t.lowerBoundP? cut = some x) :
                    x t.toList
                    theorem Batteries.RBSet.lowerBound?_mem_toList {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {t : Batteries.RBSet α cmp} (h : t.lowerBound? x = some y) :
                    y t.toList
                    theorem Batteries.RBSet.upperBoundP?_mem {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {x : α} [Batteries.OrientedCmp cmp] {t : Batteries.RBSet α cmp} (h : t.upperBoundP? cut = some x) :
                    x t
                    theorem Batteries.RBSet.lowerBoundP?_mem {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {x : α} [Batteries.OrientedCmp cmp] {t : Batteries.RBSet α cmp} (h : t.lowerBoundP? cut = some x) :
                    x t
                    theorem Batteries.RBSet.upperBound?_mem {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} [Batteries.OrientedCmp cmp] {t : Batteries.RBSet α cmp} (h : t.upperBound? x = some y) :
                    y t
                    theorem Batteries.RBSet.lowerBound?_mem {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} [Batteries.OrientedCmp cmp] {t : Batteries.RBSet α cmp} (h : t.lowerBound? x = some y) :
                    y t
                    theorem Batteries.RBSet.upperBoundP?_exists {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] :
                    (∃ (x : α), t.upperBoundP? cut = some x) ∃ (x : α), x t cut x Ordering.gt
                    theorem Batteries.RBSet.lowerBoundP?_exists {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] :
                    (∃ (x : α), t.lowerBoundP? cut = some x) ∃ (x : α), x t cut x Ordering.lt
                    theorem Batteries.RBSet.upperBound?_exists {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] :
                    (∃ (y : α), t.upperBound? x = some y) ∃ (y : α), y t cmp x y Ordering.gt
                    theorem Batteries.RBSet.lowerBound?_exists {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] :
                    (∃ (y : α), t.lowerBound? x = some y) ∃ (y : α), y t cmp x y Ordering.lt
                    theorem Batteries.RBSet.upperBoundP?_least {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {x : α} {y : α} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] (H : t.upperBoundP? cut = some x) (hy : y t) (xy : cmp y x = Ordering.lt) (hx : cut x = Ordering.lt) :

                    A statement of the least-ness of the result of upperBoundP?. If x is the return value of upperBoundP? and it is strictly greater than the cut, then any other y < x in the tree is in fact strictly less than the cut (so there is no exact match, and nothing closer to the cut).

                    theorem Batteries.RBSet.lowerBoundP?_greatest {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {x : α} {y : α} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] (H : t.lowerBoundP? cut = some x) (hy : y t) (xy : cmp x y = Ordering.lt) (hx : cut x = Ordering.gt) :

                    A statement of the greatest-ness of the result of lowerBoundP?. If x is the return value of lowerBoundP? and it is strictly less than the cut, then any other y > x in the tree is in fact strictly greater than the cut (so there is no exact match, and nothing closer to the cut).

                    theorem Batteries.RBSet.memP_iff_upperBoundP? {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] :
                    Batteries.RBSet.MemP cut t ∃ (x : α), t.upperBoundP? cut = some x cut x = Ordering.eq
                    theorem Batteries.RBSet.memP_iff_lowerBoundP? {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] [Batteries.RBNode.IsCut cmp cut] :
                    Batteries.RBSet.MemP cut t ∃ (x : α), t.lowerBoundP? cut = some x cut x = Ordering.eq
                    theorem Batteries.RBSet.mem_iff_upperBound? {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] :
                    x t ∃ (y : α), t.upperBound? x = some y cmp x y = Ordering.eq
                    theorem Batteries.RBSet.mem_iff_lowerBound? {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] :
                    x t ∃ (y : α), t.lowerBound? x = some y cmp x y = Ordering.eq
                    theorem Batteries.RBSet.lt_upperBoundP? {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {x : α} {y : α} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] [Batteries.RBNode.IsStrictCut cmp cut] (H : t.upperBoundP? cut = some x) (hy : y t) :
                    cmp y x = Ordering.lt cut y = Ordering.gt

                    A stronger version of upperBoundP?_least that holds when the cut is strict.

                    theorem Batteries.RBSet.lowerBoundP?_lt {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {x : α} {y : α} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] [Batteries.RBNode.IsStrictCut cmp cut] (H : t.lowerBoundP? cut = some x) (hy : y t) :
                    cmp x y = Ordering.lt cut y = Ordering.lt

                    A stronger version of lowerBoundP?_greatest that holds when the cut is strict.

                    theorem Batteries.RBSet.lt_upperBound? {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {z : α} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] (H : t.upperBound? x = some y) (hz : z t) :
                    cmp z y = Ordering.lt cmp z x = Ordering.lt
                    theorem Batteries.RBSet.lowerBound?_lt {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} {z : α} {t : Batteries.RBSet α cmp} [Batteries.TransCmp cmp] (H : t.lowerBound? x = some y) (hz : z t) :
                    cmp y z = Ordering.lt cmp x z = Ordering.lt
                    theorem Batteries.RBMap.val_toList {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} {t : Batteries.RBMap α β cmp} :
                    t.val.toList = t.toList
                    @[simp]
                    theorem Batteries.RBMap.mkRBSet_eq {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
                    @[simp]
                    theorem Batteries.RBMap.empty_eq {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
                    Batteries.RBMap.empty =
                    @[simp]
                    theorem Batteries.RBMap.default_eq {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
                    default =
                    @[simp]
                    theorem Batteries.RBMap.empty_toList {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
                    .toList = []
                    @[simp]
                    theorem Batteries.RBMap.single_toList {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} {a : α} {b : β} :
                    (Batteries.RBMap.single a b).toList = [(a, b)]
                    theorem Batteries.RBMap.mem_toList {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} {x : α × β} {t : Batteries.RBMap α β cmp} :
                    x t.toList x t.val
                    theorem Batteries.RBMap.foldl_eq_foldl_toList {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
                    ∀ {α_1 : Type u_3} {f : α_1αβα_1} {init : α_1} {t : Batteries.RBMap α β cmp}, Batteries.RBMap.foldl f init t = List.foldl (fun (r : α_1) (p : α × β) => f r p.fst p.snd) init t.toList
                    theorem Batteries.RBMap.foldr_eq_foldr_toList {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
                    ∀ {α_1 : Type u_3} {f : αβα_1α_1} {init : α_1} {t : Batteries.RBMap α β cmp}, Batteries.RBMap.foldr f init t = List.foldr (fun (p : α × β) (r : α_1) => f p.fst p.snd r) init t.toList
                    theorem Batteries.RBMap.foldlM_eq_foldlM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : ααOrdering} :
                    ∀ {a : Type u_1} {f : aαβm a} {init : a} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Batteries.RBMap α β cmp}, Batteries.RBMap.foldlM f init t = List.foldlM (fun (r : a) (p : α × β) => f r p.fst p.snd) init t.toList
                    theorem Batteries.RBMap.forM_eq_forM_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : ααOrdering} {f : αβm PUnit} [Monad m] [LawfulMonad m] {t : Batteries.RBMap α β cmp} :
                    Batteries.RBMap.forM f t = t.toList.forM fun (p : α × β) => f p.fst p.snd
                    theorem Batteries.RBMap.forIn_eq_forIn_toList {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {cmp : ααOrdering} :
                    ∀ {α_1 : Type u_1} {init : α_1} {f : α × βα_1m (ForInStep α_1)} [inst : Monad m] [inst_1 : LawfulMonad m] {t : Batteries.RBMap α β cmp}, forIn t init f = forIn t.toList init f
                    theorem Batteries.RBMap.toStream_eq {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} {t : Batteries.RBMap α β cmp} :
                    toStream t = t.val.toStream
                    @[simp]
                    theorem Batteries.RBMap.toStream_toList {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} {t : Batteries.RBMap α β cmp} :
                    (toStream t).toList = t.toList
                    theorem Batteries.RBMap.toList_sorted {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} {t : Batteries.RBMap α β cmp} :
                    List.Pairwise (Batteries.RBNode.cmpLT fun (x1 x2 : α × β) => cmp x1.fst x2.fst) t.toList
                    theorem Batteries.RBMap.findEntry?_some_eq_eq {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} {x : α} {y : α} {v : β} {t : Batteries.RBMap α β cmp} :
                    t.findEntry? x = some (y, v)cmp x y = Ordering.eq
                    theorem Batteries.RBMap.findEntry?_some_mem_toList {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} {x : α} {y : α × β} {t : Batteries.RBMap α β cmp} (h : t.findEntry? x = some y) :
                    y t.toList
                    theorem Batteries.RBMap.find?_some_mem_toList {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} {x : α} {v : β} {t : Batteries.RBMap α β cmp} (h : t.find? x = some v) :
                    ∃ (y : α), (y, v) t.toList cmp x y = Ordering.eq
                    theorem Batteries.RBMap.mem_toList_unique {α : Type u_1} {cmp : ααOrdering} {β : Type u_2} {x : α × β} {y : α × β} [Batteries.TransCmp cmp] {t : Batteries.RBMap α β cmp} (hx : x t.toList) (hy : y t.toList) (e : cmp x.fst y.fst = Ordering.eq) :
                    x = y
                    instance Batteries.RBMap.instIsStrictCut {α : Sort u_1} (cmp : ααOrdering) (a : α) :

                    A "representable cut" is one generated by cmp a for some a. This is always a valid cut.

                    Equations
                    • =
                    instance Batteries.RBMap.instIsStrictCutByKeyOfTransCmp {α : Sort u_1} {β : Sort u_2} (f : αβ) (cmp : ββOrdering) [Batteries.TransCmp cmp] (x : β) :
                    Batteries.RBNode.IsStrictCut (Ordering.byKey f cmp) fun (y : α) => cmp x (f y)
                    Equations
                    • =
                    theorem Batteries.RBMap.findEntry?_some {α : Type u_1} {cmp : ααOrdering} {β : Type u_2} {x : α} {y : α × β} [Batteries.TransCmp cmp] {t : Batteries.RBMap α β cmp} :
                    t.findEntry? x = some y y t.toList cmp x y.fst = Ordering.eq
                    theorem Batteries.RBMap.find?_some {α : Type u_1} {cmp : ααOrdering} {β : Type u_2} {x : α} {v : β} [Batteries.TransCmp cmp] {t : Batteries.RBMap α β cmp} :
                    t.find? x = some v ∃ (y : α), (y, v) t.toList cmp x y = Ordering.eq
                    theorem Batteries.RBMap.contains_iff_findEntry? {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} {x : α} {t : Batteries.RBMap α β cmp} :
                    t.contains x = true ∃ (v : α × β), t.findEntry? x = some v
                    theorem Batteries.RBMap.contains_iff_find? {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} {x : α} {t : Batteries.RBMap α β cmp} :
                    t.contains x = true ∃ (v : β), t.find? x = some v
                    theorem Batteries.RBMap.size_eq {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (t : Batteries.RBMap α β cmp) :
                    t.size = t.toList.length
                    theorem Batteries.RBMap.mem_toList_insert_self {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} {k : α} (v : β) (t : Batteries.RBMap α β cmp) :
                    (k, v) (t.insert k v).toList
                    theorem Batteries.RBMap.mem_toList_insert_of_mem {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} {y : α × β} {k : α} (v : β) {t : Batteries.RBMap α β cmp} (h : y t.toList) :
                    y (t.insert k v).toList cmp k y.fst = Ordering.eq
                    theorem Batteries.RBMap.mem_toList_insert {α : Type u_1} {cmp : ααOrdering} {β : Type u_2} {k : α} {v : β} {y : α × β} [Batteries.TransCmp cmp] {t : Batteries.RBMap α β cmp} :
                    y (t.insert k v).toList y t.toList t.findEntry? k some y y = (k, v)
                    theorem Batteries.RBMap.findEntry?_congr {α : Type u_1} {cmp : ααOrdering} {β : Type u_2} {k₁ : α} {k₂ : α} [Batteries.TransCmp cmp] (t : Batteries.RBMap α β cmp) (h : cmp k₁ k₂ = Ordering.eq) :
                    t.findEntry? k₁ = t.findEntry? k₂
                    theorem Batteries.RBMap.find?_congr {α : Type u_1} {cmp : ααOrdering} {β : Type u_2} {k₁ : α} {k₂ : α} [Batteries.TransCmp cmp] (t : Batteries.RBMap α β cmp) (h : cmp k₁ k₂ = Ordering.eq) :
                    t.find? k₁ = t.find? k₂
                    theorem Batteries.RBMap.findEntry?_insert_of_eq {α : Type u_1} {cmp : ααOrdering} {β : Type u_2} {k' : α} {k : α} {v : β} [Batteries.TransCmp cmp] (t : Batteries.RBMap α β cmp) (h : cmp k' k = Ordering.eq) :
                    (t.insert k v).findEntry? k' = some (k, v)
                    theorem Batteries.RBMap.find?_insert_of_eq {α : Type u_1} {cmp : ααOrdering} {β : Type u_2} {k' : α} {k : α} {v : β} [Batteries.TransCmp cmp] (t : Batteries.RBMap α β cmp) (h : cmp k' k = Ordering.eq) :
                    (t.insert k v).find? k' = some v
                    theorem Batteries.RBMap.findEntry?_insert_of_ne {α : Type u_1} {cmp : ααOrdering} {β : Type u_2} {k' : α} {k : α} {v : β} [Batteries.TransCmp cmp] (t : Batteries.RBMap α β cmp) (h : cmp k' k Ordering.eq) :
                    (t.insert k v).findEntry? k' = t.findEntry? k'
                    theorem Batteries.RBMap.find?_insert_of_ne {α : Type u_1} {cmp : ααOrdering} {β : Type u_2} {k' : α} {k : α} {v : β} [Batteries.TransCmp cmp] (t : Batteries.RBMap α β cmp) (h : cmp k' k Ordering.eq) :
                    (t.insert k v).find? k' = t.find? k'
                    theorem Batteries.RBMap.findEntry?_insert {α : Type u_1} {cmp : ααOrdering} {β : Type u_2} [Batteries.TransCmp cmp] (t : Batteries.RBMap α β cmp) (k : α) (v : β) (k' : α) :
                    (t.insert k v).findEntry? k' = if cmp k' k = Ordering.eq then some (k, v) else t.findEntry? k'
                    theorem Batteries.RBMap.find?_insert {α : Type u_1} {cmp : ααOrdering} {β : Type u_2} [Batteries.TransCmp cmp] (t : Batteries.RBMap α β cmp) (k : α) (v : β) (k' : α) :
                    (t.insert k v).find? k' = if cmp k' k = Ordering.eq then some v else t.find? k'