-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Ordered.balance1 {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) : (balance1 l v r).Ordered cmp

Proof state:
α : Type u_1
cmp : α → α → Ordering
v : α
r : RBNode α
vr : All (fun x => cmpLT cmp v x) r
hr : Ordered cmp r
x✝² : RBNode α
x✝¹ : α
x✝ a : RBNode α
x : α
b : RBNode α
y : α
c : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red (node red a x b) y c)
hl : Ordered cmp (node red (node red a x b) y c)
yv : (fun x => cmpLT cmp x v) y
left✝ : All (fun x => cmpLT cmp x v) (node red a x b)
cv : All (fun x => cmpLT cmp x v) c
⊢ Ordered cmp (node red (node black a x b) y (node black c v r))

Tactic:
have ⟨xy, yc, hx, hc⟩ := hl

Result:
α : Type u_1
cmp : α → α → Ordering
v : α
r : RBNode α
vr : All (fun x => cmpLT cmp v x) r
hr : Ordered cmp r
x✝² : RBNode α
x✝¹ : α
x✝ a : RBNode α
x : α
b : RBNode α
y : α
c : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red (node red a x b) y c)
hl : Ordered cmp (node red (node red a x b) y c)
yv : (fun x => cmpLT cmp x v) y
left✝ : All (fun x => cmpLT cmp x v) (node red a x b)
cv : All (fun x => cmpLT cmp x v) c
xy : All (fun x => cmpLT cmp x y) (node red a x b)
yc : All (fun x => cmpLT cmp y x) c
hx : Ordered cmp (node red a x b)
hc : Ordered cmp c
⊢ Ordered cmp (node red (node black a x b) y (node black c v r))

Proof state:
case h_1
α : Type u_1
cmp : α → α → Ordering
v : α
r : RBNode α
vr : All (fun x => cmpLT cmp v x) r
hr : Ordered cmp r
x✝³ : RBNode α
x✝² : α
x✝¹ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red (node red a✝ x✝ b✝) y✝ c✝)
hl : Ordered cmp (node red (node red a✝ x✝ b✝) y✝ c✝)
⊢ Ordered cmp (node red (node black a✝ x✝ b✝) y✝ (node black c✝ v r))

Tactic:
next a x b y c =>
have ⟨yv, _, cv⟩ := lv; have ⟨xy, yc, hx, hc⟩ := hl
exact ⟨xy, ⟨yv, yc, yv.trans_l vr⟩, hx, cv, vr, hc, hr⟩

Result:
no goals

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
    (match l, v, r with
    | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d)
    | node red a x (node red b y c), z, d => node red (node black a x b) y (node black c z d)
    | a, x, b => node black a x b)

Tactic:
split

Result:
case h_1
α : Type u_1
cmp : α → α → Ordering
v : α
r : RBNode α
vr : All (fun x => cmpLT cmp v x) r
hr : Ordered cmp r
x✝³ : RBNode α
x✝² : α
x✝¹ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red (node red a✝ x✝ b✝) y✝ c✝)
hl : Ordered cmp (node red (node red a✝ x✝ b✝) y✝ c✝)
⊢ Ordered cmp (node red (node black a✝ x✝ b✝) y✝ (node black c✝ v r))

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

case 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
x✝⁴ : RBNode α
x✝³ : α
x✝² : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α), l = node red (node red a x b) y c → False
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α), l = node red a x (node red b y c) → False
⊢ Ordered cmp (node black l v r)