no goals
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type ?u.6432
p : α → Prop
f✝ : (a : α) → p a → β
x✝ : Option α
f : α → β
x : Option α
g : (b : β) → b ∈ Option.map f x → Option γ
⊢ pbind (Option.map f x) g = pbind x fun a h => g (f a) (_ : f a ∈ Option.map f x)
cases x <;> rfl