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

State before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k' k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k' k = Ordering.eq
⊢ find? (insert t k v) k' = some v
Tactic:
rw [find?, findEntry?_insert_of_eq _ h]
State after:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k' k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k' k = Ordering.eq
⊢ Option.map (fun x => x.snd) (some (k, v)) = some v

State before:
α : Type u_1
cmp : α → α → Ordering
β : Type u_2
k' k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
h : cmp k' k = Ordering.eq
⊢ Option.map (fun x => x.snd) (some (k, v)) = some v
Tactic:
rfl
State after:
no goals