no goals
α✝ : Type ?u.8960
β✝ : Type ?u.8963
γ✝ : Type ?u.8966
δ : Type ?u.8969
p✝ : α✝ → Prop
f✝ : (a : α✝) → p✝ a → β✝
x✝ : Option α✝
α β γ : Type u_1
x : Option α
g : α → Option β
p : β → Prop
f : (b : β) → p b → γ
H : ∀ (a : β), a ∈ x >>= g → p a
H' : ∀ (a : α) (b : β), b ∈ g a → b ∈ x >>= g
⊢ pmap f (x >>= g) H = do
    let a ← x
    pmap f (g a) (_ : ∀ (b : β), b ∈ g a → p b)
cases x <;> simp only [pmap, bind_eq_bind, none_bind, some_bind]