no goals
α : Type u_1
β : Type u_2
o : Option α
f : α → Option β
⊢ Option.bind o f = none ↔ ∀ (b : β) (a : α), a ∈ o → ¬b ∈ f a
simp only [eq_none_iff_forall_not_mem, not_exists, not_and, mem_def, bind_eq_some]