choose an element from a fintype with positive cardinality

Stream: Is there code for X?

[David Renshaw]

I have this:

noncomputable def choose_element {α : Type} [DecidableEq α] [Fintype α]
    (hs : 0 < Fintype.card α) : α :=
  (truncOfCardPos hs).out

but that truncOfCardPos thing seems kind of ugly. Is there a better way?

[Adam Topaz]

Isn't there a Nonempty instance you can use?

[Adam Topaz]

E.g.

noncomputable def choose_element {α : Type} [DecidableEq α] [Fintype α]
    (hs : 0 < Fintype.card α) : α :=
  Nonempty.some <| Iff.mp Fintype.card_pos_iff hs

[Adam Topaz]

I don't know if that's necessarily better?

[David Renshaw]

yeah, that seems a bit more readable to me

[Kyle Miller]

There's also changing hs to Nonempty inside your proof and then using Classical.arbitrary.

I'm not suggesting making this definition, but the body is meant to simulate how it'd look in a proof.

noncomputable def choose_element {α : Type} [DecidableEq α] [Fintype α]
    (hs : 0 < Fintype.card α) : α :=
  have : Nonempty α := Fintype.card_pos_iff.mp hs -- or `rw [Fintype.card_pos_iff] at hs` in a tactic proof
  Classical.arbitrary α

[Kyle Miller]

There's also stuff like using the inhabit tactic to lift it to an Inhabited instance, which gives you default

noncomputable def choose_element {α : Type} [DecidableEq α] [Fintype α]
    (hs : 0 < Fintype.card α) : α := by
  rw [Fintype.card_pos_iff] at hs
  inhabit α
  exact default

[Kyle Miller]

(I wonder if it's out of scope for inhabit to look for hypotheses such as hs? There could be a library of @[inhabit] lemmas it consults.)

[Yaël Dillies]

I've said before that inhabit should match nontriviality in that it assumes the type is empty and tries to discharge the case using a finishing tactic.