FormalConjectures.Arxiv.«1609.08688».sIncreasingrTuples

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

The length of an $s$-increasing sequence of $r$-tuples

This file contains the formalisation of [GoLo21] up to and including Conjecture 1.8.

References:

arxiv/1609.08688 The length of an $s$-increasing sequence of $r$-tuples by W. T. Gowers, J. Long

GoLo21 The length of an $s$-increasing sequence of $r$-tuples by W. T. Gowers, J. Long, Combinatorics, Probability and Computing (2021), 686-721

namespace Arxiv.«1609.08688»

Let $a = (a_1, a_2, a_3)$ and $b = (b_1, b_2, b_3)$ be two triples of integers. Say that $a$ is $2$-less than $b$, or $a <_2 b$, if $a_i < b_i$ for at least two coordinates $i$.

def lt₂ {α : Type*} [LT α] (a b : Fin 3 → α) : Prop :=
  ∃ (i j : Fin 3), i ≠ j ∧ a i < b i ∧ a j < b j

local infix:50 " <₂ " => lt₂

@[simp, category API, AMS 5]
theorem not_lt₂ {α : Type*} [LinearOrder α] {a b : Fin 3 → α} :
    ¬a <₂ b ↔ ∀ i j, i ≠ j → a i < b i → b j ≤ a j := byα:Type u_1inst✝:LinearOrder αa:Fin 3 → αb:Fin 3 → α⊢ ¬a <₂ b ↔ ∀ (i j : Fin 3), i ≠ j → a i < b i → b j ≤ a j simp [lt₂]All goals completed! 🐙

@[category API, AMS 5]
theorem not_lt₂_of_forall_le {α : Type*} [LinearOrder α] {a b : Fin 3 → α}
    (h : ∀ i, b i ≤ a i) : ¬a <₂ b := not_lt₂.2 fun _ _ _ _ => h _



@[category API, AMS 5]
theorem not_lt₂_of_exists {α : Type*} [LinearOrder α] {a b : Fin 3 → α}
    (i j : Fin 3) (hij : i ≠ j) (hi : b i ≤ a i) (hj : b j ≤ a j) :
    ¬a <₂ b := byα:Type u_1inst✝:LinearOrder αa:Fin 3 → αb:Fin 3 → αi:Fin 3j:Fin 3hij:i ≠ jhi:b i ≤ a ihj:b j ≤ a j⊢ ¬a <₂ b
  refine not_lt₂.2 fun k l hkl h => ?_α:Type u_1inst✝:LinearOrder αa:Fin 3 → αb:Fin 3 → αi:Fin 3j:Fin 3hij:i ≠ jhi:b i ≤ a ihj:b j ≤ a jk:Fin 3l:Fin 3hkl:k ≠ lh:a k < b k⊢ b l ≤ a l
  have : k ≠ i := fun hk => not_lt.2 hi (hk ▸ h)α:Type u_1inst✝:LinearOrder αa:Fin 3 → αb:Fin 3 → αi:Fin 3j:Fin 3hij:i ≠ jhi:b i ≤ a ihj:b j ≤ a jk:Fin 3l:Fin 3hkl:k ≠ lh:a k < b kthis:k ≠ i⊢ b l ≤ a l
  have : k ≠ j := fun hk => not_lt.2 hj (hk ▸ h)α:Type u_1inst✝:LinearOrder αa:Fin 3 → αb:Fin 3 → αi:Fin 3j:Fin 3hij:i ≠ jhi:b i ≤ a ihj:b j ≤ a jk:Fin 3l:Fin 3hkl:k ≠ lh:a k < b kthis✝:k ≠ ithis:k ≠ j⊢ b l ≤ a l
  have : l = i ∨ l = j := byα:Type u_1inst✝:LinearOrder αa:Fin 3 → αb:Fin 3 → αi:Fin 3j:Fin 3hij:i ≠ jhi:b i ≤ a ihj:b j ≤ a j⊢ ¬a <₂ bα:Type u_1inst✝:LinearOrder αa:Fin 3 → αb:Fin 3 → αi:Fin 3j:Fin 3hij:i ≠ jhi:b i ≤ a ihj:b j ≤ a jk:Fin 3l:Fin 3hkl:k ≠ lh:a k < b kthis✝¹:k ≠ ithis✝:k ≠ jthis:l = i ∨ l = j⊢ b l ≤ a l omegaα:Type u_1inst✝:LinearOrder αa:Fin 3 → αb:Fin 3 → αi:Fin 3j:Fin 3hij:i ≠ jhi:b i ≤ a ihj:b j ≤ a jk:Fin 3l:Fin 3hkl:k ≠ lh:a k < b kthis✝¹:k ≠ ithis✝:k ≠ jthis:l = i ∨ l = j⊢ b l ≤ a lα:Type u_1inst✝:LinearOrder αa:Fin 3 → αb:Fin 3 → αi:Fin 3j:Fin 3hij:i ≠ jhi:b i ≤ a ihj:b j ≤ a jk:Fin 3l:Fin 3hkl:k ≠ lh:a k < b kthis✝¹:k ≠ ithis✝:k ≠ jthis:l = i ∨ l = j⊢ b l ≤ a l
  rcases this with (rfl | rfl)inlα:Type u_1inst✝:LinearOrder αa:Fin 3 → αb:Fin 3 → αj:Fin 3hj:b j ≤ a jk:Fin 3l:Fin 3hkl:k ≠ lh:a k < b kthis✝:k ≠ jhij:l ≠ jhi:b l ≤ a lthis:k ≠ l⊢ b l ≤ a linrα:Type u_1inst✝:LinearOrder αa:Fin 3 → αb:Fin 3 → αi:Fin 3hi:b i ≤ a ik:Fin 3l:Fin 3hkl:k ≠ lh:a k < b kthis✝:k ≠ ihij:i ≠ lhj:b l ≤ a lthis:k ≠ l⊢ b l ≤ a l; exact hiinrα:Type u_1inst✝:LinearOrder αa:Fin 3 → αb:Fin 3 → αi:Fin 3hi:b i ≤ a ik:Fin 3l:Fin 3hkl:k ≠ lh:a k < b kthis✝:k ≠ ihij:i ≠ lhj:b l ≤ a lthis:k ≠ l⊢ b l ≤ a l; exact hjAll goals completed! 🐙

