Working with sets of finite cardinality

Stream: new members

[Patrick Lutz]

I am having trouble figuring out how to do something very basic when working with finite sets. The following is an illustration of the kind of thing I can't figure out how to do:

import data.fintype.basic
example (X : Type) [fintype X] (a b c : X) (h : fintype.card X = 2)
    (h1 : a ≠ b) (h2 : a ≠ c) (h3 : b ≠ c) : false := sorry

What's the best way to prove this kind of thing?

[Mario Carneiro]

I would try to prove that [a,b,c] induces a finset of size 3

[Mario Carneiro]

import data.fintype.basic
example (X : Type) [fintype X] (a b c : X) (h : fintype.card X = 2)
    (h1 : a ≠ b) (h2 : a ≠ c) (h3 : b ≠ c) : false :=
begin
  let S : finset X := ⟨[a,b,c], by simp *⟩,
  have : 3 ≤ _ := finset.card_le_of_subset (finset.subset_univ S),
  rw [finset.card_univ, h] at this,
  exact absurd this dec_trivial,
end

[Patrick Lutz]

Nice, thanks. That works