no goals
α✝ : Type ?u.5024
β✝ : Type ?u.5027
γ✝ : Type ?u.5030
δ : Type ?u.5033
p : α✝ → Prop
f✝ : (a : α✝) → p a → β✝
x✝ : Option α✝
α β γ : Type u_1
f : β → γ
x : Option α
g : α → Option β
⊢ Option.map f (x >>= g) = do
    let a ← x
    Option.map f (g a)
simp only [← map_eq_map, ← bind_pure_comp, LawfulMonad.bind_assoc]