/-- **The pigeonhole principle** for the values `f 0, f 1, …, f b`: if all `b + 1` of them are
less than `b`, two of them are equal. Proof by induction on `b`: either `f (b + 1)` already
appeared, or we relabel the value `b` as `f (b + 1)` and use the induction hypothesis. -/
theorem pigeonhole : ∀ (b : Nat) (f : Nat → Nat), (∀ k, k ≤ b → f k < b) →
∃ i j, i < j ∧ j ≤ b ∧ f i = f j := by
intro b
induction b with
| zero =>
intro f hf
exact absurd (hf 0 (Nat.le_refl 0)) (Nat.not_lt_zero _)
| succ b ih =>
intro f hf
by_cases hrep : ∃ k, k ≤ b ∧ f k = f (b + 1)
· obtain ⟨k, hk, hfk⟩ := hrep
exact ⟨k, b + 1, by omega, Nat.le_refl _, hfk⟩
· -- `f (b + 1)` is new. Replace the value `b` (if it occurs) by `f (b + 1)`.
have hnew : ∀ k, k ≤ b → f k ≠ f (b + 1) := fun k hk h => hrep ⟨k, hk, h⟩
let g : Nat → Nat := fun k => if f k = b then f (b + 1) else f k
have hg : ∀ k, k ≤ b → g k < b := by
intro k hk
have h1 := hf k (by omega)
have h2 := hf (b + 1) (Nat.le_refl _)
have h3 := hnew k hk
simp only [g]
split <;> omega
obtain ⟨i, j, hij, hjb, hgij⟩ := ih g hg
refine ⟨i, j, hij, by omega, ?_⟩
have hi := hnew i (by omega)
have hj := hnew j hjb
simp only [g] at hgij
split at hgij <;> split at hgij <;> omega