-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem zoom_insert {path : Path α} {t : RBNode α} (ht : t.Balanced c n)
    (H : zoom (cmp v) t = (t', path)) :
    (path.insert t' v).setBlack = (t.insert cmp v).setBlack

Proof state:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
t' : RBNode α
v : α
path : Path α
t : RBNode α
ht : t.Balanced c n
H : zoom (cmp v) t = (t', path)
⊢ (path.insert t' v).setBlack = (RBNode.insert cmp t v).setBlack

Tactic:
have ⟨_, _, ht', hp'⟩ := ht.zoom .root H

Result:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
t' : RBNode α
v : α
path : Path α
t : RBNode α
ht : t.Balanced c n
H : zoom (cmp v) t = (t', path)
w✝¹ : RBColor
w✝ : Nat
ht' : t'.Balanced w✝¹ w✝
hp' : Path.Balanced c n path w✝¹ w✝
⊢ (path.insert t' v).setBlack = (RBNode.insert cmp t v).setBlack

Proof state:
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
t' : RBNode α
v : α
path : Path α
t : RBNode α
ht : t.Balanced c n
H : zoom (cmp v) t = (t', path)
w✝¹ : RBColor
w✝ : Nat
ht' : t'.Balanced w✝¹ w✝
hp' : Path.Balanced c n path w✝¹ w✝
⊢ (path.insert t' v).setBlack = (RBNode.insert cmp t v).setBlack

Tactic:
cases ht' with simp [insert]
| nil => simp [insertNew_eq_insert H, setBlack_idem]
| red hl hr => rw [← ins_eq_fill hp' (.red hl hr), insert_setBlack]; exact (zoom_ins H).symm
| black hl hr => rw [← ins_eq_fill hp' (.black hl hr), insert_setBlack]; exact (zoom_ins H).symm

Result:
no goals

Proof state:
case red
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : t.Balanced c n
w✝ : Nat
x✝ y✝ : RBNode α
v✝ : α
H : zoom (cmp v) t = (node red x✝ v✝ y✝, path)
hp' : Path.Balanced c n path red w✝
hl : x✝.Balanced black w✝
hr : y✝.Balanced black w✝
⊢ (path.fill (node red x✝ v y✝)).setBlack = (RBNode.insert cmp t v).setBlack

Tactic:
rw [← ins_eq_fill hp' (.red hl hr), insert_setBlack]

Result:
case red
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : t.Balanced c n
w✝ : Nat
x✝ y✝ : RBNode α
v✝ : α
H : zoom (cmp v) t = (node red x✝ v✝ y✝, path)
hp' : Path.Balanced c n path red w✝
hl : x✝.Balanced black w✝
hr : y✝.Balanced black w✝
⊢ path.ins (node red x✝ v y✝) = (RBNode.ins cmp v t).setBlack

Proof state:
case red
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : t.Balanced c n
w✝ : Nat
x✝ y✝ : RBNode α
v✝ : α
H : zoom (cmp v) t = (node red x✝ v✝ y✝, path)
hp' : Path.Balanced c n path red w✝
hl : x✝.Balanced black w✝
hr : y✝.Balanced black w✝
⊢ path.ins (node red x✝ v y✝) = (RBNode.ins cmp v t).setBlack

Tactic:
exact (zoom_ins H).symm

Result:
no goals

Proof state:
case black
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : t.Balanced c n
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : x✝.Balanced c₁✝ n✝
hr : y✝.Balanced c₂✝ n✝
H : zoom (cmp v) t = (node black x✝ v✝ y✝, path)
hp' : Path.Balanced c n path black (n✝ + 1)
⊢ path.ins (node black x✝ v y✝) = (RBNode.ins cmp v t).setBlack

Tactic:
exact (zoom_ins H).symm

Result:
no goals

Proof state:
case nil
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : t.Balanced c n
H : zoom (cmp v) t = (nil, path)
hp' : Path.Balanced c n path black 0
⊢ (path.insertNew v).setBlack = (RBNode.insert cmp t v).setBlack

Tactic:
simp [insertNew_eq_insert H, setBlack_idem]

Result:
no goals

Proof state:
case black
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : t.Balanced c n
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : x✝.Balanced c₁✝ n✝
hr : y✝.Balanced c₂✝ n✝
H : zoom (cmp v) t = (node black x✝ v✝ y✝, path)
hp' : Path.Balanced c n path black (n✝ + 1)
⊢ (path.fill (node black x✝ v y✝)).setBlack = (RBNode.insert cmp t v).setBlack

Tactic:
rw [← ins_eq_fill hp' (.black hl hr), insert_setBlack]

Result:
case black
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : t.Balanced c n
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : x✝.Balanced c₁✝ n✝
hr : y✝.Balanced c₂✝ n✝
H : zoom (cmp v) t = (node black x✝ v✝ y✝, path)
hp' : Path.Balanced c n path black (n✝ + 1)
⊢ path.ins (node black x✝ v y✝) = (RBNode.ins cmp v t).setBlack