@[category API, AMS 5]
theorem not_lt₂_self {α : Type*} [LinearOrder α] (a : Fin 3 → α) : ¬a <₂ a := byα:Type u_1inst✝:LinearOrder αa:Fin 3 → α⊢ ¬a <₂ a
  simpAll goals completed! 🐙

For example, $(3, 3, 9) <_2 (5, 6, 1)$.

@[category test, AMS 5]
theorem lt₂_example_1 : ![3, 3, 9] <₂ ![5, 6, 1] := ⟨0, 1, zero_ne_one, by⊢ ![3, 3, 9] 0 < ![5, 6, 1] 0 ∧ ![3, 3, 9] 1 < ![5, 6, 1] 1 simpAll goals completed! 🐙⟩

$(5, 6, 1) <_2 (7, 7, 7)$

@[category test, AMS 5]
theorem lt₂_example_2 : ![5, 6, 1] <₂ ![7, 7, 7] := ⟨0, 2, by⊢ 0 ≠ 2 simpAll goals completed! 🐙, by⊢ ![5, 6, 1] 0 < ![7, 7, 7] 0 ∧ ![5, 6, 1] 2 < ![7, 7, 7] 2 simpAll goals completed! 🐙⟩

$(7, 7, 7) <_2 (7, 8, 9)$

@[category test, AMS 5]
theorem lt₂_example_3 : ![7, 7, 7] <₂ ![7, 8, 9] := ⟨1, 2, by⊢ 1 ≠ 2 simpAll goals completed! 🐙, by⊢ ![7, 7, 7] 1 < ![7, 8, 9] 1 ∧ ![7, 7, 7] 2 < ![7, 8, 9] 2 simpAll goals completed! 🐙⟩

but $(1, 2, 3)$ is not $2$-less than $(1, 2, 4)$.

@[category test, AMS 5]
theorem not_lt₂_example : ¬![1, 2, 3] <₂ ![1, 2, 4] := not_lt₂_of_exists 0 1 zero_ne_one (by⊢ ![1, 2, 4] 0 ≤ ![1, 2, 3] 0 simpAll goals completed! 🐙) (by⊢ ![1, 2, 4] 1 ≤ ![1, 2, 3] 1 simpAll goals completed! 🐙)

The $2$-less relation is not transitive on the naturals.

@[category API, AMS 5]
theorem not_trans_lt₂_nat : ∃ (a b c : Fin 3 → ℕ),
    a <₂ b ∧ b <₂ c ∧ ¬a <₂ c :=
  ⟨![1, 2, 3], ![2, 3, 1], ![3, 1, 2], ⟨0, 1, zero_ne_one, by⊢ ![1, 2, 3] 0 < ![2, 3, 1] 0 ∧ ![1, 2, 3] 1 < ![2, 3, 1] 1 simpAll goals completed! 🐙⟩,
     ⟨0, 2, by⊢ 0 ≠ 2 simpAll goals completed! 🐙, by⊢ ![2, 3, 1] 0 < ![3, 1, 2] 0 ∧ ![2, 3, 1] 2 < ![3, 1, 2] 2 simpAll goals completed! 🐙⟩, not_lt₂_of_exists 1 2 (by⊢ 1 ≠ 2 simpAll goals completed! 🐙) (by⊢ ![3, 1, 2] 1 ≤ ![1, 2, 3] 1 simpAll goals completed! 🐙) (by⊢ ![3, 1, 2] 2 ≤ ![1, 2, 3] 2 simpAll goals completed! 🐙)⟩

Since the $2$-less relation is not transitive, we make a further definition to specify transivity.

def IsIncreasing₂ {α : Type*} [LT α] (s : List (Fin 3 → α)) : Prop := s.Pairwise lt₂

@[simp, category API, AMS 5]
theorem isIncreasing₂_nil {α : Type*} [LT α] : IsIncreasing₂ (α := α) [] := byα:Type u_1inst✝:LT α⊢ IsIncreasing₂ []
  simp [IsIncreasing₂]All goals completed! 🐙

@[simp, category API, AMS 5]
theorem isIncreasing₂_singleton {α : Type*} [LT α] (a : Fin 3 → α) : IsIncreasing₂ [a] := byα:Type u_1inst✝:LT αa:Fin 3 → α⊢ IsIncreasing₂ [a]
  simp [IsIncreasing₂]All goals completed! 🐙



