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

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

Tactic:
exact hl.balance2 lv vr hr

Result:
no goals

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
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ b✝)
hl : Ordered cmp (node red a✝ x✝ b✝)
⊢ Ordered cmp (node red (node black a✝ x✝ b✝) v r)

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

Result:
no goals

Proof state:
case h_2.h_2
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
lv : All (fun x => cmpLT cmp x v) l
hl : Ordered cmp l
l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
r✝ a✝ : RBNode α
y✝ : α
b✝ : RBNode α
z✝ : α
c✝ : RBNode α
vr : All (fun x => cmpLT cmp v x) (node red (node black a✝ y✝ b✝) z✝ c✝)
hr : Ordered cmp (node red (node black a✝ y✝ b✝) z✝ c✝)
vy : (fun x => cmpLT cmp v x) y✝
va : All (fun x => cmpLT cmp v x) a✝
right✝ : All (fun x => cmpLT cmp v x) b✝
yz : (fun x => cmpLT cmp x z✝) y✝
left✝ : All (fun x => cmpLT cmp x z✝) a✝
bz : All (fun x => cmpLT cmp x z✝) b✝
zc : All (fun x => cmpLT cmp z✝ x) c✝
ay : All (fun x => cmpLT cmp x y✝) a✝
yb : All (fun x => cmpLT cmp y✝ x) b✝
ha : Ordered cmp a✝
hb : Ordered cmp b✝
hc : Ordered cmp c✝
⊢ Ordered cmp (node red (node black l v a✝) y✝ (b✝.balance2 z✝ c✝.setRed))

Tactic:
exact ⟨⟨vy, vy.trans_r lv, ay⟩, balance2_All.2 ⟨yz, yb, (yz.trans_l zc).setRed⟩,
  ⟨lv, va, hl, ha⟩, hb.balance2 bz zc.setRed (Ordered.setRed.2 hc)⟩

Result:
no goals

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

Tactic:
have ⟨⟨yz, _, bz⟩, zc, ⟨ay, yb, ha, hb⟩, hc⟩ := hr

Result:
case h_2.h_2
α : Type u_1
cmp : α → α → Ordering
l : RBNode α
v : α
lv : All (fun x => cmpLT cmp x v) l
hl : Ordered cmp l
l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
r✝ a✝ : RBNode α
y✝ : α
b✝ : RBNode α
z✝ : α
c✝ : RBNode α
vr : All (fun x => cmpLT cmp v x) (node red (node black a✝ y✝ b✝) z✝ c✝)
hr : Ordered cmp (node red (node black a✝ y✝ b✝) z✝ c✝)
vy : (fun x => cmpLT cmp v x) y✝
va : All (fun x => cmpLT cmp v x) a✝
right✝ : All (fun x => cmpLT cmp v x) b✝
yz : (fun x => cmpLT cmp x z✝) y✝
left✝ : All (fun x => cmpLT cmp x z✝) a✝
bz : All (fun x => cmpLT cmp x z✝) b✝
zc : All (fun x => cmpLT cmp z✝ x) c✝
ay : All (fun x => cmpLT cmp x y✝) a✝
yb : All (fun x => cmpLT cmp y✝ x) b✝
ha : Ordered cmp a✝
hb : Ordered cmp b✝
hc : Ordered cmp c✝
⊢ Ordered cmp (node red (node black l v a✝) y✝ (b✝.balance2 z✝ c✝.setRed))

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

Tactic:
exact ⟨lv, vr, hl, 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 with
    | node red a x b => node red (node black a x b) v r
    | l =>
      match r with
      | node black a y b => l.balance2 v (node red a y b)
      | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
      | r => node red l v r)

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
l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
lv : All (fun x => cmpLT cmp x v) (node red a✝ x✝ b✝)
hl : Ordered cmp (node red a✝ x✝ b✝)
⊢ Ordered cmp (node red (node black a✝ x✝ b✝) 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 α), l = node red a x b → False
⊢ Ordered cmp
    (match r with
    | node black a y b => l.balance2 v (node red a y b)
    | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
    | r => node red l v r)

Proof state:
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 α), l = node red a x b → False
⊢ Ordered cmp
    (match r with
    | node black a y b => l.balance2 v (node red a y b)
    | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
    | r => node red l v r)

Tactic:
split

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

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

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