FormalConjectures.ErdosProblems.«107»

/-
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

Erdős Problem 107

References:

erdosproblems.com/107

Wikipedia


open Filter

open EuclideanGeometry


namespace Erdos107

The set of $N$ such that any $N$ points in the plane, no three on a line, contain a convex $n$-gon.

def cardSet (n : ℕ) := { N | ∀ (pts : Finset ℝ²), pts.card = N → NonTrilinear (pts : Set ℝ²) →
  HasConvexNGon n pts }

The function $f(n)$ specified in erdos_107.

noncomputable def f (n : ℕ) : ℕ :=
  sInf (cardSet n)

Let $f(n)$ be minimal such that any $f(n)$ points in $ℝ^2$, no three on a line, contain $n$ points which form the vertices of a convex $n$-gon. Prove that $f(n) = 2^{n-2} + 1$.

@[category research open, AMS 52]
theorem declaration uses 'sorry'erdos_107 : answer(sorry) ↔ ∀ n ≥ 3, f n = 2^(n - 2) + 1 := by⊢ True ↔ ∀ n ≥ 3, f n = 2 ^ (n - 2) + 1
  sorryAll goals completed! 🐙

For every $n ≥ 3$, there exists $N$ such that any $N$ points, no three on a line, contain a convex $n$-gon.

@[category research solved, AMS 52]
theorem declaration uses 'sorry'nonempty_cardSet : ∀ n ≥ 3, (cardSet n).Nonempty := by⊢ ∀ n ≥ 3, (cardSet n).Nonempty
  sorryAll goals completed! 🐙

Depending on details of definitions, the statement is false or trivial for $n < 3$.

@[category test, AMS 52]
theorem f_zero_eq : f 0 = 0 := by⊢ f 0 = 0
  have : ∀ P, HasConvexNGon 0 P := by⊢ f 0 = 0
    introP✝:Set ℝ²⊢ HasConvexNGon 0 P✝; use ∅hP✝:Set ℝ²⊢ ∅.card = 0 ∧ ↑∅ ⊆ P✝ ∧ ConvexIndep ↑∅; simp [ConvexIndep]All goals completed! 🐙
  simp [f, cardSet, this]All goals completed! 🐙

Three distinct non-collinear points form a convex-independent set.

