-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem zoom_ins {t : RBNode α} {cmp : α → α → Ordering} :
    t.zoom (cmp v) path = (t', path') →
    path.ins (t.ins cmp v) = path'.ins (t'.setRoot v)

Proof state:
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
cmp : α → α → Ordering
x✝² a✝ : RBNode α
y✝ : α
b✝ : RBNode α
x✝¹ : Ordering
heq✝ : cmp v y✝ = Ordering.eq
x✝ : (node black a✝ y✝ b✝, path) = (t', path')
⊢ path.ins (node black a✝ v b✝) = path.ins (setRoot v (node black a✝ y✝ b✝))

Tactic:
rfl

Result:
no goals

Proof state:
case h_3.h_2
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
cmp : α → α → Ordering
x✝¹ a✝ : RBNode α
y✝ : α
b✝ : RBNode α
x✝ : Ordering
heq✝ : cmp v y✝ = Ordering.gt
⊢ zoom (cmp v) b✝ (right black a✝ y✝ path) = (t', path') →
    path.ins (a✝.balance2 y✝ (RBNode.ins cmp v b✝)) = path'.ins (setRoot v t')

Tactic:
exact zoom_ins

Result:
no goals

Proof state:
case h_3.h_1
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
cmp : α → α → Ordering
x✝¹ a✝ : RBNode α
y✝ : α
b✝ : RBNode α
x✝ : Ordering
heq✝ : cmp v y✝ = Ordering.lt
⊢ zoom (cmp v) a✝ (left black path y✝ b✝) = (t', path') →
    path.ins ((RBNode.ins cmp v a✝).balance1 y✝ b✝) = path'.ins (setRoot v t')

Tactic:
exact zoom_ins

Result:
no goals

Proof state:
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
t : RBNode α
cmp : α → α → Ordering
⊢ zoom (cmp v) t path = (t', path') → path.ins (RBNode.ins cmp v t) = path'.ins (setRoot v t')

Tactic:
unfold RBNode.ins

Result:
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
t : RBNode α
cmp : α → α → Ordering
⊢ zoom (cmp v) t path = (t', path') →
    path.ins
        (match t with
        | nil => node red nil v nil
        | node red a y b =>
          match cmp v y with
          | Ordering.lt => node red (RBNode.ins cmp v a) y b
          | Ordering.gt => node red a y (RBNode.ins cmp v b)
          | Ordering.eq => node red a v b
        | node black a y b =>
          match cmp v y with
          | Ordering.lt => (RBNode.ins cmp v a).balance1 y b
          | Ordering.gt => a.balance2 y (RBNode.ins cmp v b)
          | Ordering.eq => node black a v b) =
      path'.ins (setRoot v t')

Proof state:
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
cmp : α → α → Ordering
x✝² : RBNode α
x✝¹ : nil = t'
x✝ : path = path'
⊢ path.ins (node red nil v nil) = path.ins (setRoot v nil)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
t : RBNode α
cmp : α → α → Ordering
⊢ zoom (cmp v) t path = (t', path') →
    path.ins
        (match t with
        | nil => node red nil v nil
        | node red a y b =>
          match cmp v y with
          | Ordering.lt => node red (RBNode.ins cmp v a) y b
          | Ordering.gt => node red a y (RBNode.ins cmp v b)
          | Ordering.eq => node red a v b
        | node black a y b =>
          match cmp v y with
          | Ordering.lt => (RBNode.ins cmp v a).balance1 y b
          | Ordering.gt => a.balance2 y (RBNode.ins cmp v b)
          | Ordering.eq => node black a v b) =
      path'.ins (setRoot v t')

Tactic:
split <;> simp [zoom]

Result:
case h_1
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
cmp : α → α → Ordering
x✝ : RBNode α
⊢ nil = t' → path = path' → path.ins (node red nil v nil) = path'.ins (setRoot v t')

