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