α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
x✝ : x ∈ t ∧ cut x = Ordering.eq
hx : x ∈ t
e : cut x = Ordering.eq
⊢ x ∈ find? cut t
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
⊢ x ∈ find? cut t ↔ x ∈ t ∧ cut x = Ordering.eq
refine ⟨fun h => ⟨find?_some_mem h, find?_some_eq_eq h⟩, fun ⟨hx, e⟩ => ?_⟩
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
x✝ : x ∈ t ∧ cut x = Ordering.eq
hx : x ∈ t
e : cut x = Ordering.eq
y : α
hy : y ∈ find? cut t
⊢ x ∈ find? cut t
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
x✝ : x ∈ t ∧ cut x = Ordering.eq
hx : x ∈ t
e : cut x = Ordering.eq
⊢ x ∈ find? cut t
have ⟨y, hy⟩ := ht.memP_iff_find?.1 (memP_def.2 ⟨_, hx, e⟩)
no goals
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
x✝ : x ∈ t ∧ cut x = Ordering.eq
hx : x ∈ t
e : cut x = Ordering.eq
y : α
hy : y ∈ find? cut t
⊢ x ∈ find? cut t
exact ht.unique hx (find?_some_mem hy) ((IsStrictCut.exact e).trans (find?_some_eq_eq hy)) ▸ hy