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