@[category API, AMS 52]
private lemma convexIndep_triple_of_not_collinear {a b c : ℝ²}
    (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
    (hcoll : ¬ Collinear ℝ ({a, b, c} : Set ℝ²)) :
    ConvexIndep ({a, b, c} : Set ℝ²) := bya:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chcoll:¬Collinear ℝ {a, b, c}⊢ ConvexIndep {a, b, c}
  intro x hxa:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chcoll:¬Collinear ℝ {a, b, c}x:ℝ²hx:x ∈ {a, b, c}⊢ x ∉ (convexHull ℝ) ({a, b, c} \ {x}) hmema:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chcoll:¬Collinear ℝ {a, b, c}x:ℝ²hx:x ∈ {a, b, c}hmem:x ∈ (convexHull ℝ) ({a, b, c} \ {x})⊢ False
  -- The point `x` lies in the affine span of `{a, b, c} \ {x}` because it
  -- lies in the convex hull of that two-element set.
  apply hcolla:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chcoll:¬Collinear ℝ {a, b, c}x:ℝ²hx:x ∈ {a, b, c}hmem:x ∈ (convexHull ℝ) ({a, b, c} \ {x})⊢ Collinear ℝ {a, b, c}
  have hx_aff : x ∈ affineSpan ℝ (({a, b, c} : Set ℝ²) \ {x}) :=
    convexHull_subset_affineSpan _ hmema:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chcoll:¬Collinear ℝ {a, b, c}x:ℝ²hx:x ∈ {a, b, c}hmem:x ∈ (convexHull ℝ) ({a, b, c} \ {x})hx_aff:x ∈ affineSpan ℝ ({a, b, c} \ {x}) := convexHull_subset_affineSpan ({a, b, c} \ {x}) hmem⊢ Collinear ℝ {a, b, c}
  rw [show ({a, b, c} : Set ℝ²) = insert x (({a, b, c} : Set ℝ²) \ {x}) from
        (Set.insert_diff_self_of_mem hx).symm,
      collinear_insert_iff_of_mem_affineSpan hx_aff]a:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chcoll:¬Collinear ℝ {a, b, c}x:ℝ²hx:x ∈ {a, b, c}hmem:x ∈ (convexHull ℝ) ({a, b, c} \ {x})hx_aff:x ∈ affineSpan ℝ ({a, b, c} \ {x}) := convexHull_subset_affineSpan ({a, b, c} \ {x}) hmem⊢ Collinear ℝ ({a, b, c} \ {x})
  -- The two-element complement is collinear.
  simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hxa:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chcoll:¬Collinear ℝ {a, b, c}x:ℝ²hmem:x ∈ (convexHull ℝ) ({a, b, c} \ {x})hx_aff:x ∈ affineSpan ℝ ({a, b, c} \ {x}) := convexHull_subset_affineSpan ({a, b, c} \ {x}) hmemhx:x = a ∨ x = b ∨ x = c⊢ Collinear ℝ ({a, b, c} \ {x})
  rcases hx with rfl | rfl | rflinlb:ℝ²c:ℝ²hbc:b ≠ cx:ℝ²hab:x ≠ bhac:x ≠ chcoll:¬Collinear ℝ {x, b, c}hmem:x ∈ (convexHull ℝ) ({x, b, c} \ {x})hx_aff:x ∈ affineSpan ℝ ({x, b, c} \ {x})⊢ Collinear ℝ ({x, b, c} \ {x})inr.inla:ℝ²c:ℝ²hac:a ≠ cx:ℝ²hab:a ≠ xhbc:x ≠ chcoll:¬Collinear ℝ {a, x, c}hmem:x ∈ (convexHull ℝ) ({a, x, c} \ {x})hx_aff:x ∈ affineSpan ℝ ({a, x, c} \ {x})⊢ Collinear ℝ ({a, x, c} \ {x})inr.inra:ℝ²b:ℝ²hab:a ≠ bx:ℝ²hac:a ≠ xhbc:b ≠ xhcoll:¬Collinear ℝ {a, b, x}hmem:x ∈ (convexHull ℝ) ({a, b, x} \ {x})hx_aff:x ∈ affineSpan ℝ ({a, b, x} \ {x})⊢ Collinear ℝ ({a, b, x} \ {x})
  ·inlb:ℝ²c:ℝ²hbc:b ≠ cx:ℝ²hab:x ≠ bhac:x ≠ chcoll:¬Collinear ℝ {x, b, c}hmem:x ∈ (convexHull ℝ) ({x, b, c} \ {x})hx_aff:x ∈ affineSpan ℝ ({x, b, c} \ {x})⊢ Collinear ℝ ({x, b, c} \ {x}) rw [show ({x, b, c} : Set ℝ²) \ {x} = ({b, c} : Set ℝ²) by ext; aesop]inlb:ℝ²c:ℝ²hbc:b ≠ cx:ℝ²hab:x ≠ bhac:x ≠ chcoll:¬Collinear ℝ {x, b, c}hmem:x ∈ (convexHull ℝ) ({x, b, c} \ {x})hx_aff:x ∈ affineSpan ℝ ({x, b, c} \ {x})⊢ Collinear ℝ {b, c}
    exact collinear_pair ℝ b cAll goals completed! 🐙
  ·inr.inla:ℝ²c:ℝ²hac:a ≠ cx:ℝ²hab:a ≠ xhbc:x ≠ chcoll:¬Collinear ℝ {a, x, c}hmem:x ∈ (convexHull ℝ) ({a, x, c} \ {x})hx_aff:x ∈ affineSpan ℝ ({a, x, c} \ {x})⊢ Collinear ℝ ({a, x, c} \ {x}) rw [show ({a, x, c} : Set ℝ²) \ {x} = ({a, c} : Set ℝ²) by ext; aesop]inr.inla:ℝ²c:ℝ²hac:a ≠ cx:ℝ²hab:a ≠ xhbc:x ≠ chcoll:¬Collinear ℝ {a, x, c}hmem:x ∈ (convexHull ℝ) ({a, x, c} \ {x})hx_aff:x ∈ affineSpan ℝ ({a, x, c} \ {x})⊢ Collinear ℝ {a, c}
    exact collinear_pair ℝ a cAll goals completed! 🐙
  ·inr.inra:ℝ²b:ℝ²hab:a ≠ bx:ℝ²hac:a ≠ xhbc:b ≠ xhcoll:¬Collinear ℝ {a, b, x}hmem:x ∈ (convexHull ℝ) ({a, b, x} \ {x})hx_aff:x ∈ affineSpan ℝ ({a, b, x} \ {x})⊢ Collinear ℝ ({a, b, x} \ {x}) rw [show ({a, b, x} : Set ℝ²) \ {x} = ({a, b} : Set ℝ²) by ext; aesop]inr.inra:ℝ²b:ℝ²hab:a ≠ bx:ℝ²hac:a ≠ xhbc:b ≠ xhcoll:¬Collinear ℝ {a, b, x}hmem:x ∈ (convexHull ℝ) ({a, b, x} \ {x})hx_aff:x ∈ affineSpan ℝ ({a, b, x} \ {x})⊢ Collinear ℝ {a, b}
    exact collinear_pair ℝ a bAll goals completed! 🐙


@[category test, AMS 52]
theorem f_three_eq : f 3 = 3 := by⊢ f 3 = 3
  -- The substantive bound: 3 ∈ cardSet 3.
  have hmem3 : (3 : ℕ) ∈ cardSet 3 := by⊢ f 3 = 3
    intro pts hptspts:Finset ℝ²hpts:pts.card = 3⊢ NonTrilinear ↑pts → HasConvexNGon 3 ↑pts hnontripts:Finset ℝ²hpts:pts.card = 3hnontri:NonTrilinear ↑pts⊢ HasConvexNGon 3 ↑pts
    obtain ⟨a, b, c, hab, hac, hbc, rfl⟩ := Finset.card_eq_three.mp hptsa:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chpts:{a, b, c}.card = 3hnontri:NonTrilinear ↑{a, b, c}⊢ HasConvexNGon 3 ↑{a, b, c}
    refine ⟨{a, b, c}, bya:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chpts:{a, b, c}.card = 3hnontri:NonTrilinear ↑{a, b, c}⊢ {a, b, c}.card = 3 simp [hab, hac, hbc]All goals completed! 🐙, subset_refl _, ?_⟩
    have hcoerce : (({a, b, c} : Finset ℝ²) : Set ℝ²) = ({a, b, c} : Set ℝ²) := by⊢ f 3 = 3 simpAll goals completed! 🐙
    have hmem : ∀ {y : ℝ²}, y ∈ ({a, b, c} : Set ℝ²) →
        y ∈ (({a, b, c} : Finset ℝ²) : Set ℝ²) := fun h => hcoerce ▸ ha:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chpts:{a, b, c}.card = 3hnontri:NonTrilinear ↑{a, b, c}hcoerce:↑{a, b, c} = {a, b, c} := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = {a, b, c})
        (Eq.trans (Finset.coe_insert a {b, c})
          (congrArg (insert a) (Eq.trans (Finset.coe_insert b {c}) (congrArg (insert b) (Finset.coe_singleton c))))))
      (eq_self {a, b, c}))hmem:∀ {y : ℝ²}, y ∈ {a, b, c} → y ∈ ↑{a, b, c} := fun {y} h => Eq.symm hcoerce ▸ h⊢ ConvexIndep ↑{a, b, c}
    have hnc : ¬ Collinear ℝ ({a, b, c} : Set ℝ²) :=
      hnontri (hmem (bya:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chpts:{a, b, c}.card = 3hnontri:NonTrilinear ↑{a, b, c}hcoerce:↑{a, b, c} = {a, b, c} := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = {a, b, c})
        (Eq.trans (Finset.coe_insert a {b, c})
          (congrArg (insert a) (Eq.trans (Finset.coe_insert b {c}) (congrArg (insert b) (Finset.coe_singleton c))))))
      (eq_self {a, b, c}))hmem:∀ {y : ℝ²}, y ∈ {a, b, c} → y ∈ ↑{a, b, c} := fun {y} h => Eq.symm hcoerce ▸ h⊢ a ∈ {a, b, c} simpAll goals completed! 🐙)) (hmem (bya:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chpts:{a, b, c}.card = 3hnontri:NonTrilinear ↑{a, b, c}hcoerce:↑{a, b, c} = {a, b, c} := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = {a, b, c})
        (Eq.trans (Finset.coe_insert a {b, c})
          (congrArg (insert a) (Eq.trans (Finset.coe_insert b {c}) (congrArg (insert b) (Finset.coe_singleton c))))))
      (eq_self {a, b, c}))hmem:∀ {y : ℝ²}, y ∈ {a, b, c} → y ∈ ↑{a, b, c} := fun {y} h => Eq.symm hcoerce ▸ h⊢ b ∈ {a, b, c} simpAll goals completed! 🐙)) (hmem (bya:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chpts:{a, b, c}.card = 3hnontri:NonTrilinear ↑{a, b, c}hcoerce:↑{a, b, c} = {a, b, c} := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = {a, b, c})
        (Eq.trans (Finset.coe_insert a {b, c})
          (congrArg (insert a) (Eq.trans (Finset.coe_insert b {c}) (congrArg (insert b) (Finset.coe_singleton c))))))
      (eq_self {a, b, c}))hmem:∀ {y : ℝ²}, y ∈ {a, b, c} → y ∈ ↑{a, b, c} := fun {y} h => Eq.symm hcoerce ▸ h⊢ c ∈ {a, b, c} simpAll goals completed! 🐙)) hab hbc hac
    rw [hcoerce]a:ℝ²b:ℝ²c:ℝ²hab:a ≠ bhac:a ≠ chbc:b ≠ chpts:{a, b, c}.card = 3hnontri:NonTrilinear ↑{a, b, c}hcoerce:↑{a, b, c} = {a, b, c} := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = {a, b, c})
        (Eq.trans (Finset.coe_insert a {b, c})
          (congrArg (insert a) (Eq.trans (Finset.coe_insert b {c}) (congrArg (insert b) (Finset.coe_singleton c))))))
      (eq_self {a, b, c}))hmem:∀ {y : ℝ²}, y ∈ {a, b, c} → y ∈ ↑{a, b, c} := fun {y} h => Eq.symm hcoerce ▸ hhnc:¬Collinear ℝ {a, b, c} := 
  hnontri
    (hmem
      (of_eq_true
        (Eq.trans Set.mem_insert_iff._simp_1
          (Eq.trans
            (congr (congrArg Or (eq_self a))
              (Eq.trans Set.mem_insert_iff._simp_1 (congrArg (Or (a = b)) Set.mem_singleton_iff._simp_1)))
            (true_or (a = b ∨ a = c))))))
    (hmem
      (of_eq_true
        (Eq.trans Set.mem_insert_iff._simp_1
          (Eq.trans
            (congrArg (Or (b = a))
              (Eq.trans Set.mem_insert_iff._simp_1
                (Eq.trans (congr (congrArg Or (eq_self b)) Set.mem_singleton_iff._simp_1) (true_or (b = c)))))
            (or_true (b = a))))))
    (hmem
      (of_eq_true
        (Eq.trans Set.mem_insert_iff._simp_1
          (Eq.trans
            (congrArg (Or (c = a))
              (Eq.trans Set.mem_insert_iff._simp_1
                (Eq.trans (congrArg (Or (c = b)) (Eq.trans Set.mem_singleton_iff._simp_1 (eq_self c)))
                  (or_true (c = b)))))
            (or_true (c = a))))))
    hab hbc hac⊢ ConvexIndep {a, b, c}
    exact convexIndep_triple_of_not_collinear hab hac hbc hncAll goals completed! 🐙
  refine le_antisymm (Nat.sInf_le hmem3) (le_csInf ⟨3, hmem3⟩ fun N hN => ?_)hmem3:3 ∈ cardSet 3 := 
  fun pts hpts hnontri =>
    Exists.casesOn (Finset.card_eq_three.mp hpts) fun a h =>
      Exists.casesOn h fun b h =>
        Exists.casesOn h fun c h =>
          And.casesOn h fun hab right =>
            And.casesOn right fun hac right =>
              And.casesOn right fun hbc right =>
                Eq.ndrec (motive := fun pts => pts.card = 3 → NonTrilinear ↑pts → HasConvexNGon 3 ↑pts)
                  (fun hpts hnontri =>
                    Exists.intro {a, b, c}
                      ⟨of_eq_true
                          (Eq.trans
                            (congrArg (fun x => x = 3)
                              (Eq.trans
                                (Finset.card_insert_of_notMem
                                  (of_eq_true
                                    (Eq.trans
                                      (congrArg Not
                                        (Eq.trans Finset.mem_insert._simp_1
                                          (Eq.trans
                                            (congr (congrArg Or (eq_false hab))
                                              (Eq.trans Finset.mem_singleton._simp_1 (eq_false hac)))
                                            (or_self False))))
                                      not_false_eq_true)))
                                (congrArg (fun x => x + 1)
                                  (Eq.trans
                                    (Finset.card_insert_of_notMem
                                      (of_eq_true
                                        (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false hbc)))
                                          not_false_eq_true)))
                                    (congrArg (fun x => x + 1) (Finset.card_singleton c))))))
                            (eq_self 3)),
                        ⟨subset_refl ↑{a, b, c},
                          have hcoerce :=
                            of_eq_true
                              (Eq.trans
                                (congrArg (fun x => x = {a, b, c})
                                  (Eq.trans (Finset.coe_insert a {b, c})
                                    (congrArg (insert a)
                                      (Eq.trans (Finset.coe_insert b {c})
                                        (congrArg (insert b) (Finset.coe_singleton c))))))
                                (eq_self {a, b, c}));
                          have hmem := fun {y} h => Eq.symm hcoerce ▸ h;
                          have hnc :=
                            hnontri
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congr (congrArg Or (eq_self a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (congrArg (Or (a = b)) Set.mem_singleton_iff._simp_1)))
                                      (true_or (a = b ∨ a = c))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (b = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans (congr (congrArg Or (eq_self b)) Set.mem_singleton_iff._simp_1)
                                            (true_or (b = c)))))
                                      (or_true (b = a))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (c = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans
                                            (congrArg (Or (c = b)) (Eq.trans Set.mem_singleton_iff._simp_1 (eq_self c)))
                                            (or_true (c = b)))))
                                      (or_true (c = a))))))
                              hab hbc hac;
                          Eq.mpr (id (congrArg (fun _a => ConvexIndep _a) hcoerce))
                            (convexIndep_triple_of_not_collinear hab hac hbc hnc)⟩⟩)
                  (Eq.symm right) hpts hnontriN:ℕhN:N ∈ cardSet 3⊢ 3 ≤ N
  -- A set with fewer than 3 points contains no 3-element subset.
  by_contra! hlthmem3:3 ∈ cardSet 3 := 
  fun pts hpts hnontri =>
    Exists.casesOn (Finset.card_eq_three.mp hpts) fun a h =>
      Exists.casesOn h fun b h =>
        Exists.casesOn h fun c h =>
          And.casesOn h fun hab right =>
            And.casesOn right fun hac right =>
              And.casesOn right fun hbc right =>
                Eq.ndrec (motive := fun pts => pts.card = 3 → NonTrilinear ↑pts → HasConvexNGon 3 ↑pts)
                  (fun hpts hnontri =>
                    Exists.intro {a, b, c}
                      ⟨of_eq_true
                          (Eq.trans
                            (congrArg (fun x => x = 3)
                              (Eq.trans
                                (Finset.card_insert_of_notMem
                                  (of_eq_true
                                    (Eq.trans
                                      (congrArg Not
                                        (Eq.trans Finset.mem_insert._simp_1
                                          (Eq.trans
                                            (congr (congrArg Or (eq_false hab))
                                              (Eq.trans Finset.mem_singleton._simp_1 (eq_false hac)))
                                            (or_self False))))
                                      not_false_eq_true)))
                                (congrArg (fun x => x + 1)
                                  (Eq.trans
                                    (Finset.card_insert_of_notMem
                                      (of_eq_true
                                        (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false hbc)))
                                          not_false_eq_true)))
                                    (congrArg (fun x => x + 1) (Finset.card_singleton c))))))
                            (eq_self 3)),
                        ⟨subset_refl ↑{a, b, c},
                          have hcoerce :=
                            of_eq_true
                              (Eq.trans
                                (congrArg (fun x => x = {a, b, c})
                                  (Eq.trans (Finset.coe_insert a {b, c})
                                    (congrArg (insert a)
                                      (Eq.trans (Finset.coe_insert b {c})
                                        (congrArg (insert b) (Finset.coe_singleton c))))))
                                (eq_self {a, b, c}));
                          have hmem := fun {y} h => Eq.symm hcoerce ▸ h;
                          have hnc :=
                            hnontri
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congr (congrArg Or (eq_self a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (congrArg (Or (a = b)) Set.mem_singleton_iff._simp_1)))
                                      (true_or (a = b ∨ a = c))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (b = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans (congr (congrArg Or (eq_self b)) Set.mem_singleton_iff._simp_1)
                                            (true_or (b = c)))))
                                      (or_true (b = a))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (c = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans
                                            (congrArg (Or (c = b)) (Eq.trans Set.mem_singleton_iff._simp_1 (eq_self c)))
                                            (or_true (c = b)))))
                                      (or_true (c = a))))))
                              hab hbc hac;
                          Eq.mpr (id (congrArg (fun _a => ConvexIndep _a) hcoerce))
                            (convexIndep_triple_of_not_collinear hab hac hbc hnc)⟩⟩)
                  (Eq.symm right) hpts hnontriN:ℕhN:N ∈ cardSet 3hlt:N < 3⊢ False
  let f : ℕ → ℝ² := fun i => EuclideanSpace.single 0 (i : ℝ)hmem3:3 ∈ cardSet 3 := 
  fun pts hpts hnontri =>
    Exists.casesOn (Finset.card_eq_three.mp hpts) fun a h =>
      Exists.casesOn h fun b h =>
        Exists.casesOn h fun c h =>
          And.casesOn h fun hab right =>
            And.casesOn right fun hac right =>
              And.casesOn right fun hbc right =>
                Eq.ndrec (motive := fun pts => pts.card = 3 → NonTrilinear ↑pts → HasConvexNGon 3 ↑pts)
                  (fun hpts hnontri =>
                    Exists.intro {a, b, c}
                      ⟨of_eq_true
                          (Eq.trans
                            (congrArg (fun x => x = 3)
                              (Eq.trans
                                (Finset.card_insert_of_notMem
                                  (of_eq_true
                                    (Eq.trans
                                      (congrArg Not
                                        (Eq.trans Finset.mem_insert._simp_1
                                          (Eq.trans
                                            (congr (congrArg Or (eq_false hab))
                                              (Eq.trans Finset.mem_singleton._simp_1 (eq_false hac)))
                                            (or_self False))))
                                      not_false_eq_true)))
                                (congrArg (fun x => x + 1)
                                  (Eq.trans
                                    (Finset.card_insert_of_notMem
                                      (of_eq_true
                                        (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false hbc)))
                                          not_false_eq_true)))
                                    (congrArg (fun x => x + 1) (Finset.card_singleton c))))))
                            (eq_self 3)),
                        ⟨subset_refl ↑{a, b, c},
                          have hcoerce :=
                            of_eq_true
                              (Eq.trans
                                (congrArg (fun x => x = {a, b, c})
                                  (Eq.trans (Finset.coe_insert a {b, c})
                                    (congrArg (insert a)
                                      (Eq.trans (Finset.coe_insert b {c})
                                        (congrArg (insert b) (Finset.coe_singleton c))))))
                                (eq_self {a, b, c}));
                          have hmem := fun {y} h => Eq.symm hcoerce ▸ h;
                          have hnc :=
                            hnontri
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congr (congrArg Or (eq_self a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (congrArg (Or (a = b)) Set.mem_singleton_iff._simp_1)))
                                      (true_or (a = b ∨ a = c))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (b = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans (congr (congrArg Or (eq_self b)) Set.mem_singleton_iff._simp_1)
                                            (true_or (b = c)))))
                                      (or_true (b = a))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (c = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans
                                            (congrArg (Or (c = b)) (Eq.trans Set.mem_singleton_iff._simp_1 (eq_self c)))
                                            (or_true (c = b)))))
                                      (or_true (c = a))))))
                              hab hbc hac;
                          Eq.mpr (id (congrArg (fun _a => ConvexIndep _a) hcoerce))
                            (convexIndep_triple_of_not_collinear hab hac hbc hnc)⟩⟩)
                  (Eq.symm right) hpts hnontriN:ℕhN:N ∈ cardSet 3hlt:N < 3f:ℕ → ℝ² := fun i => EuclideanSpace.single 0 ↑i⊢ False
  let pts : Finset ℝ² := (Finset.range N).image fhmem3:3 ∈ cardSet 3 := 
  fun pts hpts hnontri =>
    Exists.casesOn (Finset.card_eq_three.mp hpts) fun a h =>
      Exists.casesOn h fun b h =>
        Exists.casesOn h fun c h =>
          And.casesOn h fun hab right =>
            And.casesOn right fun hac right =>
              And.casesOn right fun hbc right =>
                Eq.ndrec (motive := fun pts => pts.card = 3 → NonTrilinear ↑pts → HasConvexNGon 3 ↑pts)
                  (fun hpts hnontri =>
                    Exists.intro {a, b, c}
                      ⟨of_eq_true
                          (Eq.trans
                            (congrArg (fun x => x = 3)
                              (Eq.trans
                                (Finset.card_insert_of_notMem
                                  (of_eq_true
                                    (Eq.trans
                                      (congrArg Not
                                        (Eq.trans Finset.mem_insert._simp_1
                                          (Eq.trans
                                            (congr (congrArg Or (eq_false hab))
                                              (Eq.trans Finset.mem_singleton._simp_1 (eq_false hac)))
                                            (or_self False))))
                                      not_false_eq_true)))
                                (congrArg (fun x => x + 1)
                                  (Eq.trans
                                    (Finset.card_insert_of_notMem
                                      (of_eq_true
                                        (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false hbc)))
                                          not_false_eq_true)))
                                    (congrArg (fun x => x + 1) (Finset.card_singleton c))))))
                            (eq_self 3)),
                        ⟨subset_refl ↑{a, b, c},
                          have hcoerce :=
                            of_eq_true
                              (Eq.trans
                                (congrArg (fun x => x = {a, b, c})
                                  (Eq.trans (Finset.coe_insert a {b, c})
                                    (congrArg (insert a)
                                      (Eq.trans (Finset.coe_insert b {c})
                                        (congrArg (insert b) (Finset.coe_singleton c))))))
                                (eq_self {a, b, c}));
                          have hmem := fun {y} h => Eq.symm hcoerce ▸ h;
                          have hnc :=
                            hnontri
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congr (congrArg Or (eq_self a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (congrArg (Or (a = b)) Set.mem_singleton_iff._simp_1)))
                                      (true_or (a = b ∨ a = c))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (b = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans (congr (congrArg Or (eq_self b)) Set.mem_singleton_iff._simp_1)
                                            (true_or (b = c)))))
                                      (or_true (b = a))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (c = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans
                                            (congrArg (Or (c = b)) (Eq.trans Set.mem_singleton_iff._simp_1 (eq_self c)))
                                            (or_true (c = b)))))
                                      (or_true (c = a))))))
                              hab hbc hac;
                          Eq.mpr (id (congrArg (fun _a => ConvexIndep _a) hcoerce))
                            (convexIndep_triple_of_not_collinear hab hac hbc hnc)⟩⟩)
                  (Eq.symm right) hpts hnontriN:ℕhN:N ∈ cardSet 3hlt:N < 3f:ℕ → ℝ² := fun i => EuclideanSpace.single 0 ↑ipts:Finset ℝ² := Finset.image f (Finset.range N)⊢ False
  have hinj : Function.Injective f := fun i j hij => byhmem3:3 ∈ cardSet 3 := 
  fun pts hpts hnontri =>
    Exists.casesOn (Finset.card_eq_three.mp hpts) fun a h =>
      Exists.casesOn h fun b h =>
        Exists.casesOn h fun c h =>
          And.casesOn h fun hab right =>
            And.casesOn right fun hac right =>
              And.casesOn right fun hbc right =>
                Eq.ndrec (motive := fun pts => pts.card = 3 → NonTrilinear ↑pts → HasConvexNGon 3 ↑pts)
                  (fun hpts hnontri =>
                    Exists.intro {a, b, c}
                      ⟨of_eq_true
                          (Eq.trans
                            (congrArg (fun x => x = 3)
                              (Eq.trans
                                (Finset.card_insert_of_notMem
                                  (of_eq_true
                                    (Eq.trans
                                      (congrArg Not
                                        (Eq.trans Finset.mem_insert._simp_1
                                          (Eq.trans
                                            (congr (congrArg Or (eq_false hab))
                                              (Eq.trans Finset.mem_singleton._simp_1 (eq_false hac)))
                                            (or_self False))))
                                      not_false_eq_true)))
                                (congrArg (fun x => x + 1)
                                  (Eq.trans
                                    (Finset.card_insert_of_notMem
                                      (of_eq_true
                                        (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false hbc)))
                                          not_false_eq_true)))
                                    (congrArg (fun x => x + 1) (Finset.card_singleton c))))))
                            (eq_self 3)),
                        ⟨subset_refl ↑{a, b, c},
                          have hcoerce :=
                            of_eq_true
                              (Eq.trans
                                (congrArg (fun x => x = {a, b, c})
                                  (Eq.trans (Finset.coe_insert a {b, c})
                                    (congrArg (insert a)
                                      (Eq.trans (Finset.coe_insert b {c})
                                        (congrArg (insert b) (Finset.coe_singleton c))))))
                                (eq_self {a, b, c}));
                          have hmem := fun {y} h => Eq.symm hcoerce ▸ h;
                          have hnc :=
                            hnontri
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congr (congrArg Or (eq_self a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (congrArg (Or (a = b)) Set.mem_singleton_iff._simp_1)))
                                      (true_or (a = b ∨ a = c))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (b = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans (congr (congrArg Or (eq_self b)) Set.mem_singleton_iff._simp_1)
                                            (true_or (b = c)))))
                                      (or_true (b = a))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (c = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans
                                            (congrArg (Or (c = b)) (Eq.trans Set.mem_singleton_iff._simp_1 (eq_self c)))
                                            (or_true (c = b)))))
                                      (or_true (c = a))))))
                              hab hbc hac;
                          Eq.mpr (id (congrArg (fun _a => ConvexIndep _a) hcoerce))
                            (convexIndep_triple_of_not_collinear hab hac hbc hnc)⟩⟩)
                  (Eq.symm right) hpts hnontriN:ℕhN:N ∈ cardSet 3hlt:N < 3f:ℕ → ℝ² := fun i => EuclideanSpace.single 0 ↑ipts:Finset ℝ² := Finset.image f (Finset.range N)i:ℕj:ℕhij:f i = f j⊢ i = j
    have := congrArg (fun v : ℝ² => v 0) hijhmem3:3 ∈ cardSet 3 := 
  fun pts hpts hnontri =>
    Exists.casesOn (Finset.card_eq_three.mp hpts) fun a h =>
      Exists.casesOn h fun b h =>
        Exists.casesOn h fun c h =>
          And.casesOn h fun hab right =>
            And.casesOn right fun hac right =>
              And.casesOn right fun hbc right =>
                Eq.ndrec (motive := fun pts => pts.card = 3 → NonTrilinear ↑pts → HasConvexNGon 3 ↑pts)
                  (fun hpts hnontri =>
                    Exists.intro {a, b, c}
                      ⟨of_eq_true
                          (Eq.trans
                            (congrArg (fun x => x = 3)
                              (Eq.trans
                                (Finset.card_insert_of_notMem
                                  (of_eq_true
                                    (Eq.trans
                                      (congrArg Not
                                        (Eq.trans Finset.mem_insert._simp_1
                                          (Eq.trans
                                            (congr (congrArg Or (eq_false hab))
                                              (Eq.trans Finset.mem_singleton._simp_1 (eq_false hac)))
                                            (or_self False))))
                                      not_false_eq_true)))
                                (congrArg (fun x => x + 1)
                                  (Eq.trans
                                    (Finset.card_insert_of_notMem
                                      (of_eq_true
                                        (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false hbc)))
                                          not_false_eq_true)))
                                    (congrArg (fun x => x + 1) (Finset.card_singleton c))))))
                            (eq_self 3)),
                        ⟨subset_refl ↑{a, b, c},
                          have hcoerce :=
                            of_eq_true
                              (Eq.trans
                                (congrArg (fun x => x = {a, b, c})
                                  (Eq.trans (Finset.coe_insert a {b, c})
                                    (congrArg (insert a)
                                      (Eq.trans (Finset.coe_insert b {c})
                                        (congrArg (insert b) (Finset.coe_singleton c))))))
                                (eq_self {a, b, c}));
                          have hmem := fun {y} h => Eq.symm hcoerce ▸ h;
                          have hnc :=
                            hnontri
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congr (congrArg Or (eq_self a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (congrArg (Or (a = b)) Set.mem_singleton_iff._simp_1)))
                                      (true_or (a = b ∨ a = c))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (b = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans (congr (congrArg Or (eq_self b)) Set.mem_singleton_iff._simp_1)
                                            (true_or (b = c)))))
                                      (or_true (b = a))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (c = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans
                                            (congrArg (Or (c = b)) (Eq.trans Set.mem_singleton_iff._simp_1 (eq_self c)))
                                            (or_true (c = b)))))
                                      (or_true (c = a))))))
                              hab hbc hac;
                          Eq.mpr (id (congrArg (fun _a => ConvexIndep _a) hcoerce))
                            (convexIndep_triple_of_not_collinear hab hac hbc hnc)⟩⟩)
                  (Eq.symm right) hpts hnontriN:ℕhN:N ∈ cardSet 3hlt:N < 3f:ℕ → ℝ² := fun i => EuclideanSpace.single 0 ↑ipts:Finset ℝ² := Finset.image f (Finset.range N)i:ℕj:ℕhij:f i = f jthis:(fun v => v.ofLp 0) (f i) = (fun v => v.ofLp 0) (f j) := congrArg (fun v => v.ofLp 0) hij⊢ i = j; simpa [f] using thisAll goals completed! 🐙
  have hpts_card : pts.card = N := by⊢ f 3 = 3
    simp [pts, Finset.card_image_of_injOn hinj.injOn]All goals completed! 🐙
  have hnontri : NonTrilinear (pts : Set ℝ²) := by⊢ f 3 = 3
    apply Set.triplewise_of_encard_lthhmem3:3 ∈ cardSet 3 := 
  fun pts hpts hnontri =>
    Exists.casesOn (Finset.card_eq_three.mp hpts) fun a h =>
      Exists.casesOn h fun b h =>
        Exists.casesOn h fun c h =>
          And.casesOn h fun hab right =>
            And.casesOn right fun hac right =>
              And.casesOn right fun hbc right =>
                Eq.ndrec (motive := fun pts => pts.card = 3 → NonTrilinear ↑pts → HasConvexNGon 3 ↑pts)
                  (fun hpts hnontri =>
                    Exists.intro {a, b, c}
                      ⟨of_eq_true
                          (Eq.trans
                            (congrArg (fun x => x = 3)
                              (Eq.trans
                                (Finset.card_insert_of_notMem
                                  (of_eq_true
                                    (Eq.trans
                                      (congrArg Not
                                        (Eq.trans Finset.mem_insert._simp_1
                                          (Eq.trans
                                            (congr (congrArg Or (eq_false hab))
                                              (Eq.trans Finset.mem_singleton._simp_1 (eq_false hac)))
                                            (or_self False))))
                                      not_false_eq_true)))
                                (congrArg (fun x => x + 1)
                                  (Eq.trans
                                    (Finset.card_insert_of_notMem
                                      (of_eq_true
                                        (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false hbc)))
                                          not_false_eq_true)))
                                    (congrArg (fun x => x + 1) (Finset.card_singleton c))))))
                            (eq_self 3)),
                        ⟨subset_refl ↑{a, b, c},
                          have hcoerce :=
                            of_eq_true
                              (Eq.trans
                                (congrArg (fun x => x = {a, b, c})
                                  (Eq.trans (Finset.coe_insert a {b, c})
                                    (congrArg (insert a)
                                      (Eq.trans (Finset.coe_insert b {c})
                                        (congrArg (insert b) (Finset.coe_singleton c))))))
                                (eq_self {a, b, c}));
                          have hmem := fun {y} h => Eq.symm hcoerce ▸ h;
                          have hnc :=
                            hnontri
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congr (congrArg Or (eq_self a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (congrArg (Or (a = b)) Set.mem_singleton_iff._simp_1)))
                                      (true_or (a = b ∨ a = c))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (b = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans (congr (congrArg Or (eq_self b)) Set.mem_singleton_iff._simp_1)
                                            (true_or (b = c)))))
                                      (or_true (b = a))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (c = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans
                                            (congrArg (Or (c = b)) (Eq.trans Set.mem_singleton_iff._simp_1 (eq_self c)))
                                            (or_true (c = b)))))
                                      (or_true (c = a))))))
                              hab hbc hac;
                          Eq.mpr (id (congrArg (fun _a => ConvexIndep _a) hcoerce))
                            (convexIndep_triple_of_not_collinear hab hac hbc hnc)⟩⟩)
                  (Eq.symm right) hpts hnontriN:ℕhN:N ∈ cardSet 3hlt:N < 3f:ℕ → ℝ² := fun i => EuclideanSpace.single 0 ↑ipts:Finset ℝ² := Finset.image f (Finset.range N)hinj:Function.Injective f := 
  fun i j hij =>
    have this := congrArg (fun v => v.ofLp 0) hij;
    Eq.mp
      (Eq.trans
        (congr (congrArg Eq (Eq.trans (EuclideanSpace.single_apply 0 (↑i) 0) (ite_cond_eq_true (↑i) 0 (eq_self 0))))
          (Eq.trans (EuclideanSpace.single_apply 0 (↑j) 0) (ite_cond_eq_true (↑j) 0 (eq_self 0))))
        Nat.cast_inj._simp_1)
      thishpts_card:pts.card = N := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = N)
        (Eq.trans
          ((fun x_0 => (fun x_0 => Finset.card_image_of_injOn (Function.Injective.injOn hinj)) x_0) (Finset.range N))
          (Finset.card_range N)))
      (eq_self N))⊢ (↑pts).encard < 3
    rw [Set.encard_coe_eq_coe_finsetCard, hpts_card]hhmem3:3 ∈ cardSet 3 := 
  fun pts hpts hnontri =>
    Exists.casesOn (Finset.card_eq_three.mp hpts) fun a h =>
      Exists.casesOn h fun b h =>
        Exists.casesOn h fun c h =>
          And.casesOn h fun hab right =>
            And.casesOn right fun hac right =>
              And.casesOn right fun hbc right =>
                Eq.ndrec (motive := fun pts => pts.card = 3 → NonTrilinear ↑pts → HasConvexNGon 3 ↑pts)
                  (fun hpts hnontri =>
                    Exists.intro {a, b, c}
                      ⟨of_eq_true
                          (Eq.trans
                            (congrArg (fun x => x = 3)
                              (Eq.trans
                                (Finset.card_insert_of_notMem
                                  (of_eq_true
                                    (Eq.trans
                                      (congrArg Not
                                        (Eq.trans Finset.mem_insert._simp_1
                                          (Eq.trans
                                            (congr (congrArg Or (eq_false hab))
                                              (Eq.trans Finset.mem_singleton._simp_1 (eq_false hac)))
                                            (or_self False))))
                                      not_false_eq_true)))
                                (congrArg (fun x => x + 1)
                                  (Eq.trans
                                    (Finset.card_insert_of_notMem
                                      (of_eq_true
                                        (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false hbc)))
                                          not_false_eq_true)))
                                    (congrArg (fun x => x + 1) (Finset.card_singleton c))))))
                            (eq_self 3)),
                        ⟨subset_refl ↑{a, b, c},
                          have hcoerce :=
                            of_eq_true
                              (Eq.trans
                                (congrArg (fun x => x = {a, b, c})
                                  (Eq.trans (Finset.coe_insert a {b, c})
                                    (congrArg (insert a)
                                      (Eq.trans (Finset.coe_insert b {c})
                                        (congrArg (insert b) (Finset.coe_singleton c))))))
                                (eq_self {a, b, c}));
                          have hmem := fun {y} h => Eq.symm hcoerce ▸ h;
                          have hnc :=
                            hnontri
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congr (congrArg Or (eq_self a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (congrArg (Or (a = b)) Set.mem_singleton_iff._simp_1)))
                                      (true_or (a = b ∨ a = c))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (b = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans (congr (congrArg Or (eq_self b)) Set.mem_singleton_iff._simp_1)
                                            (true_or (b = c)))))
                                      (or_true (b = a))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (c = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans
                                            (congrArg (Or (c = b)) (Eq.trans Set.mem_singleton_iff._simp_1 (eq_self c)))
                                            (or_true (c = b)))))
                                      (or_true (c = a))))))
                              hab hbc hac;
                          Eq.mpr (id (congrArg (fun _a => ConvexIndep _a) hcoerce))
                            (convexIndep_triple_of_not_collinear hab hac hbc hnc)⟩⟩)
                  (Eq.symm right) hpts hnontriN:ℕhN:N ∈ cardSet 3hlt:N < 3f:ℕ → ℝ² := fun i => EuclideanSpace.single 0 ↑ipts:Finset ℝ² := Finset.image f (Finset.range N)hinj:Function.Injective f := 
  fun i j hij =>
    have this := congrArg (fun v => v.ofLp 0) hij;
    Eq.mp
      (Eq.trans
        (congr (congrArg Eq (Eq.trans (EuclideanSpace.single_apply 0 (↑i) 0) (ite_cond_eq_true (↑i) 0 (eq_self 0))))
          (Eq.trans (EuclideanSpace.single_apply 0 (↑j) 0) (ite_cond_eq_true (↑j) 0 (eq_self 0))))
        Nat.cast_inj._simp_1)
      thishpts_card:pts.card = N := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = N)
        (Eq.trans
          ((fun x_0 => (fun x_0 => Finset.card_image_of_injOn (Function.Injective.injOn hinj)) x_0) (Finset.range N))
          (Finset.card_range N)))
      (eq_self N))⊢ ↑N < 3
    exact_mod_cast hltAll goals completed! 🐙
  obtain ⟨S, hScard, hSsub, _⟩ := hN pts hpts_card hnontrihmem3:3 ∈ cardSet 3 := 
  fun pts hpts hnontri =>
    Exists.casesOn (Finset.card_eq_three.mp hpts) fun a h =>
      Exists.casesOn h fun b h =>
        Exists.casesOn h fun c h =>
          And.casesOn h fun hab right =>
            And.casesOn right fun hac right =>
              And.casesOn right fun hbc right =>
                Eq.ndrec (motive := fun pts => pts.card = 3 → NonTrilinear ↑pts → HasConvexNGon 3 ↑pts)
                  (fun hpts hnontri =>
                    Exists.intro {a, b, c}
                      ⟨of_eq_true
                          (Eq.trans
                            (congrArg (fun x => x = 3)
                              (Eq.trans
                                (Finset.card_insert_of_notMem
                                  (of_eq_true
                                    (Eq.trans
                                      (congrArg Not
                                        (Eq.trans Finset.mem_insert._simp_1
                                          (Eq.trans
                                            (congr (congrArg Or (eq_false hab))
                                              (Eq.trans Finset.mem_singleton._simp_1 (eq_false hac)))
                                            (or_self False))))
                                      not_false_eq_true)))
                                (congrArg (fun x => x + 1)
                                  (Eq.trans
                                    (Finset.card_insert_of_notMem
                                      (of_eq_true
                                        (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false hbc)))
                                          not_false_eq_true)))
                                    (congrArg (fun x => x + 1) (Finset.card_singleton c))))))
                            (eq_self 3)),
                        ⟨subset_refl ↑{a, b, c},
                          have hcoerce :=
                            of_eq_true
                              (Eq.trans
                                (congrArg (fun x => x = {a, b, c})
                                  (Eq.trans (Finset.coe_insert a {b, c})
                                    (congrArg (insert a)
                                      (Eq.trans (Finset.coe_insert b {c})
                                        (congrArg (insert b) (Finset.coe_singleton c))))))
                                (eq_self {a, b, c}));
                          have hmem := fun {y} h => Eq.symm hcoerce ▸ h;
                          have hnc :=
                            hnontri
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congr (congrArg Or (eq_self a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (congrArg (Or (a = b)) Set.mem_singleton_iff._simp_1)))
                                      (true_or (a = b ∨ a = c))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (b = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans (congr (congrArg Or (eq_self b)) Set.mem_singleton_iff._simp_1)
                                            (true_or (b = c)))))
                                      (or_true (b = a))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (c = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans
                                            (congrArg (Or (c = b)) (Eq.trans Set.mem_singleton_iff._simp_1 (eq_self c)))
                                            (or_true (c = b)))))
                                      (or_true (c = a))))))
                              hab hbc hac;
                          Eq.mpr (id (congrArg (fun _a => ConvexIndep _a) hcoerce))
                            (convexIndep_triple_of_not_collinear hab hac hbc hnc)⟩⟩)
                  (Eq.symm right) hpts hnontriN:ℕhN:N ∈ cardSet 3hlt:N < 3f:ℕ → ℝ² := fun i => EuclideanSpace.single 0 ↑ipts:Finset ℝ² := Finset.image f (Finset.range N)hinj:Function.Injective f := 
  fun i j hij =>
    have this := congrArg (fun v => v.ofLp 0) hij;
    Eq.mp
      (Eq.trans
        (congr (congrArg Eq (Eq.trans (EuclideanSpace.single_apply 0 (↑i) 0) (ite_cond_eq_true (↑i) 0 (eq_self 0))))
          (Eq.trans (EuclideanSpace.single_apply 0 (↑j) 0) (ite_cond_eq_true (↑j) 0 (eq_self 0))))
        Nat.cast_inj._simp_1)
      thishpts_card:pts.card = N := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = N)
        (Eq.trans
          ((fun x_0 => (fun x_0 => Finset.card_image_of_injOn (Function.Injective.injOn hinj)) x_0) (Finset.range N))
          (Finset.card_range N)))
      (eq_self N))hnontri:NonTrilinear ↑pts := 
  Set.triplewise_of_encard_lt (fun x y z => ¬Collinear ℝ {x, y, z})
    (Eq.mpr (id (congrArg (fun _a => _a < 3) (Set.encard_coe_eq_coe_finsetCard pts)))
      (Eq.mpr (id (congrArg (fun _a => ↑_a < 3) hpts_card)) (cast (Eq.symm Nat.cast_lt._simp_1) hlt)))S:Finset ℝ²hScard:S.card = 3hSsub:↑S ⊆ ↑ptsright✝:ConvexIndep ↑S⊢ False
  have : S.card ≤ pts.card := Finset.card_le_card (byhmem3:3 ∈ cardSet 3 := 
  fun pts hpts hnontri =>
    Exists.casesOn (Finset.card_eq_three.mp hpts) fun a h =>
      Exists.casesOn h fun b h =>
        Exists.casesOn h fun c h =>
          And.casesOn h fun hab right =>
            And.casesOn right fun hac right =>
              And.casesOn right fun hbc right =>
                Eq.ndrec (motive := fun pts => pts.card = 3 → NonTrilinear ↑pts → HasConvexNGon 3 ↑pts)
                  (fun hpts hnontri =>
                    Exists.intro {a, b, c}
                      ⟨of_eq_true
                          (Eq.trans
                            (congrArg (fun x => x = 3)
                              (Eq.trans
                                (Finset.card_insert_of_notMem
                                  (of_eq_true
                                    (Eq.trans
                                      (congrArg Not
                                        (Eq.trans Finset.mem_insert._simp_1
                                          (Eq.trans
                                            (congr (congrArg Or (eq_false hab))
                                              (Eq.trans Finset.mem_singleton._simp_1 (eq_false hac)))
                                            (or_self False))))
                                      not_false_eq_true)))
                                (congrArg (fun x => x + 1)
                                  (Eq.trans
                                    (Finset.card_insert_of_notMem
                                      (of_eq_true
                                        (Eq.trans (congrArg Not (Eq.trans Finset.mem_singleton._simp_1 (eq_false hbc)))
                                          not_false_eq_true)))
                                    (congrArg (fun x => x + 1) (Finset.card_singleton c))))))
                            (eq_self 3)),
                        ⟨subset_refl ↑{a, b, c},
                          have hcoerce :=
                            of_eq_true
                              (Eq.trans
                                (congrArg (fun x => x = {a, b, c})
                                  (Eq.trans (Finset.coe_insert a {b, c})
                                    (congrArg (insert a)
                                      (Eq.trans (Finset.coe_insert b {c})
                                        (congrArg (insert b) (Finset.coe_singleton c))))))
                                (eq_self {a, b, c}));
                          have hmem := fun {y} h => Eq.symm hcoerce ▸ h;
                          have hnc :=
                            hnontri
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congr (congrArg Or (eq_self a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (congrArg (Or (a = b)) Set.mem_singleton_iff._simp_1)))
                                      (true_or (a = b ∨ a = c))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (b = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans (congr (congrArg Or (eq_self b)) Set.mem_singleton_iff._simp_1)
                                            (true_or (b = c)))))
                                      (or_true (b = a))))))
                              (hmem
                                (of_eq_true
                                  (Eq.trans Set.mem_insert_iff._simp_1
                                    (Eq.trans
                                      (congrArg (Or (c = a))
                                        (Eq.trans Set.mem_insert_iff._simp_1
                                          (Eq.trans
                                            (congrArg (Or (c = b)) (Eq.trans Set.mem_singleton_iff._simp_1 (eq_self c)))
                                            (or_true (c = b)))))
                                      (or_true (c = a))))))
                              hab hbc hac;
                          Eq.mpr (id (congrArg (fun _a => ConvexIndep _a) hcoerce))
                            (convexIndep_triple_of_not_collinear hab hac hbc hnc)⟩⟩)
                  (Eq.symm right) hpts hnontriN:ℕhN:N ∈ cardSet 3hlt:N < 3f:ℕ → ℝ² := fun i => EuclideanSpace.single 0 ↑ipts:Finset ℝ² := Finset.image f (Finset.range N)hinj:Function.Injective f := 
  fun i j hij =>
    have this := congrArg (fun v => v.ofLp 0) hij;
    Eq.mp
      (Eq.trans
        (congr (congrArg Eq (Eq.trans (EuclideanSpace.single_apply 0 (↑i) 0) (ite_cond_eq_true (↑i) 0 (eq_self 0))))
          (Eq.trans (EuclideanSpace.single_apply 0 (↑j) 0) (ite_cond_eq_true (↑j) 0 (eq_self 0))))
        Nat.cast_inj._simp_1)
      thishpts_card:pts.card = N := 
  of_eq_true
    (Eq.trans
      (congrArg (fun x => x = N)
        (Eq.trans
          ((fun x_0 => (fun x_0 => Finset.card_image_of_injOn (Function.Injective.injOn hinj)) x_0) (Finset.range N))
          (Finset.card_range N)))
      (eq_self N))hnontri:NonTrilinear ↑pts := 
  Set.triplewise_of_encard_lt (fun x y z => ¬Collinear ℝ {x, y, z})
    (Eq.mpr (id (congrArg (fun _a => _a < 3) (Set.encard_coe_eq_coe_finsetCard pts)))
      (Eq.mpr (id (congrArg (fun _a => ↑_a < 3) hpts_card)) (cast (Eq.symm Nat.cast_lt._simp_1) hlt)))S:Finset ℝ²hScard:S.card = 3hSsub:↑S ⊆ ↑ptsright✝:ConvexIndep ↑S⊢ S ⊆ pts exact_mod_cast hSsubAll goals completed! 🐙)
  omegaAll goals completed! 🐙


