/-
SPDX-FileCopyrightText: 2026 Advameg, Inc.
SPDX-License-Identifier: Apache-2.0
-/

import Mathlib.Data.Real.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Max
import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
import Mathlib.Tactic

/-!
# Sylvester-Gallai Theorem Seed

This file sets up an independent Atlas route for the Sylvester-Gallai theorem.
The first target is the ordinary-line statement for finite point sets in the
real affine plane, using an explicit determinant-based collinearity predicate.
The later stretch direction is to connect this interface to mathlib's affine
geometry `Collinear` API.
-/

namespace AtlasKnownTheorems.SylvesterGallai

/-- Concrete real affine-plane points for the first Sylvester-Gallai route. -/
abbrev Point : Type := ℝ × ℝ

/-- Translate a concrete point by a concrete vector. -/
def translatePoint (v p : Point) : Point :=
  (p.1 + v.1, p.2 + v.2)

/-- Uniformly scale a concrete point about the origin. -/
def scalePoint (s : ℝ) (p : Point) : Point :=
  (s * p.1, s * p.2)

/-- The linear map represented by the complex number `u + iv`. -/
def rotateScalePoint (u v : ℝ) (p : Point) : Point :=
  (u * p.1 - v * p.2, v * p.1 + u * p.2)

/-- Squared norm of the complex scalar used by `rotateScalePoint`. -/
def scalarNormSq (u v : ℝ) : ℝ :=
  u ^ 2 + v ^ 2

theorem scalarNormSq_pos {u v : ℝ} (h : u ≠ 0 ∨ v ≠ 0) : 0 < scalarNormSq u v := by
  unfold scalarNormSq
  rcases h with hu | hv
  · nlinarith [sq_pos_of_ne_zero hu, sq_nonneg v]
  · nlinarith [sq_nonneg u, sq_pos_of_ne_zero hv]

theorem translatePoint_injective (v : Point) :
    Function.Injective (translatePoint v) := by
  intro p q h
  ext
  · have hx := congrArg Prod.fst h
    simp [translatePoint] at hx
    linarith
  · have hy := congrArg Prod.snd h
    simp [translatePoint] at hy
    linarith

theorem scalePoint_injective {s : ℝ} (hs : s ≠ 0) :
    Function.Injective (scalePoint s) := by
  intro p q h
  ext
  · have hx := congrArg Prod.fst h
    simp [scalePoint] at hx
    exact hx.resolve_right hs
  · have hy := congrArg Prod.snd h
    simp [scalePoint] at hy
    exact hy.resolve_right hs

theorem rotateScalePoint_injective {u v : ℝ} (hscalar : u ≠ 0 ∨ v ≠ 0) :
    Function.Injective (rotateScalePoint u v) := by
  intro p q h
  have hx := congrArg Prod.fst h
  have hy := congrArg Prod.snd h
  simp [rotateScalePoint] at hx hy
  have hnorm : scalarNormSq u v ≠ 0 := ne_of_gt (scalarNormSq_pos hscalar)
  have hxf :
      (u * p.1 - v * p.2) - (u * q.1 - v * q.2) = 0 := sub_eq_zero.mpr hx
  have hyf :
      (v * p.1 + u * p.2) - (v * q.1 + u * q.2) = 0 := sub_eq_zero.mpr hy
  have hxmul : scalarNormSq u v * (p.1 - q.1) = 0 := by
    calc
      scalarNormSq u v * (p.1 - q.1)
          = u * ((u * p.1 - v * p.2) - (u * q.1 - v * q.2)) +
              v * ((v * p.1 + u * p.2) - (v * q.1 + u * q.2)) := by
            unfold scalarNormSq
            ring
      _ = 0 := by rw [hxf, hyf]; ring
  have hymul : scalarNormSq u v * (p.2 - q.2) = 0 := by
    calc
      scalarNormSq u v * (p.2 - q.2)
          = -v * ((u * p.1 - v * p.2) - (u * q.1 - v * q.2)) +
              u * ((v * p.1 + u * p.2) - (v * q.1 + u * q.2)) := by
            unfold scalarNormSq
            ring
      _ = 0 := by rw [hxf, hyf]; ring
  have hx0 : p.1 - q.1 = 0 := (mul_eq_zero.mp hxmul).resolve_left hnorm
  have hy0 : p.2 - q.2 = 0 := (mul_eq_zero.mp hymul).resolve_left hnorm
  ext <;> linarith

/-- Twice the signed area of the triangle `p q r`. -/
def orientationDet (p q r : Point) : ℝ :=
  (q.1 - p.1) * (r.2 - p.2) - (q.2 - p.2) * (r.1 - p.1)

/-- Three concrete plane points are collinear when their orientation determinant vanishes. -/
def Collinear3 (p q r : Point) : Prop :=
  orientationDet p q r = 0

/-- Ordered triples of points from a finite point set. -/
def pointTriples (S : Finset Point) : Finset (Point × Point × Point) :=
  S.product (S.product S)

/-- Ordered triples from `S` whose determinant collinearity test is nonzero. -/
noncomputable def noncollinearTriples (S : Finset Point) : Finset (Point × Point × Point) :=
  by
    classical
    exact (pointTriples S).filter fun t => ¬ Collinear3 t.1 t.2.1 t.2.2

/-- Absolute determinant area attached to an ordered point triple. -/
def tripleAbsDet (t : Point × Point × Point) : ℝ :=
  |orientationDet t.1 t.2.1 t.2.2|

/-- Squared Euclidean distance between two concrete points. -/
def squaredDist (a b : Point) : ℝ :=
  (b.1 - a.1) ^ 2 + (b.2 - a.2) ^ 2

theorem scalarNormSq_base (a b : Point) :
    scalarNormSq (b.1 - a.1) (-(b.2 - a.2)) = squaredDist a b := by
  unfold scalarNormSq squaredDist
  ring

/-- `c` lies strictly between `a` and `b` in affine-line coordinates based at `a`. -/
def StrictLineBetween (a b c : Point) : Prop :=
  ∃ t : ℝ, 0 < t ∧ t < 1 ∧ c = t • (b -ᵥ a) +ᵥ a

/--
Squared point-to-line distance up to the usual determinant formula. For
non-collinear triples the denominator is positive.
-/
noncomputable def linePointScore (t : Point × Point × Point) : ℝ :=
  (orientationDet t.1 t.2.1 t.2.2) ^ 2 / squaredDist t.1 t.2.1

theorem mem_pointTriples {S : Finset Point} {t : Point × Point × Point} :
    t ∈ pointTriples S ↔ t.1 ∈ S ∧ t.2.1 ∈ S ∧ t.2.2 ∈ S := by
  simp [pointTriples]

theorem mem_noncollinearTriples {S : Finset Point} {t : Point × Point × Point} :
    t ∈ noncollinearTriples S ↔
      t.1 ∈ S ∧ t.2.1 ∈ S ∧ t.2.2 ∈ S ∧ ¬ Collinear3 t.1 t.2.1 t.2.2 := by
  classical
  simp [noncollinearTriples, pointTriples, and_assoc]

/-- A finite point set is collinear if all its points lie on one line through two of its points. -/
def FinsetCollinear (S : Finset Point) : Prop :=
  ∃ a ∈ S, ∃ b ∈ S, a ≠ b ∧ ∀ c ∈ S, Collinear3 a b c

/--
`a` and `b` determine an ordinary line for `S`: the line through them contains
no point of `S` except `a` and `b`.
-/
def OrdinaryPair (S : Finset Point) (a b : Point) : Prop :=
  a ∈ S ∧ b ∈ S ∧ a ≠ b ∧
    ∀ c ∈ S, Collinear3 a b c → c = a ∨ c = b

/--
Sylvester-Gallai over finite subsets of the real affine plane.

Every finite non-collinear set of at least three points has an ordinary line.
-/
def SylvesterGallaiStatement : Prop :=
  ∀ S : Finset Point, 2 < S.card → ¬ FinsetCollinear S →
    ∃ a b : Point, OrdinaryPair S a b

theorem orientationDet_left_self (p q : Point) :
    orientationDet p p q = 0 := by
  unfold orientationDet
  ring

theorem orientationDet_right_self (p q : Point) :
    orientationDet p q p = 0 := by
  unfold orientationDet
  ring

theorem orientationDet_right_endpoint_self (p q : Point) :
    orientationDet p q q = 0 := by
  unfold orientationDet
  ring

theorem orientationDet_swap_left (p q r : Point) :
    orientationDet q p r = -orientationDet p q r := by
  unfold orientationDet
  ring

theorem orientationDet_swap_right (p q r : Point) :
    orientationDet p r q = -orientationDet p q r := by
  unfold orientationDet
  ring

theorem orientationDet_rotate_left (p q r : Point) :
    orientationDet q r p = orientationDet p q r := by
  unfold orientationDet
  ring

theorem orientationDet_rotate_right (p q r : Point) :
    orientationDet r p q = orientationDet p q r := by
  unfold orientationDet
  ring

theorem orientationDet_translate (v p q r : Point) :
    orientationDet (translatePoint v p) (translatePoint v q) (translatePoint v r) =
      orientationDet p q r := by
  unfold orientationDet translatePoint
  ring

theorem orientationDet_scale (s : ℝ) (p q r : Point) :
    orientationDet (scalePoint s p) (scalePoint s q) (scalePoint s r) =
      s ^ 2 * orientationDet p q r := by
  unfold orientationDet scalePoint
  ring

theorem orientationDet_rotateScale (u v : ℝ) (p q r : Point) :
    orientationDet (rotateScalePoint u v p) (rotateScalePoint u v q) (rotateScalePoint u v r) =
      scalarNormSq u v * orientationDet p q r := by
  unfold orientationDet rotateScalePoint scalarNormSq
  ring

theorem collinear3_left_self (p q : Point) :
    Collinear3 p p q := by
  simp [Collinear3, orientationDet_left_self]

theorem collinear3_right_self (p q : Point) :
    Collinear3 p q p := by
  simp [Collinear3, orientationDet_right_self]

theorem collinear3_right_endpoint_self (p q : Point) :
    Collinear3 p q q := by
  simp [Collinear3, orientationDet_right_endpoint_self]

theorem squaredDist_nonneg (a b : Point) : 0 ≤ squaredDist a b := by
  unfold squaredDist
  nlinarith [sq_nonneg (b.1 - a.1), sq_nonneg (b.2 - a.2)]

theorem squaredDist_pos_of_ne {a b : Point} (h : a ≠ b) : 0 < squaredDist a b := by
  unfold squaredDist
  by_contra hnonpos
  have hle : (b.1 - a.1) ^ 2 + (b.2 - a.2) ^ 2 ≤ 0 := le_of_not_gt hnonpos
  have hx0 : b.1 - a.1 = 0 := by
    nlinarith [sq_nonneg (b.1 - a.1), sq_nonneg (b.2 - a.2)]
  have hy0 : b.2 - a.2 = 0 := by
    nlinarith [sq_nonneg (b.1 - a.1), sq_nonneg (b.2 - a.2)]
  apply h
  ext <;> linarith

theorem squaredDist_smul_vsub_vadd (a b : Point) (t : ℝ) :
    squaredDist a (t • (b -ᵥ a) +ᵥ a) = t ^ 2 * squaredDist a b := by
  unfold squaredDist
  simp
  ring

theorem squaredDist_lineMap_lineMap (a b : Point) (s t : ℝ) :
    squaredDist (s • (b -ᵥ a) +ᵥ a) (t • (b -ᵥ a) +ᵥ a) =
      (t - s) ^ 2 * squaredDist a b := by
  unfold squaredDist
  simp
  ring

theorem squaredDist_translate (v a b : Point) :
    squaredDist (translatePoint v a) (translatePoint v b) = squaredDist a b := by
  unfold squaredDist translatePoint
  ring

theorem squaredDist_scale (s : ℝ) (a b : Point) :
    squaredDist (scalePoint s a) (scalePoint s b) = s ^ 2 * squaredDist a b := by
  unfold squaredDist scalePoint
  ring

theorem squaredDist_rotateScale (u v : ℝ) (a b : Point) :
    squaredDist (rotateScalePoint u v a) (rotateScalePoint u v b) =
      scalarNormSq u v * squaredDist a b := by
  unfold squaredDist rotateScalePoint scalarNormSq
  ring

theorem collinear3_swap_left {p q r : Point}
    (h : Collinear3 p q r) : Collinear3 q p r := by
  rw [Collinear3, orientationDet_swap_left, h, neg_zero]

theorem collinear3_swap_right {p q r : Point}
    (h : Collinear3 p q r) : Collinear3 p r q := by
  rw [Collinear3, orientationDet_swap_right, h, neg_zero]

