apply sum_congr rfl
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ (∑ k ∈ s, if k = d then f d else 0) = ∑ k ∈ s, if k = d then f k else 0
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ x ∈ s, (if x = d then f d else 0) = if x = d then f x else 0