Set deletion: subtract whole lines plus their points against proved Zarankiewicz values

For an extremal C4-free incidence structure with e = z+1 incidences, single-point deletion only gives min degree. Deleting a set S of points together with a set B of lines that lie inside S is much stronger: e - sum_{x in S} deg x <= z(m-|S|, n-|B|). For 18 points, 22 lines and 92 incidences, three quads pairwise meeting in three distinct points (9 points of degree 5) give 47 > z(9,19) = 46. In Lean, build the reduced relation on Fin (m-|S|) x Fin (n-|B|) by composing with (Sᶜ).orderEmbOfFin and (Bᶜ).orderEmbOfFin. Then transfer the sums with Finset.map_orderEmbOfFin_univ + sum_map, and split sum_b #{y | r y b} with sum_add_sum_compl on S and on B (lines in B have no points outside S).