-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Ordered.append {l : RBNode α} {v : α} {r : RBNode α}
    (lv : l.All (cmpLT cmp · v)) (vr : r.All (cmpLT cmp v ·))
    (hl : l.Ordered cmp) (hr : r.Ordered cmp) : (append l r).Ordered cmp

Proof state:
case h_3
α : Type u_1
cmp : α → α → Ordering
v : α
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b✝ c✝ : RBNode α
y✝ : α
d✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ b✝)
hl : Ordered cmp (node red a✝ x✝ b✝)
vr : All (fun x => cmpLT cmp v x) (node red c✝ y✝ d✝)
hr : Ordered cmp (node red c✝ y✝ d✝)
xv : (fun x => cmpLT cmp x v) x✝
left✝ : All (fun x => cmpLT cmp x v) a✝
bv : All (fun x => cmpLT cmp x v) b✝
⊢ Ordered cmp
    (match b✝.append c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))

Tactic:
have ⟨ax, xb, ha, hb⟩ := hl

Result:
case h_3
α : Type u_1
cmp : α → α → Ordering
v : α
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b✝ c✝ : RBNode α
y✝ : α
d✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ b✝)
hl : Ordered cmp (node red a✝ x✝ b✝)
vr : All (fun x => cmpLT cmp v x) (node red c✝ y✝ d✝)
hr : Ordered cmp (node red c✝ y✝ d✝)
xv : (fun x => cmpLT cmp x v) x✝
left✝ : All (fun x => cmpLT cmp x v) a✝
bv : All (fun x => cmpLT cmp x v) b✝
ax : All (fun x => cmpLT cmp x x✝) a✝
xb : All (fun x => cmpLT cmp x✝ x) b✝
ha : Ordered cmp a✝
hb : Ordered cmp b✝
⊢ Ordered cmp
    (match b✝.append c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))

Proof state:
case h_6
α : Type u_1
cmp : α → α → Ordering
v : α
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b✝ l✝ : RBNode α
v✝ : α
r✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ b✝)
hl : Ordered cmp (node red a✝ x✝ b✝)
vr : All (fun x => cmpLT cmp v x) (node black l✝ v✝ r✝)
hr : Ordered cmp (node black l✝ v✝ r✝)
xv : (fun x => cmpLT cmp x v) x✝
left✝ : All (fun x => cmpLT cmp x v) a✝
bv : All (fun x => cmpLT cmp x v) b✝
⊢ Ordered cmp (node red a✝ x✝ (b✝.append (node black l✝ v✝ r✝)))

Tactic:
have ⟨ax, xb, ha, hb⟩ := hl

Result:
case h_6
α : Type u_1
cmp : α → α → Ordering
v : α
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b✝ l✝ : RBNode α
v✝ : α
r✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ b✝)
hl : Ordered cmp (node red a✝ x✝ b✝)
vr : All (fun x => cmpLT cmp v x) (node black l✝ v✝ r✝)
hr : Ordered cmp (node black l✝ v✝ r✝)
xv : (fun x => cmpLT cmp x v) x✝
left✝ : All (fun x => cmpLT cmp x v) a✝
bv : All (fun x => cmpLT cmp x v) b✝
ax : All (fun x => cmpLT cmp x x✝) a✝
xb : All (fun x => cmpLT cmp x✝ x) b✝
ha : Ordered cmp a✝
hb : Ordered cmp b✝
⊢ Ordered cmp (node red a✝ x✝ (b✝.append (node black l✝ v✝ r✝)))

Proof state:
case h_3
α : Type u_1
cmp : α → α → Ordering
v : α
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b✝ c✝ : RBNode α
y✝ : α
d✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ b✝)
hl : Ordered cmp (node red a✝ x✝ b✝)
vr : All (fun x => cmpLT cmp v x) (node red c✝ y✝ d✝)
hr : Ordered cmp (node red c✝ y✝ d✝)
xv : (fun x => cmpLT cmp x v) x✝
left✝ : All (fun x => cmpLT cmp x v) a✝
bv : All (fun x => cmpLT cmp x v) b✝
ax : All (fun x => cmpLT cmp x x✝) a✝
xb : All (fun x => cmpLT cmp x✝ x) b✝
ha : Ordered cmp a✝
hb : Ordered cmp b✝
vy : (fun x => cmpLT cmp v x) y✝
vc : All (fun x => cmpLT cmp v x) c✝
right✝ : All (fun x => cmpLT cmp v x) d✝
⊢ Ordered cmp
    (match b✝.append c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))

Tactic:
have ⟨cy, yd, hc, hd⟩ := hr

