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

import Mathlib.Combinatorics.Pigeonhole
import Mathlib.Data.Fin.Basic
import Mathlib.Order.Basic
import Mathlib.Order.KrullDimension
import Mathlib.Tactic

/-!
# Erdős-Szekeres Monotone Subsequence Seed

This file prepares the finite monotone-subsequence theorem route. The theorem
is proved below by assigning each index its increasing and decreasing
graph-height ranks and applying pigeonhole counting.
-/

namespace AtlasKnownTheorems.ErdosSzekeresMonotone

/-- A strictly increasing subsequence encoded by a strictly increasing index map. -/
def HasStrictIncreasingSubsequence {α : Type} [Preorder α] {n : Nat}
    (a : Fin n → α) (k : Nat) : Prop :=
  ∃ idx : Fin k → Fin n, StrictMono idx ∧ StrictMono (fun i => a (idx i))

/-- A strictly decreasing subsequence encoded by a strictly increasing index map. -/
def HasStrictDecreasingSubsequence {α : Type} [Preorder α] {n : Nat}
    (a : Fin n → α) (k : Nat) : Prop :=
  ∃ idx : Fin k → Fin n, StrictMono idx ∧ StrictAnti (fun i => a (idx i))

/--
Finite Erdős-Szekeres monotone-subsequence theorem for injective sequences over
a linear order.
-/
def ErdosSzekeresMonotoneStatement : Prop :=
  ∀ (α : Type) [LinearOrder α] (r s : Nat)
    (a : Fin (r * s + 1) → α),
    Function.Injective a →
      HasStrictIncreasingSubsequence a (r + 1) ∨
      HasStrictDecreasingSubsequence a (s + 1)

theorem increasingSubsequence_of_strictMono
    {α : Type} [Preorder α] {n : Nat} (a : Fin n → α)
    (ha : StrictMono a) :
    HasStrictIncreasingSubsequence a n := by
  exact ⟨id, strictMono_id, ha⟩

theorem decreasingSubsequence_of_strictAnti
    {α : Type} [Preorder α] {n : Nat} (a : Fin n → α)
    (ha : StrictAnti a) :
    HasStrictDecreasingSubsequence a n := by
  exact ⟨id, strictMono_id, ha⟩

/-- Graph points ordered by index and value, for increasing subsequences. -/
abbrev IncreasingPoint {α : Type} [Preorder α] {n : Nat} (a : Fin n → α) :=
  {p : Fin n × α // p.2 = a p.1}

/-- Graph points ordered by index and reversed value, for decreasing subsequences. -/
abbrev DecreasingPoint {α : Type} [Preorder α] {n : Nat} (a : Fin n → α) :=
  {p : Fin n × αᵒᵈ // p.2 = OrderDual.toDual (a p.1)}

def increasingPoint {α : Type} [Preorder α] {n : Nat} (a : Fin n → α) (i : Fin n) :
    IncreasingPoint a :=
  ⟨(i, a i), rfl⟩

def decreasingPoint {α : Type} [Preorder α] {n : Nat} (a : Fin n → α) (i : Fin n) :
    DecreasingPoint a :=
  ⟨(i, OrderDual.toDual (a i)), rfl⟩

noncomputable def enatToFin {r : Nat} {x : ℕ∞} (h : x < (r : ℕ∞)) : Fin r :=
  let hx : ∃ m : Nat, (m : ℕ∞) = x :=
    WithTop.ne_top_iff_exists.mp (ne_top_of_lt (lt_trans h (ENat.coe_lt_top r)))
  ⟨hx.choose, by
    have hm := hx.choose_spec
    rw [← hm] at h
    exact ENat.coe_lt_coe.mp h⟩

theorem enatToFin_spec {r : Nat} {x : ℕ∞} (h : x < (r : ℕ∞)) :
    ((enatToFin h).1 : ℕ∞) = x := by
  unfold enatToFin
  simp only
  exact (WithTop.ne_top_iff_exists.mp
    (ne_top_of_lt (lt_trans h (ENat.coe_lt_top r)))).choose_spec

theorem increasingPoint_lt_of_index_lt_of_value_lt {α : Type} [LinearOrder α] {n : Nat}
    {a : Fin n → α} {i j : Fin n} (hij : i < j) (hval : a i < a j) :
    increasingPoint a i < increasingPoint a j := by
  rw [lt_iff_le_not_ge]
  constructor
  · show ((i, a i) : Fin n × α) ≤ (j, a j)
    rw [Prod.le_def]
    exact ⟨le_of_lt hij, le_of_lt hval⟩
  · intro hle
    have hle' : ((j, a j) : Fin n × α) ≤ (i, a i) := hle
    rw [Prod.le_def] at hle'
    exact not_lt_of_ge hle'.1 hij

theorem decreasingPoint_lt_of_index_lt_of_value_gt {α : Type} [LinearOrder α] {n : Nat}
    {a : Fin n → α} {i j : Fin n} (hij : i < j) (hval : a j < a i) :
    decreasingPoint a i < decreasingPoint a j := by
  rw [lt_iff_le_not_ge]
  constructor
  · show ((i, OrderDual.toDual (a i)) : Fin n × αᵒᵈ) ≤
        (j, OrderDual.toDual (a j))
    rw [Prod.le_def]
    exact ⟨le_of_lt hij, le_of_lt hval⟩
  · intro hle
    have hle' : ((j, OrderDual.toDual (a j)) : Fin n × αᵒᵈ) ≤
        (i, OrderDual.toDual (a i)) := hle
    rw [Prod.le_def] at hle'
    exact not_lt_of_ge hle'.1 hij

theorem increasingPoint_lt_components {α : Type} [LinearOrder α] {n : Nat}
    {a : Fin n → α} (ha : Function.Injective a)
    (p q : IncreasingPoint a) (h : p < q) :
    p.1.1 < q.1.1 ∧ p.1.2 < q.1.2 := by
  rw [lt_iff_le_not_ge] at h
  rcases h with ⟨hle, hnle⟩
  have hle' : p.1 ≤ q.1 := hle
  have hnle' : ¬ q.1 ≤ p.1 := hnle
  rw [Prod.le_def] at hle'
  rw [Prod.le_def] at hnle'
  constructor
  · exact lt_of_le_of_ne hle'.1 (fun he => by
      apply hnle'
      constructor
      · exact le_of_eq he.symm
      · rw [p.2, q.2]
        exact le_of_eq (congrArg a he.symm))
  · exact lt_of_le_of_ne hle'.2 (fun he => by
      apply hnle'
      constructor
      · rw [p.2, q.2] at he
        exact le_of_eq (ha he).symm
      · exact le_of_eq he.symm)

