Theorem: Std.RBMap.findD_insert (Etch/Verification/RBMap.lean)

State before:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
inst✝ : TransCmp cmp
t : RBMap α β cmp
k : α
v : β
k' : α
d : β
⊢ findD (insert t k v) k' d = if cmp k' k = Ordering.eq then v else findD t k' d
Tactic:
simp only [findD, find?_insert]
State after:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
inst✝ : TransCmp cmp
t : RBMap α β cmp
k : α
v : β
k' : α
d : β
⊢ Option.getD (if cmp k' k = Ordering.eq then some v else find? t k') d =
    if cmp k' k = Ordering.eq then v else Option.getD (find? t k') d

State before:
α : Type u_1
β : Type u_2
cmp : α → α → Ordering
inst✝ : TransCmp cmp
t : RBMap α β cmp
k : α
v : β
k' : α
d : β
⊢ Option.getD (if cmp k' k = Ordering.eq then some v else find? t k') d =
    if cmp k' k = Ordering.eq then v else Option.getD (find? t k') d
Tactic:
split <;> rfl
State after:
no goals