ι : Type ?u.327705
α : 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
⊢ pmap f l H =
    pmap (fun a h => f ↑{ val := a, property := h } (_ : p ↑{ val := a, property := h })) l
      (_ : ∀ (x : α), x ∈ l → x ∈ l)
ι : Type ?u.327705
α : 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
⊢ pmap f l H = map (fun x => f ↑x (_ : p ↑x)) (attach l)
rw [attach, map_pmap]
no goals
ι : Type ?u.327705
α : 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
⊢ pmap f l H =
    pmap (fun a h => f ↑{ val := a, property := h } (_ : p ↑{ val := a, property := h })) l
      (_ : ∀ (x : α), x ∈ l → x ∈ l)
exact pmap_congr l fun _ _ _ _ => rfl