Membership-Proof in `filter`

Stream: Is there code for X?

[Marcus Rossel]

I need to filter over a finset, and within the filter-predicate I need a proof that the current element is a member of the set over which I'm filtering. So in something like:

import data.finset

def aaa (t : finset ℕ) (n : { x // x ∈ t }) : Prop := sorry

def bbb (s : finset ℕ) : finset ℕ := s.filter (λ m, aaa s m)

... I would either want m to have type { y // y ∈ s }, or get some proof of m ∈ s.
Is there code for this?

[Bhavik Mehta]

docs#finset.attach