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

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