case node
α : Type u_1
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → x ∈ l✝
r_ih✝ : x ∈ find? cut r✝ → x ∈ r✝
⊢ (match cut v✝ with
      | Ordering.lt => find? cut l✝
      | Ordering.gt => find? cut r✝
      | Ordering.eq => some v✝) =
      some x →
    x = v✝ ∨ x ∈ l✝ ∨ x ∈ r✝
α : Type u_1
x : α
cut : α → Ordering
t : RBNode α
⊢ x ∈ find? cut t → x ∈ t
induction t <;> simp [find?]
no goals
case node
α : Type u_1
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → x ∈ l✝
r_ih✝ : x ∈ find? cut r✝ → x ∈ r✝
⊢ (match cut v✝ with
      | Ordering.lt => find? cut l✝
      | Ordering.gt => find? cut r✝
      | Ordering.eq => some v✝) =
      some x →
    x = v✝ ∨ x ∈ l✝ ∨ x ∈ r✝
split <;> simp (config := {contextual := true}) [*]