namespace variants

Erdős and Szekeres proved the bounds $$ 2^{n-2} + 1 ≤ f(n) ≤ \binom{2n-4}{n-2} + 1 $$ ([ErSz60] and [ErSz35] respectively).

[ErSz60] Erdős, P. and Szekeres, G., On some extremum problems in elementary geometry. Ann. Univ. Sci. Budapest. Eötvös Sect. Math. (1960/61), 53-62.

[ErSz35] Erdős, P. and Szekeres, G., A combinatorial problem in geometry. Compos. Math. (1935), 463-470.

@[category research solved, AMS 52]
theorem declaration uses 'sorry'ersz_bounds :
    ∀ n ≥ 3, 2^(n - 2) + 1 ≤ f n ∧ f n ≤ Nat.choose (2 * n - 4) (n - 2) + 1 := by⊢ ∀ n ≥ 3, 2 ^ (n - 2) + 1 ≤ f n ∧ f n ≤ (2 * n - 4).choose (n - 2) + 1
  sorryAll goals completed! 🐙

Suk [Su17] proved $$ f(n) ≤ 2^{(1+o(1))n}. $$

[Su17] Suk, Andrew, On the Erdős-Szekeres convex polygon problem. J. Amer. Math. Soc. (2017), 1047-1053.

@[category research solved, AMS 52]
theorem declaration uses 'sorry'su_bound :
    ∃ r : ℕ → ℝ, r =o[atTop] (fun n => (n : ℝ)) ∧
      ∀ n ≥ 3, (f n : ℝ) ≤ 2^(n + r n) := by⊢ ∃ r, (r =o[atTop] fun n => ↑n) ∧ ∀ n ≥ 3, ↑(f n) ≤ 2 ^ (↑n + r n)
  sorryAll goals completed! 🐙

The current best bound is due to Holmsen, Mojarrad, Pach, and Tardos [HMPT20], who prove $$ f(n) ≤ 2^{n+O(\sqrt{n\log n})}. $$

[HMPT20] Holmsen, Andreas F. and Mojarrad, Hossein Nassajian and Pach, János and Tardos, Gábor, Two extensions of the Erdős-Szekeres problem. J. Eur. Math. Soc. (JEMS) (2020), 3981-3995.

@[category research solved, AMS 52]
theorem declaration uses 'sorry'hmpt_bound :
    ∃ r : ℕ → ℝ, r =O[atTop] (fun n => Real.sqrt (n * Real.log n)) ∧
      ∀ n ≥ 3, (f n : ℝ) ≤ 2^(n + r n) := by⊢ ∃ r, (r =O[atTop] fun n => √(↑n * Real.log ↑n)) ∧ ∀ n ≥ 3, ↑(f n) ≤ 2 ^ (↑n + r n)
  sorryAll goals completed! 🐙


end Erdos107.variants