The Sylvester-Gallai theorem in Lean 4

/-
# The Sylvester–Gallai theorem

Every finite set of points of a real inner product space which is not collinear admits an
*ordinary line*: a line through exactly two of the points.

The proof formalised here is Kelly's proof: among all pairs consisting of a point `p` of the set
and a connecting line `ℓ` (a line through two points of the set) with `p ∉ ℓ`, pick one minimising
the distance from `p` to `ℓ`.  If `ℓ` contained three points of the set, two of them, `B` and `C`,
would lie on the same side of the foot of the perpendicular from `p` to `ℓ`, with `B` the closer
one; then the distance from `B` to the line through `p` and `C` would be smaller, a contradiction.

Distances are handled through the Gram determinant `gram x y = ‖x‖²‖y‖² - ⟪x,y⟫²`, which is the
square of the area of the parallelogram spanned by `x` and `y`; this way only *squared* distances
occur and no square roots are needed.
-/

import Mathlib

open RealInnerProductSpace

namespace SylvesterGallai

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]

/-! ## The Gram determinant -/

/-- The Gram determinant of two vectors, `‖x‖²‖y‖² - ⟪x,y⟫²`.  It is the square of the area of
the parallelogram spanned by `x` and `y`. -/
noncomputable def gram (x y : V) : ℝ := ‖x‖ ^ 2 * ‖y‖ ^ 2 - ⟪x, y⟫ ^ 2

lemma gram_comm (x y : V) : gram x y = gram y x := by
  simp [gram, real_inner_comm x y]; ring

lemma gram_nonneg (x y : V) : 0 ≤ gram x y := by
  have h := abs_real_inner_le_norm x y
  have h2 : ⟪x, y⟫ ^ 2 ≤ (‖x‖ * ‖y‖) ^ 2 := by
    rw [← sq_abs]; exact pow_le_pow_left₀ (abs_nonneg _) h 2
  simp only [gram]; nlinarith

lemma gram_smul_left (r : ℝ) (x y : V) : gram (r • x) y = r ^ 2 * gram x y := by
  simp [gram, norm_smul, real_inner_smul_left, mul_pow]; ring

lemma gram_neg_right (x y : V) : gram x (-y) = gram x y := by simp [gram]

lemma gram_neg_left (x y : V) : gram (-x) y = gram x y := by simp [gram]

lemma norm_add_smul_sq (r : ℝ) (x y : V) :
    ‖y + r • x‖ ^ 2 = ‖y‖ ^ 2 + 2 * r * ⟪x, y⟫ + r ^ 2 * ‖x‖ ^ 2 := by
  rw [norm_add_sq_real]
  simp [real_inner_smul_right, norm_smul, mul_pow, real_inner_comm y x]
  ring

/-- Shearing invariance: adding a multiple of `x` to `y` does not change `gram x y`. -/
lemma gram_shear (r : ℝ) (x y : V) : gram x (y + r • x) = gram x y := by
  simp only [gram, norm_add_smul_sq, inner_add_right, real_inner_smul_right,
    real_inner_self_eq_norm_sq]
  ring

/-- The Gram determinant of the sides of a triangle does not depend on the chosen vertex. -/
lemma gram_tri (x y z : V) : gram (y - x) (z - x) = gram (z - y) (x - y) := by
  have h1 : x - y = -(y - x) := by module
  have h2 : z - y = (z - x) + (-1 : ℝ) • (y - x) := by module
  rw [h2, h1, gram_comm ((z - x) + (-1 : ℝ) • (y - x)) (-(y - x)), gram_neg_left, gram_shear]

