Theorem: Complexity.CostFunction.flatMap_some (Complexity/Cost.lean)

State before:
α : Type u_3
β : Type u_2
θ : Type u_1
inst✝ : Zero θ
f : α → Option β
a : α
b : β
h : f a = some b
g : CostFunction β θ
⊢ flatMap f g a = g b
Tactic:
simp[flatMap, h]
State after:
no goals