English
If s = s' and p, p' are predicates that agree pointwise on s, then countP p s = countP p' s'.
Русский
Если s = s' и p, p' совпадают по значению на s, то countP p s = countP p' s'.
LaTeX
$$$s = s' \Rightarrow \bigl(\forall p p' : \alpha \to \text{Prop},\; (\forall x \in s, p(x) = p'(x)) \rightarrow \operatorname{countP}(p, s) = \operatorname{countP}(p', s')\bigr)$$$
Lean4
@[congr]
theorem countP_congr {s s' : Multiset α} (hs : s = s') {p p' : α → Prop} [DecidablePred p] [DecidablePred p']
(hp : ∀ x ∈ s, p x = p' x) : s.countP p = s'.countP p' :=
by
revert hs hp
exact
Quot.induction_on₂ s s'
(fun l l' hs hp => by
simp only [quot_mk_to_coe'', coe_eq_coe] at hs
apply hs.countP_congr
simpa using hp)
