Finset.sum with proof of membership?

Stream: Is there code for X?

[Michail Karatarakis]

Do we have this, or is there a common way to handle this kind of setup ?

def Finset.sum' [AddCommMonoid β] (s : Finset α)
    (f : ∀ x : α, x ∈ s → β) : β := sorry

[Andrew Yang]

import Mathlib.Algebra.BigOperators.Group.Finset

def Finset.sum' {β} [AddCommMonoid β] (s : Finset α)
    (f : ∀ x : α, x ∈ s → β) : β := ∑ i ∈ s.attach, f i.1 i.2

[Andrew Yang]

Or just ∑ i : s, f i.1 i.2. Pretty sure they are the same thing?

[Michail Karatarakis]

Yes, they are - thanks a lot