get arbitrary not mem of finset

Stream: Is there code for X?

[Kayla Thomas]

If I have L : Finset String, is there a way to obtain an arbitrary String that is not a member of L?

[Scott Morrison]

One would hope that
@loogle HasCompl.compl, Infinite, Set.Nonempty

[loogle]

:shrug: nothing found

[Scott Morrison]

I was angling for

import Mathlib.Data.Fintype.Card

#synth Infinite String

example {α : Type} [Infinite α] (s : Finset α) : (s.toSetᶜ : Set α).Nonempty  := by exact? -- fails

but it seems there something missing there.

[Yaël Dillies]

docs#Infinite.exists_not_mem_finset

[Kayla Thomas]

Thank you!

[Scott Morrison]

So I guess the better search was just @loogle Infinite, Finset

[loogle]

:search: instInfiniteFinset, Infinite.exists_not_mem_finset, and 13 more

[Scott Morrison]

@Yaël Dillies is still more effective. :-)