Theorem: Option.bind_eq_none'' (Lean4Lean/Std/Basic.lean)

State before:
α : Type u_1
β : Type u_2
o : Option α
f : α → Option β
⊢ Option.bind o f = none ↔ ∀ (a : α), o = some a → f a = none
Tactic:
cases o <;> simp
State after:
no goals