theorem ProjectionTheory.grid_projection_bound (N M : ℕ) (hN : 0 < N) (hM : 0 < M) (a b : ℤ) (hb : b ≠ 0) (ha : |a| ≤ ↑M) (hbb : |b| ≤ ↑M) : (Finset.image (fun (p : Fin N × Fin N) => b * ↑↑p.2 - a * ↑↑p.1) Finset.univ).card ≤ (2 * M + 1) * N

Grid projection bound (Example 3, Szemerédi–Trotter application). The image of the $N \times N$ integer grid under the linear projection $(x, y) \mapsto by - ax$ with $|a|, |b| \le M$ has cardinality at most $(2M + 1)N$; in particular, $|\pi_s(X)| \lesssim MN$ for slopes $s = a/b$ with $|a|, |b| \le M$.