no goals
α : Type u_1
cmp : α → α → Ordering
v : α
p : Path α
hp : Ordered cmp p
⊢ RootOrdered cmp p v ↔ (∀ (a : α), a ∈ listL p → cmpLT cmp a v) ∧ ∀ (a : α), a ∈ listR p → cmpLT cmp v a
induction p with
  (simp [All_def] at hp; simp [*, and_assoc, and_left_comm, and_comm, or_imp, forall_and])
| left _ _ x _ ih => exact fun vx _ _ _ ha => vx.trans (hp.2.1 _ ha)
| right _ _ x _ ih => exact fun xv _ _ _ ha => (hp.2.1 _ ha).trans xv
case root
α : Type u_1
cmp : α → α → Ordering
v : α
hp : True
⊢ RootOrdered cmp root v ↔ (∀ (a : α), a ∈ listL root → cmpLT cmp a v) ∧ ∀ (a : α), a ∈ listR root → cmpLT cmp v a
case root
α : Type u_1
cmp : α → α → Ordering
v : α
hp : Ordered cmp root
⊢ RootOrdered cmp root v ↔ (∀ (a : α), a ∈ listL root → cmpLT cmp a v) ∧ ∀ (a : α), a ∈ listR root → cmpLT cmp v a
simp [All_def] at hp
no goals
case root
α : Type u_1
cmp : α → α → Ordering
v : α
hp : True
⊢ RootOrdered cmp root v ↔ (∀ (a : α), a ∈ listL root → cmpLT cmp a v) ∧ ∀ (a : α), a ∈ listR root → cmpLT cmp v a
simp [*, and_assoc, and_left_comm, and_comm, or_imp, forall_and]
no goals
case left
α : Type u_1
cmp : α → α → Ordering
v : α
c✝ : RBColor
parent✝ : Path α
x : α
r✝ : RBNode α
ih :
  Ordered cmp parent✝ →
    (RootOrdered cmp parent✝ v ↔
      (∀ (a : α), a ∈ listL parent✝ → cmpLT cmp a v) ∧ ∀ (a : α), a ∈ listR parent✝ → cmpLT cmp v a)
hp :
  Ordered cmp parent✝ ∧
    (∀ (x_1 : α), x_1 ∈ r✝ → cmpLT cmp x x_1) ∧
      RootOrdered cmp parent✝ x ∧ (∀ (x : α), x ∈ r✝ → RootOrdered cmp parent✝ x) ∧ RBNode.Ordered cmp r✝
⊢ cmpLT cmp v x →
    (∀ (a : α), a ∈ listL parent✝ → cmpLT cmp a v) →
      (∀ (a : α), a ∈ listR parent✝ → cmpLT cmp v a) → ∀ (x : α), x ∈ r✝ → cmpLT cmp v x
exact fun vx _ _ _ ha => vx.trans (hp.2.1 _ ha)
no goals
case right
α : Type u_1
cmp : α → α → Ordering
v : α
c✝ : RBColor
l✝ : RBNode α
x : α
parent✝ : Path α
ih :
  Ordered cmp parent✝ →
    (RootOrdered cmp parent✝ v ↔
      (∀ (a : α), a ∈ listL parent✝ → cmpLT cmp a v) ∧ ∀ (a : α), a ∈ listR parent✝ → cmpLT cmp v a)
hp :
  Ordered cmp parent✝ ∧
    (∀ (x_1 : α), x_1 ∈ l✝ → cmpLT cmp x_1 x) ∧
      RootOrdered cmp parent✝ x ∧ (∀ (x : α), x ∈ l✝ → RootOrdered cmp parent✝ x) ∧ RBNode.Ordered cmp l✝
⊢ cmpLT cmp x v →
    (∀ (a : α), a ∈ listL parent✝ → cmpLT cmp a v) →
      (∀ (a : α), a ∈ listR parent✝ → cmpLT cmp v a) → ∀ (x : α), x ∈ l✝ → cmpLT cmp x v
exact fun xv _ _ _ ha => (hp.2.1 _ ha).trans xv