lemma gram_eq_zero_iff {x y : V} (hx : x ≠ 0) : gram x y = 0 ↔ ∃ r : ℝ, y = r • x := by
  have hx2 : (0 : ℝ) < ‖x‖ ^ 2 := by positivity
  constructor
  · intro h
    refine ⟨⟪x, y⟫ / ‖x‖ ^ 2, ?_⟩
    have key : ‖y - (⟪x, y⟫ / ‖x‖ ^ 2) • x‖ ^ 2 = 0 := by
      rw [norm_sub_sq_real, real_inner_smul_right, real_inner_comm y x, norm_smul,
        Real.norm_eq_abs, mul_pow, sq_abs]
      simp only [gram] at h
      rw [← real_inner_comm x y] at h
      field_simp
      nlinarith [h]
    have h0 : y - (⟪x, y⟫ / ‖x‖ ^ 2) • x = 0 := by
      simpa using (pow_eq_zero_iff (n := 2) (by norm_num)).mp key
    exact sub_eq_zero.mp h0
  · rintro ⟨r, rfl⟩
    simp only [gram, real_inner_smul_right, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs,
      real_inner_self_eq_norm_sq]
    ring

/-! ## Lines -/

lemma mem_line_iff {a b x : V} : x ∈ line[ℝ, a, b] ↔ ∃ t : ℝ, x = a + t • (b - a) := by
  rw [mem_affineSpan_pair_iff_exists_lineMap_eq]
  simp only [AffineMap.lineMap_apply, vsub_eq_sub, vadd_eq_add]
  constructor
  · rintro ⟨t, rfl⟩; exact ⟨t, by abel⟩
  · rintro ⟨t, rfl⟩; exact ⟨t, by abel⟩

/-- The squared distance from the point `p` to the line through `a` and `b`. -/
noncomputable def sqDistLine (p a b : V) : ℝ := gram (b - a) (p - a) / ‖b - a‖ ^ 2

lemma sqDistLine_nonneg (p a b : V) : 0 ≤ sqDistLine p a b :=
  div_nonneg (gram_nonneg _ _) (by positivity)

lemma sqDistLine_eq_zero_iff {p a b : V} (hab : a ≠ b) :
    sqDistLine p a b = 0 ↔ p ∈ line[ℝ, a, b] := by
  have hv : b - a ≠ 0 := sub_ne_zero.mpr (Ne.symm hab)
  have hv2 : (0 : ℝ) < ‖b - a‖ ^ 2 := by positivity
  rw [sqDistLine, div_eq_zero_iff]
  constructor
  · rintro (h | h)
    · obtain ⟨r, hr⟩ := (gram_eq_zero_iff hv).mp h
      exact mem_line_iff.mpr ⟨r, by rw [← hr]; abel⟩
    · exact absurd h (by positivity)
  · intro h
    obtain ⟨t, ht⟩ := mem_line_iff.mp h
    left
    exact (gram_eq_zero_iff hv).mpr ⟨t, by rw [ht]; abel⟩

lemma sqDistLine_pos {p a b : V} (hab : a ≠ b) (hp : p ∉ line[ℝ, a, b]) :
    0 < sqDistLine p a b :=
  lt_of_le_of_ne (sqDistLine_nonneg _ _ _) fun h =>
    hp ((sqDistLine_eq_zero_iff hab).mp h.symm)

lemma gram_pos_of_not_mem_line {p a b : V} (hab : a ≠ b) (hp : p ∉ line[ℝ, a, b]) :
    0 < gram (b - a) (p - a) := by
  have hv2 : (0 : ℝ) < ‖b - a‖ ^ 2 := by
    have : b - a ≠ 0 := sub_ne_zero.mpr (Ne.symm hab)
    positivity
  have := sqDistLine_pos hab hp
  rw [sqDistLine, lt_div_iff₀ hv2] at this
  linarith

