α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
t' : RBNode α
v : α
path : Path α
t : RBNode α
ht : Balanced t c n
H : zoom (cmp v) t root = (t', path)
w✝¹ : RBColor
w✝ : Nat
ht' : Balanced t' w✝¹ w✝
hp' : Path.Balanced c n path w✝¹ w✝
⊢ setBlack (insert path t' v) = setBlack (RBNode.insert cmp t v)
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
t' : RBNode α
v : α
path : Path α
t : RBNode α
ht : Balanced t c n
H : zoom (cmp v) t root = (t', path)
⊢ setBlack (insert path t' v) = setBlack (RBNode.insert cmp t v)
have ⟨_, _, ht', hp'⟩ := ht.zoom .root H
no goals
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
t' : RBNode α
v : α
path : Path α
t : RBNode α
ht : Balanced t c n
H : zoom (cmp v) t root = (t', path)
w✝¹ : RBColor
w✝ : Nat
ht' : Balanced t' w✝¹ w✝
hp' : Path.Balanced c n path w✝¹ w✝
⊢ setBlack (insert path t' v) = setBlack (RBNode.insert cmp t v)
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
no goals
case nil
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : Balanced t c n
H : zoom (cmp v) t root = (nil, path)
hp' : Path.Balanced c n path black 0
⊢ setBlack (insertNew path v) = setBlack (RBNode.insert cmp t v)
simp [insertNew_eq_insert H, setBlack_idem]
case red
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : Balanced t c n
w✝ : Nat
x✝ y✝ : RBNode α
v✝ : α
H : zoom (cmp v) t root = (node red x✝ v✝ y✝, path)
hp' : Path.Balanced c n path red w✝
hl : Balanced x✝ black w✝
hr : Balanced y✝ black w✝
⊢ ins path (node red x✝ v y✝) = setBlack (RBNode.ins cmp v t)
case red
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : Balanced t c n
w✝ : Nat
x✝ y✝ : RBNode α
v✝ : α
H : zoom (cmp v) t root = (node red x✝ v✝ y✝, path)
hp' : Path.Balanced c n path red w✝
hl : Balanced x✝ black w✝
hr : Balanced y✝ black w✝
⊢ setBlack (fill path (node red x✝ v y✝)) = setBlack (RBNode.insert cmp t v)
rw [← ins_eq_fill hp' (.red hl hr), insert_setBlack]
no goals
case red
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : Balanced t c n
w✝ : Nat
x✝ y✝ : RBNode α
v✝ : α
H : zoom (cmp v) t root = (node red x✝ v✝ y✝, path)
hp' : Path.Balanced c n path red w✝
hl : Balanced x✝ black w✝
hr : Balanced y✝ black w✝
⊢ ins path (node red x✝ v y✝) = setBlack (RBNode.ins cmp v t)
exact (zoom_ins H).symm
case black
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : Balanced t c n
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : Balanced x✝ c₁✝ n✝
hr : Balanced y✝ c₂✝ n✝
H : zoom (cmp v) t root = (node black x✝ v✝ y✝, path)
hp' : Path.Balanced c n path black (n✝ + 1)
⊢ ins path (node black x✝ v y✝) = setBlack (RBNode.ins cmp v t)
case black
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : Balanced t c n
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : Balanced x✝ c₁✝ n✝
hr : Balanced y✝ c₂✝ n✝
H : zoom (cmp v) t root = (node black x✝ v✝ y✝, path)
hp' : Path.Balanced c n path black (n✝ + 1)
⊢ setBlack (fill path (node black x✝ v y✝)) = setBlack (RBNode.insert cmp t v)
rw [← ins_eq_fill hp' (.black hl hr), insert_setBlack]
no goals
case black
α : Type u_1
c : RBColor
n : Nat
cmp : α → α → Ordering
v : α
path : Path α
t : RBNode α
ht : Balanced t c n
x✝ : RBNode α
c₁✝ : RBColor
n✝ : Nat
y✝ : RBNode α
c₂✝ : RBColor
v✝ : α
hl : Balanced x✝ c₁✝ n✝
hr : Balanced y✝ c₂✝ n✝
H : zoom (cmp v) t root = (node black x✝ v✝ y✝, path)
hp' : Path.Balanced c n path black (n✝ + 1)
⊢ ins path (node black x✝ v y✝) = setBlack (RBNode.ins cmp v t)
exact (zoom_ins H).symm