Documentation

Mathlib.Combinatorics.HalesJewett

The Hales-Jewett theorem #

We prove the Hales-Jewett theorem. We deduce Van der Waerden's theorem and the multidimensional Hales-Jewett theorem as corollaries.

The Hales-Jewett theorem is a result in Ramsey theory dealing with combinatorial lines. Given an 'alphabet' α : Type* and a b : α, an example of a combinatorial line in α^5 is { (a, x, x, b, x) | x : α }. See Combinatorics.Line for a precise general definition. The Hales-Jewett theorem states that for any fixed finite types α and κ, there exists a (potentially huge) finite type ι such that whenever ι → α is κ-colored (i.e. for any coloring C : (ι → α) → κ), there exists a monochromatic line. We prove the Hales-Jewett theorem using the idea of color focusing and a product argument. See the proof of Combinatorics.Line.exists_mono_in_high_dimension' for details.

Combinatorial subspaces are higher-dimensional analogues of combinatorial lines. See Combinatorics.Subspace. The multidimensional Hales-Jewett theorem generalises the statement above from combinatorial lines to combinatorial subspaces of a fixed dimension.

The version of Van der Waerden's theorem in this file states that whenever a commutative monoid M is finitely colored and S is a finite subset, there exists a monochromatic homothetic copy of S. This follows from the Hales-Jewett theorem by considering the map (ι → S) → M sending v to ∑ i : ι, v i, which sends a combinatorial line to a homothetic copy of S.

Main results #

Implementation details #

For convenience, we work directly with finite types instead of natural numbers. That is, we write α, ι, κ for (finite) types where one might traditionally use natural numbers n, H, c. This allows us to work directly with α, Option α, (ι → α) → κ, and ι ⊕ ι' instead of Fin n, Fin (n+1), Fin (c^(n^H)), and Fin (H + H').

TODO #

Tags #

combinatorial line, Ramsey theory, arithmetic progression

References #

theorem Combinatorics.Subspace.ext {η : Type u_5} {α : Type u_6} {ι : Type u_7} (x : Combinatorics.Subspace η α ι) (y : Combinatorics.Subspace η α ι) (idxFun : x.idxFun = y.idxFun) :
x = y
theorem Combinatorics.Subspace.ext_iff {η : Type u_5} {α : Type u_6} {ι : Type u_7} (x : Combinatorics.Subspace η α ι) (y : Combinatorics.Subspace η α ι) :
x = y x.idxFun = y.idxFun
structure Combinatorics.Subspace (η : Type u_5) (α : Type u_6) (ι : Type u_7) :
Type (max (max u_5 u_6) u_7)

The type of combinatorial subspaces. A subspace l : Subspace η α ι in the hypercube ι → α defines a function (η → α) → ι → α from η → α to the hypercube, such that for each coordinate i : ι and direction e : η, the function fun x ↦ l x i is either fun x ↦ x e for some direction e : η or constant. We require subspaces to be non-degenerate in the sense that, for every e : η, fun x ↦ l x i is fun x ↦ x e for at least one i.

Formally, a subspace is represented by a word l.idxFun : ι → α ⊕ η which says whether fun x ↦ l x i is fun x ↦ x e (corresponding to l.idxFun i = Sum.inr e) or constantly a (corresponding to l.idxFun i = Sum.inl a).

When α has size 1 there can be many elements of Subspace η α ι defining the same function.

  • idxFun : ια η

    The word representing a combinatorial subspace. l.idxfun i = Sum.inr e means that l x i = x e for all x and l.idxfun i = some a means that l x i = a for all x.

  • proper : ∀ (e : η), ∃ (i : ι), self.idxFun i = Sum.inr e

    We require combinatorial subspaces to be nontrivial in the sense that fun x ↦ l x i is fun x ↦ x e for at least one coordinate i.

