My question in the discrete mathematics in MIL

Stream: general

[Shiqiang Dong]

I an a greener. But I have a question.
In Mathematics in Lean, Chapter 6 Discrete Mathematics, Section 1 Finset and Fintypes, it said

If is a finset, is defined to be . You can use classical choice to pick an element of a nonempty finset.

But for a finset, will we need to use the axiom of choice? Isn't the axiom of choice aimed at infinte sets?
Thank you for your guidance!

[Aaron Liu]

We can get an element of a Finset without choice

[Aaron Liu]

but it will have to be in docs#Trunc

[Aaron Liu]

docs#truncOfNonemptyFintype

[Shiqiang Dong]

That means it used to maintain computability?

But the coad is says

noncomputable example (s : Finset ℕ) (h : s.Nonempty) : ℕ := Classical.choose h

I am sorry to not get your means. can you say it more simply? Thank you!

[Aaron Liu]

import Mathlib

variable {α : Type*} {s : Finset α} (hs : s.Nonempty)

-- get an element, noncomputably with choice
noncomputable def choose₁ : s := ⟨hs.choose, hs.choose_spec⟩

-- get an element computably, but you're not allowed to figure out which one it is
def choose₂ : Trunc s := truncOfCardPos (hs.card_pos.trans_eq (Fintype.card_coe s).symm)

[Shiqiang Dong]

But why don't we use Finset.choose or Finset.choose_spec?
That doesn't depend on Classical choose

[Aaron Liu]

Those work too but you need to find a predicate that holds for only one element of your finset.

[Shiqiang Dong]

Ok, I know it. Thank you very much!