no goals
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → Option γ
a : Option α
b : Option β
⊢ (Option.bind a fun x => Option.bind b (f x)) = Option.bind b fun y => Option.bind a fun x => f x y
cases a <;> cases b <;> rfl