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