Tighter Finset.toList output type

Stream: Is there code for X?

[Riyaz Ahuja]

Hi! I was wondering if there exists any better Finset.toList such that for G : Finset X, rather than G.toList : List X, it is G.toList' : List {x \\ x \in G}. Currently, I have something like:

def Finset.toList' (G : Finset S) : List {x // x ∈ G} := by
  constructor

but this clearly isn't ideal, as I'm not sure how to prove statements like:

a : S
ha : a ∈ ↑G
⊢ ⟨a, ha⟩ ∈ G.toList'

[Matt Diamond]

are you looking for docs#Finset.attach ?