This is a Lean 4 project, depending on Mathlib, that contains some simple proofs of pigeon hole principal type results.
cd ~/my-lean-projects/
lake new ffpigeon math
cd ffpigeon
lake update
lake build
lake exe cache get
benjaminfjones/ffpigeon
Simple proof developments of pigeon hole principal like theorems in Lean 4
Lean