-- 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
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))

Tactic:
exact ⟨xy, ⟨yv, yc, yv.trans_l vr⟩, hx, cv, vr, hc, hr⟩

Result:
no goals

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 α
x✝ : ∀ (a_1 : RBNode α) (x : α) (b : RBNode α), a = node red a_1 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))

Tactic:
have ⟨_, _, yv, _, cv⟩ := lv

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 α
x✝ : ∀ (a_1 : RBNode α) (x : α) (b : RBNode α), a = node red a_1 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))
left✝² : (fun x => cmpLT cmp x v) x
left✝¹ : All (fun x => cmpLT cmp x v) a
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 (node black a x b) y (node black c v r))

Proof state:
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))

Tactic:
next a x b y c _ =>
have ⟨_, _, yv, _, cv⟩ := lv; have ⟨ax, ⟨xy, xb, _⟩, ha, by_, yc, hb, hc⟩ := hl
exact ⟨⟨xy, xy.trans_r ax, by_⟩, ⟨yv, yc, yv.trans_l vr⟩, ⟨ax, xb, ha, hb⟩, 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 (l.balance1 v r)

Tactic:
unfold balance1

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, 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)

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 α
x✝ : ∀ (a_1 : RBNode α) (x : α) (b : RBNode α), a = node red a_1 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))
left✝² : (fun x => cmpLT cmp x v) x
left✝¹ : All (fun x => cmpLT cmp x v) a
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_1 => cmpLT cmp x_1 x) a
xy : (fun x_1 => cmpLT cmp x x_1) y
xb : All (fun x_1 => cmpLT cmp x x_1) b
right✝ : All (fun x_1 => cmpLT cmp x x_1) 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 (node black a x b) y (node black c v r))

Tactic:
exact ⟨⟨xy, xy.trans_r ax, by_⟩, ⟨yv, yc, yv.trans_l vr⟩, ⟨ax, xb, ha, hb⟩, cv, vr, hc, hr⟩

Result:
no goals

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 α
x✝ : ∀ (a_1 : RBNode α) (x : α) (b : RBNode α), a = node red a_1 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))
left✝² : (fun x => cmpLT cmp x v) x
left✝¹ : All (fun x => cmpLT cmp x v) a
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 (node black a x b) y (node black c v r))

Tactic:
have ⟨ax, ⟨xy, xb, _⟩, ha, by_, yc, hb, 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 α
x✝ : ∀ (a_1 : RBNode α) (x : α) (b : RBNode α), a = node red a_1 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))
left✝² : (fun x => cmpLT cmp x v) x
left✝¹ : All (fun x => cmpLT cmp x v) a
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_1 => cmpLT cmp x_1 x) a
xy : (fun x_1 => cmpLT cmp x x_1) y
xb : All (fun x_1 => cmpLT cmp x x_1) b
right✝ : All (fun x_1 => cmpLT cmp x x_1) 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 (node black a x b) y (node black c v r))

Proof state:
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)

Tactic:
exact ⟨lv, vr, hl, hr⟩

Result:
no goals

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)
⊢ Ordered cmp (node red (node black a x b) y (node black c v r))

Tactic:
have ⟨yv, _, cv⟩ := lv

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
⊢ Ordered cmp (node red (node black a x b) y (node black c v r))