case h_2
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
cmp : α → α → Ordering
x✝ a✝ : RBNode α
y✝ : α
b✝ : RBNode α
⊢ (match cmp v y✝ with
      | Ordering.lt => zoom (cmp v) a✝ (left red path y✝ b✝)
      | Ordering.gt => zoom (cmp v) b✝ (right red a✝ y✝ path)
      | Ordering.eq => (node red a✝ y✝ b✝, path)) =
      (t', path') →
    path.ins
        (match cmp v y✝ with
        | Ordering.lt => node red (RBNode.ins cmp v a✝) y✝ b✝
        | Ordering.gt => node red a✝ y✝ (RBNode.ins cmp v b✝)
        | Ordering.eq => node red a✝ v b✝) =
      path'.ins (setRoot v t')

case h_3
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
cmp : α → α → Ordering
x✝ a✝ : RBNode α
y✝ : α
b✝ : RBNode α
⊢ (match cmp v y✝ with
      | Ordering.lt => zoom (cmp v) a✝ (left black path y✝ b✝)
      | Ordering.gt => zoom (cmp v) b✝ (right black a✝ y✝ path)
      | Ordering.eq => (node black a✝ y✝ b✝, path)) =
      (t', path') →
    path.ins
        (match cmp v y✝ with
        | Ordering.lt => (RBNode.ins cmp v a✝).balance1 y✝ b✝
        | Ordering.gt => a✝.balance2 y✝ (RBNode.ins cmp v b✝)
        | Ordering.eq => node black a✝ v b✝) =
      path'.ins (setRoot v t')

Proof state:
case h_3
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
cmp : α → α → Ordering
x✝ a✝ : RBNode α
y✝ : α
b✝ : RBNode α
⊢ (match cmp v y✝ with
      | Ordering.lt => zoom (cmp v) a✝ (left black path y✝ b✝)
      | Ordering.gt => zoom (cmp v) b✝ (right black a✝ y✝ path)
      | Ordering.eq => (node black a✝ y✝ b✝, path)) =
      (t', path') →
    path.ins
        (match cmp v y✝ with
        | Ordering.lt => (RBNode.ins cmp v a✝).balance1 y✝ b✝
        | Ordering.gt => a✝.balance2 y✝ (RBNode.ins cmp v b✝)
        | Ordering.eq => node black a✝ v b✝) =
      path'.ins (setRoot v t')

Tactic:
split

Result:
case h_3.h_1
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
cmp : α → α → Ordering
x✝¹ a✝ : RBNode α
y✝ : α
b✝ : RBNode α
x✝ : Ordering
heq✝ : cmp v y✝ = Ordering.lt
⊢ zoom (cmp v) a✝ (left black path y✝ b✝) = (t', path') →
    path.ins ((RBNode.ins cmp v a✝).balance1 y✝ b✝) = path'.ins (setRoot v t')

case h_3.h_2
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
cmp : α → α → Ordering
x✝¹ a✝ : RBNode α
y✝ : α
b✝ : RBNode α
x✝ : Ordering
heq✝ : cmp v y✝ = Ordering.gt
⊢ zoom (cmp v) b✝ (right black a✝ y✝ path) = (t', path') →
    path.ins (a✝.balance2 y✝ (RBNode.ins cmp v b✝)) = path'.ins (setRoot v t')

case h_3.h_3
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
cmp : α → α → Ordering
x✝¹ a✝ : RBNode α
y✝ : α
b✝ : RBNode α
x✝ : Ordering
heq✝ : cmp v y✝ = Ordering.eq
⊢ (node black a✝ y✝ b✝, path) = (t', path') → path.ins (node black a✝ v b✝) = path'.ins (setRoot v t')

Proof state:
case h_1
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
cmp : α → α → Ordering
x✝ : RBNode α
⊢ nil = t' → path = path' → path.ins (node red nil v nil) = path'.ins (setRoot v t')

Tactic:
intro | rfl, rfl => rfl

Result:
no goals

Proof state:
case h_3.h_3
α : Type u_1
v : α
path : Path α
t' : RBNode α
path' : Path α
cmp : α → α → Ordering
x✝¹ a✝ : RBNode α
y✝ : α
b✝ : RBNode α
x✝ : Ordering
heq✝ : cmp v y✝ = Ordering.eq
⊢ (node black a✝ y✝ b✝, path) = (t', path') → path.ins (node black a✝ v b✝) = path'.ins (setRoot v t')

Tactic:
intro | rfl => rfl

Result:
no goals