no goals
ι : Type ?u.516018
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝² : CommMonoid β
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
l : List α
⊢ ∑ x in filter p (toFinset l), count x l = countp (fun b => decide (p b)) l
simp [Finset.sum, sum_map_count_dedup_filter_eq_countp p l]