find a term in a fintype

Stream: maths

[Kevin Buzzard]

example (X : Type) [fintype X] (h : fintype.card X > 1) (e : X) : ∃ (f : X), f ≠ e := sorry

I've not used fintypes before and I don't just want to blunder in if this kind of stuff is done already. I'll happily be classical and noncomputable or whatever.

[Kevin Buzzard]

Oh it's not hard to reduce to (∀ (f : X), f = e) -> card X <= 1

[Reid Barton]

I started thinking the same way and now I wonder if it's going the wrong direction

[Reid Barton]

You might also want to prove exists a b, a \ne b

[Kevin Buzzard]

subsingleton -> card <= 1? that sounds like it might be in the library

[Reid Barton]

I agree it's more likely to be in the library but if it's not I think it's the wrong logical direction for the proof.

[Kevin Buzzard]

Your exists statement feels similar. How about card >= 1 -> exists x?

[Kevin Buzzard]

card >= 1 -> nonempty

[Reid Barton]

I'm not that familiar with the library either

[Kevin Buzzard]

These statements look natural, I'll have a look in data.fintype

[Kevin Buzzard]

Bingo. Now I knew what to look for it's not hard to find. fintype.card_pos_iff and fintype.card_le_one_iff

[Kevin Buzzard]

And to top it all, fintype.exists_ne_of_one_lt_card is the question I originally asked :-) But these three lemmas are the only ones of this nature.

[Scott Morrison]

It would be good to have a pool of examples of "near-misses" for library_search, so we can know which improvements are worth making.