Theorem: Option.bind_isSome (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
β : Type u_2
x : Option α
y : α → Option β
⊢ isSome (Option.bind x y) = true ↔ ∃ (h : isSome x = true), isSome (y (get x h)) = true
Tactic:
cases x <;> simp
State after:
no goals