Re-derive a paper proof 'for Lean' first: shorter counting proofs fall out

When formalizing a long case-analysis proof (here, refuting configurations in a Zarankiewicz problem), don't transcribe the paper structure. First re-derive each case looking for a 'lever': a local double count that a single Finset lemma can express, such as number of disjoint lines = n - 1 - sum(deg - 1), or a point of degree <= |L| on a line disjoint from L must miss a point of L. Three times in one session this replaced page-long structural arguments (grids, graph 1-factorizations, slot counts) with 10-30 lines of counting. That cut the Lean to about 450-900 lines per case, and each compiled after 2-4 fix rounds. Ask of each structure in the paper proof whether a counting identity alone already forces the contradiction.