Theorem: Finset.sum_boole_mul' (LeanCamCombi/Mathlib/Algebra/BigOperators/Ring.lean)

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : ι
⊢ ∑ j ∈ s, (if i = j then 1 else 0) * f j = if i ∈ s then f i else 0
Tactic:
simp
State after:
no goals