Theorem: Std.RBSet.findP?_insert (Etch/Verification/RBMap.lean)

State before:
α : Type u_1
cmp : α → α → Ordering
inst✝¹ : TransCmp cmp
t : RBSet α cmp
v : α
cut : α → Ordering
inst✝ : IsStrictCut cmp cut
⊢ findP? (insert t v) cut = if cut v = Ordering.eq then some v else findP? t cut
Tactic:
split <;> [exact findP?_insert_of_eq t ‹_›; exact findP?_insert_of_ne t ‹_›]
State after:
no goals