no goals
ι : Type ?u.328936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
b : β
⊢ b ∈ pmap f l H ↔ ∃ a h, f a (_ : p a) = b
simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and_iff, Subtype.exists, eq_comm]