pigeonhole.lean

import data.set.finite

-- we don't need no infinite sets here
open finset
open function

-- `fin n` is the type of the first `n` natural numbers
theorem pigeonhole (n m : ℕ) (f : fin n → fin m) : n > m → ¬(injective f) :=
assume : n > m,
-- proof of negation: show contradiction
assume : injective f,
show false,
-- using ‹n > m› (these quotes refer to proofs of known facts), we can prove the
-- contradiction by proving `n ≤ m`
from suffices n ≤ m,
  from nat.lt_le_antisymm ‹n > m› ‹n ≤ m›,
   -- the type `fin n` has `n` elements
calc n = fintype.card (fin n)         : by simp
   -- ... which we can also express as the cardinality of its universal set
   ... = card (univ : finset (fin n)) : rfl
   -- ... which is the same for its image under an injective function
   ... = card (image f univ)          : by simp [card_image_of_injective univ ‹injective f›]
   -- ... which is no larger than the universal set (in `fin m`)
   ... ≤ card (univ : finset (fin m)) : card_le_of_subset (subset_univ _)
   ... = fintype.card (fin m)         : rfl
   -- ... which has `m` elements
   ... = m                            : by simp