/-- On a line, a point is determined by its inner product with the direction vector. -/
lemma line_inner_inj {p a b X Y : V} (hab : a ≠ b) (hX : X ∈ line[ℝ, a, b])
    (hY : Y ∈ line[ℝ, a, b]) (h : ⟪X - p, b - a⟫ = ⟪Y - p, b - a⟫) : X = Y := by
  have hv : b - a ≠ 0 := sub_ne_zero.mpr (Ne.symm hab)
  have hv2 : (0 : ℝ) < ‖b - a‖ ^ 2 := by positivity
  obtain ⟨s, hs⟩ := mem_line_iff.mp hX
  obtain ⟨t, ht⟩ := mem_line_iff.mp hY
  have hd : ⟪X - Y, b - a⟫ = (s - t) * ‖b - a‖ ^ 2 := by
    have : X - Y = (s - t) • (b - a) := by rw [hs, ht]; module
    rw [this, real_inner_smul_left, real_inner_self_eq_norm_sq]
  have h0 : ⟪X - Y, b - a⟫ = 0 := by
    have : X - Y = (X - p) - (Y - p) := by abel
    rw [this, inner_sub_left, h, sub_self]
  have hst : s = t := by
    rw [h0] at hd
    have : s - t = 0 := by
      rcases mul_eq_zero.mp hd.symm with h' | h'
      · exact h'
      · exact absurd h' (by positivity)
    linarith
  rw [hs, ht, hst]

/-- If `p` is off the line `ab` and `B ≠ C` are two points of that line, then `B` is not on the
line through `p` and `C`. -/
lemma not_mem_line_aux {p a b B C : V} (hp : p ∉ line[ℝ, a, b])
    (hB : B ∈ line[ℝ, a, b]) (hC : C ∈ line[ℝ, a, b]) (hBC : B ≠ C) :
    B ∉ line[ℝ, p, C] := by
  intro hmem
  have hcol : Collinear ℝ ({B, p, C} : Set V) := collinear_insert_of_mem_affineSpan_pair hmem
  have hpBC : p ∈ line[ℝ, B, C] :=
    hcol.mem_affineSpan_of_mem_of_ne (by simp) (by simp) (by simp) hBC
  have hle : line[ℝ, B, C] ≤ line[ℝ, a, b] := affineSpan_pair_le_of_mem_of_mem hB hC
  exact hp (hle hpBC)

/-! ## Kelly's key inequality -/