theorem collinear3_rotate_left {p q r : Point}
    (h : Collinear3 p q r) : Collinear3 q r p := by
  rw [Collinear3, orientationDet_rotate_left, h]

theorem collinear3_rotate_right {p q r : Point}
    (h : Collinear3 p q r) : Collinear3 r p q := by
  rw [Collinear3, orientationDet_rotate_right, h]

theorem collinear3_of_affine_collinear {p q r : Point}
    (h : Collinear ℝ ({p, q, r} : Set Point)) : Collinear3 p q r := by
  rw [collinear_iff_exists_forall_eq_smul_vadd] at h
  rcases h with ⟨p₀, v, hv⟩
  rcases hv p (by simp) with ⟨tp, hp⟩
  rcases hv q (by simp) with ⟨tq, hq⟩
  rcases hv r (by simp) with ⟨tr, hr⟩
  subst p
  subst q
  subst r
  simp [Collinear3, orientationDet]
  ring

theorem affine_collinear_of_collinear3 {p q r : Point}
    (h : Collinear3 p q r) : Collinear ℝ ({p, q, r} : Set Point) := by
  by_cases hpq : p = q
  · subst q
    simpa using (collinear_pair ℝ p r)
  · have hdet :
        (q.1 - p.1) * (r.2 - p.2) - (q.2 - p.2) * (r.1 - p.1) = 0 := by
      simpa [Collinear3, orientationDet] using h
    have hmul :
        (q.1 - p.1) * (r.2 - p.2) = (q.2 - p.2) * (r.1 - p.1) := by
      linarith
    have hnonzero : q.1 - p.1 ≠ 0 ∨ q.2 - p.2 ≠ 0 := by
      by_contra hzero
      push Not at hzero
      apply hpq
      ext <;> linarith
    have hrline : r ∈ line[ℝ, p, q] := by
      rw [← vsub_vadd r p, vadd_left_mem_affineSpan_pair]
      rcases hnonzero with hdx | hdy
      · refine ⟨(r.1 - p.1) / (q.1 - p.1), ?_⟩
        ext
        · simp
          field_simp [hdx]
        · simp
          calc
            (r.1 - p.1) / (q.1 - p.1) * (q.2 - p.2)
                = ((q.2 - p.2) * (r.1 - p.1)) / (q.1 - p.1) := by ring
            _ = ((q.1 - p.1) * (r.2 - p.2)) / (q.1 - p.1) := by rw [← hmul]
            _ = r.2 - p.2 := by field_simp [hdx]
      · refine ⟨(r.2 - p.2) / (q.2 - p.2), ?_⟩
        ext
        · simp
          calc
            (r.2 - p.2) / (q.2 - p.2) * (q.1 - p.1)
                = ((q.1 - p.1) * (r.2 - p.2)) / (q.2 - p.2) := by ring
            _ = ((q.2 - p.2) * (r.1 - p.1)) / (q.2 - p.2) := by rw [hmul]
            _ = r.1 - p.1 := by field_simp [hdy]
        · simp
          field_simp [hdy]
    convert
      (collinear_insert_of_mem_affineSpan_pair (k := ℝ) (p₁ := r) (p₂ := p) (p₃ := q) hrline)
      using 1
    ext x
    simp [or_left_comm, or_comm]

theorem collinear3_iff_affine_collinear {p q r : Point} :
    Collinear3 p q r ↔ Collinear ℝ ({p, q, r} : Set Point) :=
  ⟨affine_collinear_of_collinear3, collinear3_of_affine_collinear⟩

theorem mem_line_of_collinear3 {a b c : Point}
    (hab : a ≠ b) (h : Collinear3 a b c) : c ∈ line[ℝ, a, b] := by
  have hcol : Collinear ℝ ({a, b, c} : Set Point) :=
    collinear3_iff_affine_collinear.1 h
  exact hcol.mem_affineSpan_of_mem_of_ne (by simp) (by simp) (by simp) hab

theorem exists_line_parameter_of_collinear3 {a b c : Point}
    (hab : a ≠ b) (h : Collinear3 a b c) :
    ∃ t : ℝ, c = t • (b -ᵥ a) +ᵥ a := by
  have hc_line : c ∈ line[ℝ, a, b] := mem_line_of_collinear3 hab h
  rw [← vsub_vadd c a, vadd_left_mem_affineSpan_pair] at hc_line
  rcases hc_line with ⟨t, ht⟩
  exact ⟨t, by rw [ht, vsub_vadd]⟩

theorem collinear3_of_mem_line {a b x y z : Point}
    (hx : x ∈ line[ℝ, a, b]) (hy : y ∈ line[ℝ, a, b]) (hz : z ∈ line[ℝ, a, b]) :
    Collinear3 x y z := by
  apply collinear3_of_affine_collinear
  exact collinear_triple_of_mem_affineSpan_pair hx hy hz

theorem orientationDet_smul_vsub_vadd_left (a b p : Point) (t : ℝ) :
    orientationDet a (t • (b -ᵥ a) +ᵥ a) p =
      t * orientationDet a b p := by
  unfold orientationDet
  simp
  ring

theorem orientationDet_lineMap_lineMap (a b p : Point) (s t : ℝ) :
    orientationDet (s • (b -ᵥ a) +ᵥ a) (t • (b -ᵥ a) +ᵥ a) p =
      (t - s) * orientationDet a b p := by
  unfold orientationDet
  simp
  ring

theorem orientationDet_smul_vsub_vadd_right (a b p : Point) (t : ℝ) :
    orientationDet a b (t • (p -ᵥ a) +ᵥ a) =
      t * orientationDet a b p := by
  unfold orientationDet
  simp
  ring

theorem abs_orientationDet_smul_vsub_vadd_left (a b p : Point) (t : ℝ) :
    |orientationDet a (t • (b -ᵥ a) +ᵥ a) p| =
      |t| * |orientationDet a b p| := by
  rw [orientationDet_smul_vsub_vadd_left, abs_mul]

theorem abs_orientationDet_smul_vsub_vadd_right (a b p : Point) (t : ℝ) :
    |orientationDet a b (t • (p -ᵥ a) +ᵥ a)| =
      |t| * |orientationDet a b p| := by
  rw [orientationDet_smul_vsub_vadd_right, abs_mul]

theorem tripleAbsDet_smul_vsub_vadd_left_lt {a b p : Point} {t : ℝ}
    (ht : |t| < 1) (hdet : ¬ Collinear3 a b p) :
    tripleAbsDet (a, t • (b -ᵥ a) +ᵥ a, p) < tripleAbsDet (a, b, p) := by
  have hpos : 0 < |orientationDet a b p| := by
    exact abs_pos.mpr hdet
  rw [tripleAbsDet, tripleAbsDet, abs_orientationDet_smul_vsub_vadd_left]
  nlinarith [abs_nonneg t]

theorem tripleAbsDet_smul_vsub_vadd_right_lt {a b p : Point} {t : ℝ}
    (ht : |t| < 1) (hdet : ¬ Collinear3 a b p) :
    tripleAbsDet (a, b, t • (p -ᵥ a) +ᵥ a) < tripleAbsDet (a, b, p) := by
  have hpos : 0 < |orientationDet a b p| := by
    exact abs_pos.mpr hdet
  rw [tripleAbsDet, tripleAbsDet, abs_orientationDet_smul_vsub_vadd_right]
  nlinarith [abs_nonneg t]

theorem tripleAbsDet_swap_left (a b p : Point) :
    tripleAbsDet (b, a, p) = tripleAbsDet (a, b, p) := by
  rw [tripleAbsDet, tripleAbsDet, orientationDet_swap_left, abs_neg]

theorem strictLineBetween_collinear3 {a b c : Point}
    (h : StrictLineBetween a b c) : Collinear3 a b c := by
  rcases h with ⟨t, _ht0, _ht1, rfl⟩
  rw [Collinear3, orientationDet_smul_vsub_vadd_right, orientationDet_right_endpoint_self, mul_zero]

theorem strictLineBetween_symm {a b c : Point}
    (h : StrictLineBetween a b c) : StrictLineBetween b a c := by
  rcases h with ⟨t, ht0, ht1, rfl⟩
  refine ⟨1 - t, by linarith, by linarith, ?_⟩
  ext <;> simp <;> ring

theorem strictLineBetween_ne_left {a b c : Point}
    (hab : a ≠ b) (h : StrictLineBetween a b c) : c ≠ a := by
  rcases h with ⟨t, ht0, _ht1, rfl⟩
  intro hca
  apply hab
  ext
  · have hx := congrArg Prod.fst hca
    simp at hx
    rcases hx with ht | hx
    · exact False.elim ((ne_of_gt ht0) ht)
    · linarith
  · have hy := congrArg Prod.snd hca
    simp at hy
    rcases hy with ht | hy
    · exact False.elim ((ne_of_gt ht0) ht)
    · linarith

theorem strictLineBetween_ne_right {a b c : Point}
    (hab : a ≠ b) (h : StrictLineBetween a b c) : c ≠ b :=
  strictLineBetween_ne_left hab.symm (strictLineBetween_symm h)

theorem tripleAbsDet_strictLineBetween_left_lt {a b c p : Point}
    (hbetween : StrictLineBetween a b c) (hdet : ¬ Collinear3 a b p) :
    tripleAbsDet (a, c, p) < tripleAbsDet (a, b, p) := by
  rcases hbetween with ⟨t, ht0, ht1, rfl⟩
  exact tripleAbsDet_smul_vsub_vadd_left_lt
    (by rwa [abs_of_nonneg (le_of_lt ht0)]) hdet