@[category API, AMS 5]
theorem isIncreasing₂_const_length {α : Type*} [LinearOrder α] {val : α} {s : List (Fin 3 → α)}
    (h : IsIncreasing₂ s)
    (h_const : ∀ a ∈ s, ∀ j, a j = val) : s.length < 2 := byα:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = val⊢ s.length < 2
  by_contra!α:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.length⊢ False
  obtain ⟨i, j, -, hi, -⟩ :=
    List.pairwise_iff_getElem.1 h 0 1 (byα:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.length⊢ 0 < s.lengthα:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.lengthi:Fin 3j:Fin 3hi:s[0] i < s[1] i⊢ False linarithAll goals completed! 🐙α:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.lengthi:Fin 3j:Fin 3hi:s[0] i < s[1] i⊢ False) (byα:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.length⊢ 1 < s.lengthα:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.lengthi:Fin 3j:Fin 3hi:s[0] i < s[1] i⊢ False linarithAll goals completed! 🐙α:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.lengthi:Fin 3j:Fin 3hi:s[0] i < s[1] i⊢ False) zero_lt_oneα:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.lengthi:Fin 3j:Fin 3hi:s[0] i < s[1] i⊢ False
  rw [h_const _ (List.getElem_mem _) i,α:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.lengthi:Fin 3j:Fin 3hi:val < s[1] i⊢ Falseα:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.lengthi:Fin 3j:Fin 3hi:val < val⊢ False h_const _ (List.getElem_mem _) iα:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.lengthi:Fin 3j:Fin 3hi:val < val⊢ Falseα:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.lengthi:Fin 3j:Fin 3hi:val < val⊢ False] at hiα:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.lengthi:Fin 3j:Fin 3hi:val < val⊢ False
  exact lt_irrefl _ hiAll goals completed! 🐙

Let $F(n)$ be the maximal length of a $2$-increasing sequence of triples with each coordinate belong to $[n]$ ($= {1, 2, ..., n}$).

noncomputable def maximalLength (n : ℕ) : ℕ :=
  sSup { List.length s | (s) (_ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (_ : IsIncreasing₂ s) }

local notation "F" => maximalLength



@[category test, AMS 5]
theorem maximalLength_zero : maximalLength 0 = 0 := by⊢ F 0 = 0
  have (x : ℕ) (s : List (Fin 3 → ℕ)) :
      IsIncreasing₂ s ∧ (∀ a, a ∉ s) ∧ s.length = x ↔ s = [] ∧ x = 0 := by
    refine ⟨fun ⟨ha₁, ha₂, rfl⟩ => ?_, fun ⟨h₁, h₂⟩ => byx:ℕs:List (Fin 3 → ℕ)x✝:s = [] ∧ x = 0h₁:s = []h₂:x = 0⊢ IsIncreasing₂ s ∧ (∀ (a : Fin 3 → ℕ), a ∉ s) ∧ s.length = xthis:∀ (x : ℕ) (s : List (Fin 3 → ℕ)), IsIncreasing₂ s ∧ (∀ (a : Fin 3 → ℕ), a ∉ s) ∧ s.length = x ↔ s = [] ∧ x = 0⊢ F 0 = 0 simp [h₁, h₂]All goals completed! 🐙this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)), IsIncreasing₂ s ∧ (∀ (a : Fin 3 → ℕ), a ∉ s) ∧ s.length = x ↔ s = [] ∧ x = 0⊢ F 0 = 0⟩
    simp only [List.length_eq_zero_iff, and_self]x:ℕs:List (Fin 3 → ℕ)x✝:IsIncreasing₂ s ∧ (∀ (a : Fin 3 → ℕ), a ∉ s) ∧ s.length = xha₁:IsIncreasing₂ sha₂:∀ (a : Fin 3 → ℕ), a ∉ s⊢ s = []this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)), IsIncreasing₂ s ∧ (∀ (a : Fin 3 → ℕ), a ∉ s) ∧ s.length = x ↔ s = [] ∧ x = 0⊢ F 0 = 0
    refine List.eq_nil_of_subset_nil fun ai hai => ?_x:ℕs:List (Fin 3 → ℕ)x✝:IsIncreasing₂ s ∧ (∀ (a : Fin 3 → ℕ), a ∉ s) ∧ s.length = xha₁:IsIncreasing₂ sha₂:∀ (a : Fin 3 → ℕ), a ∉ sai:Fin 3 → ℕhai:ai ∈ s⊢ ai ∈ []this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)), IsIncreasing₂ s ∧ (∀ (a : Fin 3 → ℕ), a ∉ s) ∧ s.length = x ↔ s = [] ∧ x = 0⊢ F 0 = 0
    simpa using ha₂ ai haithis:∀ (x : ℕ) (s : List (Fin 3 → ℕ)), IsIncreasing₂ s ∧ (∀ (a : Fin 3 → ℕ), a ∉ s) ∧ s.length = x ↔ s = [] ∧ x = 0⊢ F 0 = 0this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)), IsIncreasing₂ s ∧ (∀ (a : Fin 3 → ℕ), a ∉ s) ∧ s.length = x ↔ s = [] ∧ x = 0⊢ F 0 = 0
  simp [maximalLength, fun x => exists_congr (this x)]All goals completed! 🐙



