α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ Ordered cmp
    (match r with
    | node red b y c => node red l v (node black b y c)
    | r =>
      match l with
      | node black a x b => balance1 (node red a x b) v r
      | node red a x (node black b y c) => node red (balance1 (setRed a) x b) y (node black c v r)
      | l => node red l v r)
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ Ordered cmp (balRight l v r)
unfold balRight
case h_1
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
lv : All (fun x => cmpLT cmp x v) l
hl : Ordered cmp l
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
vr : All (fun x => cmpLT cmp v x) (node red a✝ x✝ b✝)
hr : Ordered cmp (node red a✝ x✝ b✝)
⊢ Ordered cmp (node red l v (node black a✝ x✝ b✝))

case h_2
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
⊢ Ordered cmp
    (match l with
    | node black a x b => balance1 (node red a x b) v r
    | node red a x (node black b y c) => node red (balance1 (setRed a) x b) y (node black c v r)
    | l => node red l v r)
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ Ordered cmp
    (match r with
    | node red b y c => node red l v (node black b y c)
    | r =>
      match l with
      | node black a x b => balance1 (node red a x b) v r
      | node red a x (node black b y c) => node red (balance1 (setRed a) x b) y (node black c v r)
      | l => node red l v r)
split
case h_2.h_1
α : Type u_1
cmp : α → α → Ordering
v : α
r : RBNode α
vr : All (fun x => cmpLT cmp v x) r
hr : Ordered cmp r
l✝¹ : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node black a✝ x✝ b✝)
hl : Ordered cmp (node black a✝ x✝ b✝)
⊢ Ordered cmp (balance1 (node red a✝ x✝ b✝) v r)

case h_2.h_2
α : Type u_1
cmp : α → α → Ordering
v : α
r : RBNode α
vr : All (fun x => cmpLT cmp v x) r
hr : Ordered cmp r
l✝¹ : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ (node black b✝ y✝ c✝))
hl : Ordered cmp (node red a✝ x✝ (node black b✝ y✝ c✝))
⊢ Ordered cmp (node red (balance1 (setRed a✝) x✝ b✝) y✝ (node black c✝ v r))

case h_2.h_3
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
l✝¹ : RBNode α
x✝² : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
l✝ : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node black a x b → False
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α), l = node red a x (node black b y c) → False
⊢ Ordered cmp (node red l v r)
case h_2
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
⊢ Ordered cmp
    (match l with
    | node black a x b => balance1 (node red a x b) v r
    | node red a x (node black b y c) => node red (balance1 (setRed a) x b) y (node black c v r)
    | l => node red l v r)
