-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem Ordered.del : ∀ {path : Path α} {t : RBNode α} {c},
    t.Ordered cmp → path.Ordered cmp → t.All (path.RootOrdered cmp) → (path.del t c).Ordered cmp
  | .root, _, _, ht, _, _ => Ordered.setBlack.2 ht
  | .left _ parent x b, a, red, ha, ⟨hp, xb, xp, bp, hb⟩, H => by
    unfold Path.del
    have ⟨ax, ap⟩ := All_and.1 H
    exact hp.del ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
  | .right _ a x parent, b, red, hb, ⟨hp, ax, xp, ap, ha⟩, H => by
    unfold Path.del
    have ⟨xb, bp⟩ := All_and.1 H
    exact hp.del ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
  | .left _ parent x b, a, black, ha, ⟨hp, xb, xp, bp, hb⟩, H => by
    unfold Path.del
    have ⟨ax, ap⟩ := All_and.1 H
    exact hp.del (ha.balLeft ax xb hb) (ap.balLeft xp bp)
  | .right _ a x parent, b, black, hb, ⟨hp, ax, xp, ap, ha⟩, H => by
    unfold Path.del
    have ⟨xb, bp⟩ := All_and.1 H
    exact hp.del (ha.balRight ax xb hb) (ap.balRight xp bp)

Proof state:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left c✝ parent x b)) a
⊢ RBNode.Ordered cmp ((left c✝ parent x b).del a black)

Tactic:
unfold Path.del

Result:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left c✝ parent x b)) a
⊢ RBNode.Ordered cmp (parent.del (a.balLeft x b) c✝)

Proof state:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left c✝ parent x b)) a
⊢ RBNode.Ordered cmp ((left c✝ parent x b).del a red)

Tactic:
unfold Path.del

Result:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left c✝ parent x b)) a
⊢ RBNode.Ordered cmp (parent.del (node red a x b) c✝)

Proof state:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left c✝ parent x b)) a
⊢ RBNode.Ordered cmp (parent.del (a.balLeft x b) c✝)

Tactic:
have ⟨ax, ap⟩ := All_and.1 H

Result:
α : Type u_1
cmp : α → α → Ordering
c✝ : RBColor
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left c✝ parent x b)) a
ax : All (fun a => cmpLT cmp a x) a
ap : All (RootOrdered cmp parent) a
⊢ RBNode.Ordered cmp (parent.del (a.balLeft x b) c✝)