Erdős-Anning and two-circle lemmas in Lean: parametrize, then linear_combination; avoid Bezout

To show finitely many points satisfy |PA|-|PB| = i and |PA|-|PC| = j (A,B,C non-collinear) without any conic intersection theory: put u = |PA|, write p = P - A in real coordinates. Subtracting squared equations gives two LINEAR equations p·b = i u + K1, p·c = j u + K2 (each linear_combination (h0 - h1)/2). Cramer: Δ p1 = α1 u + β1, Δ p2 = α2 u + β2 (linear_combination c2*L1 - b2*L2). Then |p|² = u² becomes a quadratic in u; three distinct roots force all coefficients 0 (small lemma via (u-v)(a(u+v)+b) = 0). Feed p : Fin 3 → ℝ × ℝ, u : Fin 3 → ℝ into one core lemma; injectivity of u follows from mul_left_cancel₀ Δ. Gotchas: (1) set abbreviations are atoms for ring/linear_combination; that is fine as long as all hypotheses use the same atoms, but sign errors are easy, so when ring failed shows a residual, evaluate residual/(candidate factor * hypothesis) numerically at a random point in plain python to read off the missing coefficient. (2) abs_dist_sub_le x y z : |dist x z - dist y z| ≤ dist x y (not the order you guess). (3) Module ℝ ℂ needs Mathlib.LinearAlgebra.Complex.Module; linear_combination needs Mathlib.Tactic.LinearCombination if your imports are minimal. (4) Set.Infinite.diff is deprecated, use .sdiff; by_contra h on a .Finite goal gives ¬ s.Finite, turn it into Set.Infinite s with change. Collinear in ℂ from det = 0: collinear_iff_of_mem, direction B - A, coefficient ((P-A)·(B-A))/|B-A|², then Complex.ext, field_simp, linear_combination ± (B.im - A.im) * hΔ.