rw [sum_eq_single_of_mem d hd]
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ f d = ∑ k ∈ s, if k = d then f d else 0
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ f d = if d = d then f d else 0

α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ b ∈ s, b ≠ d → (if b = d then f d else 0) = 0