theorem decreasingPoint_lt_components {α : Type} [LinearOrder α] {n : Nat}
    {a : Fin n → α} (ha : Function.Injective a)
    (p q : DecreasingPoint a) (h : p < q) :
    p.1.1 < q.1.1 ∧ p.1.2 < q.1.2 := by
  rw [lt_iff_le_not_ge] at h
  rcases h with ⟨hle, hnle⟩
  have hle' : p.1 ≤ q.1 := hle
  have hnle' : ¬ q.1 ≤ p.1 := hnle
  rw [Prod.le_def] at hle'
  rw [Prod.le_def] at hnle'
  constructor
  · exact lt_of_le_of_ne hle'.1 (fun he => by
      apply hnle'
      constructor
      · exact le_of_eq he.symm
      · rw [p.2, q.2]
        exact le_of_eq (congrArg (fun x => OrderDual.toDual (a x)) he.symm))
  · exact lt_of_le_of_ne hle'.2 (fun he => by
      apply hnle'
      constructor
      · rw [p.2, q.2] at he
        have heα : a p.1.1 = a q.1.1 := congrArg OrderDual.ofDual he
        exact le_of_eq (ha heα).symm
      · exact le_of_eq he.symm)

theorem increasingSubsequence_of_ltSeries {α : Type} [LinearOrder α] {n : Nat}
    {a : Fin n → α} (ha : Function.Injective a) (p : LTSeries (IncreasingPoint a)) :
    HasStrictIncreasingSubsequence a (p.length + 1) := by
  refine ⟨fun i => (p i).1.1, ?_, ?_⟩
  · intro i j hij
    exact (increasingPoint_lt_components ha (p i) (p j) (p.strictMono hij)).1
  · intro i j hij
    have hv := (increasingPoint_lt_components ha (p i) (p j) (p.strictMono hij)).2
    simpa [show (p i).1.2 = a (p i).1.1 from (p i).2,
      show (p j).1.2 = a (p j).1.1 from (p j).2] using hv

theorem decreasingSubsequence_of_ltSeries {α : Type} [LinearOrder α] {n : Nat}
    {a : Fin n → α} (ha : Function.Injective a) (p : LTSeries (DecreasingPoint a)) :
    HasStrictDecreasingSubsequence a (p.length + 1) := by
  refine ⟨fun i => (p i).1.1, ?_, ?_⟩
  · intro i j hij
    exact (decreasingPoint_lt_components ha (p i) (p j) (p.strictMono hij)).1
  · intro i j hij
    have hv := (decreasingPoint_lt_components ha (p i) (p j) (p.strictMono hij)).2
    simpa [show (p i).1.2 = OrderDual.toDual (a (p i).1.1) from (p i).2,
      show (p j).1.2 = OrderDual.toDual (a (p j).1.1) from (p j).2] using hv

