-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Ordered.del : ∀ {t : RBNode α}, t.Ordered cmp → (del cut t).Ordered cmp
  | .nil, _ => ⟨⟩
  | .node _ a y b, ⟨ay, yb, ha, hb⟩ => by
    unfold del; split
    · split
      · exact ha.del.balLeft ay.del yb hb
      · exact ⟨ay.del, yb, ha.del, hb⟩
    · split
      · exact ha.balRight ay yb.del hb.del
      · exact ⟨ay, yb.del, ha, hb.del⟩
    · exact ha.append ay yb hb

Proof state:
case h_2.h_2
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝¹ : Ordering
heq✝¹ : cut y = Ordering.gt
x✝ : RBColor
heq✝ : b.isBlack = red
⊢ Ordered cmp (node red a y (del cut b))

Tactic:
exact ⟨ay, yb.del, ha, hb.del⟩

Result:
no goals

Proof state:
case h_2
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝ : Ordering
heq✝ : cut y = Ordering.gt
⊢ Ordered cmp
    (match b.isBlack with
    | black => a.balRight y (del cut b)
    | red => node red a y (del cut b))

Tactic:
split

Result:
case h_2.h_1
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝¹ : Ordering
heq✝¹ : cut y = Ordering.gt
x✝ : RBColor
heq✝ : b.isBlack = black
⊢ Ordered cmp (a.balRight y (del cut b))

case h_2.h_2
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝¹ : Ordering
heq✝¹ : cut y = Ordering.gt
x✝ : RBColor
heq✝ : b.isBlack = red
⊢ Ordered cmp (node red a y (del cut b))

Proof state:
case h_1
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝ : Ordering
heq✝ : cut y = Ordering.lt
⊢ Ordered cmp
    (match a.isBlack with
    | black => (del cut a).balLeft y b
    | red => node red (del cut a) y b)

Tactic:
split

Result:
case h_1.h_1
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝¹ : Ordering
heq✝¹ : cut y = Ordering.lt
x✝ : RBColor
heq✝ : a.isBlack = black
⊢ Ordered cmp ((del cut a).balLeft y b)

case h_1.h_2
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝¹ : Ordering
heq✝¹ : cut y = Ordering.lt
x✝ : RBColor
heq✝ : a.isBlack = red
⊢ Ordered cmp (node red (del cut a) y b)

Proof state:
case h_3
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝ : Ordering
heq✝ : cut y = Ordering.eq
⊢ Ordered cmp (a.append b)

Tactic:
exact ha.append ay yb hb

Result:
no goals

Proof state:
case h_2.h_1
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝¹ : Ordering
heq✝¹ : cut y = Ordering.gt
x✝ : RBColor
heq✝ : b.isBlack = black
⊢ Ordered cmp (a.balRight y (del cut b))

Tactic:
exact ha.balRight ay yb.del hb.del

Result:
no goals

Proof state:
case h_1.h_2
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝¹ : Ordering
heq✝¹ : cut y = Ordering.lt
x✝ : RBColor
heq✝ : a.isBlack = red
⊢ Ordered cmp (node red (del cut a) y b)

Tactic:
exact ⟨ay.del, yb, ha.del, hb⟩

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
⊢ Ordered cmp
    (match cut y with
    | Ordering.lt =>
      match a.isBlack with
      | black => (del cut a).balLeft y b
      | red => node red (del cut a) y b
    | Ordering.gt =>
      match b.isBlack with
      | black => a.balRight y (del cut b)
      | red => node red a y (del cut b)
    | Ordering.eq => a.append b)

Tactic:
split

Result:
case h_1
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝ : Ordering
heq✝ : cut y = Ordering.lt
⊢ Ordered cmp
    (match a.isBlack with
    | black => (del cut a).balLeft y b
    | red => node red (del cut a) y b)

case h_2
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝ : Ordering
heq✝ : cut y = Ordering.gt
⊢ Ordered cmp
    (match b.isBlack with
    | black => a.balRight y (del cut b)
    | red => node red a y (del cut b))

case h_3
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝ : Ordering
heq✝ : cut y = Ordering.eq
⊢ Ordered cmp (a.append b)

Proof state:
case h_1.h_1
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
x✝¹ : Ordering
heq✝¹ : cut y = Ordering.lt
x✝ : RBColor
heq✝ : a.isBlack = black
⊢ Ordered cmp ((del cut a).balLeft y b)

Tactic:
exact ha.del.balLeft ay.del yb hb

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
⊢ Ordered cmp (del cut (node c✝ a y b))

Tactic:
unfold del

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
c✝ : RBColor
a : RBNode α
y : α
b : RBNode α
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
⊢ Ordered cmp
    (match cut y with
    | Ordering.lt =>
      match a.isBlack with
      | black => (del cut a).balLeft y b
      | red => node red (del cut a) y b
    | Ordering.gt =>
      match b.isBlack with
      | black => a.balRight y (del cut b)
      | red => node red a y (del cut b)
    | Ordering.eq => a.append b)