Question about the cardinalities of Finset and Fintype

Stream: new members

[Ching-Tsun Chou]

How do I prove the following?

variable (α : Type*) [Fintype α] [DecidableEq α]

example (s : Finset α) (n : ℕ) (h : s.card = n + 1) : ↑n < Fin.last (Fintype.card α) := by
  sorry

My informal argument is as follows: If s has cardinality n + 1 and s is a Finset in the carrier type α, then surely the cardinality of Fintype.card α is at least n + 1and hence Fin.last (Fintype.card α) is at least n + 1 > n. Is my argument correct? What are the relevant results in mathlib I can use?

[Ruben Van de Velde]

Looks like your code is missing imports

[Zhang Qinchuan]

Ching-Tsun Chou said:

then surely the cardinality of Fintype.card α is at least n + 1

This is easy.

import Mathlib

variable (α : Type*) [Fintype α] [DecidableEq α]

example (s : Finset α) (n : ℕ) (h : s.card = n + 1) : n + 1 ≤ Fintype.card α := by
  rw [Fintype.card, ← h]
  apply Finset.card_le_card
  exact Finset.subset_univ s

Ching-Tsun Chou said:

hence Fin.last (Fintype.card α) is at least n + 1 > n.

This seems weird.

[Matt Diamond]

docs#Finset.card_le_univ might also help

[Ching-Tsun Chou]

Thanks a lot! I was able to finish the proof:

example (s : Finset α) (n : ℕ) (h : s.card = n + 1) : ↑n < Fin.last (Fintype.card α) := by
  have h1 := Finset.card_le_univ s
  simp [h] at h1
  have h2 : n % (Fintype.card α + 1) = n := by
    apply Nat.mod_eq_of_lt
    linarith
  apply Fin.lt_def.mpr
  simp [Fin.val_last, h2]
  linarith

It may not be the most beautiful proof, but it works.