exists a unique nth element of fin n

Stream: Is there code for X?

[Evan Lohn]

Was curious whether anyone had ideas for shortening this proof of
"There is a fourth element of fin 4"

import data.finset.basic
import tactic.linarith

example (a b c : fin 4) : ∃ d, d ≠ a ∧ d ≠ b ∧ d ≠ c :=
begin
  by_contradiction, push_neg at h,
  have : finset.univ ⊆ [a, b, c].to_finset,
  { intro x, simp, specialize h x, tauto },
  have : finset.univ.card ≤ [a, b, c].length :=
    le_trans (finset.card_le_of_subset this) (list.to_finset_card_le _),
  norm_num at this
end

P.S. Big thanks to @Jeremy Avigad for the above proof!

[Yaël Dillies]

This looks very short already. We needed the version for fin 3 a while back and couldn't find better. Small numbers are hard. I mean it.

[Mario Carneiro]

lemma fintype.list_covers {α} [fintype α] {l : list α} (h : ∀ x, x ∈ l) :
  fintype.card α ≤ l.length :=
begin
  classical,
  rw [fintype.card],
  convert ← list.to_finset_card_le l,
  apply finset.eq_univ_iff_forall.2,
  simp [h]
end

example (a b c : fin 4) : ∃ d, d ≠ a ∧ d ≠ b ∧ d ≠ c :=
suffices ¬ ∀ d, d ∈ [a, b, c], by simpa [not_or_distrib],
λ H, absurd (fintype.list_covers H) dec_trivial

[Joseph Myers]

import tactic.norm_num

example (a b c : fin 4) : ∃ d, d ≠ a ∧ d ≠ b ∧ d ≠ c :=
by dec_trivial!

[Kevin Buzzard]

Small numbers are easy now ;-)