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