English
If two dependent maps f and g agree on every element of s (with their proofs), then pmap f s H1 = pmap g s H2.
Русский
Если две зависимые отображения f и g согласны на каждом элементе s (с соответствующими доказательствами), то pmap f s H1 = pmap g s H2.
LaTeX
$$$\\forall s\\in\\mathcal{M}(\\alpha),\\ (\\forall H_1,H_2),\\ (\\forall a\\in s,\\ f a (H_1 a) = g a (H_2 a))\\Rightarrow \\operatorname{pmap}f\\ s\\ H_1 = \\operatorname{pmap}g\\ s\\ H_2.$$$
Lean4
theorem pmap_congr {p q : α → Prop} {f : ∀ a, p a → β} {g : ∀ a, q a → β} (s : Multiset α) :
∀ {H₁ H₂}, (∀ a ∈ s, ∀ (h₁ h₂), f a h₁ = g a h₂) → pmap f s H₁ = pmap g s H₂ :=
@(Quot.inductionOn s (fun l _H₁ _H₂ h => congr_arg _ <| List.pmap_congr_left l h))
