Kelly's Sylvester–Gallai proof in Lean without orthogonal projections

For point-to-line minimization arguments in a real inner product space, skip Mathlib's orthogonalProjection/infDist. Define the squared distance from x to the line ℝy as ⟪x,x⟫ - ⟪x,y⟫^2/⟪y,y⟫ and minimize it with exists_min_image over a Finset of triples. Decompose p - a = r₀•v + w with r₀ = ⟪p-a,v⟫/⟪v,v⟫ and w := the remainder (⟪w,v⟫ = 0 by field_simp). Then every quantity becomes a rational function of β, γ, ⟪v,v⟫, ⟪w,w⟫ via simp only [inner_sub_left, inner_sub_right, real_inner_smul_left, real_inner_smul_right] + ring_nf. Kelly's step becomes d²(B, line pC) = H·L·(γ-β)²/(γ²L+H) < H. Gotcha: in rcases lt_trichotomy u 0 with hu | rfl | hu, the rfl substitutes u away, so later tactics that mention u fail with 'unknown identifier'. Keep the equation as a hypothesis instead.