axiom of choice for finite collections?

Stream: Is there code for X?

[Alex Kontorovich]

Hello, is there code that proves the axiom of choice for finite collections that doesn't invoke the infinite axiom of choice? Thanks!

[Bryan Gin-ge Chen]

You might need your collection to be docs#encodable if you really want to avoid choice.

[Adam Topaz]

Maybe docs#fintype.choose

[Bhavik Mehta]

Or docs#finset.choose

[Kevin Buzzard]

You get two answers because you didn't formalise your question with a #mwe ;-)