Instances For
    theorem Combinatorics.Subspace.proper {η : Type u_5} {α : Type u_6} {ι : Type u_7} (self : Combinatorics.Subspace η α ι) (e : η) :
    ∃ (i : ι), self.idxFun i = Sum.inr e

    We require combinatorial subspaces to be nontrivial in the sense that fun x ↦ l x i is fun x ↦ x e for at least one coordinate i.

    The combinatorial subspace corresponding to the identity embedding (ι → α) → (ι → α).

    Equations
    • Combinatorics.Subspace.instInhabited = { default := { idxFun := Sum.inr, proper := } }
    def Combinatorics.Subspace.toFun {η : Type u_5} {α : Type u_6} {ι : Type u_7} (l : Combinatorics.Subspace η α ι) (x : ηα) (i : ι) :
    α

    Consider a subspace l : Subspace η α ι as a function (η → α) → ι → α.

    Equations
    Instances For
      instance Combinatorics.Subspace.instCoeFun {η : Type u_5} {α : Type u_6} {ι : Type u_7} :
      CoeFun (Combinatorics.Subspace η α ι) fun (x : Combinatorics.Subspace η α ι) => (ηα)ια
      Equations
      • Combinatorics.Subspace.instCoeFun = { coe := Combinatorics.Subspace.toFun }
      theorem Combinatorics.Subspace.coe_apply {η : Type u_5} {α : Type u_6} {ι : Type u_7} (l : Combinatorics.Subspace η α ι) (x : ηα) (i : ι) :
      l x i = Sum.elim id x (l.idxFun i)
      theorem Combinatorics.Subspace.coe_injective {η : Type u_5} {α : Type u_6} {ι : Type u_7} [Nontrivial α] :
      Function.Injective Combinatorics.Subspace.toFun
      theorem Combinatorics.Subspace.apply_def {η : Type u_5} {α : Type u_6} {ι : Type u_7} (l : Combinatorics.Subspace η α ι) (x : ηα) (i : ι) :
      l x i = Sum.elim id x (l.idxFun i)
      theorem Combinatorics.Subspace.apply_inl {η : Type u_5} {α : Type u_6} {ι : Type u_7} {l : Combinatorics.Subspace η α ι} {x : ηα} {i : ι} {a : α} (h : l.idxFun i = Sum.inl a) :
      l x i = a
      theorem Combinatorics.Subspace.apply_inr {η : Type u_5} {α : Type u_6} {ι : Type u_7} {l : Combinatorics.Subspace η α ι} {x : ηα} {i : ι} {e : η} (h : l.idxFun i = Sum.inr e) :
      l x i = x e
      def Combinatorics.Subspace.IsMono {η : Type u_5} {α : Type u_6} {ι : Type u_7} {κ : Type u_8} (C : (ια)κ) (l : Combinatorics.Subspace η α ι) :

      Given a coloring C of ι → α and a combinatorial subspace l of ι → α, l.IsMono C means that l is monochromatic with regard to C.

      Equations
      Instances For
        def Combinatorics.Subspace.reindex {η : Type u_5} {α : Type u_6} {ι : Type u_7} {η' : Type u_9} {α' : Type u_10} {ι' : Type u_11} (l : Combinatorics.Subspace η α ι) (eη : η η') (eα : α α') (eι : ι ι') :

        Change the index types of a subspace.

        Equations
        • l.reindex = { idxFun := fun (i : ι') => Sum.map () () (l.idxFun (.symm i)), proper := }
        Instances For
          @[simp]
          theorem Combinatorics.Subspace.reindex_apply {η : Type u_5} {α : Type u_6} {ι : Type u_7} {η' : Type u_9} {α' : Type u_10} {ι' : Type u_11} (l : Combinatorics.Subspace η α ι) (eη : η η') (eα : α α') (eι : ι ι') (x : η'α') (i : ι') :
          (l.reindex ) x i = (l (.symm x ) (.symm i))
          @[simp]
          theorem Combinatorics.Subspace.reindex_isMono {η : Type u_5} {α : Type u_6} {ι : Type u_7} {κ : Type u_8} {l : Combinatorics.Subspace η α ι} {η' : Type u_9} {α' : Type u_10} {ι' : Type u_11} {eη : η η'} {eα : α α'} {eι : ι ι'} {C : (ι'α')κ} :
          Combinatorics.Subspace.IsMono C (l.reindex ) Combinatorics.Subspace.IsMono (fun (x : ια) => C ( x .symm)) l
          theorem Combinatorics.Subspace.IsMono.reindex {η : Type u_5} {α : Type u_6} {ι : Type u_7} {κ : Type u_8} {l : Combinatorics.Subspace η α ι} {η' : Type u_9} {α' : Type u_10} {ι' : Type u_11} {eη : η η'} {eα : α α'} {eι : ι ι'} {C : (ια)κ} (hl : Combinatorics.Subspace.IsMono C l) :
          Combinatorics.Subspace.IsMono (fun (x : ι'α') => C (.symm x )) (l.reindex )
          theorem Combinatorics.Line.ext_iff {α : Type u_5} {ι : Type u_6} (x : Combinatorics.Line α ι) (y : Combinatorics.Line α ι) :
          x = y x.idxFun = y.idxFun
          theorem Combinatorics.Line.ext {α : Type u_5} {ι : Type u_6} (x : Combinatorics.Line α ι) (y : Combinatorics.Line α ι) (idxFun : x.idxFun = y.idxFun) :
          x = y
          structure Combinatorics.Line (α : Type u_5) (ι : Type u_6) :
          Type (max u_5 u_6)

          The type of combinatorial lines. A line l : Line α ι in the hypercube ι → α defines a function α → ι → α from α to the hypercube, such that for each coordinate i : ι, the function fun x ↦ l x i is either id or constant. We require lines to be nontrivial in the sense that fun x ↦ l x i is id for at least one i.

          Formally, a line is represented by a word l.idxFun : ι → Option α which says whether fun x ↦ l x i is id (corresponding to l.idxFun i = none) or constantly y (corresponding to l.idxFun i = some y).

          When α has size 1 there can be many elements of Line α ι defining the same function.

          • idxFun : ιOption α

            The word representing a combinatorial line. l.idxfun i = none means that l x i = x for all x and l.idxfun i = some y means that l x i = y.

          • proper : ∃ (i : ι), self.idxFun i = none

            We require combinatorial lines to be nontrivial in the sense that fun x ↦ l x i is id for at least one coordinate i.

          Instances For
            theorem Combinatorics.Line.proper {α : Type u_5} {ι : Type u_6} (self : Combinatorics.Line α ι) :
            ∃ (i : ι), self.idxFun i = none

            We require combinatorial lines to be nontrivial in the sense that fun x ↦ l x i is id for at least one coordinate i.

            def Combinatorics.Line.toFun {α : Type u_2} {ι : Type u_3} (l : Combinatorics.Line α ι) (x : α) (i : ι) :
            α

            Consider a line l : Line α ι as a function α → ι → α.

            Equations
            • l x i = (l.idxFun i).getD x
            Instances For
              instance Combinatorics.Line.instCoeFun {α : Type u_2} {ι : Type u_3} :
              CoeFun (Combinatorics.Line α ι) fun (x : Combinatorics.Line α ι) => αια
              Equations
              • Combinatorics.Line.instCoeFun = { coe := fun (l : Combinatorics.Line α ι) (x : α) (i : ι) => (l.idxFun i).getD x }
              theorem Combinatorics.Line.coe_apply {α : Type u_2} {ι : Type u_3} (l : Combinatorics.Line α ι) (x : α) (i : ι) :
              (fun (x : α) (i : ι) => (l.idxFun i).getD x) x i = (l.idxFun i).getD x
              theorem Combinatorics.Line.coe_injective {α : Type u_2} {ι : Type u_3} [Nontrivial α] :
              Function.Injective fun (x : Combinatorics.Line α ι) (x_1 : α) (i : ι) => (x.idxFun i).getD x_1
              def Combinatorics.Line.IsMono {α : Type u_5} {ι : Type u_6} {κ : Sort u_7} (C : (ια)κ) (l : Combinatorics.Line α ι) :

              A line is monochromatic if all its points are the same color.

              Equations
              Instances For

                Consider a line as a one-dimensional subspace.

                Equations
                • l.toSubspaceUnit = { idxFun := fun (i : ι) => (l.idxFun i).elim (Sum.inr ()) Sum.inl, proper := }
                Instances For
                  @[simp]
                  theorem Combinatorics.Line.toSubspaceUnit_apply {α : Type u_2} {ι : Type u_3} (l : Combinatorics.Line α ι) (a : Unitα) :
                  l.toSubspaceUnit a = (fun (x : α) (i : ι) => (l.idxFun i).getD x) (a ())
                  @[simp]
                  theorem Combinatorics.Line.toSubspaceUnit_isMono {α : Type u_2} {ι : Type u_3} {κ : Type u_4} {l : Combinatorics.Line α ι} {C : (ια)κ} :
                  theorem Combinatorics.Line.IsMono.toSubspaceUnit {α : Type u_2} {ι : Type u_3} {κ : Type u_4} {l : Combinatorics.Line α ι} {C : (ια)κ} :

                  Alias of the reverse direction of Combinatorics.Line.toSubspaceUnit_isMono.

                  def Combinatorics.Line.toSubspace {η : Type u_1} {α : Type u_2} {ι : Type u_3} (l : Combinatorics.Line (ηα) ι) :

                  Consider a line in ι → η → α as a η-dimensional subspace in ι × η → α.

                  Equations
                  • l.toSubspace = { idxFun := fun (ie : ι × η) => (l.idxFun ie.1).elim (Sum.inr ie.2) fun (f : ηα) => Sum.inl (f ie.2), proper := }
                  Instances For
                    @[simp]
                    theorem Combinatorics.Line.toSubspace_apply {η : Type u_1} {α : Type u_2} {ι : Type u_3} (l : Combinatorics.Line (ηα) ι) (a : ηα) (ie : ι × η) :
                    l.toSubspace a ie = (fun (x : ηα) (i : ι) => (l.idxFun i).getD x) a ie.1 ie.2
                    @[simp]
                    theorem Combinatorics.Line.toSubspace_isMono {η : Type u_1} {α : Type u_2} {ι : Type u_3} {κ : Type u_4} {l : Combinatorics.Line (ηα) ι} {C : (ι × ηα)κ} :
                    Combinatorics.Subspace.IsMono C l.toSubspace Combinatorics.Line.IsMono (fun (x : ιηα) => C fun (x_1 : ι × η) => match x_1 with | (i, e) => x i e) l
                    theorem Combinatorics.Line.IsMono.toSubspace {η : Type u_1} {α : Type u_2} {ι : Type u_3} {κ : Type u_4} {l : Combinatorics.Line (ηα) ι} {C : (ι × ηα)κ} :
                    Combinatorics.Line.IsMono (fun (x : ιηα) => C fun (x_1 : ι × η) => match x_1 with | (i, e) => x i e) lCombinatorics.Subspace.IsMono C l.toSubspace

                    Alias of the reverse direction of Combinatorics.Line.toSubspace_isMono.

                    def Combinatorics.Line.diagonal (α : Type u_5) (ι : Type u_6) [Nonempty ι] :

                    The diagonal line. It is the identity at every coordinate.

                    Equations
                    Instances For
                      structure Combinatorics.Line.AlmostMono {α : Type u_5} {ι : Type u_6} {κ : Type u_7} (C : (ιOption α)κ) :
                      Type (max (max u_5 u_6) u_7)

                      The type of lines that are only one color except possibly at their endpoints.

                      • line : Combinatorics.Line (Option α) ι

                        The underlying line of an almost monochromatic line, where the coordinate dimension α is extended by an additional symbol none, thought to be marking the endpoint of the line.

                      • color : κ

                        The main color of an almost monochromatic line.

                      • has_color : ∀ (x : α), C ((fun (x : Option α) (i : ι) => (self.line.idxFun i).getD x) (some x)) = self.color

                        The proposition that the underlying line of an almost monochromatic line assumes its main color except possibly at the endpoints.

                      Instances For
                        theorem Combinatorics.Line.AlmostMono.has_color {α : Type u_5} {ι : Type u_6} {κ : Type u_7} {C : (ιOption α)κ} (self : Combinatorics.Line.AlmostMono C) (x : α) :
                        C ((fun (x : Option α) (i : ι) => (self.line.idxFun i).getD x) (some x)) = self.color

                        The proposition that the underlying line of an almost monochromatic line assumes its main color except possibly at the endpoints.

                        instance Combinatorics.Line.instInhabitedAlmostMonoDefaultOfNonempty {α : Type u_5} {ι : Type u_6} {κ : Type u_7} [Nonempty ι] [Inhabited κ] :
                        Inhabited (Combinatorics.Line.AlmostMono fun (x : ιOption α) => default)
                        Equations
                        • Combinatorics.Line.instInhabitedAlmostMonoDefaultOfNonempty = { default := { line := default, color := default, has_color := } }
                        structure Combinatorics.Line.ColorFocused {α : Type u_5} {ι : Type u_6} {κ : Type u_7} (C : (ιOption α)κ) :
                        Type (max (max u_5 u_6) u_7)

                        The type of collections of lines such that

                        • each line is only one color except possibly at its endpoint
                        • the lines all have the same endpoint
                        • the colors of the lines are distinct. Used in the proof exists_mono_in_high_dimension.
                        • The underlying multiset of almost monochromatic lines of a color-focused collection.

                        • focus : ιOption α

                          The common endpoint of the lines in the color-focused collection.

                        • is_focused : pself.lines, (fun (x : Option α) (i : ι) => (p.line.idxFun i).getD x) none = self.focus

                          The proposition that all lines in a color-focused collection have the same endpoint.

                        • distinct_colors : (Multiset.map Combinatorics.Line.AlmostMono.color self.lines).Nodup

                          The proposition that all lines in a color-focused collection of lines have distinct colors.

                        Instances For
                          theorem Combinatorics.Line.ColorFocused.is_focused {α : Type u_5} {ι : Type u_6} {κ : Type u_7} {C : (ιOption α)κ} (self : Combinatorics.Line.ColorFocused C) (p : Combinatorics.Line.AlmostMono C) :
                          p self.lines(fun (x : Option α) (i : ι) => (p.line.idxFun i).getD x) none = self.focus

                          The proposition that all lines in a color-focused collection have the same endpoint.

                          theorem Combinatorics.Line.ColorFocused.distinct_colors {α : Type u_5} {ι : Type u_6} {κ : Type u_7} {C : (ιOption α)κ} (self : Combinatorics.Line.ColorFocused C) :
                          (Multiset.map Combinatorics.Line.AlmostMono.color self.lines).Nodup

                          The proposition that all lines in a color-focused collection of lines have distinct colors.

                          instance Combinatorics.Line.instInhabitedColorFocused {α : Type u_5} {ι : Type u_6} {κ : Type u_7} (C : (ιOption α)κ) :
                          Equations
                          def Combinatorics.Line.map {α : Type u_5} {α' : Type u_6} {ι : Type u_7} (f : αα') (l : Combinatorics.Line α ι) :

                          A function f : α → α' determines a function line α ι → line α' ι. For a coordinate i l.map f is the identity at i if l is, and constantly f y if l is constantly y at i.

                          Equations
                          Instances For
                            def Combinatorics.Line.vertical {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (v : ια) (l : Combinatorics.Line α ι') :

                            A point in ι → α and a line in ι' → α determine a line in ι ⊕ ι' → α.

                            Equations
                            Instances For
                              def Combinatorics.Line.horizontal {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (l : Combinatorics.Line α ι) (v : ι'α) :

                              A line in ι → α and a point in ι' → α determine a line in ι ⊕ ι' → α.

                              Equations
                              • l.horizontal v = { idxFun := Sum.elim l.idxFun (some v), proper := }
                              Instances For
                                def Combinatorics.Line.prod {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (l : Combinatorics.Line α ι) (l' : Combinatorics.Line α ι') :

                                One line in ι → α and one in ι' → α together determine a line in ι ⊕ ι' → α.

                                Equations
                                • l.prod l' = { idxFun := Sum.elim l.idxFun l'.idxFun, proper := }
                                Instances For
                                  theorem Combinatorics.Line.apply_def {α : Type u_2} {ι : Type u_3} (l : Combinatorics.Line α ι) (x : α) :
                                  (fun (x : α) (i : ι) => (l.idxFun i).getD x) x = fun (i : ι) => (l.idxFun i).getD x
                                  theorem Combinatorics.Line.apply_none {α : Type u_5} {ι : Type u_6} (l : Combinatorics.Line α ι) (x : α) (i : ι) (h : l.idxFun i = none) :
                                  (fun (x : α) (i : ι) => (l.idxFun i).getD x) x i = x
                                  theorem Combinatorics.Line.apply_some {α : Type u_2} {ι : Type u_3} {l : Combinatorics.Line α ι} {i : ι} {a : α} {x : α} (h : l.idxFun i = some a) :
                                  (fun (x : α) (i : ι) => (l.idxFun i).getD x) x i = a
                                  @[simp]
                                  theorem Combinatorics.Line.map_apply {α : Type u_5} {α' : Type u_6} {ι : Type u_7} (f : αα') (l : Combinatorics.Line α ι) (x : α) :
                                  (fun (x : α') (i : ι) => ((Combinatorics.Line.map f l).idxFun i).getD x) (f x) = f (fun (x : α) (i : ι) => (l.idxFun i).getD x) x
                                  @[simp]
                                  theorem Combinatorics.Line.vertical_apply {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (v : ια) (l : Combinatorics.Line α ι') (x : α) :
                                  (fun (x : α) (i : ι ι') => ((Combinatorics.Line.vertical v l).idxFun i).getD x) x = Sum.elim v ((fun (x : α) (i : ι') => (l.idxFun i).getD x) x)
                                  @[simp]
                                  theorem Combinatorics.Line.horizontal_apply {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (l : Combinatorics.Line α ι) (v : ι'α) (x : α) :
                                  (fun (x : α) (i : ι ι') => ((l.horizontal v).idxFun i).getD x) x = Sum.elim ((fun (x : α) (i : ι) => (l.idxFun i).getD x) x) v
                                  @[simp]
                                  theorem Combinatorics.Line.prod_apply {α : Type u_5} {ι : Type u_6} {ι' : Type u_7} (l : Combinatorics.Line α ι) (l' : Combinatorics.Line α ι') (x : α) :
                                  (fun (x : α) (i : ι ι') => ((l.prod l').idxFun i).getD x) x = Sum.elim ((fun (x : α) (i : ι) => (l.idxFun i).getD x) x) ((fun (x : α) (i : ι') => (l'.idxFun i).getD x) x)
                                  @[simp]
                                  theorem Combinatorics.Line.diagonal_apply {α : Type u_5} {ι : Type u_6} [Nonempty ι] (x : α) :
                                  (fun (x : α) (i : ι) => ((Combinatorics.Line.diagonal α ι).idxFun i).getD x) x = fun (x_1 : ι) => x
                                  theorem Combinatorics.Line.exists_mono_in_high_dimension (α : Type u) [Finite α] (κ : Type v) [Finite κ] :
                                  ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ια)κ), ∃ (l : Combinatorics.Line α ι), Combinatorics.Line.IsMono C l

                                  The Hales-Jewett theorem: For any finite types α and κ, there exists a finite type ι such that whenever the hypercube ι → α is κ-colored, there is a monochromatic combinatorial line.

                                  theorem Combinatorics.exists_mono_homothetic_copy {M : Type u_5} {κ : Type u_6} [AddCommMonoid M] (S : Finset M) [Finite κ] (C : Mκ) :
                                  a > 0, ∃ (b : M) (c : κ), sS, C (a s + b) = c

                                  A generalization of Van der Waerden's theorem: if M is a finitely colored commutative monoid, and S is a finite subset, then there exists a monochromatic homothetic copy of S.

                                  theorem Combinatorics.Subspace.exists_mono_in_high_dimension (α : Type u_5) (κ : Type u_6) (η : Type u_7) [Fintype α] [Fintype κ] [Fintype η] :
                                  ∃ (ι : Type) (x : Fintype ι), ∀ (C : (ια)κ), ∃ (l : Combinatorics.Subspace η α ι), Combinatorics.Subspace.IsMono C l

                                  The multidimensional Hales-Jewett theorem, aka extended Hales-Jewett theorem: For any finite types η, α and κ, there exists a finite type ι such that whenever the hypercube ι → α is κ-colored, there is a monochromatic combinatorial subspace of dimension η.

                                  theorem Combinatorics.Subspace.exists_mono_in_high_dimension_fin (α : Type u_5) (κ : Type u_6) (η : Type u_7) [Fintype α] [Fintype κ] [Fintype η] :
                                  ∃ (n : ), ∀ (C : (Fin nα)κ), ∃ (l : Combinatorics.Subspace η α (Fin n)), Combinatorics.Subspace.IsMono C l

                                  A variant of the extended Hales-Jewett theorem exists_mono_in_high_dimension where the returned type is some Fin n instead of a general fintype.