noncomputable def Finset.toListWithProof {α : Type u} [DecidableEq α] (s : Finset α) : List ↥s

A helper to convert a finset into a list whose elements are the members of the finset, i.e. come with a proof that they belong to the finset.

@[simp]

theorem Finset.toListWithProof_empty {α : Type u} [DecidableEq α] : ∅.toListWithProof = []

theorem Finset.toListWithProof_mem {α : Type u} [DecidableEq α] {x : α} {s : Finset α} (hx : x ∈ s) : ⟨x, hx⟩ ∈ s.toListWithProof

@[simp]

theorem Finset.toListWithProof_eq_toList {α : Type u} [DecidableEq α] {s : Finset α} : List.map (fun (x : ↥s) => ↑x) s.toListWithProof = s.toList