no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.6070
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : β → γ
x : Option α
g : (a : α) → a ∈ x → Option β
⊢ Option.map f (pbind x g) = pbind x fun a H => Option.map f (g a H)
cases x <;> simp only [pbind, map_none']