returning a unique element given a `Finset` of card = 1

Stream: Is there code for X?

[Jihoon Hyun]

/-- returns a unique element in `s` -/
def getUniqueElement {α : Type _} [Fintype α] [DecidableEq α]
  (s : Finset α) (hs : s.card = 1) : α := sorry

I'm stuck with exists and Sort. Will there be a code for this?

[Alex J. Best]

Do you want something computable? Or are you happy using classical axioms? What application do you have in mind?

[Eric Rodriguez]

docs4#Fintype.choose

[Kyle Miller]

There's also docs4#Finset.choose

[Kyle Miller]

and docs4#Finset.singleton_iff_unique_mem and docs4#Finset.card_eq_one

[Eric Rodriguez]

Kyle Miller said:

There's also docs4#Finset.choose

this is probably the best option, as true is a decidable pred

[Jihoon Hyun]

In my case, noncomputable is not an option. Will that be required if I want the definition?

[Eric Rodriguez]

these are computable as far as I know

[Jihoon Hyun]

Eric Rodriguez 말함:

Kyle Miller said:

There's also docs4#Finset.choose

this is probably the best option, as true is a decidable pred

This seems like a way!
Thanks for sharing your knowledge!

[Jihoon Hyun]

Just letting you know how the proof worked:

def getUniqueElement {α : Type _} [Fintype α] [DecidableEq α]
    (s : Finset α) (hs : s.card = 1) : α :=
  Finset.choose (fun _ => True) s (let ⟨x, hx⟩ := Finset.card_eq_one.mp hs; ⟨x, by simp_all⟩)