-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Balanced.del {t : RBNode α} (h : t.Balanced c n) :
    (t.del cut).DelProp t.isBlack n

Proof state:
case red
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
n : Nat
b : RBNode α
v✝ : α
ha : a.Balanced black n
hb : b.Balanced black n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
⊢ DelProp (node red a v✝ b).isBlack (del cut (node red a v✝ b)) n

Tactic:
unfold del

Result:
case red
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
n : Nat
b : RBNode α
v✝ : α
ha : a.Balanced black n
hb : b.Balanced black n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
⊢ DelProp (node red a v✝ b).isBlack
    (match cut v✝ with
    | Ordering.lt =>
      match a.isBlack with
      | black => (del cut a).balLeft v✝ b
      | red => node red (del cut a) v✝ b
    | Ordering.gt =>
      match b.isBlack with
      | black => a.balRight v✝ (del cut b)
      | red => node red a v✝ (del cut b)
    | Ordering.eq => a.append b)
    n

Proof state:
case red
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
n : Nat
b : RBNode α
v✝ : α
ha : a.Balanced black n
hb : b.Balanced black n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
⊢ DelProp (node red a v✝ b).isBlack
    (match cut v✝ with
    | Ordering.lt =>
      match a.isBlack with
      | black => (del cut a).balLeft v✝ b
      | red => node red (del cut a) v✝ b
    | Ordering.gt =>
      match b.isBlack with
      | black => a.balRight v✝ (del cut b)
      | red => node red a v✝ (del cut b)
    | Ordering.eq => a.append b)
    n

Tactic:
split

Result:
case red.h_1
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
n : Nat
b : RBNode α
v✝ : α
ha : a.Balanced black n
hb : b.Balanced black n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ DelProp (node red a v✝ b).isBlack
    (match a.isBlack with
    | black => (del cut a).balLeft v✝ b
    | red => node red (del cut a) v✝ b)
    n

case red.h_2
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
n : Nat
b : RBNode α
v✝ : α
ha : a.Balanced black n
hb : b.Balanced black n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ DelProp (node red a v✝ b).isBlack
    (match b.isBlack with
    | black => a.balRight v✝ (del cut b)
    | red => node red a v✝ (del cut b))
    n

case red.h_3
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
n : Nat
b : RBNode α
v✝ : α
ha : a.Balanced black n
hb : b.Balanced black n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ DelProp (node red a v✝ b).isBlack (a.append b) n

Proof state:
case black.h_1
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
c₁✝ : RBColor
n : Nat
b : RBNode α
c₂✝ : RBColor
v✝ : α
ha : a.Balanced c₁✝ n
hb : b.Balanced c₂✝ n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ RedRed True
    (match a.isBlack with
    | black => (del cut a).balLeft v✝ b
    | red => node red (del cut a) v✝ b)
    n

Tactic:
exact match a, n, iha with
| .nil, _, ⟨c, ha⟩ | .node red .., _, ⟨c, ha⟩ => .redred ⟨⟩ ha hb
| .node black .., _, ⟨n, rfl, ha⟩ => (hb.balLeft ha).imp fun _ => ⟨⟩

Result:
no goals

Proof state:
case black
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
c₁✝ : RBColor
n : Nat
b : RBNode α
c₂✝ : RBColor
v✝ : α
ha : a.Balanced c₁✝ n
hb : b.Balanced c₂✝ n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
⊢ DelProp (node black a v✝ b).isBlack (del cut (node black a v✝ b)) (n + 1)

Tactic:
refine ⟨_, rfl, ?_⟩

Result:
case black
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
c₁✝ : RBColor
n : Nat
b : RBNode α
c₂✝ : RBColor
v✝ : α
ha : a.Balanced c₁✝ n
hb : b.Balanced c₂✝ n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
⊢ RedRed True (del cut (node black a v✝ b)) n

Proof state:
case black.h_2
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
c₁✝ : RBColor
n : Nat
b : RBNode α
c₂✝ : RBColor
v✝ : α
ha : a.Balanced c₁✝ n
hb : b.Balanced c₂✝ n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ RedRed True
    (match b.isBlack with
    | black => a.balRight v✝ (del cut b)
    | red => node red a v✝ (del cut b))
    n

Tactic:
exact match b, n, ihb with
| .nil, _, ⟨c, hb⟩ | .node .red .., _, ⟨c, hb⟩ => .redred ⟨⟩ ha hb
| .node black .., _, ⟨n, rfl, hb⟩ => (ha.balRight hb).imp fun _ => ⟨⟩

Result:
no goals

Proof state:
case black.h_3
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
c₁✝ : RBColor
n : Nat
b : RBNode α
c₂✝ : RBColor
v✝ : α
ha : a.Balanced c₁✝ n
hb : b.Balanced c₂✝ n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ RedRed True (a.append b) n

Tactic:
exact (ha.append hb).imp fun _ => ⟨⟩

Result:
no goals

Proof state:
case red.h_2
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
n : Nat
b : RBNode α
v✝ : α
ha : a.Balanced black n
hb : b.Balanced black n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ DelProp (node red a v✝ b).isBlack
    (match b.isBlack with
    | black => a.balRight v✝ (del cut b)
    | red => node red a v✝ (del cut b))
    n

Tactic:
exact match b, n, ihb with
| .nil, _, _ => ⟨_, .red ha hb⟩
| .node black .., _, ⟨n, rfl, hb⟩ => (ha.balRight hb).of_false nofun

Result:
no goals

Proof state:
case black
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
c₁✝ : RBColor
n : Nat
b : RBNode α
c₂✝ : RBColor
v✝ : α
ha : a.Balanced c₁✝ n
hb : b.Balanced c₂✝ n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
⊢ RedRed True
    (match cut v✝ with
    | Ordering.lt =>
      match a.isBlack with
      | black => (del cut a).balLeft v✝ b
      | red => node red (del cut a) v✝ b
    | Ordering.gt =>
      match b.isBlack with
      | black => a.balRight v✝ (del cut b)
      | red => node red a v✝ (del cut b)
    | Ordering.eq => a.append b)
    n

Tactic:
split

Result:
case black.h_1
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
c₁✝ : RBColor
n : Nat
b : RBNode α
c₂✝ : RBColor
v✝ : α
ha : a.Balanced c₁✝ n
hb : b.Balanced c₂✝ n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ RedRed True
    (match a.isBlack with
    | black => (del cut a).balLeft v✝ b
    | red => node red (del cut a) v✝ b)
    n

case black.h_2
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
c₁✝ : RBColor
n : Nat
b : RBNode α
c₂✝ : RBColor
v✝ : α
ha : a.Balanced c₁✝ n
hb : b.Balanced c₂✝ n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ RedRed True
    (match b.isBlack with
    | black => a.balRight v✝ (del cut b)
    | red => node red a v✝ (del cut b))
    n

case black.h_3
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
c₁✝ : RBColor
n : Nat
b : RBNode α
c₂✝ : RBColor
v✝ : α
ha : a.Balanced c₁✝ n
hb : b.Balanced c₂✝ n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ RedRed True (a.append b) n