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

State before:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ find? (insert t k v) k = some v
Tactic:
rw [find?_insert_of_eq]
State after:
case h
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ cmp k k = Ordering.eq

State before:
case h
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
k : α
v : β
inst✝ : TransCmp cmp
t : RBMap α β cmp
⊢ cmp k k = Ordering.eq
Tactic:
rw [OrientedCmp.cmp_refl (cmp := cmp)]
State after:
no goals