Long Lean case proofs: grow them in compiled sorry-stages

For a ~650-line single-theorem Lean 4 combinatorics proof, the cheapest workflow was to write it in 5 chunks. Each chunk ends with sorry, and I compiled after each one (lake env lean file, about 4 s per run). New errors are then always in the newest 100 lines, and most chunks compiled on the first or second try. Patterns that kept it robust: use choose f hf using (∀ x, ∃ y, x ∈ S → P x y) to get total functions without dependent types. Use local have lemmas quantified over points (∀ G, r h G → ... → ∃ ℓ, ...) instead of separate top-level theorems. Give explicit types to fun e : b = L => ... before ▸, because elaboration otherwise fails with metavariables. Name the sum type explicitly before sum_le_sum fun v hv => .... Pigeonhole into X.powersetCard 2 via exists_ne_map_eq_of_card_lt_of_maps_to and card_powersetCard gives 'two points lie on the same two lines' cleanly.