-- 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:
α : 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✝
this :
  Ordered cmp (b✝¹.append c✝) ∧
    All (fun x => cmpLT cmp x✝¹ x) (b✝¹.append c✝) ∧ All (fun x => cmpLT cmp x y✝) (b✝¹.append c✝)
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
H : b✝¹.append c✝ = node red a✝ x✝ b✝
b'z : All (fun x => cmpLT cmp x x✝) a✝
c'z : All (fun x => cmpLT cmp x✝ x) b✝
hb' : Ordered cmp a✝
hc' : Ordered cmp b✝
xz : (fun x => cmpLT cmp x✝¹ x) x✝
xb' : All (fun x => cmpLT cmp x✝¹ x) a✝
right✝ : All (fun x => cmpLT cmp x✝¹ x) b✝
zy : (fun x => cmpLT cmp x y✝) x✝
left✝ : All (fun x => cmpLT cmp x y✝) a✝
c'y : All (fun x => cmpLT cmp x y✝) b✝
az : All (fun x => cmpLT cmp x x✝) a✝¹
⊢ Ordered cmp (node red (node red a✝¹ x✝¹ a✝) x✝ (node red b✝ y✝ d✝))

Tactic:
have zd := zy.trans_l yd

Result:
α : 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✝
this :
  Ordered cmp (b✝¹.append c✝) ∧
    All (fun x => cmpLT cmp x✝¹ x) (b✝¹.append c✝) ∧ All (fun x => cmpLT cmp x y✝) (b✝¹.append c✝)
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
H : b✝¹.append c✝ = node red a✝ x✝ b✝
b'z : All (fun x => cmpLT cmp x x✝) a✝
c'z : All (fun x => cmpLT cmp x✝ x) b✝
hb' : Ordered cmp a✝
hc' : Ordered cmp b✝
xz : (fun x => cmpLT cmp x✝¹ x) x✝
xb' : All (fun x => cmpLT cmp x✝¹ x) a✝
right✝ : All (fun x => cmpLT cmp x✝¹ x) b✝
zy : (fun x => cmpLT cmp x y✝) x✝
left✝ : All (fun x => cmpLT cmp x y✝) a✝
c'y : All (fun x => cmpLT cmp x y✝) b✝
az : All (fun x => cmpLT cmp x x✝) a✝¹
zd : All (fun x => cmpLT cmp x✝ x) d✝
⊢ Ordered cmp (node red (node red a✝¹ x✝¹ a✝) x✝ (node red b✝ y✝ d✝))

Proof state:
α : 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 (l.append r)

Tactic:
unfold append

Result:
α : 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 l, r with
    | nil, x => x
    | x, nil => x
    | node red a x b, node red c y d =>
      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)
    | node black a x b, node black c y d =>
      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)
    | a@h:(node black l v r), node red b x c => node red (a.append b) x c
    | node red a x b, c@h:(node black l v r) => node red a x (b.append c))

Proof state:
α : 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✝
this :
  Ordered cmp (b✝¹.append c✝) ∧
    All (fun x => cmpLT cmp x✝¹ x) (b✝¹.append c✝) ∧ All (fun x => cmpLT cmp x y✝) (b✝¹.append c✝)
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
H : b✝¹.append c✝ = node red a✝ x✝ b✝
b'z : All (fun x => cmpLT cmp x x✝) a✝
c'z : All (fun x => cmpLT cmp x✝ x) b✝
hb' : Ordered cmp a✝
hc' : Ordered cmp b✝
xz : (fun x => cmpLT cmp x✝¹ x) x✝
xb' : All (fun x => cmpLT cmp x✝¹ x) a✝
right✝ : All (fun x => cmpLT cmp x✝¹ x) b✝
zy : (fun x => cmpLT cmp x y✝) x✝
left✝ : All (fun x => cmpLT cmp x y✝) a✝
c'y : All (fun x => cmpLT cmp x y✝) b✝
⊢ Ordered cmp (node red (node red a✝¹ x✝¹ a✝) x✝ (node red b✝ y✝ d✝))

Tactic:
have az := xz.trans_r ax

Result:
α : 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✝
this :
  Ordered cmp (b✝¹.append c✝) ∧
    All (fun x => cmpLT cmp x✝¹ x) (b✝¹.append c✝) ∧ All (fun x => cmpLT cmp x y✝) (b✝¹.append c✝)
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
H : b✝¹.append c✝ = node red a✝ x✝ b✝
b'z : All (fun x => cmpLT cmp x x✝) a✝
c'z : All (fun x => cmpLT cmp x✝ x) b✝
hb' : Ordered cmp a✝
hc' : Ordered cmp b✝
xz : (fun x => cmpLT cmp x✝¹ x) x✝
xb' : All (fun x => cmpLT cmp x✝¹ x) a✝
right✝ : All (fun x => cmpLT cmp x✝¹ x) b✝
zy : (fun x => cmpLT cmp x y✝) x✝
left✝ : All (fun x => cmpLT cmp x y✝) a✝
c'y : All (fun x => cmpLT cmp x y✝) b✝
az : All (fun x => cmpLT cmp x x✝) a✝¹
⊢ Ordered cmp (node red (node red a✝¹ x✝¹ a✝) x✝ (node red b✝ y✝ d✝))

Proof state:
case h_2
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
lv : All (fun x => cmpLT cmp x v) l
hl : Ordered cmp l
x✝² x✝¹ : RBNode α
x✝ : l = nil → False
vr : All (fun x => cmpLT cmp v x) nil
hr : Ordered cmp nil
⊢ Ordered cmp l

Tactic:
exact hl

Result:
no goals