theorem tripleAbsDet_strictLineBetween_right_lt {a b c p : Point}
    (hbetween : StrictLineBetween a b c) (hdet : ¬ Collinear3 a b p) :
    tripleAbsDet (c, b, p) < tripleAbsDet (a, b, p) := by
  rw [tripleAbsDet_swap_left b c p, ← tripleAbsDet_swap_left a b p]
  exact tripleAbsDet_strictLineBetween_left_lt (strictLineBetween_symm hbetween)
    (by
      intro h'
      exact hdet (collinear3_swap_left h'))

theorem not_collinear3_swap_left {p q r : Point}
    (h : ¬ Collinear3 p q r) : ¬ Collinear3 q p r := by
  intro h'
  exact h (collinear3_swap_left h')

theorem not_collinear3_swap_right {p q r : Point}
    (h : ¬ Collinear3 p q r) : ¬ Collinear3 p r q := by
  intro h'
  exact h (collinear3_swap_right h')

theorem not_collinear3_rotate_left {p q r : Point}
    (h : ¬ Collinear3 p q r) : ¬ Collinear3 q r p := by
  intro h'
  exact h (collinear3_rotate_right h')

theorem not_collinear3_rotate_right {p q r : Point}
    (h : ¬ Collinear3 p q r) : ¬ Collinear3 r p q := by
  intro h'
  exact h (collinear3_rotate_left h')

theorem not_collinear3_ne_left {p q r : Point}
    (h : ¬ Collinear3 p q r) : p ≠ q := by
  intro hpq
  apply h
  subst q
  exact collinear3_left_self p r

theorem not_collinear3_ne_right {p q r : Point}
    (h : ¬ Collinear3 p q r) : p ≠ r := by
  intro hpr
  apply h
  subst r
  exact collinear3_right_self p q

theorem not_collinear3_ne_endpoints {p q r : Point}
    (h : ¬ Collinear3 p q r) : q ≠ r := by
  intro hqr
  apply h
  subst r
  exact collinear3_right_endpoint_self p q

theorem linePointScore_pos_of_noncollinear {t : Point × Point × Point}
    (ht : ¬ Collinear3 t.1 t.2.1 t.2.2) : 0 < linePointScore t := by
  have hdet : orientationDet t.1 t.2.1 t.2.2 ≠ 0 := ht
  have hden : 0 < squaredDist t.1 t.2.1 :=
    squaredDist_pos_of_ne (not_collinear3_ne_left ht)
  unfold linePointScore
  positivity

theorem linePointScore_smul_vsub_vadd_eq {a b p : Point} {t : ℝ}
    (ht : t ≠ 0) :
    linePointScore (a, t • (b -ᵥ a) +ᵥ a, p) = linePointScore (a, b, p) := by
  unfold linePointScore
  rw [orientationDet_smul_vsub_vadd_left, squaredDist_smul_vsub_vadd]
  field_simp [ht]

theorem linePointScore_line_parameters_eq {a b p : Point} {s t : ℝ}
    (hab : a ≠ b) (hst : s ≠ t) :
    linePointScore (s • (b -ᵥ a) +ᵥ a, t • (b -ᵥ a) +ᵥ a, p) =
      linePointScore (a, b, p) := by
  have hden : squaredDist a b ≠ 0 := ne_of_gt (squaredDist_pos_of_ne hab)
  have hts : t - s ≠ 0 := sub_ne_zero.mpr hst.symm
  unfold linePointScore
  rw [orientationDet_lineMap_lineMap, squaredDist_lineMap_lineMap]
  field_simp [hden, hts]

theorem linePointScore_eq_of_collinear_base {a b x y p : Point}
    (hab : a ≠ b) (hxy : x ≠ y) (hx : Collinear3 a b x) (hy : Collinear3 a b y) :
    linePointScore (x, y, p) = linePointScore (a, b, p) := by
  rcases exists_line_parameter_of_collinear3 hab hx with ⟨s, rfl⟩
  rcases exists_line_parameter_of_collinear3 hab hy with ⟨t, rfl⟩
  apply linePointScore_line_parameters_eq hab
  intro hst
  apply hxy
  rw [hst]

theorem linePointScore_strictLineBetween_left_eq {a b c p : Point}
    (hbetween : StrictLineBetween a b c) :
    linePointScore (a, c, p) = linePointScore (a, b, p) := by
  rcases hbetween with ⟨t, ht0, _ht1, rfl⟩
  exact linePointScore_smul_vsub_vadd_eq (ne_of_gt ht0)

theorem linePointScore_translate (v a b p : Point) :
    linePointScore (translatePoint v a, translatePoint v b, translatePoint v p) =
      linePointScore (a, b, p) := by
  unfold linePointScore
  rw [orientationDet_translate, squaredDist_translate]

theorem linePointScore_scale {s : ℝ} {a b p : Point}
    (hs : s ≠ 0) (hden : squaredDist a b ≠ 0) :
    linePointScore (scalePoint s a, scalePoint s b, scalePoint s p) =
      s ^ 2 * linePointScore (a, b, p) := by
  unfold linePointScore
  rw [orientationDet_scale, squaredDist_scale]
  field_simp [hs, hden]

theorem linePointScore_scale_lt_iff {s : ℝ} {a b p c d q : Point}
    (hs : s ≠ 0) (hab : squaredDist a b ≠ 0) (hcd : squaredDist c d ≠ 0) :
    linePointScore (scalePoint s a, scalePoint s b, scalePoint s p) <
        linePointScore (scalePoint s c, scalePoint s d, scalePoint s q) ↔
      linePointScore (a, b, p) < linePointScore (c, d, q) := by
  rw [linePointScore_scale hs hab, linePointScore_scale hs hcd]
  have hspos : 0 < s ^ 2 := sq_pos_of_ne_zero hs
  constructor <;> intro h <;> nlinarith

theorem linePointScore_rotateScale {u v : ℝ} {a b p : Point}
    (hscalar : u ≠ 0 ∨ v ≠ 0) (hden : squaredDist a b ≠ 0) :
    linePointScore (rotateScalePoint u v a, rotateScalePoint u v b, rotateScalePoint u v p) =
      scalarNormSq u v * linePointScore (a, b, p) := by
  unfold linePointScore
  rw [orientationDet_rotateScale, squaredDist_rotateScale]
  have hnorm : scalarNormSq u v ≠ 0 := ne_of_gt (scalarNormSq_pos hscalar)
  field_simp [hnorm, hden]

theorem linePointScore_rotateScale_lt_iff {u v : ℝ} {a b p c d q : Point}
    (hscalar : u ≠ 0 ∨ v ≠ 0) (hab : squaredDist a b ≠ 0) (hcd : squaredDist c d ≠ 0) :
    linePointScore (rotateScalePoint u v a, rotateScalePoint u v b, rotateScalePoint u v p) <
        linePointScore (rotateScalePoint u v c, rotateScalePoint u v d, rotateScalePoint u v q) ↔
      linePointScore (a, b, p) < linePointScore (c, d, q) := by
  rw [linePointScore_rotateScale hscalar hab, linePointScore_rotateScale hscalar hcd]
  have hpos : 0 < scalarNormSq u v := scalarNormSq_pos hscalar
  constructor <;> intro h <;> nlinarith

noncomputable def normalizeToXAxis (a b p : Point) : Point :=
  scalePoint (squaredDist a b)⁻¹
    (rotateScalePoint (b.1 - a.1) (-(b.2 - a.2))
      (translatePoint (-a.1, -a.2) p))

theorem normalizeToXAxis_left (a b : Point) :
    normalizeToXAxis a b a = (0, 0) := by
  unfold normalizeToXAxis scalePoint rotateScalePoint translatePoint
  ext <;> simp

theorem normalizeToXAxis_right {a b : Point} (hab : a ≠ b) :
    normalizeToXAxis a b b = (1, 0) := by
  have hden : squaredDist a b ≠ 0 := ne_of_gt (squaredDist_pos_of_ne hab)
  unfold normalizeToXAxis scalePoint rotateScalePoint translatePoint
  ext
  · field_simp [hden]
    unfold squaredDist
    ring
  · field_simp [hden]
    ring

theorem normalizeToXAxis_snd (a b p : Point) :
    (normalizeToXAxis a b p).2 =
      orientationDet a b p / squaredDist a b := by
  unfold normalizeToXAxis scalePoint rotateScalePoint translatePoint orientationDet
  ring

theorem normalizeToXAxis_snd_ne_zero_of_not_collinear3 {a b p : Point}
    (h : ¬ Collinear3 a b p) :
    (normalizeToXAxis a b p).2 ≠ 0 := by
  rw [normalizeToXAxis_snd]
  have hden : squaredDist a b ≠ 0 := ne_of_gt (squaredDist_pos_of_ne (not_collinear3_ne_left h))
  exact div_ne_zero h hden

theorem normalizeToXAxis_snd_eq_zero_of_collinear3 {a b c : Point}
    (h : Collinear3 a b c) :
    (normalizeToXAxis a b c).2 = 0 := by
  rw [normalizeToXAxis_snd]
  simp [Collinear3] at h
  simp [h]

theorem exists_normalizeToXAxis_parameter_of_collinear3 {a b c : Point}
    (h : Collinear3 a b c) :
    ∃ t : ℝ, normalizeToXAxis a b c = (t, 0) := by
  exact ⟨(normalizeToXAxis a b c).1, by ext <;> simp [normalizeToXAxis_snd_eq_zero_of_collinear3 h]⟩

theorem normalizeToXAxis_injective {a b : Point} (hab : a ≠ b) :
    Function.Injective (normalizeToXAxis a b) := by
  have hden : squaredDist a b ≠ 0 := ne_of_gt (squaredDist_pos_of_ne hab)
  have hinv : (squaredDist a b)⁻¹ ≠ 0 := inv_ne_zero hden
  have hscalar : b.1 - a.1 ≠ 0 ∨ -(b.2 - a.2) ≠ 0 := by
    by_contra h
    push Not at h
    apply hab
    ext <;> linarith
  intro p q h
  unfold normalizeToXAxis at h
  have hscale := scalePoint_injective hinv h
  have hrotate := rotateScalePoint_injective hscalar hscale
  exact translatePoint_injective (-a.1, -a.2) hrotate

theorem normalizeToXAxis_eq_left_iff {a b p : Point} (hab : a ≠ b) :
    normalizeToXAxis a b p = (0, 0) ↔ p = a := by
  constructor
  · intro h
    exact normalizeToXAxis_injective hab (h.trans (normalizeToXAxis_left a b).symm)
  · intro h
    rw [h]
    exact normalizeToXAxis_left a b

theorem normalizeToXAxis_eq_right_iff {a b p : Point} (hab : a ≠ b) :
    normalizeToXAxis a b p = (1, 0) ↔ p = b := by
  constructor
  · intro h
    exact normalizeToXAxis_injective hab (h.trans (normalizeToXAxis_right hab).symm)
  · intro h
    rw [h]
    exact normalizeToXAxis_right hab

theorem exists_normalizeToXAxis_parameter_ne_endpoints_of_collinear3 {a b c : Point}
    (hab : a ≠ b) (hcol : Collinear3 a b c) (hca : c ≠ a) (hcb : c ≠ b) :
    ∃ t : ℝ, t ≠ 0 ∧ t ≠ 1 ∧ normalizeToXAxis a b c = (t, 0) := by
  rcases exists_normalizeToXAxis_parameter_of_collinear3 hcol with ⟨t, ht⟩
  refine ⟨t, ?_, ?_, ht⟩
  · intro ht0
    apply hca
    exact (normalizeToXAxis_eq_left_iff hab).1 (by simpa [ht0] using ht)
  · intro ht1
    apply hcb
    exact (normalizeToXAxis_eq_right_iff hab).1 (by simpa [ht1] using ht)

theorem collinear3_normalizeToXAxis {a b x y z : Point}
    (h : Collinear3 x y z) :
    Collinear3 (normalizeToXAxis a b x) (normalizeToXAxis a b y)
      (normalizeToXAxis a b z) := by
  unfold normalizeToXAxis Collinear3
  rw [orientationDet_scale, orientationDet_rotateScale, orientationDet_translate, h]
  ring

theorem snd_eq_zero_of_collinear3_xAxis_pair {x y : ℝ} {q : Point}
    (hxy : x ≠ y) (h : Collinear3 ((x, 0) : Point) ((y, 0) : Point) q) :
    q.2 = 0 := by
  have hdet : (y - x) * q.2 = 0 := by
    simpa [Collinear3, orientationDet] using h
  exact eq_zero_of_ne_zero_of_mul_left_eq_zero (sub_ne_zero.mpr hxy.symm) hdet

theorem collinear3_of_normalizeToXAxis_snd_eq_zero {a b c : Point}
    (hab : a ≠ b) (h : (normalizeToXAxis a b c).2 = 0) :
    Collinear3 a b c := by
  rw [normalizeToXAxis_snd] at h
  have hden : squaredDist a b ≠ 0 := ne_of_gt (squaredDist_pos_of_ne hab)
  exact (div_eq_zero_iff.mp h).resolve_right hden

theorem collinear3_of_collinear3_selected_base {a b X Y C : Point} {x y : ℝ}
    (hab : a ≠ b) (hxy : x ≠ y)
    (hX : normalizeToXAxis a b X = (x, 0))
    (hY : normalizeToXAxis a b Y = (y, 0))
    (hC : Collinear3 X Y C) :
    Collinear3 a b C := by
  have hnorm := collinear3_normalizeToXAxis (a := a) (b := b) hC
  rw [hX, hY] at hnorm
  exact collinear3_of_normalizeToXAxis_snd_eq_zero hab
    (snd_eq_zero_of_collinear3_xAxis_pair hxy hnorm)

noncomputable def baseLineParameters (S : Finset Point) (a b : Point) : Finset ℝ := by
  classical
  exact (S.filter fun c => Collinear3 a b c).image fun c => (normalizeToXAxis a b c).1

theorem mem_baseLineParameters_of_collinear {S : Finset Point} {a b c : Point}
    (hcS : c ∈ S) (hcol : Collinear3 a b c) :
    (normalizeToXAxis a b c).1 ∈ baseLineParameters S a b := by
  classical
  apply Finset.mem_image.mpr
  exact ⟨c, by simp [hcS, hcol], rfl⟩

theorem exists_of_mem_baseLineParameters {S : Finset Point} {a b : Point} {t : ℝ}
    (ht : t ∈ baseLineParameters S a b) :
    ∃ c ∈ S, Collinear3 a b c ∧ normalizeToXAxis a b c = (t, 0) := by
  classical
  rcases Finset.mem_image.mp ht with ⟨c, hcfilter, rfl⟩
  have hcS : c ∈ S := (Finset.mem_filter.mp hcfilter).1
  have hcol : Collinear3 a b c := (Finset.mem_filter.mp hcfilter).2
  refine ⟨c, hcS, hcol, ?_⟩
  ext <;> simp [normalizeToXAxis_snd_eq_zero_of_collinear3 hcol]

theorem left_mem_baseLineParameters {S : Finset Point} {a b : Point}
    (haS : a ∈ S) :
    0 ∈ baseLineParameters S a b := by
  have hmem :=
    mem_baseLineParameters_of_collinear (S := S) (a := a) (b := b) (c := a)
      haS (collinear3_right_self a b)
  simpa [normalizeToXAxis_left] using hmem

theorem right_mem_baseLineParameters {S : Finset Point} {a b : Point}
    (hbS : b ∈ S) (hab : a ≠ b) :
    1 ∈ baseLineParameters S a b := by
  have hmem :=
    mem_baseLineParameters_of_collinear (S := S) (a := a) (b := b) (c := b)
      hbS (collinear3_right_endpoint_self a b)
  simpa [normalizeToXAxis_right hab] using hmem

theorem one_lt_card_baseLineParameters {S : Finset Point} {a b : Point}
    (haS : a ∈ S) (hbS : b ∈ S) (hab : a ≠ b) :
    1 < (baseLineParameters S a b).card := by
  exact Finset.one_lt_card.mpr
    ⟨0, left_mem_baseLineParameters haS, 1, right_mem_baseLineParameters hbS hab, by norm_num⟩

theorem linePointScore_normalizeToXAxis {a b x y z : Point}
    (hab : a ≠ b) (hxy : squaredDist x y ≠ 0) :
    linePointScore (normalizeToXAxis a b x, normalizeToXAxis a b y, normalizeToXAxis a b z) =
      (squaredDist a b)⁻¹ * linePointScore (x, y, z) := by
  let shift : Point := (-a.1, -a.2)
  let u : ℝ := b.1 - a.1
  let v : ℝ := -(b.2 - a.2)
  let s : ℝ := (squaredDist a b)⁻¹
  have hden : squaredDist a b ≠ 0 := ne_of_gt (squaredDist_pos_of_ne hab)
  have hs : s ≠ 0 := inv_ne_zero hden
  have hscalar : u ≠ 0 ∨ v ≠ 0 := by
    by_contra h
    push Not at h
    apply hab
    ext <;> dsimp [u, v] at h ⊢ <;> linarith
  have hshift_xy : squaredDist (translatePoint shift x) (translatePoint shift y) ≠ 0 := by
    rwa [squaredDist_translate]
  have hnorm : scalarNormSq u v ≠ 0 := ne_of_gt (scalarNormSq_pos hscalar)
  have hrot_xy :
      squaredDist (rotateScalePoint u v (translatePoint shift x))
        (rotateScalePoint u v (translatePoint shift y)) ≠ 0 := by
    rw [squaredDist_rotateScale]
    exact mul_ne_zero hnorm hshift_xy
  unfold normalizeToXAxis
  change
    linePointScore
        (scalePoint s (rotateScalePoint u v (translatePoint shift x)),
          scalePoint s (rotateScalePoint u v (translatePoint shift y)),
          scalePoint s (rotateScalePoint u v (translatePoint shift z))) =
      (squaredDist a b)⁻¹ * linePointScore (x, y, z)
  rw [linePointScore_scale hs hrot_xy, linePointScore_rotateScale hscalar hshift_xy,
    linePointScore_translate]
  have hbase : scalarNormSq u v = squaredDist a b := by
    dsimp [u, v]
    exact scalarNormSq_base a b
  rw [hbase]
  dsimp [s]
  field_simp [hden]

theorem linePointScore_normalizeToXAxis_lt_iff {a b x y z c d q : Point}
    (hab : a ≠ b) (hxy : squaredDist x y ≠ 0) (hcd : squaredDist c d ≠ 0) :
    linePointScore (normalizeToXAxis a b x, normalizeToXAxis a b y, normalizeToXAxis a b z) <
        linePointScore (normalizeToXAxis a b c, normalizeToXAxis a b d, normalizeToXAxis a b q) ↔
      linePointScore (x, y, z) < linePointScore (c, d, q) := by
  rw [linePointScore_normalizeToXAxis hab hxy, linePointScore_normalizeToXAxis hab hcd]
  have hfactor : 0 < (squaredDist a b)⁻¹ := inv_pos.mpr (squaredDist_pos_of_ne hab)
  constructor <;> intro h <;> nlinarith

theorem linePointScore_xAxis (u v : ℝ) :
    linePointScore (((0, 0) : Point), ((1, 0) : Point), ((u, v) : Point)) = v ^ 2 := by
  unfold linePointScore orientationDet squaredDist
  norm_num

theorem linePointScore_xAxis_pair {x y u v : ℝ} (hxy : x ≠ y) :
    linePointScore (((x, 0) : Point), ((y, 0) : Point), ((u, v) : Point)) = v ^ 2 := by
  unfold linePointScore orientationDet squaredDist
  field_simp [sub_ne_zero.mpr hxy.symm]
  ring

theorem linePointScore_canonical_cross (u v t : ℝ) :
    linePointScore (((u, v) : Point), ((t, 0) : Point), ((1, 0) : Point)) =
      v ^ 2 * (1 - t) ^ 2 / ((t - u) ^ 2 + v ^ 2) := by
  unfold linePointScore orientationDet squaredDist
  norm_num
  ring

theorem linePointScore_canonical_cross_left (u v t : ℝ) :
    linePointScore (((u, v) : Point), ((t, 0) : Point), ((0, 0) : Point)) =
      v ^ 2 * t ^ 2 / ((t - u) ^ 2 + v ^ 2) := by
  unfold linePointScore orientationDet squaredDist
  norm_num
  ring

theorem linePointScore_xAxis_cross (u v t e : ℝ) :
    linePointScore (((u, v) : Point), ((t, 0) : Point), ((e, 0) : Point)) =
      v ^ 2 * (e - t) ^ 2 / ((t - u) ^ 2 + v ^ 2) := by
  unfold linePointScore orientationDet squaredDist
  norm_num
  ring

theorem linePointScore_canonical_cross_lt_xAxis {u v t : ℝ}
    (hv : v ≠ 0) (hineq : (1 - t) ^ 2 < (t - u) ^ 2 + v ^ 2) :
    linePointScore (((u, v) : Point), ((t, 0) : Point), ((1, 0) : Point)) <
      linePointScore (((0, 0) : Point), ((1, 0) : Point), ((u, v) : Point)) := by
  rw [linePointScore_canonical_cross, linePointScore_xAxis]
  have hvpos : 0 < v ^ 2 := sq_pos_of_ne_zero hv
  have hdenpos : 0 < (t - u) ^ 2 + v ^ 2 := by positivity
  rw [div_lt_iff₀ hdenpos]
  nlinarith [sq_nonneg (1 - t)]

theorem linePointScore_canonical_cross_left_lt_xAxis {u v t : ℝ}
    (hv : v ≠ 0) (hineq : t ^ 2 < (t - u) ^ 2 + v ^ 2) :
    linePointScore (((u, v) : Point), ((t, 0) : Point), ((0, 0) : Point)) <
      linePointScore (((0, 0) : Point), ((1, 0) : Point), ((u, v) : Point)) := by
  rw [linePointScore_canonical_cross_left, linePointScore_xAxis]
  have hvpos : 0 < v ^ 2 := sq_pos_of_ne_zero hv
  have hdenpos : 0 < (t - u) ^ 2 + v ^ 2 := by positivity
  rw [div_lt_iff₀ hdenpos]
  nlinarith [sq_nonneg t]

theorem endpoint_parameter_ineq_of_between_projection_general {e u v t : ℝ}
    (hv : v ≠ 0) (hbetween : (u ≤ e ∧ e ≤ t) ∨ (t ≤ e ∧ e ≤ u)) :
    (e - t) ^ 2 < (t - u) ^ 2 + v ^ 2 := by
  have hvpos : 0 < v ^ 2 := sq_pos_of_ne_zero hv
  rcases hbetween with ⟨hue, het⟩ | ⟨hte, heu⟩
  · nlinarith [sq_nonneg (e - u)]
  · nlinarith [sq_nonneg (e - u)]

theorem linePointScore_xAxis_cross_lt_xAxis_pair {x y u v t e : ℝ}
    (hxy : x ≠ y) (hv : v ≠ 0)
    (hbetween : (u ≤ e ∧ e ≤ t) ∨ (t ≤ e ∧ e ≤ u)) :
    linePointScore (((u, v) : Point), ((t, 0) : Point), ((e, 0) : Point)) <
      linePointScore (((x, 0) : Point), ((y, 0) : Point), ((u, v) : Point)) := by
  rw [linePointScore_xAxis_cross, linePointScore_xAxis_pair hxy]
  have hineq := endpoint_parameter_ineq_of_between_projection_general hv hbetween
  have hvpos : 0 < v ^ 2 := sq_pos_of_ne_zero hv
  have hdenpos : 0 < (t - u) ^ 2 + v ^ 2 := by positivity
  rw [div_lt_iff₀ hdenpos]
  nlinarith [sq_nonneg (e - t)]

theorem left_endpoint_parameter_ineq_of_between_projection {u v t : ℝ}
    (hv : v ≠ 0) (hbetween : (u ≤ 0 ∧ 0 ≤ t) ∨ (t ≤ 0 ∧ 0 ≤ u)) :
    t ^ 2 < (t - u) ^ 2 + v ^ 2 := by
  have hvpos : 0 < v ^ 2 := sq_pos_of_ne_zero hv
  rcases hbetween with ⟨hu, ht⟩ | ⟨ht, hu⟩
  · nlinarith [sq_nonneg u]
  · nlinarith [sq_nonneg u]

theorem right_endpoint_parameter_ineq_of_between_projection {u v t : ℝ}
    (hv : v ≠ 0) (hbetween : (u ≤ 1 ∧ 1 ≤ t) ∨ (t ≤ 1 ∧ 1 ≤ u)) :
    (1 - t) ^ 2 < (t - u) ^ 2 + v ^ 2 := by
  have hvpos : 0 < v ^ 2 := sq_pos_of_ne_zero hv
  rcases hbetween with ⟨hu, ht⟩ | ⟨ht, hu⟩
  · nlinarith [sq_nonneg (u - 1)]
  · nlinarith [sq_nonneg (u - 1)]

theorem endpoint_parameter_ineq_of_projection_mem_Icc_of_parameter_outside
    {u v t : ℝ} (hv : v ≠ 0) (hu0 : 0 ≤ u) (hu1 : u ≤ 1)
    (ht : t ≤ 0 ∨ 1 ≤ t) :
    t ^ 2 < (t - u) ^ 2 + v ^ 2 ∨
      (1 - t) ^ 2 < (t - u) ^ 2 + v ^ 2 := by
  rcases ht with ht | ht
  · exact Or.inl
      (left_endpoint_parameter_ineq_of_between_projection hv (Or.inr ⟨ht, hu0⟩))
  · exact Or.inr
      (right_endpoint_parameter_ineq_of_between_projection hv (Or.inl ⟨hu1, ht⟩))

def StrictAdjacentParametersAround (T : Finset ℝ) (u x y : ℝ) : Prop :=
  x ∈ T ∧ y ∈ T ∧ x < u ∧ u < y ∧ ∀ z ∈ T, z ≤ x ∨ y ≤ z

def RightAdjacentParametersAfterProjection (T : Finset ℝ) (u x y : ℝ) : Prop :=
  x ∈ T ∧ y ∈ T ∧ u < x ∧ x < y ∧ ∀ z ∈ T, z ≠ x → y ≤ z

def LeftAdjacentParametersBeforeProjection (T : Finset ℝ) (u x y : ℝ) : Prop :=
  x ∈ T ∧ y ∈ T ∧ x < y ∧ y < u ∧ ∀ z ∈ T, z ≠ y → z ≤ x

def ProjectionLeftAdjacentParameter (T : Finset ℝ) (u y : ℝ) : Prop :=
  u ∈ T ∧ y ∈ T ∧ u < y ∧ ∀ z ∈ T, z ≠ u → z ≠ y → z ≤ u ∨ y ≤ z

def ProjectionRightAdjacentParameter (T : Finset ℝ) (u x : ℝ) : Prop :=
  x ∈ T ∧ u ∈ T ∧ x < u ∧ ∀ z ∈ T, z ≠ x → z ≠ u → z ≤ x ∨ u ≤ z

theorem exists_strictAdjacentParametersAround_of_not_mem_of_exists_lt_gt
    {T : Finset ℝ} {u : ℝ} (huT : u ∉ T)
    (hleft : ∃ x ∈ T, x < u) (hright : ∃ y ∈ T, u < y) :
    ∃ x y : ℝ, StrictAdjacentParametersAround T u x y := by
  classical
  let L : Finset ℝ := T.filter fun z => z < u
  let R : Finset ℝ := T.filter fun z => u < z
  have hLne : L.Nonempty := by
    rcases hleft with ⟨x, hxT, hxu⟩
    exact ⟨x, by simp [L, hxT, hxu]⟩
  have hRne : R.Nonempty := by
    rcases hright with ⟨y, hyT, huy⟩
    exact ⟨y, by simp [R, hyT, huy]⟩
  refine ⟨L.max' hLne, R.min' hRne, ?_⟩
  have hxmem := L.max'_mem hLne
  have hymem := R.min'_mem hRne
  have hxT : L.max' hLne ∈ T := by
    exact (Finset.mem_filter.mp hxmem).1
  have hyT : R.min' hRne ∈ T := by
    exact (Finset.mem_filter.mp hymem).1
  have hxu : L.max' hLne < u := by
    exact (Finset.mem_filter.mp hxmem).2
  have huy : u < R.min' hRne := by
    exact (Finset.mem_filter.mp hymem).2
  refine ⟨hxT, hyT, hxu, huy, ?_⟩
  intro z hzT
  by_cases hzu : z < u
  · exact Or.inl (L.le_max' z (by simp [L, hzT, hzu]))
  · have huz : u ≤ z := le_of_not_gt hzu
    have hzne : z ≠ u := by
      intro hzu_eq
      exact huT (hzu_eq ▸ hzT)
    have huzlt : u < z := lt_of_le_of_ne huz hzne.symm
    exact Or.inr (R.min'_le z (by simp [R, hzT, huzlt]))

theorem exists_rightAdjacentParametersAfterProjection_of_forall_gt
    {T : Finset ℝ} {u : ℝ} (hcard : 1 < T.card)
    (hall : ∀ z ∈ T, u < z) :
    ∃ x y : ℝ, RightAdjacentParametersAfterProjection T u x y := by
  classical
  rcases Finset.one_lt_card.mp hcard with ⟨p, hpT, q, hqT, hpq⟩
  let hTne : T.Nonempty := ⟨p, hpT⟩
  let x : ℝ := T.min' hTne
  have hxT : x ∈ T := T.min'_mem hTne
  have herase : (T.erase x).Nonempty := by
    by_cases hpx : p = x
    · refine ⟨q, ?_⟩
      rw [Finset.mem_erase]
      exact ⟨by intro hqx; exact hpq (hpx.trans hqx.symm), hqT⟩
    · refine ⟨p, ?_⟩
      rw [Finset.mem_erase]
      exact ⟨hpx, hpT⟩
  let y : ℝ := (T.erase x).min' herase
  have hyerase : y ∈ T.erase x := (T.erase x).min'_mem herase
  have hy_ne_x : y ≠ x := (Finset.mem_erase.mp hyerase).1
  have hyT : y ∈ T := (Finset.mem_erase.mp hyerase).2
  have hxy : x < y := by
    exact lt_of_le_of_ne (T.min'_le y hyT) (Ne.symm hy_ne_x)
  refine ⟨x, y, hxT, hyT, hall x hxT, hxy, ?_⟩
  intro z hzT hzx
  exact (T.erase x).min'_le z (by rw [Finset.mem_erase]; exact ⟨hzx, hzT⟩)

theorem exists_leftAdjacentParametersBeforeProjection_of_forall_lt
    {T : Finset ℝ} {u : ℝ} (hcard : 1 < T.card)
    (hall : ∀ z ∈ T, z < u) :
    ∃ x y : ℝ, LeftAdjacentParametersBeforeProjection T u x y := by
  classical
  rcases Finset.one_lt_card.mp hcard with ⟨p, hpT, q, hqT, hpq⟩
  let hTne : T.Nonempty := ⟨p, hpT⟩
  let y : ℝ := T.max' hTne
  have hyT : y ∈ T := T.max'_mem hTne
  have herase : (T.erase y).Nonempty := by
    by_cases hpy : p = y
    · refine ⟨q, ?_⟩
      rw [Finset.mem_erase]
      exact ⟨by intro hqy; exact hpq (hpy.trans hqy.symm), hqT⟩
    · refine ⟨p, ?_⟩
      rw [Finset.mem_erase]
      exact ⟨hpy, hpT⟩
  let x : ℝ := (T.erase y).max' herase
  have hxerase : x ∈ T.erase y := (T.erase y).max'_mem herase
  have hx_ne_y : x ≠ y := (Finset.mem_erase.mp hxerase).1
  have hxT : x ∈ T := (Finset.mem_erase.mp hxerase).2
  have hxy : x < y := by
    exact lt_of_le_of_ne (T.le_max' x hxT) hx_ne_y
  refine ⟨x, y, hxT, hyT, hxy, hall y hyT, ?_⟩
  intro z hzT hzy
  exact (T.erase y).le_max' z (by rw [Finset.mem_erase]; exact ⟨hzy, hzT⟩)

theorem exists_projectionLeftAdjacentParameter_of_mem_of_exists_gt
    {T : Finset ℝ} {u : ℝ} (huT : u ∈ T) (hright : ∃ y ∈ T, u < y) :
    ∃ y : ℝ, ProjectionLeftAdjacentParameter T u y := by
  classical
  let R : Finset ℝ := T.filter fun z => u < z
  have hRne : R.Nonempty := by
    rcases hright with ⟨y, hyT, huy⟩
    exact ⟨y, by simp [R, hyT, huy]⟩
  let y : ℝ := R.min' hRne
  have hymem : y ∈ R := R.min'_mem hRne
  have hyT : y ∈ T := (Finset.mem_filter.mp hymem).1
  have huy : u < y := (Finset.mem_filter.mp hymem).2
  refine ⟨y, huT, hyT, huy, ?_⟩
  intro z hzT hzu hzy
  by_cases huz : u < z
  · exact Or.inr (R.min'_le z (by simp [R, hzT, huz]))
  · exact Or.inl (le_of_not_gt huz)

theorem exists_projectionRightAdjacentParameter_of_mem_of_exists_lt
    {T : Finset ℝ} {u : ℝ} (huT : u ∈ T) (hleft : ∃ x ∈ T, x < u) :
    ∃ x : ℝ, ProjectionRightAdjacentParameter T u x := by
  classical
  let L : Finset ℝ := T.filter fun z => z < u
  have hLne : L.Nonempty := by
    rcases hleft with ⟨x, hxT, hxu⟩
    exact ⟨x, by simp [L, hxT, hxu]⟩
  let x : ℝ := L.max' hLne
  have hxmem : x ∈ L := L.max'_mem hLne
  have hxT : x ∈ T := (Finset.mem_filter.mp hxmem).1
  have hxu : x < u := (Finset.mem_filter.mp hxmem).2
  refine ⟨x, hxT, huT, hxu, ?_⟩
  intro z hzT hzx hzu
  by_cases hzu_lt : z < u
  · exact Or.inl (L.le_max' z (by simp [L, hzT, hzu_lt]))
  · exact Or.inr (le_of_not_gt hzu_lt)

theorem linePointScore_normalized_cross_right_lt {a b p c : Point} {u v t : ℝ}
    (hab : a ≠ b) (hpc : squaredDist p c ≠ 0)
    (hp : normalizeToXAxis a b p = (u, v))
    (hc : normalizeToXAxis a b c = (t, 0))
    (hv : v ≠ 0) (hineq : (1 - t) ^ 2 < (t - u) ^ 2 + v ^ 2) :
    linePointScore (p, c, b) < linePointScore (a, b, p) := by
  have hbase : squaredDist a b ≠ 0 := ne_of_gt (squaredDist_pos_of_ne hab)
  apply (linePointScore_normalizeToXAxis_lt_iff hab hpc hbase).1
  rw [hp, hc, normalizeToXAxis_right hab, normalizeToXAxis_left]
  exact linePointScore_canonical_cross_lt_xAxis hv hineq

theorem linePointScore_normalized_cross_left_lt {a b p c : Point} {u v t : ℝ}
    (hab : a ≠ b) (hpc : squaredDist p c ≠ 0)
    (hp : normalizeToXAxis a b p = (u, v))
    (hc : normalizeToXAxis a b c = (t, 0))
    (hv : v ≠ 0) (hineq : t ^ 2 < (t - u) ^ 2 + v ^ 2) :
    linePointScore (p, c, a) < linePointScore (a, b, p) := by
  have hbase : squaredDist a b ≠ 0 := ne_of_gt (squaredDist_pos_of_ne hab)
  apply (linePointScore_normalizeToXAxis_lt_iff hab hpc hbase).1
  rw [hp, hc, normalizeToXAxis_left, normalizeToXAxis_right hab]
  exact linePointScore_canonical_cross_left_lt_xAxis hv hineq

theorem not_collinear3_cross_right_of_base {a b p c : Point}
    (hcol : Collinear3 a b c) (hcb : c ≠ b) (hp : ¬ Collinear3 a b p) :
    ¬ Collinear3 p c b := by
  intro hpcb
  have ha_cb : a ∈ line[ℝ, c, b] :=
    mem_line_of_collinear3 hcb (collinear3_swap_right (collinear3_rotate_right hcol))
  have hb_cb : b ∈ line[ℝ, c, b] :=
    mem_line_of_collinear3 hcb (collinear3_right_endpoint_self c b)
  have hp_cb : p ∈ line[ℝ, c, b] :=
    mem_line_of_collinear3 hcb (collinear3_rotate_left hpcb)
  exact hp (collinear3_of_mem_line ha_cb hb_cb hp_cb)

theorem not_collinear3_cross_left_of_base {a b p c : Point}
    (hcol : Collinear3 a b c) (hca : c ≠ a) (hp : ¬ Collinear3 a b p) :
    ¬ Collinear3 p c a := by
  intro hpca
  have ha_ca : a ∈ line[ℝ, c, a] :=
    mem_line_of_collinear3 hca (collinear3_right_endpoint_self c a)
  have hb_ca : b ∈ line[ℝ, c, a] :=
    mem_line_of_collinear3 hca (collinear3_rotate_right hcol)
  have hp_ca : p ∈ line[ℝ, c, a] :=
    mem_line_of_collinear3 hca (collinear3_rotate_left hpca)
  exact hp (collinear3_of_mem_line ha_ca hb_ca hp_ca)

theorem mem_noncollinearTriples_cross_right {S : Finset Point} {a b p c : Point}
    (hpS : p ∈ S) (hcS : c ∈ S) (hbS : b ∈ S)
    (hcol : Collinear3 a b c) (hcb : c ≠ b) (hp : ¬ Collinear3 a b p) :
    (p, c, b) ∈ noncollinearTriples S := by
  rw [mem_noncollinearTriples]
  exact ⟨hpS, hcS, hbS, not_collinear3_cross_right_of_base hcol hcb hp⟩

theorem mem_noncollinearTriples_cross_left {S : Finset Point} {a b p c : Point}
    (hpS : p ∈ S) (hcS : c ∈ S) (haS : a ∈ S)
    (hcol : Collinear3 a b c) (hca : c ≠ a) (hp : ¬ Collinear3 a b p) :
    (p, c, a) ∈ noncollinearTriples S := by
  rw [mem_noncollinearTriples]
  exact ⟨hpS, hcS, haS, not_collinear3_cross_left_of_base hcol hca hp⟩

theorem not_collinear3_cross_of_base_pair {a b p c d : Point}
    (hab : a ≠ b) (hc : Collinear3 a b c) (hd : Collinear3 a b d)
    (hcd : c ≠ d) (hp : ¬ Collinear3 a b p) :
    ¬ Collinear3 p c d := by
  intro hpcd
  have hc_ab : c ∈ line[ℝ, a, b] := mem_line_of_collinear3 hab hc
  have hd_ab : d ∈ line[ℝ, a, b] := mem_line_of_collinear3 hab hd
  have ha_ab : a ∈ line[ℝ, a, b] :=
    mem_line_of_collinear3 hab (collinear3_right_self a b)
  have hb_ab : b ∈ line[ℝ, a, b] :=
    mem_line_of_collinear3 hab (collinear3_right_endpoint_self a b)
  have ha_cd : a ∈ line[ℝ, c, d] :=
    mem_line_of_collinear3 hcd (collinear3_of_mem_line hc_ab hd_ab ha_ab)
  have hb_cd : b ∈ line[ℝ, c, d] :=
    mem_line_of_collinear3 hcd (collinear3_of_mem_line hc_ab hd_ab hb_ab)
  have hp_cd : p ∈ line[ℝ, c, d] :=
    mem_line_of_collinear3 hcd (collinear3_rotate_left hpcd)
  exact hp (collinear3_of_mem_line ha_cd hb_cd hp_cd)

theorem mem_noncollinearTriples_cross_base_pair {S : Finset Point} {a b p c d : Point}
    (hpS : p ∈ S) (hcS : c ∈ S) (hdS : d ∈ S)
    (hab : a ≠ b) (hc : Collinear3 a b c) (hd : Collinear3 a b d)
    (hcd : c ≠ d) (hp : ¬ Collinear3 a b p) :
    (p, c, d) ∈ noncollinearTriples S := by
  rw [mem_noncollinearTriples]
  exact ⟨hpS, hcS, hdS, not_collinear3_cross_of_base_pair hab hc hd hcd hp⟩

theorem cross_right_descent_of_normalized_parameter {S : Finset Point}
    {a b p c : Point} {u v t : ℝ}
    (hpS : p ∈ S) (hcS : c ∈ S) (hbS : b ∈ S)
    (hcol : Collinear3 a b c) (hcb : c ≠ b) (hp : ¬ Collinear3 a b p)
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (hcnorm : normalizeToXAxis a b c = (t, 0))
    (hineq : (1 - t) ^ 2 < (t - u) ^ 2 + v ^ 2) :
    (p, c, b) ∈ noncollinearTriples S ∧
      linePointScore (p, c, b) < linePointScore (a, b, p) := by
  have hab : a ≠ b := not_collinear3_ne_left hp
  have hpc_ne : p ≠ c := by
    intro hpc
    apply hp
    rw [hpc]
    exact hcol
  have hpc_dist : squaredDist p c ≠ 0 := ne_of_gt (squaredDist_pos_of_ne hpc_ne)
  have hv : v ≠ 0 := by
    have hvnorm := normalizeToXAxis_snd_ne_zero_of_not_collinear3 hp
    rw [hpnorm] at hvnorm
    exact hvnorm
  exact
    ⟨mem_noncollinearTriples_cross_right hpS hcS hbS hcol hcb hp,
      linePointScore_normalized_cross_right_lt hab hpc_dist hpnorm hcnorm hv hineq⟩

theorem cross_left_descent_of_normalized_parameter {S : Finset Point}
    {a b p c : Point} {u v t : ℝ}
    (hpS : p ∈ S) (hcS : c ∈ S) (haS : a ∈ S)
    (hcol : Collinear3 a b c) (hca : c ≠ a) (hp : ¬ Collinear3 a b p)
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (hcnorm : normalizeToXAxis a b c = (t, 0))
    (hineq : t ^ 2 < (t - u) ^ 2 + v ^ 2) :
    (p, c, a) ∈ noncollinearTriples S ∧
      linePointScore (p, c, a) < linePointScore (a, b, p) := by
  have hab : a ≠ b := not_collinear3_ne_left hp
  have hpc_ne : p ≠ c := by
    intro hpc
    apply hp
    rw [hpc]
    exact hcol
  have hpc_dist : squaredDist p c ≠ 0 := ne_of_gt (squaredDist_pos_of_ne hpc_ne)
  have hv : v ≠ 0 := by
    have hvnorm := normalizeToXAxis_snd_ne_zero_of_not_collinear3 hp
    rw [hpnorm] at hvnorm
    exact hvnorm
  exact
    ⟨mem_noncollinearTriples_cross_left hpS hcS haS hcol hca hp,
      linePointScore_normalized_cross_left_lt hab hpc_dist hpnorm hcnorm hv hineq⟩

theorem ordinaryPair_left_mem {S : Finset Point} {a b : Point}
    (h : OrdinaryPair S a b) : a ∈ S :=
  h.1

theorem ordinaryPair_right_mem {S : Finset Point} {a b : Point}
    (h : OrdinaryPair S a b) : b ∈ S :=
  h.2.1

theorem ordinaryPair_ne {S : Finset Point} {a b : Point}
    (h : OrdinaryPair S a b) : a ≠ b :=
  h.2.2.1

theorem ordinaryPair_collinear_cases {S : Finset Point} {a b c : Point}
    (h : OrdinaryPair S a b) (hcS : c ∈ S) (hcol : Collinear3 a b c) :
    c = a ∨ c = b :=
  h.2.2.2 c hcS hcol

theorem exists_collinear_ne_of_not_ordinaryPair {S : Finset Point} {a b : Point}
    (haS : a ∈ S) (hbS : b ∈ S) (hab : a ≠ b) (hnot : ¬ OrdinaryPair S a b) :
    ∃ c ∈ S, Collinear3 a b c ∧ c ≠ a ∧ c ≠ b := by
  by_contra hnone
  apply hnot
  refine ⟨haS, hbS, hab, ?_⟩
  intro c hcS hcol
  by_contra hcase
  push Not at hcase
  exact hnone ⟨c, hcS, hcol, hcase.1, hcase.2⟩

theorem exists_baseLineParameter_ne_endpoints_of_not_ordinaryPair
    {S : Finset Point} {a b : Point}
    (haS : a ∈ S) (hbS : b ∈ S) (hab : a ≠ b) (hnot : ¬ OrdinaryPair S a b) :
    ∃ t ∈ baseLineParameters S a b, t ≠ 0 ∧ t ≠ 1 := by
  rcases exists_collinear_ne_of_not_ordinaryPair haS hbS hab hnot with
    ⟨c, hcS, hcol, hca, hcb⟩
  rcases exists_normalizeToXAxis_parameter_ne_endpoints_of_collinear3 hab hcol hca hcb with
    ⟨t, ht0, ht1, hnorm⟩
  refine ⟨t, ?_, ht0, ht1⟩
  have hmem := mem_baseLineParameters_of_collinear (S := S) (a := a) (b := b) hcS hcol
  rw [hnorm] at hmem
  exact hmem

theorem exists_descent_of_normalized_adjacent_baseLineParameters
    {S : Finset Point} {a b p : Point} {u v : ℝ}
    (haS : a ∈ S) (hbS : b ∈ S) (hpS : p ∈ S)
    (hnp : ¬ Collinear3 a b p)
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (hu0 : 0 ≤ u) (hu1 : u ≤ 1)
    (hout :
      ∀ t ∈ baseLineParameters S a b, t ≠ 0 → t ≠ 1 → t ≤ 0 ∨ 1 ≤ t)
    (hnot : ¬ OrdinaryPair S a b) :
    ∃ w ∈ noncollinearTriples S, linePointScore w < linePointScore (a, b, p) := by
  have hab : a ≠ b := not_collinear3_ne_left hnp
  rcases exists_baseLineParameter_ne_endpoints_of_not_ordinaryPair haS hbS hab hnot with
    ⟨t, htT, ht0, ht1⟩
  rcases exists_of_mem_baseLineParameters htT with ⟨c, hcS, hcol, hcnorm⟩
  have hv : v ≠ 0 := by
    have hvnorm := normalizeToXAxis_snd_ne_zero_of_not_collinear3 hnp
    rw [hpnorm] at hvnorm
    exact hvnorm
  rcases endpoint_parameter_ineq_of_projection_mem_Icc_of_parameter_outside
      hv hu0 hu1 (hout t htT ht0 ht1) with hleft | hright
  · have hca : c ≠ a := by
      intro hca
      apply ht0
      have htmp := hcnorm
      rw [hca, normalizeToXAxis_left] at htmp
      exact (congrArg Prod.fst htmp).symm
    have hdesc :=
      cross_left_descent_of_normalized_parameter hpS hcS haS hcol hca hnp
        hpnorm hcnorm hleft
    exact ⟨(p, c, a), hdesc.1, hdesc.2⟩
  · have hcb : c ≠ b := by
      intro hcb
      apply ht1
      have htmp := hcnorm
      rw [hcb, normalizeToXAxis_right hab] at htmp
      exact (congrArg Prod.fst htmp).symm
    have hdesc :=
      cross_right_descent_of_normalized_parameter hpS hcS hbS hcol hcb hnp
        hpnorm hcnorm hright
    exact ⟨(p, c, b), hdesc.1, hdesc.2⟩

theorem exists_normalized_cross_descent_of_adjacent_parameters
    {S : Finset Point} {a b p : Point} {x y u v t : ℝ}
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (hxy : x < y)
    (htT : t ∈ baseLineParameters S a b)
    (htx : t ≠ x) (hty : t ≠ y)
    (hu : x ≤ u ∧ u ≤ y)
    (hout :
      ∀ t ∈ baseLineParameters S a b, t ≠ x → t ≠ y → t ≤ x ∨ y ≤ t)
    (hnp : ¬ Collinear3 a b p) :
    ∃ c ∈ S,
      Collinear3 a b c ∧ normalizeToXAxis a b c = (t, 0) ∧
        (linePointScore (((u, v) : Point), ((t, 0) : Point), ((x, 0) : Point)) <
            linePointScore (((x, 0) : Point), ((y, 0) : Point), ((u, v) : Point)) ∨
          linePointScore (((u, v) : Point), ((t, 0) : Point), ((y, 0) : Point)) <
            linePointScore (((x, 0) : Point), ((y, 0) : Point), ((u, v) : Point))) := by
  rcases exists_of_mem_baseLineParameters htT with ⟨c, hcS, hcol, hcnorm⟩
  have hv : v ≠ 0 := by
    have hvnorm := normalizeToXAxis_snd_ne_zero_of_not_collinear3 hnp
    rw [hpnorm] at hvnorm
    exact hvnorm
  refine ⟨c, hcS, hcol, hcnorm, ?_⟩
  rcases hout t htT htx hty with htxle | hylet
  · exact Or.inl
      (linePointScore_xAxis_cross_lt_xAxis_pair (ne_of_lt hxy) hv
        (Or.inr ⟨htxle, hu.1⟩))
  · exact Or.inr
      (linePointScore_xAxis_cross_lt_xAxis_pair (ne_of_lt hxy) hv
        (Or.inl ⟨hu.2, hylet⟩))

theorem exists_descent_of_adjacent_baseLineParameters
    {S : Finset Point} {a b p : Point} {x y u v t : ℝ}
    (hpS : p ∈ S) (hab : a ≠ b) (hnp : ¬ Collinear3 a b p)
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (hxy : x < y)
    (hxT : x ∈ baseLineParameters S a b)
    (hyT : y ∈ baseLineParameters S a b)
    (htT : t ∈ baseLineParameters S a b)
    (htx : t ≠ x) (hty : t ≠ y)
    (hu : x ≤ u ∧ u ≤ y)
    (hout :
      ∀ r ∈ baseLineParameters S a b, r ≠ x → r ≠ y → r ≤ x ∨ y ≤ r) :
    ∃ w ∈ noncollinearTriples S, linePointScore w < linePointScore (a, b, p) := by
  rcases exists_of_mem_baseLineParameters hxT with ⟨X, hXS, hXcol, hXnorm⟩
  rcases exists_of_mem_baseLineParameters hyT with ⟨Y, hYS, hYcol, hYnorm⟩
  have hXY : X ≠ Y := by
    intro hXYeq
    have htmp := hXnorm
    rw [hXYeq, hYnorm] at htmp
    have hxy_eq : x = y := (congrArg Prod.fst htmp).symm
    linarith
  have hxydist : squaredDist X Y ≠ 0 := ne_of_gt (squaredDist_pos_of_ne hXY)
  rcases exists_normalized_cross_descent_of_adjacent_parameters
      hpnorm hxy htT htx hty hu hout hnp with
    ⟨C, hCS, hCcol, hCnorm, hineq⟩
  have hpC : p ≠ C := by
    intro hpc
    apply hnp
    rw [hpc]
    exact hCcol
  have hpcdist : squaredDist p C ≠ 0 := ne_of_gt (squaredDist_pos_of_ne hpC)
  have hCX : C ≠ X := by
    intro hCXeq
    apply htx
    have htmp := hCnorm
    rw [hCXeq, hXnorm] at htmp
    exact (congrArg Prod.fst htmp).symm
  have hCY : C ≠ Y := by
    intro hCYeq
    apply hty
    have htmp := hCnorm
    rw [hCYeq, hYnorm] at htmp
    exact (congrArg Prod.fst htmp).symm
  have hscoreXY : linePointScore (X, Y, p) = linePointScore (a, b, p) :=
    linePointScore_eq_of_collinear_base hab hXY hXcol hYcol
  rcases hineq with hleft | hright
  · have hlt :
        linePointScore (p, C, X) < linePointScore (X, Y, p) := by
      apply (linePointScore_normalizeToXAxis_lt_iff hab hpcdist hxydist).1
      rw [hpnorm, hCnorm, hXnorm, hYnorm]
      exact hleft
    refine ⟨(p, C, X), ?_, ?_⟩
    · exact mem_noncollinearTriples_cross_base_pair hpS hCS hXS hab hCcol hXcol hCX hnp
    · exact hlt.trans_eq hscoreXY
  · have hlt :
        linePointScore (p, C, Y) < linePointScore (X, Y, p) := by
      apply (linePointScore_normalizeToXAxis_lt_iff hab hpcdist hxydist).1
      rw [hpnorm, hCnorm, hXnorm, hYnorm]
      exact hright
    refine ⟨(p, C, Y), ?_, ?_⟩
    · exact mem_noncollinearTriples_cross_base_pair hpS hCS hYS hab hCcol hYcol hCY hnp
    · exact hlt.trans_eq hscoreXY

theorem exists_descent_of_selected_endpoint_baseLineParameter
    {S : Finset Point} {a b p : Point} {x y u v t e : ℝ}
    (hpS : p ∈ S) (hab : a ≠ b) (hnp : ¬ Collinear3 a b p)
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (hxy : x < y)
    (hxT : x ∈ baseLineParameters S a b)
    (hyT : y ∈ baseLineParameters S a b)
    (htT : t ∈ baseLineParameters S a b)
    (he : e = x ∨ e = y) (hte : t ≠ e)
    (hbetween : (u ≤ e ∧ e ≤ t) ∨ (t ≤ e ∧ e ≤ u)) :
    ∃ w ∈ noncollinearTriples S, linePointScore w < linePointScore (a, b, p) := by
  rcases exists_of_mem_baseLineParameters hxT with ⟨X, hXS, hXcol, hXnorm⟩
  rcases exists_of_mem_baseLineParameters hyT with ⟨Y, hYS, hYcol, hYnorm⟩
  rcases exists_of_mem_baseLineParameters htT with ⟨C, hCS, hCcol, hCnorm⟩
  have hXY : X ≠ Y := by
    intro hXYeq
    have htmp := hXnorm
    rw [hXYeq, hYnorm] at htmp
    have hxy_eq : x = y := (congrArg Prod.fst htmp).symm
    linarith
  have hxydist : squaredDist X Y ≠ 0 := ne_of_gt (squaredDist_pos_of_ne hXY)
  have hpC : p ≠ C := by
    intro hpc
    apply hnp
    rw [hpc]
    exact hCcol
  have hpcdist : squaredDist p C ≠ 0 := ne_of_gt (squaredDist_pos_of_ne hpC)
  have hv : v ≠ 0 := by
    have hvnorm := normalizeToXAxis_snd_ne_zero_of_not_collinear3 hnp
    rw [hpnorm] at hvnorm
    exact hvnorm
  have hscoreXY : linePointScore (X, Y, p) = linePointScore (a, b, p) :=
    linePointScore_eq_of_collinear_base hab hXY hXcol hYcol
  rcases he with heq | heq
  · have hCX : C ≠ X := by
      intro hCXeq
      apply hte
      rw [heq]
      have htmp := hCnorm
      rw [hCXeq, hXnorm] at htmp
      exact (congrArg Prod.fst htmp).symm
    have hbetweenx : (u ≤ x ∧ x ≤ t) ∨ (t ≤ x ∧ x ≤ u) := by
      simpa [heq] using hbetween
    have hnormlt :
        linePointScore (((u, v) : Point), ((t, 0) : Point), ((x, 0) : Point)) <
          linePointScore (((x, 0) : Point), ((y, 0) : Point), ((u, v) : Point)) :=
      linePointScore_xAxis_cross_lt_xAxis_pair (ne_of_lt hxy) hv hbetweenx
    have hlt :
        linePointScore (p, C, X) < linePointScore (X, Y, p) := by
      apply (linePointScore_normalizeToXAxis_lt_iff hab hpcdist hxydist).1
      rw [hpnorm, hCnorm, hXnorm, hYnorm]
      exact hnormlt
    refine ⟨(p, C, X), ?_, hlt.trans_eq hscoreXY⟩
    exact mem_noncollinearTriples_cross_base_pair hpS hCS hXS hab hCcol hXcol hCX hnp
  · have hCY : C ≠ Y := by
      intro hCYeq
      apply hte
      rw [heq]
      have htmp := hCnorm
      rw [hCYeq, hYnorm] at htmp
      exact (congrArg Prod.fst htmp).symm
    have hbetweeny : (u ≤ y ∧ y ≤ t) ∨ (t ≤ y ∧ y ≤ u) := by
      simpa [heq] using hbetween
    have hnormlt :
        linePointScore (((u, v) : Point), ((t, 0) : Point), ((y, 0) : Point)) <
          linePointScore (((x, 0) : Point), ((y, 0) : Point), ((u, v) : Point)) :=
      linePointScore_xAxis_cross_lt_xAxis_pair (ne_of_lt hxy) hv hbetweeny
    have hlt :
        linePointScore (p, C, Y) < linePointScore (X, Y, p) := by
      apply (linePointScore_normalizeToXAxis_lt_iff hab hpcdist hxydist).1
      rw [hpnorm, hCnorm, hXnorm, hYnorm]
      exact hnormlt
    refine ⟨(p, C, Y), ?_, hlt.trans_eq hscoreXY⟩
    exact mem_noncollinearTriples_cross_base_pair hpS hCS hYS hab hCcol hYcol hCY hnp

theorem ordinary_or_descent_of_adjacent_baseLineParameters
    {S : Finset Point} {a b p : Point} {x y u v : ℝ}
    (hpS : p ∈ S) (hab : a ≠ b) (hnp : ¬ Collinear3 a b p)
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (hxy : x < y)
    (hxT : x ∈ baseLineParameters S a b)
    (hyT : y ∈ baseLineParameters S a b)
    (hu : x ≤ u ∧ u ≤ y)
    (hout :
      ∀ r ∈ baseLineParameters S a b, r ≠ x → r ≠ y → r ≤ x ∨ y ≤ r) :
    (∃ X Y : Point, OrdinaryPair S X Y) ∨
      ∃ w ∈ noncollinearTriples S, linePointScore w < linePointScore (a, b, p) := by
  rcases exists_of_mem_baseLineParameters hxT with ⟨X, hXS, hXcol, hXnorm⟩
  rcases exists_of_mem_baseLineParameters hyT with ⟨Y, hYS, hYcol, hYnorm⟩
  have hXY : X ≠ Y := by
    intro hXYeq
    have htmp := hXnorm
    rw [hXYeq, hYnorm] at htmp
    have hxy_eq : x = y := (congrArg Prod.fst htmp).symm
    linarith
  by_cases hOrd : OrdinaryPair S X Y
  · exact Or.inl ⟨X, Y, hOrd⟩
  · rcases exists_collinear_ne_of_not_ordinaryPair hXS hYS hXY hOrd with
      ⟨C, hCS, hCXY, hCX, hCY⟩
    have hCold : Collinear3 a b C :=
      collinear3_of_collinear3_selected_base hab (ne_of_lt hxy) hXnorm hYnorm hCXY
    let t : ℝ := (normalizeToXAxis a b C).1
    have htT : t ∈ baseLineParameters S a b :=
      mem_baseLineParameters_of_collinear hCS hCold
    have htx : t ≠ x := by
      intro htxeq
      apply hCX
      apply normalizeToXAxis_injective hab
      rw [hXnorm]
      exact Prod.ext htxeq (normalizeToXAxis_snd_eq_zero_of_collinear3 hCold)
    have hty : t ≠ y := by
      intro htyeq
      apply hCY
      apply normalizeToXAxis_injective hab
      rw [hYnorm]
      exact Prod.ext htyeq (normalizeToXAxis_snd_eq_zero_of_collinear3 hCold)
    exact Or.inr
      (exists_descent_of_adjacent_baseLineParameters hpS hab hnp hpnorm hxy
        hxT hyT htT htx hty hu hout)

theorem exists_ordinaryPair_of_min_adjacent_baseLineParameters
    {S : Finset Point} {a b p : Point} {x y u v : ℝ}
    (hpS : p ∈ S) (hab : a ≠ b) (hnp : ¬ Collinear3 a b p)
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (hxy : x < y)
    (hxT : x ∈ baseLineParameters S a b)
    (hyT : y ∈ baseLineParameters S a b)
    (hu : x ≤ u ∧ u ≤ y)
    (hout :
      ∀ r ∈ baseLineParameters S a b, r ≠ x → r ≠ y → r ≤ x ∨ y ≤ r)
    (hmin : ∀ w ∈ noncollinearTriples S,
      linePointScore (a, b, p) ≤ linePointScore w) :
    ∃ X Y : Point, OrdinaryPair S X Y := by
  rcases ordinary_or_descent_of_adjacent_baseLineParameters hpS hab hnp hpnorm hxy
      hxT hyT hu hout with hOrd | hdesc
  · exact hOrd
  · rcases hdesc with ⟨w, hw, hlt⟩
    have hle := hmin w hw
    exact False.elim (not_lt_of_ge hle hlt)

theorem exists_ordinaryPair_of_min_strict_bracket_baseLineParameters
    {S : Finset Point} {a b p : Point} {u v : ℝ}
    (hpS : p ∈ S) (hab : a ≠ b) (hnp : ¬ Collinear3 a b p)
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (huT : u ∉ baseLineParameters S a b)
    (hleft : ∃ x ∈ baseLineParameters S a b, x < u)
    (hright : ∃ y ∈ baseLineParameters S a b, u < y)
    (hmin : ∀ w ∈ noncollinearTriples S,
      linePointScore (a, b, p) ≤ linePointScore w) :
    ∃ X Y : Point, OrdinaryPair S X Y := by
  rcases exists_strictAdjacentParametersAround_of_not_mem_of_exists_lt_gt
      huT hleft hright with ⟨x, y, hxT, hyT, hxu, huy, hout⟩
  exact exists_ordinaryPair_of_min_adjacent_baseLineParameters hpS hab hnp hpnorm
    (by linarith) hxT hyT ⟨le_of_lt hxu, le_of_lt huy⟩
    (fun r hrT _ _ => hout r hrT) hmin

theorem exists_ordinaryPair_of_min_rightAdjacent_baseLineParameters
    {S : Finset Point} {a b p : Point} {x y u v : ℝ}
    (hpS : p ∈ S) (hab : a ≠ b) (hnp : ¬ Collinear3 a b p)
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (hadj : RightAdjacentParametersAfterProjection (baseLineParameters S a b) u x y)
    (hmin : ∀ w ∈ noncollinearTriples S,
      linePointScore (a, b, p) ≤ linePointScore w) :
    ∃ X Y : Point, OrdinaryPair S X Y := by
  rcases hadj with ⟨hxT, hyT, hux, hxy, hout⟩
  rcases exists_of_mem_baseLineParameters hxT with ⟨X, hXS, hXcol, hXnorm⟩
  rcases exists_of_mem_baseLineParameters hyT with ⟨Y, hYS, hYcol, hYnorm⟩
  have hXY : X ≠ Y := by
    intro hXYeq
    have htmp := hXnorm
    rw [hXYeq, hYnorm] at htmp
    have hxy_eq : x = y := (congrArg Prod.fst htmp).symm
    linarith
  by_cases hOrd : OrdinaryPair S X Y
  · exact ⟨X, Y, hOrd⟩
  · rcases exists_collinear_ne_of_not_ordinaryPair hXS hYS hXY hOrd with
      ⟨C, hCS, hCXY, hCX, hCY⟩
    have hCold : Collinear3 a b C :=
      collinear3_of_collinear3_selected_base hab (ne_of_lt hxy) hXnorm hYnorm hCXY
    let t : ℝ := (normalizeToXAxis a b C).1
    have htT : t ∈ baseLineParameters S a b :=
      mem_baseLineParameters_of_collinear hCS hCold
    have htx : t ≠ x := by
      intro htxeq
      apply hCX
      apply normalizeToXAxis_injective hab
      rw [hXnorm]
      exact Prod.ext htxeq (normalizeToXAxis_snd_eq_zero_of_collinear3 hCold)
    have hty : t ≠ y := by
      intro htyeq
      apply hCY
      apply normalizeToXAxis_injective hab
      rw [hYnorm]
      exact Prod.ext htyeq (normalizeToXAxis_snd_eq_zero_of_collinear3 hCold)
    have hbetween : (u ≤ y ∧ y ≤ t) ∨ (t ≤ y ∧ y ≤ u) :=
      Or.inl ⟨le_of_lt (hux.trans hxy), hout t htT htx⟩
    rcases exists_descent_of_selected_endpoint_baseLineParameter hpS hab hnp hpnorm
        hxy hxT hyT htT (Or.inr rfl) hty hbetween with ⟨w, hw, hlt⟩
    have hle := hmin w hw
    exact False.elim (not_lt_of_ge hle hlt)

theorem exists_ordinaryPair_of_min_leftAdjacent_baseLineParameters
    {S : Finset Point} {a b p : Point} {x y u v : ℝ}
    (hpS : p ∈ S) (hab : a ≠ b) (hnp : ¬ Collinear3 a b p)
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (hadj : LeftAdjacentParametersBeforeProjection (baseLineParameters S a b) u x y)
    (hmin : ∀ w ∈ noncollinearTriples S,
      linePointScore (a, b, p) ≤ linePointScore w) :
    ∃ X Y : Point, OrdinaryPair S X Y := by
  rcases hadj with ⟨hxT, hyT, hxy, hyu, hout⟩
  rcases exists_of_mem_baseLineParameters hxT with ⟨X, hXS, hXcol, hXnorm⟩
  rcases exists_of_mem_baseLineParameters hyT with ⟨Y, hYS, hYcol, hYnorm⟩
  have hXY : X ≠ Y := by
    intro hXYeq
    have htmp := hXnorm
    rw [hXYeq, hYnorm] at htmp
    have hxy_eq : x = y := (congrArg Prod.fst htmp).symm
    linarith
  by_cases hOrd : OrdinaryPair S X Y
  · exact ⟨X, Y, hOrd⟩
  · rcases exists_collinear_ne_of_not_ordinaryPair hXS hYS hXY hOrd with
      ⟨C, hCS, hCXY, hCX, hCY⟩
    have hCold : Collinear3 a b C :=
      collinear3_of_collinear3_selected_base hab (ne_of_lt hxy) hXnorm hYnorm hCXY
    let t : ℝ := (normalizeToXAxis a b C).1
    have htT : t ∈ baseLineParameters S a b :=
      mem_baseLineParameters_of_collinear hCS hCold
    have htx : t ≠ x := by
      intro htxeq
      apply hCX
      apply normalizeToXAxis_injective hab
      rw [hXnorm]
      exact Prod.ext htxeq (normalizeToXAxis_snd_eq_zero_of_collinear3 hCold)
    have hty : t ≠ y := by
      intro htyeq
      apply hCY
      apply normalizeToXAxis_injective hab
      rw [hYnorm]
      exact Prod.ext htyeq (normalizeToXAxis_snd_eq_zero_of_collinear3 hCold)
    have hbetween : (u ≤ x ∧ x ≤ t) ∨ (t ≤ x ∧ x ≤ u) :=
      Or.inr ⟨hout t htT hty, le_of_lt (hxy.trans hyu)⟩
    rcases exists_descent_of_selected_endpoint_baseLineParameter hpS hab hnp hpnorm
        hxy hxT hyT htT (Or.inl rfl) htx hbetween with ⟨w, hw, hlt⟩
    have hle := hmin w hw
    exact False.elim (not_lt_of_ge hle hlt)

theorem exists_ordinaryPair_of_min_projectionLeft_baseLineParameters
    {S : Finset Point} {a b p : Point} {u v y : ℝ}
    (hpS : p ∈ S) (hab : a ≠ b) (hnp : ¬ Collinear3 a b p)
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (hadj : ProjectionLeftAdjacentParameter (baseLineParameters S a b) u y)
    (hmin : ∀ w ∈ noncollinearTriples S,
      linePointScore (a, b, p) ≤ linePointScore w) :
    ∃ X Y : Point, OrdinaryPair S X Y := by
  rcases hadj with ⟨huT, hyT, huy, hout⟩
  exact exists_ordinaryPair_of_min_adjacent_baseLineParameters hpS hab hnp hpnorm
    huy huT hyT ⟨le_rfl, le_of_lt huy⟩
    (fun r hrT hru hry => hout r hrT hru hry) hmin

theorem exists_ordinaryPair_of_min_projectionRight_baseLineParameters
    {S : Finset Point} {a b p : Point} {x u v : ℝ}
    (hpS : p ∈ S) (hab : a ≠ b) (hnp : ¬ Collinear3 a b p)
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (hadj : ProjectionRightAdjacentParameter (baseLineParameters S a b) u x)
    (hmin : ∀ w ∈ noncollinearTriples S,
      linePointScore (a, b, p) ≤ linePointScore w) :
    ∃ X Y : Point, OrdinaryPair S X Y := by
  rcases hadj with ⟨hxT, huT, hxu, hout⟩
  exact exists_ordinaryPair_of_min_adjacent_baseLineParameters hpS hab hnp hpnorm
    hxu hxT huT ⟨le_of_lt hxu, le_rfl⟩
    (fun r hrT hrx hru => hout r hrT hrx hru) hmin

theorem exists_ordinaryPair_of_min_baseLineParameters
    {S : Finset Point} {a b p : Point} {u v : ℝ}
    (haS : a ∈ S) (hbS : b ∈ S) (hpS : p ∈ S)
    (hab : a ≠ b) (hnp : ¬ Collinear3 a b p)
    (hpnorm : normalizeToXAxis a b p = (u, v))
    (hmin : ∀ w ∈ noncollinearTriples S,
      linePointScore (a, b, p) ≤ linePointScore w) :
    ∃ X Y : Point, OrdinaryPair S X Y := by
  classical
  let T : Finset ℝ := baseLineParameters S a b
  have hcard : 1 < T.card := one_lt_card_baseLineParameters haS hbS hab
  by_cases huT : u ∈ T
  · by_cases hright : ∃ y ∈ T, u < y
    · rcases exists_projectionLeftAdjacentParameter_of_mem_of_exists_gt huT hright with
        ⟨y, hadj⟩
      exact exists_ordinaryPair_of_min_projectionLeft_baseLineParameters hpS hab hnp
        hpnorm hadj hmin
    · have hleft : ∃ x ∈ T, x < u := by
        rcases Finset.one_lt_card.mp hcard with ⟨r, hrT, s, hsT, hrs⟩
        have hne : ∃ z ∈ T, z ≠ u := by
          by_cases hru : r = u
          · refine ⟨s, hsT, ?_⟩
            intro hsu
            exact hrs (hru.trans hsu.symm)
          · exact ⟨r, hrT, hru⟩
        rcases hne with ⟨z, hzT, hzu⟩
        rcases lt_or_gt_of_ne hzu with hzu_lt | huz_lt
        · exact ⟨z, hzT, hzu_lt⟩
        · exact False.elim (hright ⟨z, hzT, huz_lt⟩)
      rcases exists_projectionRightAdjacentParameter_of_mem_of_exists_lt huT hleft with
        ⟨x, hadj⟩
      exact exists_ordinaryPair_of_min_projectionRight_baseLineParameters hpS hab hnp
        hpnorm hadj hmin
  · by_cases hleft : ∃ x ∈ T, x < u
    · by_cases hright : ∃ y ∈ T, u < y
      · exact exists_ordinaryPair_of_min_strict_bracket_baseLineParameters hpS hab hnp
          hpnorm huT hleft hright hmin
      · have hall_lt : ∀ z ∈ T, z < u := by
          intro z hzT
          have hnot_gt : ¬ u < z := by
            intro huz
            exact hright ⟨z, hzT, huz⟩
          have hzu_ne : z ≠ u := by
            intro hzu
            exact huT (hzu ▸ hzT)
          exact lt_of_le_of_ne (le_of_not_gt hnot_gt) hzu_ne
        rcases exists_leftAdjacentParametersBeforeProjection_of_forall_lt hcard hall_lt with
          ⟨x, y, hadj⟩
        exact exists_ordinaryPair_of_min_leftAdjacent_baseLineParameters hpS hab hnp
          hpnorm hadj hmin
    · have hall_gt : ∀ z ∈ T, u < z := by
        intro z hzT
        have hnot_lt : ¬ z < u := by
          intro hzu
          exact hleft ⟨z, hzT, hzu⟩
        have hzu_ne : z ≠ u := by
          intro hzu
          exact huT (hzu ▸ hzT)
        exact lt_of_le_of_ne (le_of_not_gt hnot_lt) hzu_ne.symm
      rcases exists_rightAdjacentParametersAfterProjection_of_forall_gt hcard hall_gt with
        ⟨x, y, hadj⟩
      exact exists_ordinaryPair_of_min_rightAdjacent_baseLineParameters hpS hab hnp
        hpnorm hadj hmin

theorem ordinaryPair_symm {S : Finset Point} {a b : Point}
    (h : OrdinaryPair S a b) : OrdinaryPair S b a := by
  refine ⟨ordinaryPair_right_mem h, ordinaryPair_left_mem h, ?_, ?_⟩
  · intro hba
    exact ordinaryPair_ne h hba.symm
  · intro c hcS hcol
    rcases ordinaryPair_collinear_cases h hcS (collinear3_swap_left hcol) with hca | hcb
    · exact Or.inr hca
    · exact Or.inl hcb

theorem ordinaryPair_comm {S : Finset Point} {a b : Point} :
    OrdinaryPair S a b ↔ OrdinaryPair S b a :=
  ⟨ordinaryPair_symm, ordinaryPair_symm⟩

theorem exists_not_collinear3_of_not_finsetCollinear {S : Finset Point}
    (hcard : 2 < S.card) (hS : ¬ FinsetCollinear S) :
    ∃ a ∈ S, ∃ b ∈ S, ∃ c ∈ S, ¬ Collinear3 a b c := by
  classical
  have hcard_one : 1 < S.card := by omega
  rcases (Finset.one_lt_card.mp hcard_one) with ⟨a, haS, b, hbS, hab⟩
  by_contra h
  apply hS
  refine ⟨a, haS, b, hbS, hab, ?_⟩
  intro c hcS
  by_contra hcol
  exact h ⟨a, haS, b, hbS, c, hcS, hcol⟩

theorem all_collinear3_of_finsetCollinear {S : Finset Point}
    (hS : FinsetCollinear S) :
    ∀ ⦃x⦄, x ∈ S → ∀ ⦃y⦄, y ∈ S → ∀ ⦃z⦄, z ∈ S → Collinear3 x y z := by
  rcases hS with ⟨a, _haS, b, _hbS, hab, hall⟩
  intro x hxS y hyS z hzS
  exact collinear3_of_mem_line
    (mem_line_of_collinear3 hab (hall x hxS))
    (mem_line_of_collinear3 hab (hall y hyS))
    (mem_line_of_collinear3 hab (hall z hzS))

theorem not_finsetCollinear_iff_exists_not_collinear3 {S : Finset Point}
    (hcard : 2 < S.card) :
    ¬ FinsetCollinear S ↔
      ∃ a ∈ S, ∃ b ∈ S, ∃ c ∈ S, ¬ Collinear3 a b c := by
  constructor
  · exact exists_not_collinear3_of_not_finsetCollinear hcard
  · rintro ⟨a, haS, b, hbS, c, hcS, habc⟩ hS
    exact habc (all_collinear3_of_finsetCollinear hS haS hbS hcS)

theorem noncollinearTriples_nonempty {S : Finset Point}
    (hcard : 2 < S.card) (hS : ¬ FinsetCollinear S) :
    (noncollinearTriples S).Nonempty := by
  classical
  rcases exists_not_collinear3_of_not_finsetCollinear hcard hS with
    ⟨a, haS, b, hbS, c, hcS, habc⟩
  exact ⟨(a, b, c), by simp [mem_noncollinearTriples, haS, hbS, hcS, habc]⟩

theorem exists_min_tripleAbsDet_noncollinear {S : Finset Point}
    (hcard : 2 < S.card) (hS : ¬ FinsetCollinear S) :
    ∃ t ∈ noncollinearTriples S, ∀ u ∈ noncollinearTriples S,
      tripleAbsDet t ≤ tripleAbsDet u := by
  classical
  exact Finset.exists_min_image (noncollinearTriples S) tripleAbsDet
    (noncollinearTriples_nonempty hcard hS)

theorem exists_min_linePointScore_noncollinear {S : Finset Point}
    (hcard : 2 < S.card) (hS : ¬ FinsetCollinear S) :
    ∃ t ∈ noncollinearTriples S, ∀ u ∈ noncollinearTriples S,
      linePointScore t ≤ linePointScore u := by
  classical
  exact Finset.exists_min_image (noncollinearTriples S) linePointScore
    (noncollinearTriples_nonempty hcard hS)

def origin : Point := (0, 0)

def xAxisOne : Point := (1, 0)

def yAxisOne : Point := (0, 1)

theorem coordinate_axes_not_collinear :
    ¬ Collinear3 origin xAxisOne yAxisOne := by
  norm_num [Collinear3, orientationDet, origin, xAxisOne, yAxisOne]

/-- The Sylvester-Gallai theorem for finite subsets of the concrete real affine plane. -/
theorem sylvesterGallai :
    SylvesterGallaiStatement := by
  intro S hcard hS
  rcases exists_min_linePointScore_noncollinear hcard hS with ⟨t, htmem, hmin⟩
  rcases t with ⟨a, b, p⟩
  rcases (mem_noncollinearTriples.mp htmem) with ⟨haS, hbS, hpS, hnp⟩
  have hab : a ≠ b := not_collinear3_ne_left hnp
  exact exists_ordinaryPair_of_min_baseLineParameters
    (S := S) (a := a) (b := b) (p := p)
    (u := (normalizeToXAxis a b p).1) (v := (normalizeToXAxis a b p).2)
    haS hbS hpS hab hnp (by ext <;> rfl) hmin

/-- Checked statement wrapper for the minimum theorem. -/
theorem sylvesterGallai_statement :
    SylvesterGallaiStatement ↔ SylvesterGallaiStatement := by
  rfl

end AtlasKnownTheorems.SylvesterGallai