Result:
case h_3
α : Type u_1
cmp : α → α → Ordering
v : α
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b✝ c✝ : RBNode α
y✝ : α
d✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ b✝)
hl : Ordered cmp (node red a✝ x✝ b✝)
vr : All (fun x => cmpLT cmp v x) (node red c✝ y✝ d✝)
hr : Ordered cmp (node red c✝ y✝ d✝)
xv : (fun x => cmpLT cmp x v) x✝
left✝ : All (fun x => cmpLT cmp x v) a✝
bv : All (fun x => cmpLT cmp x v) b✝
ax : All (fun x => cmpLT cmp x x✝) a✝
xb : All (fun x => cmpLT cmp x✝ x) b✝
ha : Ordered cmp a✝
hb : Ordered cmp b✝
vy : (fun x => cmpLT cmp v x) y✝
vc : All (fun x => cmpLT cmp v x) c✝
right✝ : All (fun x => cmpLT cmp v x) d✝
cy : All (fun x => cmpLT cmp x y✝) c✝
yd : All (fun x => cmpLT cmp y✝ x) d✝
hc : Ordered cmp c✝
hd : Ordered cmp d✝
⊢ Ordered cmp
    (match b✝.append c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))

Proof state:
case h_4
α : Type u_1
cmp : α → α → Ordering
v : α
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b✝ c✝ : RBNode α
y✝ : α
d✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node black a✝ x✝ b✝)
hl : Ordered cmp (node black a✝ x✝ b✝)
vr : All (fun x => cmpLT cmp v x) (node black c✝ y✝ d✝)
hr : Ordered cmp (node black c✝ y✝ d✝)
⊢ Ordered cmp
    (match b✝.append c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => a✝.balLeft x✝ (node black bc y✝ d✝))

Tactic:
have ⟨xv, _, bv⟩ := lv

Result:
case h_4
α : Type u_1
cmp : α → α → Ordering
v : α
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b✝ c✝ : RBNode α
y✝ : α
d✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node black a✝ x✝ b✝)
hl : Ordered cmp (node black a✝ x✝ b✝)
vr : All (fun x => cmpLT cmp v x) (node black c✝ y✝ d✝)
hr : Ordered cmp (node black c✝ y✝ d✝)
xv : (fun x => cmpLT cmp x v) x✝
left✝ : All (fun x => cmpLT cmp x v) a✝
bv : All (fun x => cmpLT cmp x v) b✝
⊢ Ordered cmp
    (match b✝.append c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => a✝.balLeft x✝ (node black bc y✝ d✝))

Proof state:
case h_4
α : Type u_1
cmp : α → α → Ordering
v : α
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b✝ c✝ : RBNode α
y✝ : α
d✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node black a✝ x✝ b✝)
hl : Ordered cmp (node black a✝ x✝ b✝)
vr : All (fun x => cmpLT cmp v x) (node black c✝ y✝ d✝)
hr : Ordered cmp (node black c✝ y✝ d✝)
xv : (fun x => cmpLT cmp x v) x✝
left✝ : All (fun x => cmpLT cmp x v) a✝
bv : All (fun x => cmpLT cmp x v) b✝
ax : All (fun x => cmpLT cmp x x✝) a✝
xb : All (fun x => cmpLT cmp x✝ x) b✝
ha : Ordered cmp a✝
hb : Ordered cmp b✝
vy : (fun x => cmpLT cmp v x) y✝
vc : All (fun x => cmpLT cmp v x) c✝
right✝ : All (fun x => cmpLT cmp v x) d✝
⊢ Ordered cmp
    (match b✝.append c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => a✝.balLeft x✝ (node black bc y✝ d✝))

Tactic:
have ⟨cy, yd, hc, hd⟩ := hr

Result:
case h_4
α : Type u_1
cmp : α → α → Ordering
v : α
x✝² x✝¹ a✝ : RBNode α
x✝ : α
b✝ c✝ : RBNode α
y✝ : α
d✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node black a✝ x✝ b✝)
hl : Ordered cmp (node black a✝ x✝ b✝)
vr : All (fun x => cmpLT cmp v x) (node black c✝ y✝ d✝)
hr : Ordered cmp (node black c✝ y✝ d✝)
xv : (fun x => cmpLT cmp x v) x✝
left✝ : All (fun x => cmpLT cmp x v) a✝
bv : All (fun x => cmpLT cmp x v) b✝
ax : All (fun x => cmpLT cmp x x✝) a✝
xb : All (fun x => cmpLT cmp x✝ x) b✝
ha : Ordered cmp a✝
hb : Ordered cmp b✝
vy : (fun x => cmpLT cmp v x) y✝
vc : All (fun x => cmpLT cmp v x) c✝
right✝ : All (fun x => cmpLT cmp v x) d✝
cy : All (fun x => cmpLT cmp x y✝) c✝
yd : All (fun x => cmpLT cmp y✝ x) d✝
hc : Ordered cmp c✝
hd : Ordered cmp d✝
⊢ Ordered cmp
    (match b✝.append c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => a✝.balLeft x✝ (node black bc y✝ d✝))