no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.5541
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : β → γ
x : Option α
g : α → Option β
⊢ Option.map f (Option.bind x g) = Option.bind x fun a => Option.map f (g a)
cases x <;> simp