Pigeonhole principles

Given pigeons (possibly infinitely many) in pigeonholes, the pigeonhole principle states that, if there are more pigeons than pigeonholes, then there is a pigeonhole with two or more pigeons.

There are a few variations on this statement, and the conclusion can be made stronger depending on how many pigeons you know you might have.

The basic statements of the pigeonhole principle appear in the following locations:

• Data.Finset.Basic has Finset.exists_ne_map_eq_of_card_lt_of_maps_to
• Data.Fintype.Basic has Fintype.exists_ne_map_eq_of_card_lt
• Data.Fintype.Basic has Finite.exists_ne_map_eq_of_infinite
• Data.Fintype.Basic has Finite.exists_infinite_fiber
• Data.Set.Finite has Set.infinite.exists_ne_map_eq_of_mapsTo

This module gives access to these pigeonhole principles along with 20 more. The versions vary by:

• using a function between Fintypes or a function between possibly infinite types restricted to Finsets;
• counting pigeons by a general weight function (∑ x ∈ s, w x) or by heads (#s);
• using strict or non-strict inequalities;
• establishing upper or lower estimate on the number (or the total weight) of the pigeons in one pigeonhole;
• in case when we count pigeons by some weight function w and consider a function f between Finsets s and t, we can either assume that each pigeon is in one of the pigeonholes (∀ x ∈ s, f x ∈ t), or assume that for y ∉ t, the total weight of the pigeons in this pigeonhole ∑ x ∈ s with f x = y, w x is nonpositive or nonnegative depending on the inequality we are proving.

Lemma names follow mathlib convention (e.g., Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum); "pigeonhole principle" is mentioned in the docstrings instead of the names.

See also

• Ordinal.infinite_pigeonhole: pigeonhole principle for cardinals, formulated using cofinality;

• MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure, MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_sum_measure: pigeonhole principle in a measure space.

Tags

pigeonhole principle

The pigeonhole principles on Finsets, pigeons counted by weight

In this section we prove the following version of the pigeonhole principle: if the total weight of a finite set of pigeons is greater than n • b, and they are sorted into n pigeonholes, then for some pigeonhole, the total weight of the pigeons in this pigeonhole is greater than b, and a few variations of this theorem.

The principle is formalized in the following way, see Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum: if f : α → β is a function which maps all elements of s : Finset α to t : Finset β and #t • b < ∑ x ∈ s, w x, where w : α → M is a weight function taking values in a LinearOrderedCancelAddCommMonoid, then for some y ∈ t, the sum of the weights of all x ∈ s such that f x = y is greater than b.

There are a few bits we can change in this theorem:

• reverse all inequalities, with obvious adjustments to the name;
• replace the assumption ∀ a ∈ s, f a ∈ t with ∀ y ∉ t, ∑ x ∈ s with f x = y, w x ≤ 0, and replace of_maps_to with of_sum_fiber_nonpos in the name;
• use non-strict inequalities assuming t is nonempty.

We can do all these variations independently, so we have eight versions of the theorem.

Strict inequality versions

theorem Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [LinearOrderedCancelAddCommMonoid M] (hf : ∀ a ∈ s, f a ∈ t) (hb : t.card • b < ∑ x ∈ s, w x) : ∃ y ∈ t, b < ∑ x ∈ Finset.filter (fun (x : α) => f x = y) s, w x

The pigeonhole principle for finitely many pigeons counted by weight, strict inequality version: if the total weight of a finite set of pigeons is greater than n • b, and they are sorted into n pigeonholes, then for some pigeonhole, the total weight of the pigeons in this pigeonhole is greater than b.

theorem Finset.exists_sum_fiber_lt_of_maps_to_of_sum_lt_nsmul {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [LinearOrderedCancelAddCommMonoid M] (hf : ∀ a ∈ s, f a ∈ t) (hb : ∑ x ∈ s, w x < t.card • b) : ∃ y ∈ t, ∑ x ∈ Finset.filter (fun (x : α) => f x = y) s, w x < b

The pigeonhole principle for finitely many pigeons counted by weight, strict inequality version: if the total weight of a finite set of pigeons is less than n • b, and they are sorted into n pigeonholes, then for some pigeonhole, the total weight of the pigeons in this pigeonhole is less than b.

theorem Finset.exists_lt_sum_fiber_of_sum_fiber_nonpos_of_nsmul_lt_sum {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [LinearOrderedCancelAddCommMonoid M] (ht : ∀ y ∉ t, ∑ x ∈ Finset.filter (fun (x : α) => f x = y) s, w x ≤ 0) (hb : t.card • b < ∑ x ∈ s, w x) : ∃ y ∈ t, b < ∑ x ∈ Finset.filter (fun (x : α) => f x = y) s, w x

The pigeonhole principle for finitely many pigeons counted by weight, strict inequality version: if the total weight of a finite set of pigeons is greater than n • b, they are sorted into some pigeonholes, and for all but n pigeonholes the total weight of the pigeons there is nonpositive, then for at least one of these n pigeonholes, the total weight of the pigeons in this pigeonhole is greater than b.

theorem Finset.exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [LinearOrderedCancelAddCommMonoid M] (ht : ∀ y ∉ t, 0 ≤ ∑ x ∈ Finset.filter (fun (x : α) => f x = y) s, w x) (hb : ∑ x ∈ s, w x < t.card • b) : ∃ y ∈ t, ∑ x ∈ Finset.filter (fun (x : α) => f x = y) s, w x < b

The pigeonhole principle for finitely many pigeons counted by weight, strict inequality version: if the total weight of a finite set of pigeons is less than n • b, they are sorted into some pigeonholes, and for all but n pigeonholes the total weight of the pigeons there is nonnegative, then for at least one of these n pigeonholes, the total weight of the pigeons in this pigeonhole is less than b.

Non-strict inequality versions

theorem Finset.exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [LinearOrderedCancelAddCommMonoid M] (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Nonempty) (hb : t.card • b ≤ ∑ x ∈ s, w x) : ∃ y ∈ t, b ≤ ∑ x ∈ Finset.filter (fun (x : α) => f x = y) s, w x

The pigeonhole principle for finitely many pigeons counted by weight, non-strict inequality version: if the total weight of a finite set of pigeons is greater than or equal to n • b, and they are sorted into n > 0 pigeonholes, then for some pigeonhole, the total weight of the pigeons in this pigeonhole is greater than or equal to b.

theorem Finset.exists_sum_fiber_le_of_maps_to_of_sum_le_nsmul {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [LinearOrderedCancelAddCommMonoid M] (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Nonempty) (hb : ∑ x ∈ s, w x ≤ t.card • b) : ∃ y ∈ t, ∑ x ∈ Finset.filter (fun (x : α) => f x = y) s, w x ≤ b

The pigeonhole principle for finitely many pigeons counted by weight, non-strict inequality version: if the total weight of a finite set of pigeons is less than or equal to n • b, and they are sorted into n > 0 pigeonholes, then for some pigeonhole, the total weight of the pigeons in this pigeonhole is less than or equal to b.

theorem Finset.exists_le_sum_fiber_of_sum_fiber_nonpos_of_nsmul_le_sum {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [LinearOrderedCancelAddCommMonoid M] (hf : ∀ y ∉ t, ∑ x ∈ Finset.filter (fun (x : α) => f x = y) s, w x ≤ 0) (ht : t.Nonempty) (hb : t.card • b ≤ ∑ x ∈ s, w x) : ∃ y ∈ t, b ≤ ∑ x ∈ Finset.filter (fun (x : α) => f x = y) s, w x

The pigeonhole principle for finitely many pigeons counted by weight, non-strict inequality version: if the total weight of a finite set of pigeons is greater than or equal to n • b, they are sorted into some pigeonholes, and for all but n > 0 pigeonholes the total weight of the pigeons there is nonpositive, then for at least one of these n pigeonholes, the total weight of the pigeons in this pigeonhole is greater than or equal to b.

theorem Finset.exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M} {b : M} [LinearOrderedCancelAddCommMonoid M] (hf : ∀ y ∉ t, 0 ≤ ∑ x ∈ Finset.filter (fun (x : α) => f x = y) s, w x) (ht : t.Nonempty) (hb : ∑ x ∈ s, w x ≤ t.card • b) : ∃ y ∈ t, ∑ x ∈ Finset.filter (fun (x : α) => f x = y) s, w x ≤ b

The pigeonhole principle for finitely many pigeons counted by weight, non-strict inequality version: if the total weight of a finite set of pigeons is less than or equal to n • b, they are sorted into some pigeonholes, and for all but n > 0 pigeonholes the total weight of the pigeons there is nonnegative, then for at least one of these n pigeonholes, the total weight of the pigeons in this pigeonhole is less than or equal to b.

The pigeonhole principles on Finsets, pigeons counted by heads

In this section we formalize a few versions of the following pigeonhole principle: there is a pigeonhole with at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes.

First, we can use strict or non-strict inequalities. While the versions with non-strict inequalities are weaker than those with strict inequalities, sometimes it might be more convenient to apply the weaker version. Second, we can either state that there exists a pigeonhole with at least n pigeons, or state that there exists a pigeonhole with at most n pigeons. In the latter case we do not need the assumption ∀ a ∈ s, f a ∈ t.

So, we prove four theorems: Finset.exists_lt_card_fiber_of_maps_to_of_mul_lt_card, Finset.exists_le_card_fiber_of_maps_to_of_mul_le_card, Finset.exists_card_fiber_lt_of_card_lt_mul, and Finset.exists_card_fiber_le_of_card_le_mul.

theorem Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {b : M} [LinearOrderedCommSemiring M] (hf : ∀ a ∈ s, f a ∈ t) (ht : t.card • b < ↑s.card) : ∃ y ∈ t, b < ↑(Finset.filter (fun (x : α) => f x = y) s).card

The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes.

theorem Finset.exists_lt_card_fiber_of_mul_lt_card_of_maps_to {α : Type u} {β : Type v} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ} (hf : ∀ a ∈ s, f a ∈ t) (hn : t.card * n < s.card) : ∃ y ∈ t, n < (Finset.filter (fun (x : α) => f x = y) s).card

The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes. ("The maximum is at least the mean" specialized to integers.)

More formally, given a function between finite sets s and t and a natural number n such that #t * n < #s, there exists y ∈ t such that its preimage in s has more than n elements.

theorem Finset.exists_card_fiber_lt_of_card_lt_nsmul {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {b : M} [LinearOrderedCommSemiring M] (ht : ↑s.card < t.card • b) : ∃ y ∈ t, ↑(Finset.filter (fun (x : α) => f x = y) s).card < b

The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with at most as many pigeons as the floor of the average number of pigeons across all pigeonholes.

theorem Finset.exists_card_fiber_lt_of_card_lt_mul {α : Type u} {β : Type v} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ} (hn : s.card < t.card * n) : ∃ y ∈ t, (Finset.filter (fun (x : α) => f x = y) s).card < n

The pigeonhole principle for finitely many pigeons counted by heads: there is a pigeonhole with at most as many pigeons as the floor of the average number of pigeons across all pigeonholes. ("The minimum is at most the mean" specialized to integers.)

More formally, given a function f, a finite sets s in its domain, a finite set t in its codomain, and a natural number n such that #s < #t * n, there exists y ∈ t such that its preimage in s has less than n elements.

theorem Finset.exists_le_card_fiber_of_nsmul_le_card_of_maps_to {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {b : M} [LinearOrderedCommSemiring M] (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Nonempty) (hb : t.card • b ≤ ↑s.card) : ∃ y ∈ t, b ≤ ↑(Finset.filter (fun (x : α) => f x = y) s).card

The pigeonhole principle for finitely many pigeons counted by heads: given a function between finite sets s and t and a number b such that #t • b ≤ #s, there exists y ∈ t such that its preimage in s has at least b elements. See also Finset.exists_lt_card_fiber_of_nsmul_lt_card_of_maps_to for a stronger statement.

theorem Finset.exists_le_card_fiber_of_mul_le_card_of_maps_to {α : Type u} {β : Type v} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ} (hf : ∀ a ∈ s, f a ∈ t) (ht : t.Nonempty) (hn : t.card * n ≤ s.card) : ∃ y ∈ t, n ≤ (Finset.filter (fun (x : α) => f x = y) s).card

The pigeonhole principle for finitely many pigeons counted by heads: given a function between finite sets s and t and a natural number b such that #t * n ≤ #s, there exists y ∈ t such that its preimage in s has at least n elements. See also Finset.exists_lt_card_fiber_of_mul_lt_card_of_maps_to for a stronger statement.

theorem Finset.exists_card_fiber_le_of_card_le_nsmul {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {b : M} [LinearOrderedCommSemiring M] (ht : t.Nonempty) (hb : ↑s.card ≤ t.card • b) : ∃ y ∈ t, ↑(Finset.filter (fun (x : α) => f x = y) s).card ≤ b

The pigeonhole principle for finitely many pigeons counted by heads: given a function f, a finite sets s and t, and a number b such that #s ≤ #t • b, there exists y ∈ t such that its preimage in s has no more than b elements. See also Finset.exists_card_fiber_lt_of_card_lt_nsmul for a stronger statement.

theorem Finset.exists_card_fiber_le_of_card_le_mul {α : Type u} {β : Type v} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {n : ℕ} (ht : t.Nonempty) (hn : s.card ≤ t.card * n) : ∃ y ∈ t, (Finset.filter (fun (x : α) => f x = y) s).card ≤ n

The pigeonhole principle for finitely many pigeons counted by heads: given a function f, a finite sets s in its domain, a finite set t in its codomain, and a natural number n such that #s ≤ #t * n, there exists y ∈ t such that its preimage in s has no more than n elements. See also Finset.exists_card_fiber_lt_of_card_lt_mul for a stronger statement.

The pigeonhole principles on Fintypess, pigeons counted by weight

In this section we specialize theorems from the previous section to the special case of functions between Fintypes and s = univ, t = univ. In this case the assumption ∀ x ∈ s, f x ∈ t always holds, so we have four theorems instead of eight.

theorem Fintype.exists_lt_sum_fiber_of_nsmul_lt_sum {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {w : α → M} {b : M} [LinearOrderedCancelAddCommMonoid M] (hb : Fintype.card β • b < ∑ x : α, w x) : ∃ (y : β), b < ∑ x ∈ Finset.filter (fun (x : α) => f x = y) Finset.univ, w x

The pigeonhole principle for finitely many pigeons of different weights, strict inequality version: there is a pigeonhole with the total weight of pigeons in it greater than b provided that the total number of pigeonholes times b is less than the total weight of all pigeons.

theorem Fintype.exists_le_sum_fiber_of_nsmul_le_sum {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {w : α → M} {b : M} [LinearOrderedCancelAddCommMonoid M] [Nonempty β] (hb : Fintype.card β • b ≤ ∑ x : α, w x) : ∃ (y : β), b ≤ ∑ x ∈ Finset.filter (fun (x : α) => f x = y) Finset.univ, w x

The pigeonhole principle for finitely many pigeons of different weights, non-strict inequality version: there is a pigeonhole with the total weight of pigeons in it greater than or equal to b provided that the total number of pigeonholes times b is less than or equal to the total weight of all pigeons.

theorem Fintype.exists_sum_fiber_lt_of_sum_lt_nsmul {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {w : α → M} {b : M} [LinearOrderedCancelAddCommMonoid M] (hb : ∑ x : α, w x < Fintype.card β • b) : ∃ (y : β), ∑ x ∈ Finset.filter (fun (x : α) => f x = y) Finset.univ, w x < b

The pigeonhole principle for finitely many pigeons of different weights, strict inequality version: there is a pigeonhole with the total weight of pigeons in it less than b provided that the total number of pigeonholes times b is greater than the total weight of all pigeons.

theorem Fintype.exists_sum_fiber_le_of_sum_le_nsmul {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {w : α → M} {b : M} [LinearOrderedCancelAddCommMonoid M] [Nonempty β] (hb : ∑ x : α, w x ≤ Fintype.card β • b) : ∃ (y : β), ∑ x ∈ Finset.filter (fun (x : α) => f x = y) Finset.univ, w x ≤ b

The pigeonhole principle for finitely many pigeons of different weights, non-strict inequality version: there is a pigeonhole with the total weight of pigeons in it less than or equal to b provided that the total number of pigeonholes times b is greater than or equal to the total weight of all pigeons.

theorem Fintype.exists_lt_card_fiber_of_nsmul_lt_card {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {b : M} [LinearOrderedCommSemiring M] (hb : Fintype.card β • b < ↑(Fintype.card α)) : ∃ (y : β), b < ↑(Finset.filter (fun (x : α) => f x = y) Finset.univ).card

The strong pigeonhole principle for finitely many pigeons and pigeonholes. There is a pigeonhole with at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes.

theorem Fintype.exists_lt_card_fiber_of_mul_lt_card {α : Type u} {β : Type v} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {n : ℕ} (hn : Fintype.card β * n < Fintype.card α) : ∃ (y : β), n < (Finset.filter (fun (x : α) => f x = y) Finset.univ).card

The strong pigeonhole principle for finitely many pigeons and pigeonholes. There is a pigeonhole with at least as many pigeons as the ceiling of the average number of pigeons across all pigeonholes. ("The maximum is at least the mean" specialized to integers.)

More formally, given a function f between finite types α and β and a number n such that card β * n < card α, there exists an element y : β such that its preimage has more than n elements.

theorem Fintype.exists_card_fiber_lt_of_card_lt_nsmul {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {b : M} [LinearOrderedCommSemiring M] (hb : ↑(Fintype.card α) < Fintype.card β • b) : ∃ (y : β), ↑(Finset.filter (fun (x : α) => f x = y) Finset.univ).card < b

The strong pigeonhole principle for finitely many pigeons and pigeonholes. There is a pigeonhole with at most as many pigeons as the floor of the average number of pigeons across all pigeonholes.

theorem Fintype.exists_card_fiber_lt_of_card_lt_mul {α : Type u} {β : Type v} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {n : ℕ} (hn : Fintype.card α < Fintype.card β * n) : ∃ (y : β), (Finset.filter (fun (x : α) => f x = y) Finset.univ).card < n

The strong pigeonhole principle for finitely many pigeons and pigeonholes. There is a pigeonhole with at most as many pigeons as the floor of the average number of pigeons across all pigeonholes. ("The minimum is at most the mean" specialized to integers.)

More formally, given a function f between finite types α and β and a number n such that card α < card β * n, there exists an element y : β such that its preimage has less than n elements.

theorem Fintype.exists_le_card_fiber_of_nsmul_le_card {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {b : M} [LinearOrderedCommSemiring M] [Nonempty β] (hb : Fintype.card β • b ≤ ↑(Fintype.card α)) : ∃ (y : β), b ≤ ↑(Finset.filter (fun (x : α) => f x = y) Finset.univ).card

The strong pigeonhole principle for finitely many pigeons and pigeonholes. Given a function f between finite types α and β and a number b such that card β • b ≤ card α, there exists an element y : β such that its preimage has at least b elements. See also Fintype.exists_lt_card_fiber_of_nsmul_lt_card for a stronger statement.

theorem Fintype.exists_le_card_fiber_of_mul_le_card {α : Type u} {β : Type v} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {n : ℕ} [Nonempty β] (hn : Fintype.card β * n ≤ Fintype.card α) : ∃ (y : β), n ≤ (Finset.filter (fun (x : α) => f x = y) Finset.univ).card

The strong pigeonhole principle for finitely many pigeons and pigeonholes. Given a function f between finite types α and β and a number n such that card β * n ≤ card α, there exists an element y : β such that its preimage has at least n elements. See also Fintype.exists_lt_card_fiber_of_mul_lt_card for a stronger statement.

theorem Fintype.exists_card_fiber_le_of_card_le_nsmul {α : Type u} {β : Type v} {M : Type w} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {b : M} [LinearOrderedCommSemiring M] [Nonempty β] (hb : ↑(Fintype.card α) ≤ Fintype.card β • b) : ∃ (y : β), ↑(Finset.filter (fun (x : α) => f x = y) Finset.univ).card ≤ b

The strong pigeonhole principle for finitely many pigeons and pigeonholes. Given a function f between finite types α and β and a number b such that card α ≤ card β • b, there exists an element y : β such that its preimage has at most b elements. See also Fintype.exists_card_fiber_lt_of_card_lt_nsmul for a stronger statement.

theorem Fintype.exists_card_fiber_le_of_card_le_mul {α : Type u} {β : Type v} [DecidableEq β] [Fintype α] [Fintype β] (f : α → β) {n : ℕ} [Nonempty β] (hn : Fintype.card α ≤ Fintype.card β * n) : ∃ (y : β), (Finset.filter (fun (x : α) => f x = y) Finset.univ).card ≤ n

The strong pigeonhole principle for finitely many pigeons and pigeonholes. Given a function f between finite types α and β and a number n such that card α ≤ card β * n, there exists an element y : β such that its preimage has at most n elements. See also Fintype.exists_card_fiber_lt_of_card_lt_mul for a stronger statement.

theorem Nat.exists_lt_modEq_of_infinite {s : Set ℕ} (hs : s.Infinite) {k : ℕ} (hk : 0 < k) : ∃ m ∈ s, ∃ n ∈ s, m < n ∧ m ≡ n [MOD k]

If s is an infinite set of natural numbers and k > 0, then s contains two elements m < n that are equal mod k.