α : Type u_1
cmp : α → α → Ordering
v : α
t : RBNode α
⊢ setBlack
      (match isRed t with
      | red => setBlack (ins cmp v t)
      | black => ins cmp v t) =
    setBlack (ins cmp v t)
α : Type u_1
cmp : α → α → Ordering
v : α
t : RBNode α
⊢ setBlack (insert cmp t v) = setBlack (ins cmp v t)
unfold insert
no goals
α : Type u_1
cmp : α → α → Ordering
v : α
t : RBNode α
⊢ setBlack
      (match isRed t with
      | red => setBlack (ins cmp v t)
      | black => ins cmp v t) =
    setBlack (ins cmp v t)
split <;> simp [setBlack_idem]