no goals
ι : Type ?u.817559
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
s : Finset α
p : α → Prop
inst✝ : NonAssocSemiring β
hp : DecidablePred p
⊢ (∑ x in s, if p x then 1 else 0) = ↑(card (filter p s))
simp only [add_zero, mul_one, Finset.sum_const, nsmul_eq_mul, eq_self_iff_true,
  Finset.sum_const_zero, Finset.sum_ite, mul_zero]