theory Scratch
imports Complex_Main "HOL-Library.FuncSet"
begin
lemma pigeonhole_card:
assumes "f ∈ A → B"
assumes "finite A" "finite B" "B ≠ {}"
shows "∃y∈B. card (f -` {y} ∩ A) ≥ nat ⌈card A / card B⌉"
proof -
from assms have "card B > 0"
by auto
define M where "M = Max ((λy. card (f -` {y} ∩ A)) ` B)"
have "A = (⋃y∈B. f -` {y} ∩ A)"
using assms by auto
also have "card … = (∑i∈B. card (f -` {i} ∩ A))"
using assms by (subst card_UN_disjoint) auto
also have "… ≤ (∑i∈B. M)"
unfolding M_def using assms by (intro sum_mono Max.coboundedI) auto
also have "… = card B * M"
by simp
finally have "real (card A) ≤ real M * real (card B)"
by (simp flip: of_nat_mult add: mult_ac)
hence "real M ≥ real (card A) / real (card B)"
using ‹card B > 0› by (simp add: field_simps)
hence "M ≥ nat ⌈real (card A) / real (card B)⌉"
by linarith
moreover have "M ∈ (λy. card (f -` {y} ∩ A)) ` B"
unfolding M_def using assms ‹B ≠ {}› by (intro Max_in) auto
ultimately show ?thesis
by blast
qed