split
no goals
case h_1
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
lv : All (fun x => cmpLT cmp x v) l
hl : Ordered cmp l
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
vr : All (fun x => cmpLT cmp v x) (node red a✝ x✝ b✝)
hr : Ordered cmp (node red a✝ x✝ b✝)
⊢ Ordered cmp (node red l v (node black a✝ x✝ b✝))
exact ⟨lv, vr, hl, hr⟩
no goals
case h_2.h_1
α : Type u_1
cmp : α → α → Ordering
v : α
r : RBNode α
vr : All (fun x => cmpLT cmp v x) r
hr : Ordered cmp r
l✝¹ : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node black a✝ x✝ b✝)
hl : Ordered cmp (node black a✝ x✝ b✝)
⊢ Ordered cmp (balance1 (node red a✝ x✝ b✝) v r)
exact hl.balance1 lv vr hr
case h_2.h_2
α : Type u_1
cmp : α → α → Ordering
v : α
r : RBNode α
vr : All (fun x => cmpLT cmp v x) r
hr : Ordered cmp r
l✝¹ : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ (node black b✝ y✝ c✝))
hl : Ordered cmp (node red a✝ x✝ (node black b✝ y✝ c✝))
yv : (fun x => cmpLT cmp x v) y✝
left✝ : All (fun x => cmpLT cmp x v) b✝
cv : All (fun x => cmpLT cmp x v) c✝
⊢ Ordered cmp (node red (balance1 (setRed a✝) x✝ b✝) y✝ (node black c✝ v r))
case h_2.h_2
α : Type u_1
cmp : α → α → Ordering
v : α
r : RBNode α
vr : All (fun x => cmpLT cmp v x) r
hr : Ordered cmp r
l✝¹ : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ (node black b✝ y✝ c✝))
hl : Ordered cmp (node red a✝ x✝ (node black b✝ y✝ c✝))
⊢ Ordered cmp (node red (balance1 (setRed a✝) x✝ b✝) y✝ (node black c✝ v r))
have ⟨yv, _, cv⟩ := lv.2.2
case h_2.h_2
α : Type u_1
cmp : α → α → Ordering
v : α
r : RBNode α
vr : All (fun x => cmpLT cmp v x) r
hr : Ordered cmp r
l✝¹ : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ (node black b✝ y✝ c✝))
hl : Ordered cmp (node red a✝ x✝ (node black b✝ y✝ c✝))
yv : (fun x => cmpLT cmp x v) y✝
left✝ : All (fun x => cmpLT cmp x v) b✝
cv : All (fun x => cmpLT cmp x v) c✝
ax : All (fun x => cmpLT cmp x x✝) a✝
xy : (fun x => cmpLT cmp x✝ x) y✝
xb : All (fun x => cmpLT cmp x✝ x) b✝
right✝ : All (fun x => cmpLT cmp x✝ x) c✝
ha : Ordered cmp a✝
by_ : All (fun x => cmpLT cmp x y✝) b✝
yc : All (fun x => cmpLT cmp y✝ x) c✝
hb : Ordered cmp b✝
hc : Ordered cmp c✝
⊢ Ordered cmp (node red (balance1 (setRed a✝) x✝ b✝) y✝ (node black c✝ v r))
case h_2.h_2
α : Type u_1
cmp : α → α → Ordering
v : α
r : RBNode α
vr : All (fun x => cmpLT cmp v x) r
hr : Ordered cmp r
l✝¹ : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ (node black b✝ y✝ c✝))
hl : Ordered cmp (node red a✝ x✝ (node black b✝ y✝ c✝))
yv : (fun x => cmpLT cmp x v) y✝
left✝ : All (fun x => cmpLT cmp x v) b✝
cv : All (fun x => cmpLT cmp x v) c✝
⊢ Ordered cmp (node red (balance1 (setRed a✝) x✝ b✝) y✝ (node black c✝ v r))
have ⟨ax, ⟨xy, xb, _⟩, ha, by_, yc, hb, hc⟩ := hl
no goals
case h_2.h_2
α : Type u_1
cmp : α → α → Ordering
v : α
r : RBNode α
vr : All (fun x => cmpLT cmp v x) r
hr : Ordered cmp r
l✝¹ : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ (node black b✝ y✝ c✝))
hl : Ordered cmp (node red a✝ x✝ (node black b✝ y✝ c✝))
yv : (fun x => cmpLT cmp x v) y✝
left✝ : All (fun x => cmpLT cmp x v) b✝
cv : All (fun x => cmpLT cmp x v) c✝
ax : All (fun x => cmpLT cmp x x✝) a✝
xy : (fun x => cmpLT cmp x✝ x) y✝
xb : All (fun x => cmpLT cmp x✝ x) b✝
right✝ : All (fun x => cmpLT cmp x✝ x) c✝
ha : Ordered cmp a✝
by_ : All (fun x => cmpLT cmp x y✝) b✝
yc : All (fun x => cmpLT cmp y✝ x) c✝
hb : Ordered cmp b✝
hc : Ordered cmp c✝
⊢ Ordered cmp (node red (balance1 (setRed a✝) x✝ b✝) y✝ (node black c✝ v r))
exact ⟨balance1_All.2 ⟨xy, (xy.trans_r ax).setRed, by_⟩, ⟨yv, yc, yv.trans_l vr⟩,
  (Ordered.setRed.2 ha).balance1 ax.setRed xb hb, cv, vr, hc, hr⟩
no goals
case h_2.h_3
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
r : RBNode α
lv : All (fun x => cmpLT cmp x v) l
vr : All (fun x => cmpLT cmp v x) r
hl : Ordered cmp l
hr : Ordered cmp r
l✝¹ : RBNode α
x✝² : ∀ (a : RBNode α) (x : α) (b : RBNode α), r = node red a x b → False
l✝ : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node black a x b → False
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α), l = node red a x (node black b y c) → False
⊢ Ordered cmp (node red l v r)
exact ⟨lv, vr, hl, hr⟩