/-- Erdős-Szekeres monotone-subsequence theorem by the rank-pair proof. -/
theorem erdosSzekeresMonotone :
    ErdosSzekeresMonotoneStatement := by
  intro α _ r s a ha
  by_cases hr : r = 0
  · left
    subst r
    have hm : StrictMono a := by
      intro i j hij
      omega
    simpa using increasingSubsequence_of_strictMono a hm
  by_cases hs : s = 0
  · right
    subst s
    have hm : StrictAnti a := by
      intro i j hij
      omega
    simpa using decreasingSubsequence_of_strictAnti a hm
  by_cases hinc : HasStrictIncreasingSubsequence a (r + 1)
  · exact Or.inl hinc
  by_cases hdec : HasStrictDecreasingSubsequence a (s + 1)
  · exact Or.inr hdec
  exfalso
  have inc_lt : ∀ i : Fin (r * s + 1),
      Order.height (increasingPoint a i) < (r : ℕ∞) := by
    intro i
    apply lt_of_not_ge
    intro hge
    obtain ⟨p, _hp_last, hp_len⟩ :=
      Order.exists_series_of_le_height (increasingPoint a i) (n := r) hge
    exact hinc (by
      have hs' := increasingSubsequence_of_ltSeries ha p
      simpa [hp_len] using hs')
  have dec_lt : ∀ i : Fin (r * s + 1),
      Order.height (decreasingPoint a i) < (s : ℕ∞) := by
    intro i
    apply lt_of_not_ge
    intro hge
    obtain ⟨p, _hp_last, hp_len⟩ :=
      Order.exists_series_of_le_height (decreasingPoint a i) (n := s) hge
    exact hdec (by
      have hs' := decreasingSubsequence_of_ltSeries ha p
      simpa [hp_len] using hs')
  let rank : Fin (r * s + 1) → Fin r × Fin s := fun i =>
    (enatToFin (inc_lt i), enatToFin (dec_lt i))
  have rank_ne_of_lt : ∀ {i j : Fin (r * s + 1)}, i < j → rank i ≠ rank j := by
    intro i j hij hrank
    have hvalne : a i ≠ a j := ha.ne (ne_of_lt hij)
    rcases lt_or_gt_of_ne hvalne with hval | hval
    · have hpt : increasingPoint a i < increasingPoint a j :=
        increasingPoint_lt_of_index_lt_of_value_lt hij hval
      have hstrict : Order.height (increasingPoint a i) <
          Order.height (increasingPoint a j) :=
        Order.height_strictMono hpt (lt_trans (inc_lt i) (ENat.coe_lt_top r))
      have hfst : (rank i).1.1 = (rank j).1.1 := by
        exact congrArg (fun p : Fin r × Fin s => p.1.1) hrank
      have hheight : Order.height (increasingPoint a i) =
          Order.height (increasingPoint a j) := by
        have hi := enatToFin_spec (inc_lt i)
        have hj := enatToFin_spec (inc_lt j)
        rw [← hi, ← hj, hfst]
      exact (ne_of_lt hstrict) hheight
    · have hpt : decreasingPoint a i < decreasingPoint a j :=
        decreasingPoint_lt_of_index_lt_of_value_gt hij hval
      have hstrict : Order.height (decreasingPoint a i) <
          Order.height (decreasingPoint a j) :=
        Order.height_strictMono hpt (lt_trans (dec_lt i) (ENat.coe_lt_top s))
      have hsnd : (rank i).2.1 = (rank j).2.1 := by
        exact congrArg (fun p : Fin r × Fin s => p.2.1) hrank
      have hheight : Order.height (decreasingPoint a i) =
          Order.height (decreasingPoint a j) := by
        have hi := enatToFin_spec (dec_lt i)
        have hj := enatToFin_spec (dec_lt j)
        rw [← hi, ← hj, hsnd]
      exact (ne_of_lt hstrict) hheight
  have rank_inj : Function.Injective rank := by
    intro i j hij
    by_contra hne
    have hijlt_or : i < j ∨ j < i := lt_or_gt_of_ne hne
    cases hijlt_or with
    | inl hlt => exact rank_ne_of_lt hlt hij
    | inr hgt => exact rank_ne_of_lt hgt hij.symm
  have hcard := Fintype.card_le_of_injective rank rank_inj
  simp [Fintype.card_fin, Fintype.card_prod] at hcard

/-- Checked statement wrapper for the minimum theorem. -/
theorem erdosSzekeresMonotone_statement :
    ErdosSzekeresMonotoneStatement ↔ ErdosSzekeresMonotoneStatement := by
  rfl

end AtlasKnownTheorems.ErdosSzekeresMonotone