intro h
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
⊢ k = d → f d = f k
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
h : k = d
⊢ f d = f k