-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem All.del : ∀ {t : RBNode α}, t.All p → (del cut t).All p
  | .nil, h => h
  | .node .., ⟨hy, ha, hb⟩ => by
    unfold del; split
    · split
      · exact ha.del.balLeft hy hb
      · exact ⟨hy, ha.del, hb⟩
    · split
      · exact ha.balRight hy hb.del
      · exact ⟨hy, ha, hb.del⟩
    · exact ha.append hb

Proof state:
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
⊢ All p (del cut (node c✝ a✝² a✝¹ a✝))

Tactic:
unfold del

Result:
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
⊢ All p
    (match cut a✝¹ with
    | Ordering.lt =>
      match a✝².isBlack with
      | black => (del cut a✝²).balLeft a✝¹ a✝
      | red => node red (del cut a✝²) a✝¹ a✝
    | Ordering.gt =>
      match a✝.isBlack with
      | black => a✝².balRight a✝¹ (del cut a✝)
      | red => node red a✝² a✝¹ (del cut a✝)
    | Ordering.eq => a✝².append a✝)

Proof state:
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
⊢ All p
    (match cut a✝¹ with
    | Ordering.lt =>
      match a✝².isBlack with
      | black => (del cut a✝²).balLeft a✝¹ a✝
      | red => node red (del cut a✝²) a✝¹ a✝
    | Ordering.gt =>
      match a✝.isBlack with
      | black => a✝².balRight a✝¹ (del cut a✝)
      | red => node red a✝² a✝¹ (del cut a✝)
    | Ordering.eq => a✝².append a✝)

Tactic:
split

Result:
case h_1
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝ : Ordering
heq✝ : cut a✝¹ = Ordering.lt
⊢ All p
    (match a✝².isBlack with
    | black => (del cut a✝²).balLeft a✝¹ a✝
    | red => node red (del cut a✝²) a✝¹ a✝)

case h_2
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝ : Ordering
heq✝ : cut a✝¹ = Ordering.gt
⊢ All p
    (match a✝.isBlack with
    | black => a✝².balRight a✝¹ (del cut a✝)
    | red => node red a✝² a✝¹ (del cut a✝))

case h_3
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝ : Ordering
heq✝ : cut a✝¹ = Ordering.eq
⊢ All p (a✝².append a✝)

Proof state:
case h_2.h_1
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.gt
x✝ : RBColor
heq✝ : a✝.isBlack = black
⊢ All p (a✝².balRight a✝¹ (del cut a✝))

Tactic:
exact ha.balRight hy hb.del

Result:
no goals

Proof state:
case h_3
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝ : Ordering
heq✝ : cut a✝¹ = Ordering.eq
⊢ All p (a✝².append a✝)

Tactic:
exact ha.append hb

Result:
no goals

Proof state:
case h_1.h_1
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.lt
x✝ : RBColor
heq✝ : a✝².isBlack = black
⊢ All p ((del cut a✝²).balLeft a✝¹ a✝)

Tactic:
exact ha.del.balLeft hy hb

Result:
no goals

Proof state:
case h_1
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝ : Ordering
heq✝ : cut a✝¹ = Ordering.lt
⊢ All p
    (match a✝².isBlack with
    | black => (del cut a✝²).balLeft a✝¹ a✝
    | red => node red (del cut a✝²) a✝¹ a✝)

Tactic:
split

Result:
case h_1.h_1
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.lt
x✝ : RBColor
heq✝ : a✝².isBlack = black
⊢ All p ((del cut a✝²).balLeft a✝¹ a✝)

case h_1.h_2
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.lt
x✝ : RBColor
heq✝ : a✝².isBlack = red
⊢ All p (node red (del cut a✝²) a✝¹ a✝)

Proof state:
case h_1.h_2
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.lt
x✝ : RBColor
heq✝ : a✝².isBlack = red
⊢ All p (node red (del cut a✝²) a✝¹ a✝)

Tactic:
exact ⟨hy, ha.del, hb⟩

Result:
no goals

Proof state:
case h_2
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝ : Ordering
heq✝ : cut a✝¹ = Ordering.gt
⊢ All p
    (match a✝.isBlack with
    | black => a✝².balRight a✝¹ (del cut a✝)
    | red => node red a✝² a✝¹ (del cut a✝))

Tactic:
split

Result:
case h_2.h_1
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.gt
x✝ : RBColor
heq✝ : a✝.isBlack = black
⊢ All p (a✝².balRight a✝¹ (del cut a✝))

case h_2.h_2
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.gt
x✝ : RBColor
heq✝ : a✝.isBlack = red
⊢ All p (node red a✝² a✝¹ (del cut a✝))

Proof state:
case h_2.h_2
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.gt
x✝ : RBColor
heq✝ : a✝.isBlack = red
⊢ All p (node red a✝² a✝¹ (del cut a✝))

Tactic:
exact ⟨hy, ha, hb.del⟩

Result:
no goals