α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
H : MemP cut t
⊢ ∃ x, x ∈ find? cut t
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
⊢ MemP cut t ↔ ∃ x, x ∈ find? cut t
refine ⟨fun H => ?_, fun ⟨x, h⟩ => find?_some_memP h⟩
no goals
case nil
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp nil
H : MemP cut nil
⊢ False
cases H
case node
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
H : MemP cut (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ ∃ x,
    (match cut v✝ with
      | Ordering.lt => find? cut l
      | Ordering.gt => find? cut r
      | Ordering.eq => some v✝) =
      some x
case node
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
H : MemP cut (node c✝ l v✝ r)
⊢ ∃ x,
    (match cut v✝ with
      | Ordering.lt => find? cut l
      | Ordering.gt => find? cut r
      | Ordering.eq => some v✝) =
      some x
let ⟨lx, xr, hl, hr⟩ := ht
case node.h_1
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
H : MemP cut (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ ∃ x, find? cut l = some x

case node.h_2
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
H : MemP cut (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
heq✝ : cut v✝ = Ordering.gt
⊢ ∃ x, find? cut r = some x

case node.h_3
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
H : MemP cut (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ ∃ x, some v✝ = some x
case node
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
H : MemP cut (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
⊢ ∃ x,
    (match cut v✝ with
      | Ordering.lt => find? cut l
      | Ordering.gt => find? cut r
      | Ordering.eq => some v✝) =
      some x
split
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
H : MemP cut (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.lt
⊢ MemP cut l
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
H : MemP cut (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.lt
⊢ ∃ x, find? cut l = some x
refine ihl hl ?_
case inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.lt
ev' : cut v✝ = Ordering.eq
⊢ MemP cut l

case inr.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.lt
hx : Any (fun x => cut x = Ordering.eq) l
⊢ MemP cut l

case inr.inr
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.lt
hx : Any (fun x => cut x = Ordering.eq) r
⊢ MemP cut l
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
H : MemP cut (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.lt
⊢ MemP cut l
rcases H with ev' | hx | hx
no goals
case inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.lt
ev' : cut v✝ = Ordering.eq
⊢ MemP cut l
cases ev.symm.trans ev'
no goals
case inr.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.lt
hx : Any (fun x => cut x = Ordering.eq) l
⊢ MemP cut l
exact hx
case inr.inr
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.lt
hx : Any (fun x => cut x = Ordering.eq) r
z : α
hz : z ∈ r
ez : cut z = Ordering.eq
⊢ MemP cut l
case inr.inr
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.lt
hx : Any (fun x => cut x = Ordering.eq) r
⊢ MemP cut l
have ⟨z, hz, ez⟩ := Any_def.1 hx
no goals
case inr.inr
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.lt
hx : Any (fun x => cut x = Ordering.eq) r
z : α
hz : z ∈ r
ez : cut z = Ordering.eq
⊢ MemP cut l
cases ez.symm.trans <| IsCut.lt_trans (All_def.1 xr _ hz).1 ev
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
H : MemP cut (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.gt
⊢ MemP cut r
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
H : MemP cut (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.gt
⊢ ∃ x, find? cut r = some x
refine ihr hr ?_
case inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.gt
ev' : cut v✝ = Ordering.eq
⊢ MemP cut r

case inr.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.gt
hx : Any (fun x => cut x = Ordering.eq) l
⊢ MemP cut r

case inr.inr
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.gt
hx : Any (fun x => cut x = Ordering.eq) r
⊢ MemP cut r
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
H : MemP cut (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.gt
⊢ MemP cut r
rcases H with ev' | hx | hx
no goals
case inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.gt
ev' : cut v✝ = Ordering.eq
⊢ MemP cut r
cases ev.symm.trans ev'
case inr.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.gt
hx : Any (fun x => cut x = Ordering.eq) l
z : α
hz : z ∈ l
ez : cut z = Ordering.eq
⊢ MemP cut r
case inr.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.gt
hx : Any (fun x => cut x = Ordering.eq) l
⊢ MemP cut r
have ⟨z, hz, ez⟩ := Any_def.1 hx
no goals
case inr.inl
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.gt
hx : Any (fun x => cut x = Ordering.eq) l
z : α
hz : z ∈ l
ez : cut z = Ordering.eq
⊢ MemP cut r
cases ez.symm.trans <| IsCut.gt_trans (All_def.1 lx _ hz).1 ev
no goals
case inr.inr
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
ev : cut v✝ = Ordering.gt
hx : Any (fun x => cut x = Ordering.eq) r
⊢ MemP cut r
exact hx
no goals
case node.h_3
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
c✝ : RBColor
l : RBNode α
v✝ : α
r : RBNode α
ihl : Ordered cmp l → MemP cut l → ∃ x, x ∈ find? cut l
ihr : Ordered cmp r → MemP cut r → ∃ x, x ∈ find? cut r
ht : Ordered cmp (node c✝ l v✝ r)
H : MemP cut (node c✝ l v✝ r)
lx : All (fun x => cmpLT cmp x v✝) l
xr : All (fun x => cmpLT cmp v✝ x) r
hl : Ordered cmp l
hr : Ordered cmp r
x✝ : Ordering
heq✝ : cut v✝ = Ordering.eq
⊢ ∃ x, some v✝ = some x
exact ⟨_, rfl⟩