/-- **Kelly's step.**  Let `p` be a point off the line `ab`, and let `B`, `C` be two distinct
points of that line lying on the same side of the foot of the perpendicular from `p`, with `B`
no further from the foot than `C` (this is expressed by the two hypotheses on the inner products
`⟪B - p, b - a⟫` and `⟪C - p, b - a⟫`, which are, up to a positive factor, the signed
coordinates of `B` and `C` relative to that foot).  Then `B` is strictly closer to the line `pC`
than `p` is to the line `ab`. -/
lemma kelly {p a b B C : V} (hab : a ≠ b) (hp : p ∉ line[ℝ, a, b])
    (hB : B ∈ line[ℝ, a, b]) (hC : C ∈ line[ℝ, a, b])
    (hsign : 0 ≤ ⟪B - p, b - a⟫ * ⟪C - p, b - a⟫)
    (hsq : ⟪B - p, b - a⟫ ^ 2 ≤ ⟪C - p, b - a⟫ ^ 2) :
    sqDistLine B p C < sqDistLine p a b := by
  have hv : b - a ≠ 0 := sub_ne_zero.mpr (Ne.symm hab)
  have hv2 : (0 : ℝ) < ‖b - a‖ ^ 2 := by positivity
  set v := b - a with hvdef
  obtain ⟨s, hs⟩ := mem_line_iff.mp hB
  obtain ⟨t, ht⟩ := mem_line_iff.mp hC
  set G := gram v (p - a) with hGdef
  have hG : 0 < G := gram_pos_of_not_mem_line hab hp
  set al := ⟪B - p, v⟫ with haldef
  set be := ⟪C - p, v⟫ with hbedef
  have hCp : (0 : ℝ) < ‖C - p‖ ^ 2 := by
    have h1 : C ≠ p := fun h => hp (h ▸ hC)
    have h2 : C - p ≠ 0 := sub_ne_zero.mpr h1
    positivity
  have F1 : gram (C - p) (B - p) = (t - s) ^ 2 * G := by
    have e1 : gram (C - p) (B - p) = gram (B - C) (p - C) := gram_tri p C B
    have e2 : B - C = (s - t) • v := by rw [hs, ht]; module
    have e3 : p - C = (p - a) + (-t) • v := by rw [ht]; module
    rw [e1, e2, e3, gram_smul_left, gram_shear]
    ring
  have F2 : ‖C - p‖ ^ 2 * ‖v‖ ^ 2 = G + be ^ 2 := by
    have e3 : C - p = -(p - a) + t • v := by rw [ht]; module
    have h1 : gram v (C - p) = G := by rw [e3, gram_shear, gram_neg_right]
    have h2 : ⟪v, C - p⟫ = be := real_inner_comm (C - p) v
    simp only [gram, h2] at h1
    linear_combination h1
  have F3 : be - al = (t - s) * ‖v‖ ^ 2 := by
    rw [haldef, hbedef, ← inner_sub_left]
    have e : C - p - (B - p) = (t - s) • v := by rw [hs, ht]; module
    rw [e, real_inner_smul_left, real_inner_self_eq_norm_sq]
  have hprod : al ^ 2 ≤ al * be := by
    nlinarith [hsign, hsq, sq_nonneg al, sq_nonneg (al * be - al ^ 2)]
  have hmain : (be - al) ^ 2 < G + be ^ 2 := by nlinarith [hprod, hsign, hG]
  rw [sqDistLine, sqDistLine, div_lt_div_iff₀ hCp hv2]
  have hLHS : gram (C - p) (B - p) * ‖v‖ ^ 2 * ‖v‖ ^ 2 = G * (be - al) ^ 2 := by
    rw [F1, F3]; ring
  have hRHS : G * ‖C - p‖ ^ 2 * ‖v‖ ^ 2 = G * (G + be ^ 2) := by rw [mul_assoc, F2]
  have hlt : gram (C - p) (B - p) * ‖v‖ ^ 2 * ‖v‖ ^ 2 < G * ‖C - p‖ ^ 2 * ‖v‖ ^ 2 := by
    rw [hLHS, hRHS]; exact mul_lt_mul_of_pos_left hmain hG
  nlinarith [hlt, hv2]

/-! ## Pigeonhole -/

/-- Among any three reals, two have a nonnegative product. -/
lemma exists_same_sign (x y z : ℝ) : 0 ≤ x * y ∨ 0 ≤ y * z ∨ 0 ≤ x * z := by
  rcases le_total 0 x with hx | hx <;> rcases le_total 0 y with hy | hy <;>
    rcases le_total 0 z with hz | hz <;>
    first
      | (left; nlinarith)
      | (right; left; nlinarith)
      | (right; right; nlinarith)

/-- Among three distinct reals there are two distinct ones, `f i` and `f j`, of the same sign
with `|f i| ≤ |f j|`. -/
lemma exists_pair_same_side (f : Fin 3 → ℝ) (hf : Function.Injective f) :
    ∃ i j, f i ≠ f j ∧ 0 ≤ f i * f j ∧ (f i) ^ 2 ≤ (f j) ^ 2 := by
  have key : ∀ i j : Fin 3, i ≠ j → 0 ≤ f i * f j →
      ∃ i' j', f i' ≠ f j' ∧ 0 ≤ f i' * f j' ∧ (f i') ^ 2 ≤ (f j') ^ 2 := by
    intro i j hij h
    rcases le_total ((f i) ^ 2) ((f j) ^ 2) with h' | h'
    · exact ⟨i, j, fun e => hij (hf e), h, h'⟩
    · exact ⟨j, i, fun e => hij (hf e).symm, by rwa [mul_comm], h'⟩
  rcases exists_same_sign (f 0) (f 1) (f 2) with h | h | h
  · exact key 0 1 (by decide) h
  · exact key 1 2 (by decide) h
  · exact key 0 2 (by decide) h

