α : Type u_1
β : Type ?u.143075
γ : Type ?u.143078
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l (_ : ∀ (x : α), x ∈ l → (fun a_2 => a_2 ∈ a ::ₘ Quotient.mk (isSetoid α) l) x) =
    List.pmap
      (fun a_1 h =>
        { val := ↑{ val := a_1, property := h },
          property := (_ : ↑{ val := a_1, property := h } ∈ a ::ₘ Quotient.mk (isSetoid α) l) })
      l (_ : ∀ (_a : α), _a ∈ Quotient.mk (isSetoid α) l → _a ∈ Quotient.mk (isSetoid α) l)
α : Type u_1
β : Type ?u.143075
γ : Type ?u.143078
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l (_ : ∀ (x : α), x ∈ l → (fun a_2 => a_2 ∈ a ::ₘ Quotient.mk (isSetoid α) l) x) =
    List.map (fun p => { val := ↑p, property := (_ : ↑p ∈ a ::ₘ Quotient.mk (isSetoid α) l) })
      (List.pmap mk l (_ : ∀ (_a : α), _a ∈ Quotient.mk (isSetoid α) l → _a ∈ Quotient.mk (isSetoid α) l))
rw [List.map_pmap]
no goals
α : Type u_1
β : Type ?u.143075
γ : Type ?u.143078
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l (_ : ∀ (x : α), x ∈ l → (fun a_2 => a_2 ∈ a ::ₘ Quotient.mk (isSetoid α) l) x) =
    List.pmap
      (fun a_1 h =>
        { val := ↑{ val := a_1, property := h },
          property := (_ : ↑{ val := a_1, property := h } ∈ a ::ₘ Quotient.mk (isSetoid α) l) })
      l (_ : ∀ (_a : α), _a ∈ Quotient.mk (isSetoid α) l → _a ∈ Quotient.mk (isSetoid α) l)
exact List.pmap_congr _ fun _ _ _ _ => Subtype.eq rfl