Pigeonhole principle

import Mathlib

theorem pigeonhole {α β : Type} [Fintype α] [Fintype β] (f : α → β) (h : Fintype.card β < Fintype.card α) : ∃ a₁ a₂, a₁ ≠ a₂ ∧ f a₁ = f a₂ :=Fintype.exists_ne_map_eq_of_card_lt f h