/-! ## The theorem -/

/-- **The Sylvester–Gallai theorem** in a real inner product space: a finite set of points that
is not collinear has an *ordinary line*, i.e. two of its points `a ≠ b` such that the line
through `a` and `b` contains no other point of the set. -/
theorem sylvester_gallai (S : Finset V) (hS : ¬ Collinear ℝ (S : Set V)) :
    ∃ a ∈ S, ∃ b ∈ S, a ≠ b ∧ ∀ p ∈ S, p ∈ line[ℝ, a, b] → p = a ∨ p = b := by
  classical
  -- `T` is the set of all triples `(p, a, b)` of points of `S` with `a ≠ b` and `p` off the
  -- line through `a` and `b`.
  set T : Finset (V × V × V) :=
    (S ×ˢ S ×ˢ S).filter (fun q => q.2.1 ≠ q.2.2 ∧ q.1 ∉ line[ℝ, q.2.1, q.2.2]) with hT
  have hmemT : ∀ q : V × V × V, q ∈ T ↔
      ((q.1 ∈ S ∧ q.2.1 ∈ S ∧ q.2.2 ∈ S) ∧ q.2.1 ≠ q.2.2 ∧ q.1 ∉ line[ℝ, q.2.1, q.2.2]) := by
    intro q
    simp [hT, Finset.mem_filter, Finset.mem_product, and_assoc]
  -- `S` is not collinear, so `T` is nonempty.
  have hTne : T.Nonempty := by
    rw [Finset.nonempty_iff_ne_empty]
    intro hempty
    apply hS
    rcases Finset.eq_empty_or_nonempty S with rfl | ⟨a, ha⟩
    · simpa using collinear_empty ℝ V
    by_cases hall : ∀ x ∈ S, x = a
    · exact (collinear_singleton ℝ a).subset (fun x hx => hall x hx)
    push_neg at hall
    obtain ⟨b, hb, hba⟩ := hall
    have hmem : ∀ x ∈ S, x ∈ line[ℝ, a, b] := by
      intro x hx
      by_contra hcon
      have : (x, a, b) ∈ T := (hmemT _).mpr ⟨⟨hx, ha, hb⟩, Ne.symm hba, hcon⟩
      rw [hempty] at this
      exact absurd this (Finset.notMem_empty _)
    rw [collinear_iff_of_mem (show a ∈ (S : Set V) from ha)]
    refine ⟨b - a, fun x hx => ?_⟩
    obtain ⟨r, hr⟩ := mem_line_iff.mp (hmem x hx)
    exact ⟨r, by rw [hr]; simp [add_comm]⟩
  -- Choose a triple minimising the distance from the point to the line.
  obtain ⟨⟨p, a, b⟩, hqT, hmin⟩ :=
    T.exists_min_image (fun q => sqDistLine q.1 q.2.1 q.2.2) hTne
  obtain ⟨⟨hpS, haS, hbS⟩, hab, hp⟩ := (hmemT _).mp hqT
  refine ⟨a, haS, b, hbS, hab, ?_⟩
  -- Suppose the line through `a` and `b` contained a third point `c` of `S`.
  intro c hcS hc
  by_contra hcon
  push_neg at hcon
  obtain ⟨hca, hcb⟩ := hcon
  set P : Fin 3 → V := ![a, b, c] with hP
  have hPS : ∀ i, P i ∈ S := by intro i; fin_cases i <;> assumption
  have hPline : ∀ i, P i ∈ line[ℝ, a, b] := by
    intro i
    fin_cases i
    · exact left_mem_affineSpan_pair ℝ a b
    · exact right_mem_affineSpan_pair ℝ a b
    · exact hc
  have hPinj : Function.Injective P := by
    intro i j hij
    fin_cases i <;> fin_cases j <;> simp_all
  set f : Fin 3 → ℝ := fun i => ⟪P i - p, b - a⟫ with hf
  have hfinj : Function.Injective f :=
    fun i j hij => hPinj (line_inner_inj hab (hPline i) (hPline j) hij)
  obtain ⟨i, j, hne, hsign, hsq⟩ := exists_pair_same_side f hfinj
  have hBC : P i ≠ P j := fun h => hne (by rw [hf]; simp only [h])
  have hlt : sqDistLine (P i) p (P j) < sqDistLine p a b :=
    kelly hab hp (hPline i) (hPline j) hsign hsq
  have hpj : p ≠ P j := fun h => hp (h ▸ hPline j)
  have hmemT' : (P i, p, P j) ∈ T :=
    (hmemT _).mpr ⟨⟨hPS i, hpS, hPS j⟩, hpj, not_mem_line_aux hp (hPline i) (hPline j) hBC⟩
  exact absurd (hmin _ hmemT') (not_le.mpr hlt)

/-- The Sylvester–Gallai theorem in the Euclidean plane. -/
theorem sylvester_gallai_plane (S : Finset (EuclideanSpace ℝ (Fin 2)))
    (hS : ¬ Collinear ℝ (S : Set (EuclideanSpace ℝ (Fin 2)))) :
    ∃ a ∈ S, ∃ b ∈ S, a ≠ b ∧ ∀ p ∈ S, p ∈ line[ℝ, a, b] → p = a ∨ p = b :=
  sylvester_gallai S hS

/-- The same statement, phrased as: some connecting line meets the set in exactly two points. -/
theorem sylvester_gallai_plane' (S : Finset (EuclideanSpace ℝ (Fin 2)))
    (hS : ¬ Collinear ℝ (S : Set (EuclideanSpace ℝ (Fin 2)))) :
    ∃ a ∈ S, ∃ b ∈ S, a ≠ b ∧
      (S : Set (EuclideanSpace ℝ (Fin 2))) ∩ (line[ℝ, a, b] : Set _) = {a, b} := by
  obtain ⟨a, ha, b, hb, hab, h⟩ := sylvester_gallai_plane S hS
  refine ⟨a, ha, b, hb, hab, ?_⟩
  ext x
  simp only [Set.mem_inter_iff, Set.mem_insert_iff, Set.mem_singleton_iff,
    SetLike.mem_coe]
  constructor
  · rintro ⟨hx, hx'⟩; exact h x hx hx'
  · rintro (rfl | rfl)
    · exact ⟨ha, left_mem_affineSpan_pair ℝ _ _⟩
    · exact ⟨hb, right_mem_affineSpan_pair ℝ _ _⟩

/-! ## A sanity check: the hypothesis is satisfiable -/

/-- The three vertices of a right triangle in the plane are not collinear, so the hypothesis of
the theorem above is not vacuous. -/
example : ¬ Collinear ℝ
    ({!₂[(0:ℝ), 0], !₂[(1:ℝ), 0], !₂[(0:ℝ), 1]} : Set (EuclideanSpace ℝ (Fin 2))) := by
  intro h
  rw [collinear_iff_of_mem (show (!₂[(0:ℝ), 0] : EuclideanSpace ℝ (Fin 2)) ∈ _ by simp)] at h
  obtain ⟨v, hv⟩ := h
  obtain ⟨r, hr⟩ := hv !₂[(1:ℝ), 0] (by simp)
  obtain ⟨s, hs⟩ := hv !₂[(0:ℝ), 1] (by simp)
  have h1 := congrFun (congrArg WithLp.ofLp hr) 0
  have h4 := congrFun (congrArg WithLp.ofLp hs) 1
  have h3 := congrFun (congrArg WithLp.ofLp hs) 0
  simp at h1 h3 h4
  rcases h3 with h3 | h3 <;> simp [h3] at h1 h4

#print axioms SylvesterGallai.sylvester_gallai_plane
#print axioms SylvesterGallai.sylvester_gallai_plane'

end SylvesterGallai