α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : optParam (Path α) Path.root
⊢ (match cut v✝ with
    | Ordering.lt => find? cut l✝
    | Ordering.gt => find? cut r✝
    | Ordering.eq => some v✝) =
    root?
      (match cut v✝ with
        | Ordering.lt => zoom cut l✝ (Path.left c✝ x✝ v✝ r✝)
        | Ordering.gt => zoom cut r✝ (Path.right c✝ l✝ v✝ x✝)
        | Ordering.eq => (node c✝ l✝ v✝ r✝, x✝)).fst
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : optParam (Path α) Path.root
⊢ find? cut (node c✝ l✝ v✝ r✝) = root? (zoom cut (node c✝ l✝ v✝ r✝) x✝).fst
unfold find? zoom
no goals
α : Type u_1
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : optParam (Path α) Path.root
⊢ (match cut v✝ with
    | Ordering.lt => find? cut l✝
    | Ordering.gt => find? cut r✝
    | Ordering.eq => some v✝) =
    root?
      (match cut v✝ with
        | Ordering.lt => zoom cut l✝ (Path.left c✝ x✝ v✝ r✝)
        | Ordering.gt => zoom cut r✝ (Path.right c✝ l✝ v✝ x✝)
        | Ordering.eq => (node c✝ l✝ v✝ r✝, x✝)).fst
split <;> [apply find?_eq_zoom; apply find?_eq_zoom; rfl]