@[category test, AMS 5]
theorem maximalLength_one : maximalLength 1 = 1 := by⊢ F 1 = 1
  classical
  have (x : ℕ) (s : List (Fin 3 → ℕ)) :
      IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ i, a i = 1) ∧ s.length = x ↔
        s = [fun _ => 1] ∧ x = 1 ∨ s = [] ∧ x = 0 := by
    refine ⟨fun ⟨hs₁, hs₂, hx⟩ => ?_, fun h => byx:ℕs:List (Fin 3 → ℕ)h:s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = xthis:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ F 1 = 1 aesopAll goals completed! 🐙this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ F 1 = 1⟩
    have := hx ▸ isIncreasing₂_const_length hs₁ hs₂x:ℕs:List (Fin 3 → ℕ)x✝:IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = xhs₁:IsIncreasing₂ shs₂:∀ a ∈ s, ∀ (i : Fin 3), a i = 1hx:s.length = xthis:x < 2⊢ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ F 1 = 1
    interval_cases x«0»x:ℕs:List (Fin 3 → ℕ)hs₁:IsIncreasing₂ shs₂:∀ a ∈ s, ∀ (i : Fin 3), a i = 1x✝:IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = 0hx:s.length = 0this:0 < 2⊢ s = [fun x ↦ 1] ∧ 0 = 1 ∨ s = [] ∧ 0 = 0«1»x:ℕs:List (Fin 3 → ℕ)hs₁:IsIncreasing₂ shs₂:∀ a ∈ s, ∀ (i : Fin 3), a i = 1x✝:IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = 1hx:s.length = 1this:1 < 2⊢ s = [fun x ↦ 1] ∧ 1 = 1 ∨ s = [] ∧ 1 = 0this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ F 1 = 1; simp [List.length_eq_zero_iff.1 hx]«1»x:ℕs:List (Fin 3 → ℕ)hs₁:IsIncreasing₂ shs₂:∀ a ∈ s, ∀ (i : Fin 3), a i = 1x✝:IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = 1hx:s.length = 1this:1 < 2⊢ s = [fun x ↦ 1] ∧ 1 = 1 ∨ s = [] ∧ 1 = 0this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ F 1 = 1; simp«1»x:ℕs:List (Fin 3 → ℕ)hs₁:IsIncreasing₂ shs₂:∀ a ∈ s, ∀ (i : Fin 3), a i = 1x✝:IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = 1hx:s.length = 1this:1 < 2⊢ s = [fun x ↦ 1]this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ F 1 = 1
    obtain ⟨a, rfl⟩ := List.length_eq_one_iff.1 hx«1»x:ℕthis:1 < 2a:Fin 3 → ℕhs₁:IsIncreasing₂ [a]hs₂:∀ a_1 ∈ [a], ∀ (i : Fin 3), a_1 i = 1x✝:IsIncreasing₂ [a] ∧ (∀ a_1 ∈ [a], ∀ (i : Fin 3), a_1 i = 1) ∧ [a].length = 1hx:[a].length = 1⊢ [a] = [fun x ↦ 1]this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ F 1 = 1
    simp at hs₂«1»x:ℕthis:1 < 2a:Fin 3 → ℕhs₁:IsIncreasing₂ [a]x✝:IsIncreasing₂ [a] ∧ (∀ a_1 ∈ [a], ∀ (i : Fin 3), a_1 i = 1) ∧ [a].length = 1hx:[a].length = 1hs₂:∀ (i : Fin 3), a i = 1⊢ [a] = [fun x ↦ 1]this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ F 1 = 1
    rw [show a = fun _ => 1 from funext fun i => byx:ℕthis:1 < 2a:Fin 3 → ℕhs₁:IsIncreasing₂ [a]x✝:IsIncreasing₂ [a] ∧ (∀ a_1 ∈ [a], ∀ (i : Fin 3), a_1 i = 1) ∧ [a].length = 1hx:[a].length = 1hs₂:∀ (i : Fin 3), a i = 1i:Fin 3⊢ a i = 1this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ F 1 = 1 simp [hs₂ i]All goals completed! 🐙this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ F 1 = 1]this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ F 1 = 1this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ F 1 = 1
  simp [maximalLength, fun x => exists_congr (this x)]this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ sSup {x | ∃ a, a = [fun x ↦ 1] ∧ x = 1 ∨ a = [] ∧ x = 0} = 1
  rw [Nat.sSup_def ⟨1, bythis:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ ∀ a ∈ {x | ∃ a, a = [fun x ↦ 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ 1this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ (∀ a ∈ {x | ∃ a, a = [fun x ↦ 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ 1) ∧
  ∀ n < 1, ¬∀ a ∈ {x | ∃ a, a = [fun x ↦ 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ n aesopAll goals completed! 🐙this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ (∀ a ∈ {x | ∃ a, a = [fun x ↦ 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ 1) ∧
  ∀ n < 1, ¬∀ a ∈ {x | ∃ a, a = [fun x ↦ 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ n⟩, Nat.find_eq_iffthis:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ (∀ a ∈ {x | ∃ a, a = [fun x ↦ 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ 1) ∧
  ∀ n < 1, ¬∀ a ∈ {x | ∃ a, a = [fun x ↦ 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ nthis:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ (∀ a ∈ {x | ∃ a, a = [fun x ↦ 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ 1) ∧
  ∀ n < 1, ¬∀ a ∈ {x | ∃ a, a = [fun x ↦ 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ n]this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ (∀ a ∈ {x | ∃ a, a = [fun x ↦ 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ 1) ∧
  ∀ n < 1, ¬∀ a ∈ {x | ∃ a, a = [fun x ↦ 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ n
  refine ⟨bythis:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0⊢ ∀ a ∈ {x | ∃ a, a = [fun x ↦ 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ 1 aesopAll goals completed! 🐙, fun n hn => ?_⟩
  simp [Nat.lt_one_iff.1 hn]this:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0n:ℕhn:n < 1⊢ ∃ x, (∃ x_1, x_1 = [fun x ↦ 1] ∧ x = 1 ∨ x_1 = [] ∧ x = 0) ∧ ¬x = 0
  exact ⟨1, ⟨[fun _ => 1], bythis:∀ (x : ℕ) (s : List (Fin 3 → ℕ)),
  IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x ↔ s = [fun x ↦ 1] ∧ x = 1 ∨ s = [] ∧ x = 0n:ℕhn:n < 1⊢ [fun x ↦ 1] = [fun x ↦ 1] ∧ 1 = 1 ∨ [fun x ↦ 1] = [] ∧ 1 = 0 simpAll goals completed! 🐙⟩, one_ne_zero⟩

@[category test, AMS 5]
theorem maximalLength_four : maximalLength 4 = 8 := by⊢ F 4 = 8
  sorryAll goals completed! 🐙

In a set of more than $n^2$ triples with coordinates from ${1, ..., n}$ we must have two triples that are equal in their first two coordinates.


@[category API, AMS 5]
lemma exists_pair_of_mem_Icc {s : List (Fin 3 → ℕ)} {n : ℕ} (_hn : 2 ≤ n)
    (hs₁ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (hs₂ : s.length > n ^ 2) :
    ∃ (i j : Fin s.length), i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1 := bys:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
  classical
  let f : Fin s.length → ℕ × ℕ := fun k => (s[k] 0, s[k] 1)s:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
  let t : Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 ns:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 n⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
  have ht_card : t.card < (Finset.univ : Finset (Fin s.length)).card := bys:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1s:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.card⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
    simp only [t, Finset.card_univ, Fintype.card_fin, Finset.card_product,
      Nat.card_Icc, Nat.add_sub_cancel, ← sq]s:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 n⊢ n ^ 2 < s.lengths:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.card⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
    exact hs₂s:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.card⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1s:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.card⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
  have hf : ∀ k ∈ (Finset.univ : Finset (Fin s.length)), f k ∈ t := bys:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1s:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardhf:∀ k ∈ Finset.univ, f k ∈ t⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
    intro k _s:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardk:Fin s.lengtha✝:k ∈ Finset.univ⊢ f k ∈ ts:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardhf:∀ k ∈ Finset.univ, f k ∈ t⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
    have hmem : s[k] ∈ s := List.getElem_mem k.isLts:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardk:Fin s.lengtha✝:k ∈ Finset.univhmem:s[k] ∈ s⊢ f k ∈ ts:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardhf:∀ k ∈ Finset.univ, f k ∈ t⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
    have h0 := hs₁ _ hmem ⟨0, rfl⟩s:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardk:Fin s.lengtha✝:k ∈ Finset.univhmem:s[k] ∈ sh0:s[k] 0 ∈ Set.Icc 1 n⊢ f k ∈ ts:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardhf:∀ k ∈ Finset.univ, f k ∈ t⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
    have h1 := hs₁ _ hmem ⟨1, rfl⟩s:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardk:Fin s.lengtha✝:k ∈ Finset.univhmem:s[k] ∈ sh0:s[k] 0 ∈ Set.Icc 1 nh1:s[k] 1 ∈ Set.Icc 1 n⊢ f k ∈ ts:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardhf:∀ k ∈ Finset.univ, f k ∈ t⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
    rw [Set.mem_Iccs:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardk:Fin s.lengtha✝:k ∈ Finset.univhmem:s[k] ∈ sh0:1 ≤ s[k] 0 ∧ s[k] 0 ≤ nh1:1 ≤ s[k] 1 ∧ s[k] 1 ≤ n⊢ f k ∈ ts:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardk:Fin s.lengtha✝:k ∈ Finset.univhmem:s[k] ∈ sh0:1 ≤ s[k] 0 ∧ s[k] 0 ≤ nh1:1 ≤ s[k] 1 ∧ s[k] 1 ≤ n⊢ f k ∈ ts:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardhf:∀ k ∈ Finset.univ, f k ∈ t⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1] at h0 h1s:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardk:Fin s.lengtha✝:k ∈ Finset.univhmem:s[k] ∈ sh0:1 ≤ s[k] 0 ∧ s[k] 0 ≤ nh1:1 ≤ s[k] 1 ∧ s[k] 1 ≤ n⊢ f k ∈ ts:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardhf:∀ k ∈ Finset.univ, f k ∈ t⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
    simp only [t, f, Finset.mem_product, Finset.mem_Icc]s:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardk:Fin s.lengtha✝:k ∈ Finset.univhmem:s[k] ∈ sh0:1 ≤ s[k] 0 ∧ s[k] 0 ≤ nh1:1 ≤ s[k] 1 ∧ s[k] 1 ≤ n⊢ (1 ≤ s[k] 0 ∧ s[k] 0 ≤ n) ∧ 1 ≤ s[k] 1 ∧ s[k] 1 ≤ ns:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardhf:∀ k ∈ Finset.univ, f k ∈ t⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
    exact ⟨h0, h1⟩s:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardhf:∀ k ∈ Finset.univ, f k ∈ t⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1s:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardhf:∀ k ∈ Finset.univ, f k ∈ t⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
  obtain ⟨i, _, j, _, hij, hfij⟩ :=
    Finset.exists_ne_map_eq_of_card_lt_of_maps_to ht_card hfs:List (Fin 3 → ℕ)n:ℕ_hn:2 ≤ nhs₁:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs₂:s.length > n ^ 2f:Fin s.length → ℕ × ℕ := fun k ↦ (s[k] 0, s[k] 1)t:Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 nht_card:t.card < Finset.univ.cardhf:∀ k ∈ Finset.univ, f k ∈ ti:Fin s.lengthleft✝¹:i ∈ Finset.univj:Fin s.lengthleft✝:j ∈ Finset.univhij:i ≠ jhfij:f i = f j⊢ ∃ i j, i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1
  exact ⟨i, j, hij, congrArg Prod.fst hfij, congrArg Prod.snd hfij⟩All goals completed! 🐙

For all $n$ we have $F(n) \leq n^2$.

This is the upper bound in [GoLo21, Proposition 1.4], proved by applying the pigeonhole principle to the first two coordinates.


@[category research solved, AMS 5]
theorem maximalLength_le (n : ℕ) : F n ≤ n ^ 2 := byn:ℕ⊢ F n ≤ n ^ 2
  by_cases hn : 2 ≤ nposn:ℕhn:2 ≤ n⊢ F n ≤ n ^ 2negn:ℕhn:¬2 ≤ n⊢ F n ≤ n ^ 2
  ·posn:ℕhn:2 ≤ n⊢ F n ≤ n ^ 2 rw [maximalLengthposn:ℕhn:2 ≤ n⊢ sSup {x | ∃ s, ∃ (_ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (_ : IsIncreasing₂ s), s.length = x} ≤ n ^ 2posn:ℕhn:2 ≤ n⊢ sSup {x | ∃ s, ∃ (_ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (_ : IsIncreasing₂ s), s.length = x} ≤ n ^ 2]posn:ℕhn:2 ≤ n⊢ sSup {x | ∃ s, ∃ (_ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (_ : IsIncreasing₂ s), s.length = x} ≤ n ^ 2
    refine csSup_le ?_ ?_pos.refine_1n:ℕhn:2 ≤ n⊢ {x | ∃ s, ∃ (_ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (_ : IsIncreasing₂ s), s.length = x}.Nonemptypos.refine_2n:ℕhn:2 ≤ n⊢ ∀ b ∈ {x | ∃ s, ∃ (_ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (_ : IsIncreasing₂ s), s.length = x}, b ≤ n ^ 2
    ·pos.refine_1n:ℕhn:2 ≤ n⊢ {x | ∃ s, ∃ (_ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (_ : IsIncreasing₂ s), s.length = x}.Nonempty exact ⟨0, ⟨[], byn:ℕhn:2 ≤ n⊢ ∀ a ∈ [], Set.range a ⊆ Set.Icc 1 n simpAll goals completed! 🐙, isIncreasing₂_nil, rfl⟩⟩
    ·pos.refine_2n:ℕhn:2 ≤ n⊢ ∀ b ∈ {x | ∃ s, ∃ (_ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (_ : IsIncreasing₂ s), s.length = x}, b ≤ n ^ 2 intro _ hmpos.refine_2n:ℕhn:2 ≤ nb✝:ℕhm:b✝ ∈ {x | ∃ s, ∃ (_ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (_ : IsIncreasing₂ s), s.length = x}⊢ b✝ ≤ n ^ 2
      rcases hm with ⟨s, hs_range, hs_inc, rfl⟩pos.refine_2n:ℕhn:2 ≤ ns:List (Fin 3 → ℕ)hs_range:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs_inc:IsIncreasing₂ s⊢ s.length ≤ n ^ 2
      by_contra hlepos.refine_2n:ℕhn:2 ≤ ns:List (Fin 3 → ℕ)hs_range:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs_inc:IsIncreasing₂ shle:¬s.length ≤ n ^ 2⊢ False
      have hs_length : n ^ 2 < s.length := Nat.lt_of_not_ge hlepos.refine_2n:ℕhn:2 ≤ ns:List (Fin 3 → ℕ)hs_range:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs_inc:IsIncreasing₂ shle:¬s.length ≤ n ^ 2hs_length:n ^ 2 < s.length⊢ False
      obtain ⟨i, j, hij, h0, h1⟩ :=
        exists_pair_of_mem_Icc hn hs_range hs_lengthpos.refine_2n:ℕhn:2 ≤ ns:List (Fin 3 → ℕ)hs_range:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs_inc:IsIncreasing₂ shle:¬s.length ≤ n ^ 2hs_length:n ^ 2 < s.lengthi:Fin s.lengthj:Fin s.lengthhij:i ≠ jh0:s[i] 0 = s[j] 0h1:s[i] 1 = s[j] 1⊢ False
      have hp : s.Pairwise lt₂ := hs_incpos.refine_2n:ℕhn:2 ≤ ns:List (Fin 3 → ℕ)hs_range:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs_inc:IsIncreasing₂ shle:¬s.length ≤ n ^ 2hs_length:n ^ 2 < s.lengthi:Fin s.lengthj:Fin s.lengthhij:i ≠ jh0:s[i] 0 = s[j] 0h1:s[i] 1 = s[j] 1hp:List.Pairwise lt₂ s⊢ False
      rcases lt_or_gt_of_ne hij with hij | hjipos.refine_2.inln:ℕhn:2 ≤ ns:List (Fin 3 → ℕ)hs_range:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs_inc:IsIncreasing₂ shle:¬s.length ≤ n ^ 2hs_length:n ^ 2 < s.lengthi:Fin s.lengthj:Fin s.lengthhij✝:i ≠ jh0:s[i] 0 = s[j] 0h1:s[i] 1 = s[j] 1hp:List.Pairwise lt₂ shij:i < j⊢ Falsepos.refine_2.inrn:ℕhn:2 ≤ ns:List (Fin 3 → ℕ)hs_range:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs_inc:IsIncreasing₂ shle:¬s.length ≤ n ^ 2hs_length:n ^ 2 < s.lengthi:Fin s.lengthj:Fin s.lengthhij:i ≠ jh0:s[i] 0 = s[j] 0h1:s[i] 1 = s[j] 1hp:List.Pairwise lt₂ shji:j < i⊢ False
      ·pos.refine_2.inln:ℕhn:2 ≤ ns:List (Fin 3 → ℕ)hs_range:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs_inc:IsIncreasing₂ shle:¬s.length ≤ n ^ 2hs_length:n ^ 2 < s.lengthi:Fin s.lengthj:Fin s.lengthhij✝:i ≠ jh0:s[i] 0 = s[j] 0h1:s[i] 1 = s[j] 1hp:List.Pairwise lt₂ shij:i < j⊢ False exact (not_lt₂_of_exists 0 1 zero_ne_one h0.ge h1.ge)
          (List.pairwise_iff_get.1 hp i j hij)All goals completed! 🐙
      ·pos.refine_2.inrn:ℕhn:2 ≤ ns:List (Fin 3 → ℕ)hs_range:∀ a ∈ s, Set.range a ⊆ Set.Icc 1 nhs_inc:IsIncreasing₂ shle:¬s.length ≤ n ^ 2hs_length:n ^ 2 < s.lengthi:Fin s.lengthj:Fin s.lengthhij:i ≠ jh0:s[i] 0 = s[j] 0h1:s[i] 1 = s[j] 1hp:List.Pairwise lt₂ shji:j < i⊢ False exact (not_lt₂_of_exists 0 1 zero_ne_one h0.le h1.le)
          (List.pairwise_iff_get.1 hp j i hji)All goals completed! 🐙
  ·negn:ℕhn:¬2 ≤ n⊢ F n ≤ n ^ 2 cases n with
    | zero =>neg.zerohn:¬2 ≤ 0⊢ F 0 ≤ 0 ^ 2 simp [maximalLength_zero]All goals completed! 🐙
    | succ n =>neg.succn:ℕhn:¬2 ≤ n + 1⊢ F (n + 1) ≤ (n + 1) ^ 2
      cases n with
      | zero =>neg.succ.zerohn:¬2 ≤ 0 + 1⊢ F (0 + 1) ≤ (0 + 1) ^ 2 simp [maximalLength_one]All goals completed! 🐙
      | succ n =>neg.succ.succn:ℕhn:¬2 ≤ n + 1 + 1⊢ F (n + 1 + 1) ≤ (n + 1 + 1) ^ 2
        exact (hn (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _)))).elimAll goals completed! 🐙

Moreover, whenever $n$ is a perfect square we have $F(n) \geq n^{3/2}$.

@[category research solved, AMS 5]
theorem maximalLength_ge_of_isSquare {n : ℕ} (h : IsSquare n) :
    n.sqrt ^ 3 ≤ F n := byn:ℕh:IsSquare n⊢ n.sqrt ^ 3 ≤ F n
  sorryAll goals completed! 🐙

Two triples $t_1$ and $t_2$ are $2$-comparable if one of them is $2$-less than the other.

def IsComparable₂ {α : Type*} [LT α] (t₁ t₂ : Fin 3 → α) : Prop :=
  t₁ <₂ t₂ ∨ t₂ <₂ t₁

A set of triples is $2$-comparable if any two of them are $2$-comparable.

def IsComparableSet₂ {α : Type*} [LT α] (s : List (Fin 3 → α)) : Prop :=
  ∃ t₁ t₂, t₁ ≠ t₂ ∧ t₁ ∈ s ∧ t₂ ∈ s ∧ IsComparable₂ t₁ t₂

open Filter in

$F(n) \leq n^2 / \exp(\Omega(\log^*(n)))$.

@[category research solved, AMS 5]
theorem maximalLength_le_isBigO : ∃ Ω : ℕ → ℝ,
    (fun (n : ℕ) => (Real.iteratedLog n : ℝ)) =O[atTop] Ω ∧
      ∀ n, F n ≤ n ^ 2 / Real.exp (Ω n) := by⊢ ∃ Ω, (fun n ↦ ↑(↑n).iteratedLog) =O[atTop] Ω ∧ ∀ (n : ℕ), ↑(F n) ≤ ↑n ^ 2 / Real.exp (Ω n)
  sorryAll goals completed! 🐙

We define the product of two triples $(a, b, c)$ and $(d, e, f)$ by $((a, d), (b, e), (c, f))$, where the pairs are arranged in lexicographical order.

def tripleProduct {α : Type*} (a b : Fin 3 → α) : Πₗ (_ : Fin 3), α × α := toLex (Function.prod a b)

@[simp, category API, AMS 5]
theorem tripleProduct_const {α : Type*} (a : α) :
    tripleProduct (fun _ => a) (fun _ => a) = toLex (fun _ => (a, a)) := byα:Type u_1a:α⊢ (tripleProduct (fun x ↦ a) fun x ↦ a) = toLex fun x ↦ (a, a)
  simpa [tripleProduct] using funext fun i => byα:Type u_1a:αi:Fin 3⊢ Function.prod (fun x ↦ a) (fun x ↦ a) i = (a, a) simpAll goals completed! 🐙

@[simp, category API, AMS 5]
theorem tripleProduct_vecConst_const {α : Type*} (a : α) :
    tripleProduct ![a, a, a] ![a, a, a] = toLex ![(a, a), (a, a), (a, a)] := byα:Type u_1a:α⊢ tripleProduct ![a, a, a] ![a, a, a] = toLex ![(a, a), (a, a), (a, a)]
  simp [tripleProduct]α:Type u_1a:α⊢ Function.prod ![a, a, a] ![a, a, a] = ![(a, a), (a, a), (a, a)]
  ext ifstα:Type u_1a:αi:Fin 3⊢ (Function.prod ![a, a, a] ![a, a, a] i).1 = (![(a, a), (a, a), (a, a)] i).1sndα:Type u_1a:αi:Fin 3⊢ (Function.prod ![a, a, a] ![a, a, a] i).2 = (![(a, a), (a, a), (a, a)] i).2 <;>fstα:Type u_1a:αi:Fin 3⊢ (Function.prod ![a, a, a] ![a, a, a] i).1 = (![(a, a), (a, a), (a, a)] i).1sndα:Type u_1a:αi:Fin 3⊢ (Function.prod ![a, a, a] ![a, a, a] i).2 = (![(a, a), (a, a), (a, a)] i).2 fin_cases isnd.«0»α:Type u_1a:α⊢ (Function.prod ![a, a, a] ![a, a, a] ((fun i ↦ i) ⟨0, ⋯⟩)).2 = (![(a, a), (a, a), (a, a)] ((fun i ↦ i) ⟨0, ⋯⟩)).2snd.«1»α:Type u_1a:α⊢ (Function.prod ![a, a, a] ![a, a, a] ((fun i ↦ i) ⟨1, ⋯⟩)).2 = (![(a, a), (a, a), (a, a)] ((fun i ↦ i) ⟨1, ⋯⟩)).2snd.«2»α:Type u_1a:α⊢ (Function.prod ![a, a, a] ![a, a, a] ((fun i ↦ i) ⟨2, ⋯⟩)).2 = (![(a, a), (a, a), (a, a)] ((fun i ↦ i) ⟨2, ⋯⟩)).2 <;>fst.«0»α:Type u_1a:α⊢ (Function.prod ![a, a, a] ![a, a, a] ((fun i ↦ i) ⟨0, ⋯⟩)).1 = (![(a, a), (a, a), (a, a)] ((fun i ↦ i) ⟨0, ⋯⟩)).1fst.«1»α:Type u_1a:α⊢ (Function.prod ![a, a, a] ![a, a, a] ((fun i ↦ i) ⟨1, ⋯⟩)).1 = (![(a, a), (a, a), (a, a)] ((fun i ↦ i) ⟨1, ⋯⟩)).1fst.«2»α:Type u_1a:α⊢ (Function.prod ![a, a, a] ![a, a, a] ((fun i ↦ i) ⟨2, ⋯⟩)).1 = (![(a, a), (a, a), (a, a)] ((fun i ↦ i) ⟨2, ⋯⟩)).1snd.«0»α:Type u_1a:α⊢ (Function.prod ![a, a, a] ![a, a, a] ((fun i ↦ i) ⟨0, ⋯⟩)).2 = (![(a, a), (a, a), (a, a)] ((fun i ↦ i) ⟨0, ⋯⟩)).2snd.«1»α:Type u_1a:α⊢ (Function.prod ![a, a, a] ![a, a, a] ((fun i ↦ i) ⟨1, ⋯⟩)).2 = (![(a, a), (a, a), (a, a)] ((fun i ↦ i) ⟨1, ⋯⟩)).2snd.«2»α:Type u_1a:α⊢ (Function.prod ![a, a, a] ![a, a, a] ((fun i ↦ i) ⟨2, ⋯⟩)).2 = (![(a, a), (a, a), (a, a)] ((fun i ↦ i) ⟨2, ⋯⟩)).2 simpAll goals completed! 🐙

We define the product $\otimes$ of two sequences $(a_i, b_i, c_i)$ and $(d_i, e_i, f_i)$ by the sequence $((a_i, d_j), (b_i, e_j), (c_i, f_j))$, where the indices $(i, j)$ are arranged lexicographically, and the pairs are also ordered lexicographically.

def sequenceProduct {α : Type*} (s t : List (Fin 3 → α)) : Lex (List (Πₗ (_ : Fin 3), α × α)) :=
  toLex (s.flatMap (fun a => List.map (tripleProduct a) t))

local infix:100 " ⊗₂ " => sequenceProduct

@[category test, AMS 5]
theorem sequenceProduct_example : [![1, 1, 1]] ⊗₂ [![1, 1, 1]] = toLex [toLex ![(1, 1), (1, 1), (1, 1)]] := by⊢ [![1, 1, 1]] ⊗₂ [![1, 1, 1]] = toLex [toLex ![(1, 1), (1, 1), (1, 1)]]
  simp [sequenceProduct]All goals completed! 🐙

Suppose that for some $n$ we have $F(n) = n ^ {\alpha}$. Then there are arbitrarily large $m$ such that $F(m) \geq m^{\alpha}$.

@[category research solved, AMS 5]
theorem maximalLength_pow {n : ℕ} {e : ℝ} (hn : 1 < n) (h : F n = (n : ℝ) ^ e) :
    ∀ᶠ m : ℕ in Filter.atTop, (m : ℝ) ^ e ≤ F m := byn:ℕe:ℝhn:1 < nh:↑(F n) = ↑n ^ e⊢ ∀ᶠ (m : ℕ) in Filter.atTop, ↑m ^ e ≤ ↑(F m)
  sorryAll goals completed! 🐙

$F(n) \leq n^{3/2}$.

@[category research open, AMS 5]
theorem maximalLength_le_strong (n : ℕ) : F n ≤ Real.sqrt n ^ 3 := byn:ℕ⊢ ↑(F n) ≤ √↑n ^ 3
  sorryAll goals completed! 🐙

end Arxiv.«1609.08688»