Theorem: Complexity.CostFunction.flatmap_bind (HMem/Complexity/BitTree.lean)

State before:
θ : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : Zero θ
x : CostFunction α θ
f : β → Option α
g : γ → Option β
c : γ
⊢ flatMap (flip Option.bind f ∘ g) x c = flatMap g (flatMap f x) c
Tactic:
cases hg:g c <;> simp [flatMap, flip, Option.bind, hg]
State after:
no goals