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