-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem zoom_del {t : RBNode α} :
    t.zoom cut path = (t', path') →
    path.del (t.del cut) (match t with | node c .. => c | _ => red) =
    path'.del t'.delRoot (match t' with | node c .. => c | _ => red)

Proof state:
case h_1
α : Type u_1
cut : α → Ordering
path : Path α
t' : RBNode α
path' : Path α
x✝¹ : RBNode α
c : RBColor
a : RBNode α
y : α
b : RBNode α
x✝ : Ordering
heq✝ : cut y = Ordering.lt
IH :
  ∀ (cut : α → Ordering) (path : Path α) (t' : RBNode α) (path' : Path α),
    zoom cut a path = (t', path') →
      path.del (RBNode.del cut a)
          (match a with
          | node c l v r => c
          | x => red) =
        path'.del t'.delRoot
          (match t' with
          | node c l v r => c
          | x => red)
⊢ zoom cut a (left c path y b) = (t', path') →
    path.del
        (match a.isBlack with
        | black => (RBNode.del cut a).balLeft y b
        | red => node red (RBNode.del cut a) y b)
        c =
      path'.del t'.delRoot
        (match t' with
        | node c l v r => c
        | x => red)

Tactic:
match a with
| nil => intro | rfl => rfl
| node black .. | node red .. => apply IH

Result:
no goals

Proof state:
α : Type u_1
cut : α → Ordering
path : Path α
t' : RBNode α
path' : Path α
x✝¹ : RBNode α
c : RBColor
a : RBNode α
y : α
b : RBNode α
x✝ : Ordering
heq✝ : cut y = Ordering.gt
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
IH :
  ∀ (cut : α → Ordering) (path : Path α) (t' : RBNode α) (path' : Path α),
    zoom cut (node red l✝ v✝ r✝) path = (t', path') →
      path.del (RBNode.del cut (node red l✝ v✝ r✝))
          (match node red l✝ v✝ r✝ with
          | node c l v r => c
          | x => red) =
        path'.del t'.delRoot
          (match t' with
          | node c l v r => c
          | x => red)
⊢ zoom cut (node red l✝ v✝ r✝) (right c a y path) = (t', path') →
    path.del
        (match (node red l✝ v✝ r✝).isBlack with
        | black => a.balRight y (RBNode.del cut (node red l✝ v✝ r✝))
        | red => node red a y (RBNode.del cut (node red l✝ v✝ r✝)))
        c =
      path'.del t'.delRoot
        (match t' with
        | node c l v r => c
        | x => red)

Tactic:
apply IH

Result:
no goals

Proof state:
case h_2
α : Type u_1
cut : α → Ordering
path : Path α
t' : RBNode α
path' : Path α
x✝¹ : RBNode α
c : RBColor
a : RBNode α
y : α
b : RBNode α
x✝ : Ordering
heq✝ : cut y = Ordering.gt
⊢ zoom cut b (right c a y path) = (t', path') →
    path.del
        (match b.isBlack with
        | black => a.balRight y (RBNode.del cut b)
        | red => node red a y (RBNode.del cut b))
        c =
      path'.del t'.delRoot
        (match t' with
        | node c l v r => c
        | x => red)

Tactic:
have IH := @zoom_del (t := b)

Result:
case h_2
α : Type u_1
cut : α → Ordering
path : Path α
t' : RBNode α
path' : Path α
x✝¹ : RBNode α
c : RBColor
a : RBNode α
y : α
b : RBNode α
x✝ : Ordering
heq✝ : cut y = Ordering.gt
IH :
  ∀ (cut : α → Ordering) (path : Path α) (t' : RBNode α) (path' : Path α),
    zoom cut b path = (t', path') →
      path.del (RBNode.del cut b)
          (match b with
          | node c l v r => c
          | x => red) =
        path'.del t'.delRoot
          (match t' with
          | node c l v r => c
          | x => red)
⊢ zoom cut b (right c a y path) = (t', path') →
    path.del
        (match b.isBlack with
        | black => a.balRight y (RBNode.del cut b)
        | red => node red a y (RBNode.del cut b))
        c =
      path'.del t'.delRoot
        (match t' with
        | node c l v r => c
        | x => red)

Proof state:
α : Type u_1
cut : α → Ordering
path : Path α
t' : RBNode α
path' : Path α
x✝¹ : RBNode α
c : RBColor
a : RBNode α
y : α
b : RBNode α
x✝ : Ordering
heq✝ : cut y = Ordering.lt
IH :
  ∀ (cut : α → Ordering) (path : Path α) (t' : RBNode α) (path' : Path α),
    zoom cut nil path = (t', path') →
      path.del (RBNode.del cut nil)
          (match nil with
          | node c l v r => c
          | x => red) =
        path'.del t'.delRoot
          (match t' with
          | node c l v r => c
          | x => red)
⊢ zoom cut nil (left c path y b) = (t', path') →
    path.del
        (match nil.isBlack with
        | black => (RBNode.del cut nil).balLeft y b
        | red => node red (RBNode.del cut nil) y b)
        c =
      path'.del t'.delRoot
        (match t' with
        | node c l v r => c
        | x => red)

Tactic:
intro | rfl => rfl

Result:
no goals

Proof state:
α : Type u_1
cut : α → Ordering
path : Path α
t' : RBNode α
path' : Path α
x✝² : RBNode α
x✝¹ : nil = t'
x✝ : path = path'
⊢ path.del nil red =
    path.del nil.delRoot
      (match nil with
      | node c l v r => c
      | x => red)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
cut : α → Ordering
path : Path α
t' : RBNode α
path' : Path α
x✝² : RBNode α
c : RBColor
a : RBNode α
y : α
b : RBNode α
x✝¹ : Ordering
heq✝ : cut y = Ordering.lt
IH :
  ∀ (cut : α → Ordering) (path : Path α) (t' : RBNode α) (path' : Path α),
    zoom cut nil path = (t', path') →
      path.del (RBNode.del cut nil)
          (match nil with
          | node c l v r => c
          | x => red) =
        path'.del t'.delRoot
          (match t' with
          | node c l v r => c
          | x => red)
x✝ : zoom cut nil (left c path y b) = (t', path')
⊢ path.del
      (match nil.isBlack with
      | black => (RBNode.del cut nil).balLeft y b
      | red => node red (RBNode.del cut nil) y b)
      c =
    (left c path y b).del nil.delRoot
      (match nil with
      | node c l v r => c
      | x => red)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
cut : α → Ordering
path : Path α
t' : RBNode α
path' : Path α
x✝² : RBNode α
c : RBColor
a : RBNode α
y : α
b : RBNode α
x✝¹ : Ordering
heq✝ : cut y = Ordering.eq
x✝ : (node c a y b, path) = (t', path')
⊢ path.del (a.append b) c =
    path.del (node c a y b).delRoot
      (match node c a y b with
      | node c l v r => c
      | x => red)

Tactic:
rfl

Result:
no goals

Proof state:
case h_2
α : Type u_1
cut : α → Ordering
path : Path α
t' : RBNode α
path' : Path α
x✝¹ : RBNode α
c : RBColor
a : RBNode α
y : α
b : RBNode α
x✝ : Ordering
heq✝ : cut y = Ordering.gt
IH :
  ∀ (cut : α → Ordering) (path : Path α) (t' : RBNode α) (path' : Path α),
    zoom cut b path = (t', path') →
      path.del (RBNode.del cut b)
          (match b with
          | node c l v r => c
          | x => red) =
        path'.del t'.delRoot
          (match t' with
          | node c l v r => c
          | x => red)
⊢ zoom cut b (right c a y path) = (t', path') →
    path.del
        (match b.isBlack with
        | black => a.balRight y (RBNode.del cut b)
        | red => node red a y (RBNode.del cut b))
        c =
      path'.del t'.delRoot
        (match t' with
        | node c l v r => c
        | x => red)

Tactic:
match b with
| nil => intro | rfl => rfl
| node black .. | node red .. => apply IH

Result:
no goals