-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Ordered.memP_iff_find? [@TransCmp α cmp] [IsCut cmp cut] (ht : Ordered cmp t) :
    MemP cut t ↔ ∃ x, t.find? cut = some x

Proof state:
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, find? cut l = some x
ihr : Ordered cmp r → MemP cut r → ∃ x, find? cut r = some x
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

Tactic:
have ⟨z, hz, ez⟩ := Any_def.1 hx

Result:
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, find? cut l = some x
ihr : Ordered cmp r → MemP cut r → ∃ x, find? cut r = some x
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

Proof state:
α : 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, find? cut l = some x
ihr : Ordered cmp r → MemP cut r → ∃ x, find? cut r = some x
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

Tactic:
rcases H with ev' | hx | hx

Result:
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, find? cut l = some x
ihr : Ordered cmp r → MemP cut r → ∃ x, find? cut r = some x
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, find? cut l = some x
ihr : Ordered cmp r → MemP cut r → ∃ x, find? cut r = some x
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, find? cut l = some x
ihr : Ordered cmp r → MemP cut r → ∃ x, find? cut r = some x
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