case node
α : Type u_1
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → cut x = Ordering.eq
r_ih✝ : x ∈ find? cut r✝ → cut x = Ordering.eq
⊢ (match cut v✝ with
      | Ordering.lt => find? cut l✝
      | Ordering.gt => find? cut r✝
      | Ordering.eq => some v✝) =
      some x →
    cut x = Ordering.eq
α : Type u_1
x : α
cut : α → Ordering
t : RBNode α
⊢ x ∈ find? cut t → cut x = Ordering.eq
induction t <;> simp [find?]
case node.h_3
α : Type u_1
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → cut x = Ordering.eq
r_ih✝ : x ∈ find? cut r✝ → cut x = Ordering.eq
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ some v✝ = some x → cut x = Ordering.eq
case node
α : Type u_1
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → cut x = Ordering.eq
r_ih✝ : x ∈ find? cut r✝ → cut x = Ordering.eq
⊢ (match cut v✝ with
      | Ordering.lt => find? cut l✝
      | Ordering.gt => find? cut r✝
      | Ordering.eq => some v✝) =
      some x →
    cut x = Ordering.eq
split <;> try assumption
no goals
case node.h_3
α : Type u_1
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → cut x = Ordering.eq
r_ih✝ : x ∈ find? cut r✝ → cut x = Ordering.eq
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ some v✝ = some x → cut x = Ordering.eq
intro | rfl => assumption
case node.h_3
α : Type u_1
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → cut x = Ordering.eq
r_ih✝ : x ∈ find? cut r✝ → cut x = Ordering.eq
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ some v✝ = some x → cut x = Ordering.eq
case node.h_3
α : Type u_1
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
l_ih✝ : x ∈ find? cut l✝ → cut x = Ordering.eq
r_ih✝ : x ∈ find? cut r✝ → cut x = Ordering.eq
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ some v✝ = some x → cut x = Ordering.eq
assumption
no goals
α : Type u_1
x : α
cut : α → Ordering
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝¹ : Ordering
heq✝ : cut v✝ = Ordering.eq
x✝ : some v✝ = some x
l_ih✝ : v✝ ∈ find? cut l✝ → cut v✝ = Ordering.eq
r_ih✝ : v✝ ∈ find? cut r✝ → cut v✝ = Ordering.eq
⊢ cut v✝ = Ordering.eq
assumption