enumerating a fintype

Stream: Is there code for X?

[Jalex Stark]

I have a fintype of known cardinality, and I have a proposed enumeration of its elements. I want to show that this enumeration covers everything. I think I want the following theorem, which I don't understand fintype well enough to find / prove:

import tactic
example (α : Type) [fintype α] (X : finset α) (h : finset.card X = fintype.card α) : ∀ x : α, x ∈ X := begin
sorry
end```

[Mario Carneiro]

I don't think we have this particular proof but it is not hard:

example (α : Type) [fintype α] (X : finset α) (h : finset.card X = fintype.card α) : ∀ x : α, x ∈ X :=
begin
  suffices : finset.univ ⊆ X, {exact λ x, this (finset.mem_univ _)},
  classical,
  rw [← finset.sdiff_eq_empty_iff_subset, ← finset.card_eq_zero, finset.card_univ_diff],
  simp [h]
end

[Jalex Stark]

wow, thanks!

[Mario Carneiro]

the key fact is finset.card_univ_diff

[Mario Carneiro]

there is also a constructive proof but meh

[Mario Carneiro]

actually there is an even better match, finset.eq_of_subset_of_card_le:

example (α : Type) [fintype α] (X : finset α) (h : finset.card X = fintype.card α) : ∀ x : α, x ∈ X :=
by rw finset.eq_of_subset_of_card_le (finset.subset_univ _) (ge_of_eq h);
   apply finset.mem_univ