no goals
α : Type u_1
cmp : α → α → Ordering
t : RBNode α
⊢ Ordered cmp t ↔ List.Pairwise (cmpLT cmp) (toList t)
induction t with
| nil => simp
| node c l v r ihl ihr =>
  simp [*, List.pairwise_append, Ordered, All_def,
    and_assoc, and_left_comm, and_comm, imp_and, forall_and]
  exact fun _ _ hl hr a ha b hb => (hl _ ha).trans (hr _ hb)
no goals
case nil
α : Type u_1
cmp : α → α → Ordering
⊢ Ordered cmp nil ↔ List.Pairwise (cmpLT cmp) (toList nil)
simp
case node
α : Type u_1
cmp : α → α → Ordering
c : RBColor
l : RBNode α
v : α
r : RBNode α
ihl : Ordered cmp l ↔ List.Pairwise (cmpLT cmp) (toList l)
ihr : Ordered cmp r ↔ List.Pairwise (cmpLT cmp) (toList r)
⊢ List.Pairwise (cmpLT cmp) (toList l) →
    List.Pairwise (cmpLT cmp) (toList r) →
      (∀ (x : α), x ∈ l → cmpLT cmp x v) →
        (∀ (x : α), x ∈ r → cmpLT cmp v x) → ∀ (x : α), x ∈ l → ∀ (a : α), a ∈ r → cmpLT cmp x a
case node
α : Type u_1
cmp : α → α → Ordering
c : RBColor
l : RBNode α
v : α
r : RBNode α
ihl : Ordered cmp l ↔ List.Pairwise (cmpLT cmp) (toList l)
ihr : Ordered cmp r ↔ List.Pairwise (cmpLT cmp) (toList r)
⊢ Ordered cmp (node c l v r) ↔ List.Pairwise (cmpLT cmp) (toList (node c l v r))
simp [*, List.pairwise_append, Ordered, All_def,
  and_assoc, and_left_comm, and_comm, imp_and, forall_and]
no goals
case node
α : Type u_1
cmp : α → α → Ordering
c : RBColor
l : RBNode α
v : α
r : RBNode α
ihl : Ordered cmp l ↔ List.Pairwise (cmpLT cmp) (toList l)
ihr : Ordered cmp r ↔ List.Pairwise (cmpLT cmp) (toList r)
⊢ List.Pairwise (cmpLT cmp) (toList l) →
    List.Pairwise (cmpLT cmp) (toList r) →
      (∀ (x : α), x ∈ l → cmpLT cmp x v) →
        (∀ (x : α), x ∈ r → cmpLT cmp v x) → ∀ (x : α), x ∈ l → ∀ (a : α), a ∈ r → cmpLT cmp x a
exact fun _ _ hl hr a ha b hb => (hl _ ha).trans (hr _ hb)