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

State before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
inst✝ : TransCmp cmp
t : RBMap α β cmp
k : α
v : β
k' : α
⊢ find? (insert t k v) k' = if cmp k' k = Ordering.eq then some v else find? t k'
Tactic:
split <;> [exact find?_insert_of_eq t ‹_›; exact find?_insert_of_ne t ‹_›]
State after:
no goals