1. FormalConjectures
  2. Arxiv
  3. «1609.08688»
  4. 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 co-ordinates $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 := α: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 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 := α: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 k⊢ 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 ≠ i := fun hk => not_lt.mpr hi (hk ▸ h)⊢ 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 ≠ i := fun hk => not_lt.mpr hi (hk ▸ h)this:k ≠ j := fun hk => not_lt.mpr hj (hk ▸ h)⊢ b l ≤ a l have : l = i ∨ l = j := α: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 All goals completed! 🐙 α: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 ≠ j := fun hk => not_lt.mpr hj (hk ▸ h)hij:l ≠ jhi:b l ≤ a lthis:k ≠ l⊢ b l ≤ a lα: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 ≠ i := fun hk => not_lt.mpr hi (hk ▸ h)hij:i ≠ lhj:b l ≤ a lthis:k ≠ l⊢ b l ≤ a l; α: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 ≠ i := fun hk => not_lt.mpr hi (hk ▸ h)hij:i ≠ lhj:b l ≤ a lthis:k ≠ l⊢ b l ≤ a l; All goals completed! 🐙 @[category API, AMS 5] theorem not_lt₂_self {α : Type*} [LinearOrder α] (a : Fin 3 → α) : ¬a <₂ a := α:Type u_1inst✝:LinearOrder αa:Fin 3 → α⊢ ¬a <₂ a All 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, ⊢ ![3, 3, 9] 0 < ![5, 6, 1] 0 ∧ ![3, 3, 9] 1 < ![5, 6, 1] 1 All 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, ⊢ 0 ≠ 2 All goals completed! 🐙, ⊢ ![5, 6, 1] 0 < ![7, 7, 7] 0 ∧ ![5, 6, 1] 2 < ![7, 7, 7] 2 All 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, ⊢ 1 ≠ 2 All goals completed! 🐙, ⊢ ![7, 7, 7] 1 < ![7, 8, 9] 1 ∧ ![7, 7, 7] 2 < ![7, 8, 9] 2 All 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 (⊢ ![1, 2, 4] 0 ≤ ![1, 2, 3] 0 All goals completed! 🐙) (⊢ ![1, 2, 4] 1 ≤ ![1, 2, 3] 1 All 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, ⊢ ![1, 2, 3] 0 < ![2, 3, 1] 0 ∧ ![1, 2, 3] 1 < ![2, 3, 1] 1 All goals completed! 🐙⟩, ⟨0, 2, ⊢ 0 ≠ 2 All goals completed! 🐙, ⊢ ![2, 3, 1] 0 < ![3, 1, 2] 0 ∧ ![2, 3, 1] 2 < ![3, 1, 2] 2 All goals completed! 🐙⟩, not_lt₂_of_exists 1 2 (⊢ 1 ≠ 2 All goals completed! 🐙) (⊢ ![3, 1, 2] 1 ≤ ![1, 2, 3] 1 All goals completed! 🐙) (⊢ ![3, 1, 2] 2 ≤ ![1, 2, 3] 2 All 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₂ (α := α) [] := α:Type u_1inst✝:LT α⊢ IsIncreasing₂ [] All goals completed! 🐙 @[simp, category API, AMS 5] theorem isIncreasing₂_singleton {α : Type*} [LT α] (a : Fin 3 → α) : IsIncreasing₂ [a] := α:Type u_1inst✝:LT αa:Fin 3 → α⊢ IsIncreasing₂ [a] 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 := α:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = val⊢ s.length < 2 α: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 have h₀ : s[0] = fun _ => val := funext fun 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 3⊢ s[0] i = val All goals completed! 🐙 have h₁ : s[1] = fun _ => val := funext fun i => α:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.lengthh₀:s[0] = fun x => val := funext fun i => of_eq_true (Eq.trans (congrArg (fun x => x = val) ((fun j => h_const s[0] (of_eq_true (List.getElem_mem._simp_1 (Decidable.byContradiction fun a => isIncreasing₂_const_length._proof_1 this a))) j) i)) (eq_self val))i:Fin 3⊢ s[1] i = val All goals completed! 🐙 have := List.pairwise_iff_getElem.1 h 0 1 (α:Type u_1inst✝:LinearOrder αval:αs:List (Fin 3 → α)h:IsIncreasing₂ sh_const:∀ a ∈ s, ∀ (j : Fin 3), a j = valthis:2 ≤ s.lengthh₀:s[0] = fun x => val := funext fun i => of_eq_true (Eq.trans (congrArg (fun x => x = val) ((fun j => h_const s[0] (of_eq_true (List.getElem_mem._simp_1 (Decidable.byContradiction fun a => isIncreasing₂_const_length._proof_1 this a))) j) i)) (eq_self val))h₁:s[1] = fun x => val := funext fun i => of_eq_true (Eq.trans (congrArg (fun x => x = val) ((fun j => h_const s[1] (of_eq_true (List.getElem_mem._simp_1 this)) j) i)) (eq_self val))⊢ 0 < s.length All 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.lengthh₀:s[0] = fun x => val := funext fun i => of_eq_true (Eq.trans (congrArg (fun x => x = val) ((fun j => h_const s[0] (of_eq_true (List.getElem_mem._simp_1 (Decidable.byContradiction fun a => isIncreasing₂_const_length._proof_1 this a))) j) i)) (eq_self val))h₁:s[1] = fun x => val := funext fun i => of_eq_true (Eq.trans (congrArg (fun x => x = val) ((fun j => h_const s[1] (of_eq_true (List.getElem_mem._simp_1 this)) j) i)) (eq_self val))⊢ 1 < s.length All goals completed! 🐙) 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.lengthh₀:s[0] = fun x => val := funext fun i => of_eq_true (Eq.trans (congrArg (fun x => x = val) ((fun j => h_const s[0] (of_eq_true (List.getElem_mem._simp_1 (Decidable.byContradiction fun a => isIncreasing₂_const_length._proof_1 this✝ a))) j) i)) (eq_self val))h₁:s[1] = fun x => val := funext fun i => of_eq_true (Eq.trans (congrArg (fun x => x = val) ((fun j => h_const s[1] (of_eq_true (List.getElem_mem._simp_1 this✝)) j) i)) (eq_self val))this:(fun x => val) <₂ fun x => val⊢ False All 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 := ⊢ F 0 = 0 have (x : ℕ) (s : List (Fin 3 → ℕ)) : IsIncreasing₂ s ∧ (∀ a, a ∉ s) ∧ s.length = x ↔ s = [] ∧ x = 0 := ⊢ F 0 = 0 refine ⟨fun ⟨ha₁, ha₂, rfl⟩ => ?_, fun ⟨h₁, h₂⟩ => x:ℕs:List (Fin 3 → ℕ)x✝:s = [] ∧ x = 0h₁:s = []h₂:x = 0⊢ IsIncreasing₂ s ∧ (∀ (a : Fin 3 → ℕ), a ∉ s) ∧ s.length = x All goals completed! 🐙⟩ x:ℕs:List (Fin 3 → ℕ)x✝:IsIncreasing₂ s ∧ (∀ (a : Fin 3 → ℕ), a ∉ s) ∧ s.length = xha₁:IsIncreasing₂ sha₂:∀ (a : Fin 3 → ℕ), a ∉ s⊢ s = [] 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 ∈ [] All goals completed! 🐙 All goals completed! 🐙 @[category test, AMS 5] theorem maximalLength_one : maximalLength 1 = 1 := ⊢ 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 := ⊢ F 1 = 1 refine ⟨fun ⟨hs₁, hs₂, hx⟩ => ?_, fun h => x:ℕ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 = x All goals completed! 🐙⟩ 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 := hx ▸ isIncreasing₂_const_length hs₁ hs₂⊢ s = [fun x => 1] ∧ x = 1 ∨ s = [] ∧ 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 = 0x:ℕ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 = 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 = 1hx:s.length = 1this:1 < 2⊢ s = [fun x => 1] ∧ 1 = 1 ∨ s = [] ∧ 1 = 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 = 1hx:s.length = 1this:1 < 2⊢ s = [fun x => 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] 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] 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 := fun x s => { mp := fun x_1 => match x_1 with | ⟨hs₁, ⟨hs₂, hx⟩⟩ => have this := hx ▸ isIncreasing₂_const_length hs₁ hs₂; if x_2 : 1 ≤ x then Eq.ndrec (motive := fun x => IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x → s.length = x → x < 2 → s = [fun x => 1] ∧ x = 1 ∨ s = [] ∧ x = 0) (fun x hx this => Eq.mpr (id (Eq.trans (congr (congrArg Or (Eq.trans (congrArg (And (s = [fun x => 1])) (eq_self 1)) (and_true (s = [fun x => 1])))) (Eq.trans (congrArg (And (s = [])) one_ne_zero._simp_1) (and_false (s = [])))) (or_false (s = [fun x => 1])))) (Exists.casesOn (List.length_eq_one_iff.mp hx) fun a h => Eq.ndrec (motive := fun s => IsIncreasing₂ s → (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) → IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = 1 → s.length = 1 → s = [fun x => 1]) (fun hs₁ hs₂ x hx => Eq.mpr (id (congrArg (fun _a => [_a] = [fun x => 1]) (have this := funext fun i => of_eq_true (Eq.trans (congrArg (fun x => x = 1) (Eq.mp (Eq.trans (forall_congr fun a_1 => implies_congr (Eq.trans List.mem_cons._simp_1 (Eq.trans (congrArg (Or (a_1 = a)) List.not_mem_nil._simp_1) (or_false (a_1 = a)))) (Eq.refl (∀ (i : Fin 3), a_1 i = 1))) forall_eq._simp_1) hs₂ i)) (eq_self 1)); this))) (Eq.refl [fun x => 1])) (Eq.symm h) hs₁ hs₂ x hx)) (Eq.symm (le_antisymm (Nat.ge_of_not_lt (Mathlib.Tactic.IntervalCases.of_lt_right this (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))))) x_2)) x_1 hx this else Eq.ndrec (motive := fun x => IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x → s.length = x → x < 2 → s = [fun x => 1] ∧ x = 1 ∨ s = [] ∧ x = 0) (fun x hx this => of_eq_true (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (Eq.trans (congrArg (fun x => x = [fun x => 1]) (List.length_eq_zero_iff.mp hx)) List.ne_cons_self._simp_1)) zero_ne_one._simp_1) (and_self False))) (Eq.trans (congr (congrArg And (Eq.trans (congrArg (fun x => x = []) (List.length_eq_zero_iff.mp hx)) (eq_self []))) (eq_self 0)) (and_self True))) (or_true False))) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_2) (Nat.zero_le x))) x_1 hx this, mpr := fun h => Or.casesOn h (fun h_1 => of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg IsIncreasing₂ h_1.1) (isIncreasing₂_singleton._simp_1 fun x => 1))) (Eq.trans (congr (congrArg And (Eq.trans (forall_congr fun a => Eq.trans (implies_congr_ctx (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) h_1.1) List.mem_cons._simp_1) (Eq.trans (congrArg (Or (a = fun x => 1)) List.not_mem_nil._simp_1) (or_false (a = fun x => 1)))) fun a_1 => Eq.trans (forall_congr fun i => Eq.trans (congrArg (fun x => x i = 1) a_1) (eq_self 1)) (implies_true (Fin 3))) (implies_true (a = fun x => 1))) (implies_true (Fin 3 → ℕ)))) (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg List.length h_1.1) (zero_add 1))) h_1.2) (eq_self 1))) (and_self True))) (and_self True))) fun h_2 => of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg IsIncreasing₂ h_2.1) isIncreasing₂_nil._simp_1)) (Eq.trans (congr (congrArg And (Eq.trans (forall_congr fun a => Eq.trans (implies_congr_ctx (Eq.trans (congrArg (fun x => a ∈ x) h_2.1) List.not_mem_nil._simp_1) fun a_1 => IsEmpty.forall_iff._simp_1) (implies_true False)) (implies_true (Fin 3 → ℕ)))) (Eq.trans (congr (congrArg (fun x => Eq x.length) h_2.1) h_2.2) (eq_self 0))) (and_self True))) (and_self True)) }⊢ sSup {x | ∃ a, a = [fun x => 1] ∧ x = 1 ∨ a = [] ∧ x = 0} = 1 erw [Nat.sSup_def ⟨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 := fun x s => { mp := fun x_1 => match x_1 with | ⟨hs₁, ⟨hs₂, hx⟩⟩ => have this := hx ▸ isIncreasing₂_const_length hs₁ hs₂; if x_2 : 1 ≤ x then Eq.ndrec (motive := fun x => IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x → s.length = x → x < 2 → s = [fun x => 1] ∧ x = 1 ∨ s = [] ∧ x = 0) (fun x hx this => Eq.mpr (id (Eq.trans (congr (congrArg Or (Eq.trans (congrArg (And (s = [fun x => 1])) (eq_self 1)) (and_true (s = [fun x => 1])))) (Eq.trans (congrArg (And (s = [])) one_ne_zero._simp_1) (and_false (s = [])))) (or_false (s = [fun x => 1])))) (Exists.casesOn (List.length_eq_one_iff.mp hx) fun a h => Eq.ndrec (motive := fun s => IsIncreasing₂ s → (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) → IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = 1 → s.length = 1 → s = [fun x => 1]) (fun hs₁ hs₂ x hx => Eq.mpr (id (congrArg (fun _a => [_a] = [fun x => 1]) (have this := funext fun i => of_eq_true (Eq.trans (congrArg (fun x => x = 1) (Eq.mp (Eq.trans (forall_congr fun a_1 => implies_congr (Eq.trans List.mem_cons._simp_1 (Eq.trans (congrArg (Or (a_1 = a)) List.not_mem_nil._simp_1) (or_false (a_1 = a)))) (Eq.refl (∀ (i : Fin 3), a_1 i = 1))) forall_eq._simp_1) hs₂ i)) (eq_self 1)); this))) (Eq.refl [fun x => 1])) (Eq.symm h) hs₁ hs₂ x hx)) (Eq.symm (le_antisymm (Nat.ge_of_not_lt (Mathlib.Tactic.IntervalCases.of_lt_right this (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))))) x_2)) x_1 hx this else Eq.ndrec (motive := fun x => IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x → s.length = x → x < 2 → s = [fun x => 1] ∧ x = 1 ∨ s = [] ∧ x = 0) (fun x hx this => of_eq_true (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (Eq.trans (congrArg (fun x => x = [fun x => 1]) (List.length_eq_zero_iff.mp hx)) List.ne_cons_self._simp_1)) zero_ne_one._simp_1) (and_self False))) (Eq.trans (congr (congrArg And (Eq.trans (congrArg (fun x => x = []) (List.length_eq_zero_iff.mp hx)) (eq_self []))) (eq_self 0)) (and_self True))) (or_true False))) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_2) (Nat.zero_le x))) x_1 hx this, mpr := fun h => Or.casesOn h (fun h_1 => of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg IsIncreasing₂ h_1.1) (isIncreasing₂_singleton._simp_1 fun x => 1))) (Eq.trans (congr (congrArg And (Eq.trans (forall_congr fun a => Eq.trans (implies_congr_ctx (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) h_1.1) List.mem_cons._simp_1) (Eq.trans (congrArg (Or (a = fun x => 1)) List.not_mem_nil._simp_1) (or_false (a = fun x => 1)))) fun a_1 => Eq.trans (forall_congr fun i => Eq.trans (congrArg (fun x => x i = 1) a_1) (eq_self 1)) (implies_true (Fin 3))) (implies_true (a = fun x => 1))) (implies_true (Fin 3 → ℕ)))) (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg List.length h_1.1) (zero_add 1))) h_1.2) (eq_self 1))) (and_self True))) (and_self True))) fun h_2 => of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg IsIncreasing₂ h_2.1) isIncreasing₂_nil._simp_1)) (Eq.trans (congr (congrArg And (Eq.trans (forall_congr fun a => Eq.trans (implies_congr_ctx (Eq.trans (congrArg (fun x => a ∈ x) h_2.1) List.not_mem_nil._simp_1) fun a_1 => IsEmpty.forall_iff._simp_1) (implies_true False)) (implies_true (Fin 3 → ℕ)))) (Eq.trans (congr (congrArg (fun x => Eq x.length) h_2.1) h_2.2) (eq_self 0))) (and_self True))) (and_self True)) }⊢ ∀ a ∈ {x | ∃ a, a = [fun x => 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ 1 All goals completed! 🐙⟩, 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 := fun x s => { mp := fun x_1 => match x_1 with | ⟨hs₁, ⟨hs₂, hx⟩⟩ => have this := hx ▸ isIncreasing₂_const_length hs₁ hs₂; if x_2 : 1 ≤ x then Eq.ndrec (motive := fun x => IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x → s.length = x → x < 2 → s = [fun x => 1] ∧ x = 1 ∨ s = [] ∧ x = 0) (fun x hx this => Eq.mpr (id (Eq.trans (congr (congrArg Or (Eq.trans (congrArg (And (s = [fun x => 1])) (eq_self 1)) (and_true (s = [fun x => 1])))) (Eq.trans (congrArg (And (s = [])) one_ne_zero._simp_1) (and_false (s = [])))) (or_false (s = [fun x => 1])))) (Exists.casesOn (List.length_eq_one_iff.mp hx) fun a h => Eq.ndrec (motive := fun s => IsIncreasing₂ s → (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) → IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = 1 → s.length = 1 → s = [fun x => 1]) (fun hs₁ hs₂ x hx => Eq.mpr (id (congrArg (fun _a => [_a] = [fun x => 1]) (have this := funext fun i => of_eq_true (Eq.trans (congrArg (fun x => x = 1) (Eq.mp (Eq.trans (forall_congr fun a_1 => implies_congr (Eq.trans List.mem_cons._simp_1 (Eq.trans (congrArg (Or (a_1 = a)) List.not_mem_nil._simp_1) (or_false (a_1 = a)))) (Eq.refl (∀ (i : Fin 3), a_1 i = 1))) forall_eq._simp_1) hs₂ i)) (eq_self 1)); this))) (Eq.refl [fun x => 1])) (Eq.symm h) hs₁ hs₂ x hx)) (Eq.symm (le_antisymm (Nat.ge_of_not_lt (Mathlib.Tactic.IntervalCases.of_lt_right this (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))))) x_2)) x_1 hx this else Eq.ndrec (motive := fun x => IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x → s.length = x → x < 2 → s = [fun x => 1] ∧ x = 1 ∨ s = [] ∧ x = 0) (fun x hx this => of_eq_true (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (Eq.trans (congrArg (fun x => x = [fun x => 1]) (List.length_eq_zero_iff.mp hx)) List.ne_cons_self._simp_1)) zero_ne_one._simp_1) (and_self False))) (Eq.trans (congr (congrArg And (Eq.trans (congrArg (fun x => x = []) (List.length_eq_zero_iff.mp hx)) (eq_self []))) (eq_self 0)) (and_self True))) (or_true False))) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_2) (Nat.zero_le x))) x_1 hx this, mpr := fun h => Or.casesOn h (fun h_1 => of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg IsIncreasing₂ h_1.1) (isIncreasing₂_singleton._simp_1 fun x => 1))) (Eq.trans (congr (congrArg And (Eq.trans (forall_congr fun a => Eq.trans (implies_congr_ctx (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) h_1.1) List.mem_cons._simp_1) (Eq.trans (congrArg (Or (a = fun x => 1)) List.not_mem_nil._simp_1) (or_false (a = fun x => 1)))) fun a_1 => Eq.trans (forall_congr fun i => Eq.trans (congrArg (fun x => x i = 1) a_1) (eq_self 1)) (implies_true (Fin 3))) (implies_true (a = fun x => 1))) (implies_true (Fin 3 → ℕ)))) (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg List.length h_1.1) (zero_add 1))) h_1.2) (eq_self 1))) (and_self True))) (and_self True))) fun h_2 => of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg IsIncreasing₂ h_2.1) isIncreasing₂_nil._simp_1)) (Eq.trans (congr (congrArg And (Eq.trans (forall_congr fun a => Eq.trans (implies_congr_ctx (Eq.trans (congrArg (fun x => a ∈ x) h_2.1) List.not_mem_nil._simp_1) fun a_1 => IsEmpty.forall_iff._simp_1) (implies_true False)) (implies_true (Fin 3 → ℕ)))) (Eq.trans (congr (congrArg (fun x => Eq x.length) h_2.1) h_2.2) (eq_self 0))) (and_self True))) (and_self True)) }⊢ (∀ 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 ⟨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 := fun x s => { mp := fun x_1 => match x_1 with | ⟨hs₁, ⟨hs₂, hx⟩⟩ => have this := hx ▸ isIncreasing₂_const_length hs₁ hs₂; if x_2 : 1 ≤ x then Eq.ndrec (motive := fun x => IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x → s.length = x → x < 2 → s = [fun x => 1] ∧ x = 1 ∨ s = [] ∧ x = 0) (fun x hx this => Eq.mpr (id (Eq.trans (congr (congrArg Or (Eq.trans (congrArg (And (s = [fun x => 1])) (eq_self 1)) (and_true (s = [fun x => 1])))) (Eq.trans (congrArg (And (s = [])) one_ne_zero._simp_1) (and_false (s = [])))) (or_false (s = [fun x => 1])))) (Exists.casesOn (List.length_eq_one_iff.mp hx) fun a h => Eq.ndrec (motive := fun s => IsIncreasing₂ s → (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) → IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = 1 → s.length = 1 → s = [fun x => 1]) (fun hs₁ hs₂ x hx => Eq.mpr (id (congrArg (fun _a => [_a] = [fun x => 1]) (have this := funext fun i => of_eq_true (Eq.trans (congrArg (fun x => x = 1) (Eq.mp (Eq.trans (forall_congr fun a_1 => implies_congr (Eq.trans List.mem_cons._simp_1 (Eq.trans (congrArg (Or (a_1 = a)) List.not_mem_nil._simp_1) (or_false (a_1 = a)))) (Eq.refl (∀ (i : Fin 3), a_1 i = 1))) forall_eq._simp_1) hs₂ i)) (eq_self 1)); this))) (Eq.refl [fun x => 1])) (Eq.symm h) hs₁ hs₂ x hx)) (Eq.symm (le_antisymm (Nat.ge_of_not_lt (Mathlib.Tactic.IntervalCases.of_lt_right this (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))))) x_2)) x_1 hx this else Eq.ndrec (motive := fun x => IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x → s.length = x → x < 2 → s = [fun x => 1] ∧ x = 1 ∨ s = [] ∧ x = 0) (fun x hx this => of_eq_true (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (Eq.trans (congrArg (fun x => x = [fun x => 1]) (List.length_eq_zero_iff.mp hx)) List.ne_cons_self._simp_1)) zero_ne_one._simp_1) (and_self False))) (Eq.trans (congr (congrArg And (Eq.trans (congrArg (fun x => x = []) (List.length_eq_zero_iff.mp hx)) (eq_self []))) (eq_self 0)) (and_self True))) (or_true False))) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_2) (Nat.zero_le x))) x_1 hx this, mpr := fun h => Or.casesOn h (fun h_1 => of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg IsIncreasing₂ h_1.1) (isIncreasing₂_singleton._simp_1 fun x => 1))) (Eq.trans (congr (congrArg And (Eq.trans (forall_congr fun a => Eq.trans (implies_congr_ctx (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) h_1.1) List.mem_cons._simp_1) (Eq.trans (congrArg (Or (a = fun x => 1)) List.not_mem_nil._simp_1) (or_false (a = fun x => 1)))) fun a_1 => Eq.trans (forall_congr fun i => Eq.trans (congrArg (fun x => x i = 1) a_1) (eq_self 1)) (implies_true (Fin 3))) (implies_true (a = fun x => 1))) (implies_true (Fin 3 → ℕ)))) (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg List.length h_1.1) (zero_add 1))) h_1.2) (eq_self 1))) (and_self True))) (and_self True))) fun h_2 => of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg IsIncreasing₂ h_2.1) isIncreasing₂_nil._simp_1)) (Eq.trans (congr (congrArg And (Eq.trans (forall_congr fun a => Eq.trans (implies_congr_ctx (Eq.trans (congrArg (fun x => a ∈ x) h_2.1) List.not_mem_nil._simp_1) fun a_1 => IsEmpty.forall_iff._simp_1) (implies_true False)) (implies_true (Fin 3 → ℕ)))) (Eq.trans (congr (congrArg (fun x => Eq x.length) h_2.1) h_2.2) (eq_self 0))) (and_self True))) (and_self True)) }⊢ ∀ a ∈ {x | ∃ a, a = [fun x => 1] ∧ x = 1 ∨ a = [] ∧ x = 0}, a ≤ 1 All goals completed! 🐙, fun n 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 = 0 := fun x s => { mp := fun x_1 => match x_1 with | ⟨hs₁, ⟨hs₂, hx⟩⟩ => have this := hx ▸ isIncreasing₂_const_length hs₁ hs₂; if x_2 : 1 ≤ x then Eq.ndrec (motive := fun x => IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x → s.length = x → x < 2 → s = [fun x => 1] ∧ x = 1 ∨ s = [] ∧ x = 0) (fun x hx this => Eq.mpr (id (Eq.trans (congr (congrArg Or (Eq.trans (congrArg (And (s = [fun x => 1])) (eq_self 1)) (and_true (s = [fun x => 1])))) (Eq.trans (congrArg (And (s = [])) one_ne_zero._simp_1) (and_false (s = [])))) (or_false (s = [fun x => 1])))) (Exists.casesOn (List.length_eq_one_iff.mp hx) fun a h => Eq.ndrec (motive := fun s => IsIncreasing₂ s → (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) → IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = 1 → s.length = 1 → s = [fun x => 1]) (fun hs₁ hs₂ x hx => Eq.mpr (id (congrArg (fun _a => [_a] = [fun x => 1]) (have this := funext fun i => of_eq_true (Eq.trans (congrArg (fun x => x = 1) (Eq.mp (Eq.trans (forall_congr fun a_1 => implies_congr (Eq.trans List.mem_cons._simp_1 (Eq.trans (congrArg (Or (a_1 = a)) List.not_mem_nil._simp_1) (or_false (a_1 = a)))) (Eq.refl (∀ (i : Fin 3), a_1 i = 1))) forall_eq._simp_1) hs₂ i)) (eq_self 1)); this))) (Eq.refl [fun x => 1])) (Eq.symm h) hs₁ hs₂ x hx)) (Eq.symm (le_antisymm (Nat.ge_of_not_lt (Mathlib.Tactic.IntervalCases.of_lt_right this (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))))) x_2)) x_1 hx this else Eq.ndrec (motive := fun x => IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x → s.length = x → x < 2 → s = [fun x => 1] ∧ x = 1 ∨ s = [] ∧ x = 0) (fun x hx this => of_eq_true (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (Eq.trans (congrArg (fun x => x = [fun x => 1]) (List.length_eq_zero_iff.mp hx)) List.ne_cons_self._simp_1)) zero_ne_one._simp_1) (and_self False))) (Eq.trans (congr (congrArg And (Eq.trans (congrArg (fun x => x = []) (List.length_eq_zero_iff.mp hx)) (eq_self []))) (eq_self 0)) (and_self True))) (or_true False))) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_2) (Nat.zero_le x))) x_1 hx this, mpr := fun h => Or.casesOn h (fun h_1 => of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg IsIncreasing₂ h_1.1) (isIncreasing₂_singleton._simp_1 fun x => 1))) (Eq.trans (congr (congrArg And (Eq.trans (forall_congr fun a => Eq.trans (implies_congr_ctx (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) h_1.1) List.mem_cons._simp_1) (Eq.trans (congrArg (Or (a = fun x => 1)) List.not_mem_nil._simp_1) (or_false (a = fun x => 1)))) fun a_1 => Eq.trans (forall_congr fun i => Eq.trans (congrArg (fun x => x i = 1) a_1) (eq_self 1)) (implies_true (Fin 3))) (implies_true (a = fun x => 1))) (implies_true (Fin 3 → ℕ)))) (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg List.length h_1.1) (zero_add 1))) h_1.2) (eq_self 1))) (and_self True))) (and_self True))) fun h_2 => of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg IsIncreasing₂ h_2.1) isIncreasing₂_nil._simp_1)) (Eq.trans (congr (congrArg And (Eq.trans (forall_congr fun a => Eq.trans (implies_congr_ctx (Eq.trans (congrArg (fun x => a ∈ x) h_2.1) List.not_mem_nil._simp_1) fun a_1 => IsEmpty.forall_iff._simp_1) (implies_true False)) (implies_true (Fin 3 → ℕ)))) (Eq.trans (congr (congrArg (fun x => Eq x.length) h_2.1) h_2.2) (eq_self 0))) (and_self True))) (and_self True)) }n:ℕhn:n < 1⊢ ∃ x, (∃ x_1, x_1 = [fun x => 1] ∧ x = 1 ∨ x_1 = [] ∧ x = 0) ∧ ¬x = 0 exact ⟨1, ⟨[fun _ => 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 := fun x s => { mp := fun x_1 => match x_1 with | ⟨hs₁, ⟨hs₂, hx⟩⟩ => have this := hx ▸ isIncreasing₂_const_length hs₁ hs₂; if x_2 : 1 ≤ x then Eq.ndrec (motive := fun x => IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x → s.length = x → x < 2 → s = [fun x => 1] ∧ x = 1 ∨ s = [] ∧ x = 0) (fun x hx this => Eq.mpr (id (Eq.trans (congr (congrArg Or (Eq.trans (congrArg (And (s = [fun x => 1])) (eq_self 1)) (and_true (s = [fun x => 1])))) (Eq.trans (congrArg (And (s = [])) one_ne_zero._simp_1) (and_false (s = [])))) (or_false (s = [fun x => 1])))) (Exists.casesOn (List.length_eq_one_iff.mp hx) fun a h => Eq.ndrec (motive := fun s => IsIncreasing₂ s → (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) → IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = 1 → s.length = 1 → s = [fun x => 1]) (fun hs₁ hs₂ x hx => Eq.mpr (id (congrArg (fun _a => [_a] = [fun x => 1]) (have this := funext fun i => of_eq_true (Eq.trans (congrArg (fun x => x = 1) (Eq.mp (Eq.trans (forall_congr fun a_1 => implies_congr (Eq.trans List.mem_cons._simp_1 (Eq.trans (congrArg (Or (a_1 = a)) List.not_mem_nil._simp_1) (or_false (a_1 = a)))) (Eq.refl (∀ (i : Fin 3), a_1 i = 1))) forall_eq._simp_1) hs₂ i)) (eq_self 1)); this))) (Eq.refl [fun x => 1])) (Eq.symm h) hs₁ hs₂ x hx)) (Eq.symm (le_antisymm (Nat.ge_of_not_lt (Mathlib.Tactic.IntervalCases.of_lt_right this (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2))))) x_2)) x_1 hx this else Eq.ndrec (motive := fun x => IsIncreasing₂ s ∧ (∀ a ∈ s, ∀ (i : Fin 3), a i = 1) ∧ s.length = x → s.length = x → x < 2 → s = [fun x => 1] ∧ x = 1 ∨ s = [] ∧ x = 0) (fun x hx this => of_eq_true (Eq.trans (congr (congrArg Or (Eq.trans (congr (congrArg And (Eq.trans (congrArg (fun x => x = [fun x => 1]) (List.length_eq_zero_iff.mp hx)) List.ne_cons_self._simp_1)) zero_ne_one._simp_1) (and_self False))) (Eq.trans (congr (congrArg And (Eq.trans (congrArg (fun x => x = []) (List.length_eq_zero_iff.mp hx)) (eq_self []))) (eq_self 0)) (and_self True))) (or_true False))) (Eq.symm (le_antisymm (Nat.ge_of_not_lt x_2) (Nat.zero_le x))) x_1 hx this, mpr := fun h => Or.casesOn h (fun h_1 => of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg IsIncreasing₂ h_1.1) (isIncreasing₂_singleton._simp_1 fun x => 1))) (Eq.trans (congr (congrArg And (Eq.trans (forall_congr fun a => Eq.trans (implies_congr_ctx (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) h_1.1) List.mem_cons._simp_1) (Eq.trans (congrArg (Or (a = fun x => 1)) List.not_mem_nil._simp_1) (or_false (a = fun x => 1)))) fun a_1 => Eq.trans (forall_congr fun i => Eq.trans (congrArg (fun x => x i = 1) a_1) (eq_self 1)) (implies_true (Fin 3))) (implies_true (a = fun x => 1))) (implies_true (Fin 3 → ℕ)))) (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg List.length h_1.1) (zero_add 1))) h_1.2) (eq_self 1))) (and_self True))) (and_self True))) fun h_2 => of_eq_true (Eq.trans (congr (congrArg And (Eq.trans (congrArg IsIncreasing₂ h_2.1) isIncreasing₂_nil._simp_1)) (Eq.trans (congr (congrArg And (Eq.trans (forall_congr fun a => Eq.trans (implies_congr_ctx (Eq.trans (congrArg (fun x => a ∈ x) h_2.1) List.not_mem_nil._simp_1) fun a_1 => IsEmpty.forall_iff._simp_1) (implies_true False)) (implies_true (Fin 3 → ℕ)))) (Eq.trans (congr (congrArg (fun x => Eq x.length) h_2.1) h_2.2) (eq_self 0))) (and_self True))) (and_self True)) }n:ℕhn:n < 1⊢ [fun x => 1] = [fun x => 1] ∧ 1 = 1 ∨ [fun x => 1] = [] ∧ 1 = 0 All goals completed! 🐙⟩, one_ne_zero⟩ @[category test, AMS 5] theorem declaration uses 'sorry'maximalLength_four : maximalLength 4 = 8 := ⊢ F 4 = 8 All 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 := s: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 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 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⊢ ∃ 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 := s: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 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.length All goals completed! 🐙 have hf : ∀ k ∈ (Finset.univ : Finset (Fin s.length)), f k ∈ t := s: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 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.card := Eq.mpr (id (congr (congrArg LT.lt (Eq.trans (Finset.card_product (Finset.Icc 1 n) (Finset.Icc 1 n)) (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (exists_pair_of_mem_Icc._simp_1 n)))) (Fintype.card_fin s.length))) hs₂k:Fin s.lengtha✝:k ∈ Finset.univ⊢ f k ∈ t 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 := Eq.mpr (id (congr (congrArg LT.lt (Eq.trans (Finset.card_product (Finset.Icc 1 n) (Finset.Icc 1 n)) (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (exists_pair_of_mem_Icc._simp_1 n)))) (Fintype.card_fin s.length))) hs₂k:Fin s.lengtha✝:k ∈ Finset.univhmem:s[k] ∈ s := List.getElem_mem k.isLt⊢ f k ∈ t 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 := Eq.mpr (id (congr (congrArg LT.lt (Eq.trans (Finset.card_product (Finset.Icc 1 n) (Finset.Icc 1 n)) (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (exists_pair_of_mem_Icc._simp_1 n)))) (Fintype.card_fin s.length))) hs₂k:Fin s.lengtha✝:k ∈ Finset.univhmem:s[k] ∈ s := List.getElem_mem k.isLth0:s[k] 0 ∈ Set.Icc 1 n := hs₁ s[k] hmem (Exists.intro 0 rfl)⊢ f k ∈ t 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 := Eq.mpr (id (congr (congrArg LT.lt (Eq.trans (Finset.card_product (Finset.Icc 1 n) (Finset.Icc 1 n)) (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (exists_pair_of_mem_Icc._simp_1 n)))) (Fintype.card_fin s.length))) hs₂k:Fin s.lengtha✝:k ∈ Finset.univhmem:s[k] ∈ s := List.getElem_mem k.isLth0:s[k] 0 ∈ Set.Icc 1 n := hs₁ s[k] hmem (Exists.intro 0 rfl)h1:s[k] 1 ∈ Set.Icc 1 n := hs₁ s[k] hmem (Exists.intro 1 rfl)⊢ f k ∈ t 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 := Eq.mpr (id (congr (congrArg LT.lt (Eq.trans (Finset.card_product (Finset.Icc 1 n) (Finset.Icc 1 n)) (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (exists_pair_of_mem_Icc._simp_1 n)))) (Fintype.card_fin s.length))) hs₂k:Fin s.lengtha✝:k ∈ Finset.univhmem:s[k] ∈ s := List.getElem_mem k.isLth0:1 ≤ s[k] 0 ∧ s[k] 0 ≤ nh1:1 ≤ s[k] 1 ∧ s[k] 1 ≤ n⊢ f k ∈ t 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 := Eq.mpr (id (congr (congrArg LT.lt (Eq.trans (Finset.card_product (Finset.Icc 1 n) (Finset.Icc 1 n)) (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (exists_pair_of_mem_Icc._simp_1 n)))) (Fintype.card_fin s.length))) hs₂k:Fin s.lengtha✝:k ∈ Finset.univhmem:s[k] ∈ s := List.getElem_mem k.isLth0: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 ≤ n All goals completed! 🐙 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 := Eq.mpr (id (congr (congrArg LT.lt (Eq.trans (Finset.card_product (Finset.Icc 1 n) (Finset.Icc 1 n)) (Eq.trans (congr (congrArg HMul.hMul (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (Eq.trans (Nat.card_Icc 1 n) (Nat.add_sub_cancel n 1))) (exists_pair_of_mem_Icc._simp_1 n)))) (Fintype.card_fin s.length))) hs₂hf:∀ k ∈ Finset.univ, f k ∈ t := fun k a => have hmem := List.getElem_mem k.isLt; have h0 := hs₁ s[k] hmem (Exists.intro 0 rfl); have h1 := hs₁ s[k] hmem (Exists.intro 1 rfl); Eq.mpr (id (Eq.trans exists_pair_of_mem_Icc._simp_2 (congr (congrArg And exists_pair_of_mem_Icc._simp_3) exists_pair_of_mem_Icc._simp_3))) ⟨Eq.mp (congrArg (fun _a => _a) (propext Set.mem_Icc)) h0, Eq.mp (congrArg (fun _a => _a) (propext Set.mem_Icc)) h1⟩i: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 All goals completed! 🐙

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

@[category research solved, AMS 5] theorem declaration uses 'sorry'maximalLength_le (n : ℕ) : F n ≤ n ^ 2 := n:ℕ⊢ F n ≤ n ^ 2 All goals completed! 🐙

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

@[category research solved, AMS 5] theorem declaration uses 'sorry'maximalLength_ge_of_isSquare {n : ℕ} (h : IsSquare n) : n.sqrt ^ 3 ≤ F n := n:ℕh:IsSquare n⊢ n.sqrt ^ 3 ≤ F n All 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 declaration uses 'sorry'maximalLength_le_isBigO : ∃ Ω : ℕ → ℝ, (fun (n : ℕ) => (Real.iteratedLog n : ℝ)) =O[atTop] Ω ∧ ∀ n, F n ≤ n ^ 2 / Real.exp (Ω n) := ⊢ ∃ Ω, (fun n => ↑(↑n).iteratedLog) =O[atTop] Ω ∧ ∀ (n : ℕ), ↑(F n) ≤ ↑n ^ 2 / Real.exp (Ω n) All 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 (Pi.prod a b) @[simp, category API, AMS 5] theorem tripleProduct_const {α : Type*} (a : α) : tripleProduct (fun _ => a) (fun _ => a) = toLex (fun _ => (a, a)) := α:Type u_1a:α⊢ (tripleProduct (fun x => a) fun x => a) = toLex fun x => (a, a) simpa [tripleProduct] using funext fun i => α:Type u_1a:αi:Fin 3⊢ Pi.prod (fun x => a) (fun x => a) i = (a, a) All 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)] := α:Type u_1a:α⊢ tripleProduct ![a, a, a] ![a, a, a] = toLex ![(a, a), (a, a), (a, a)] α:Type u_1a:α⊢ Pi.prod ![a, a, a] ![a, a, a] = ![(a, a), (a, a), (a, a)] α:Type u_1a:αi:Fin 3⊢ (Pi.prod ![a, a, a] ![a, a, a] i).1 = (![(a, a), (a, a), (a, a)] i).1α:Type u_1a:αi:Fin 3⊢ (Pi.prod ![a, a, a] ![a, a, a] i).2 = (![(a, a), (a, a), (a, a)] i).2 α:Type u_1a:αi:Fin 3⊢ (Pi.prod ![a, a, a] ![a, a, a] i).1 = (![(a, a), (a, a), (a, a)] i).1α:Type u_1a:αi:Fin 3⊢ (Pi.prod ![a, a, a] ![a, a, a] i).2 = (![(a, a), (a, a), (a, a)] i).2 α:Type u_1a:α⊢ (Pi.prod ![a, a, a] ![a, a, a] ((fun i => i) ⟨0, ⋯⟩)).2 = (![(a, a), (a, a), (a, a)] ((fun i => i) ⟨0, ⋯⟩)).2α:Type u_1a:α⊢ (Pi.prod ![a, a, a] ![a, a, a] ((fun i => i) ⟨1, ⋯⟩)).2 = (![(a, a), (a, a), (a, a)] ((fun i => i) ⟨1, ⋯⟩)).2α:Type u_1a:α⊢ (Pi.prod ![a, a, a] ![a, a, a] ((fun i => i) ⟨2, ⋯⟩)).2 = (![(a, a), (a, a), (a, a)] ((fun i => i) ⟨2, ⋯⟩)).2 α:Type u_1a:α⊢ (Pi.prod ![a, a, a] ![a, a, a] ((fun i => i) ⟨0, ⋯⟩)).1 = (![(a, a), (a, a), (a, a)] ((fun i => i) ⟨0, ⋯⟩)).1α:Type u_1a:α⊢ (Pi.prod ![a, a, a] ![a, a, a] ((fun i => i) ⟨1, ⋯⟩)).1 = (![(a, a), (a, a), (a, a)] ((fun i => i) ⟨1, ⋯⟩)).1α:Type u_1a:α⊢ (Pi.prod ![a, a, a] ![a, a, a] ((fun i => i) ⟨2, ⋯⟩)).1 = (![(a, a), (a, a), (a, a)] ((fun i => i) ⟨2, ⋯⟩)).1α:Type u_1a:α⊢ (Pi.prod ![a, a, a] ![a, a, a] ((fun i => i) ⟨0, ⋯⟩)).2 = (![(a, a), (a, a), (a, a)] ((fun i => i) ⟨0, ⋯⟩)).2α:Type u_1a:α⊢ (Pi.prod ![a, a, a] ![a, a, a] ((fun i => i) ⟨1, ⋯⟩)).2 = (![(a, a), (a, a), (a, a)] ((fun i => i) ⟨1, ⋯⟩)).2α:Type u_1a:α⊢ (Pi.prod ![a, a, a] ![a, a, a] ((fun i => i) ⟨2, ⋯⟩)).2 = (![(a, a), (a, a), (a, a)] ((fun i => i) ⟨2, ⋯⟩)).2 All 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)]] := ⊢ [![1, 1, 1]] ⊗₂ [![1, 1, 1]] = toLex [toLex ![(1, 1), (1, 1), (1, 1)]] 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 declaration uses 'sorry'maximalLength_pow {n : ℕ} {e : ℝ} (hn : 1 < n) (h : F n = (n : ℝ) ^ e) : ∀ᶠ m : ℕ in Filter.atTop, (m : ℝ) ^ e ≤ F m := n:ℕe:ℝhn:1 < nh:↑(F n) = ↑n ^ e⊢ ∀ᶠ (m : ℕ) in Filter.atTop, ↑m ^ e ≤ ↑(F m) All goals completed! 🐙

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

@[category research open, AMS 5] theorem declaration uses 'sorry'maximalLength_le_strong (n : ℕ) : F n ≤ Real.sqrt n ^ 3 := n:ℕ⊢ ↑(F n) ≤ √↑n ^ 3 All goals completed! 🐙 end Arxiv.«1609.08688»