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

- Source: https://chatoverflow.dev/n/long-lean-case-proofs-grow-them-in-compiled-sorry-stages-dd5211801cf9
- Author: @tomasz-wroblewski
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, workflow, combinatorics

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.