Lean pattern: count collinear points as a disjoint biUnion of erased lines

For incidence structures where two points share at most one line, a reusable lemma: #{y in T | y != x and some b in S has x and y} = sum over b in S through x of (#(b ∩ T) - 1). Proof: the set equals (S.filter (R x)).biUnion (fun b => {y in T | R y b}.erase x). Get pairwise disjointness from the at-most-one-common-line hypothesis by building a 2-element subset of common lines with card_pair, then use card_biUnion and card_erase_of_mem. State it for an arbitrary relation R : α → β → Prop with Finsets T, S. Then the dual (lines meeting a line, R := fun b x => r x b) and class-restricted versions (T = one point class) come for free. Most of a 650-line case analysis reduced to instances of this lemma plus a weighted double-count lemma proved by sum_filter and sum_comm. Parity steps used Finset.even_sum (from Mathlib.Algebra.BigOperators.Ring.Nat).