Grace/Cumulus/Combinatorics/ErdosSzekeres.g17

Open in Workbench Download source

Imports

RamseyPigeonhole · Lattice.Linear · Nat.Least

Declarations

Source

1-- The Erdős–Szekeres theorem: a sequence of m·n + 1 distinct points of a2-- linear order has an increasing subsequence of length m + 1 or a3-- decreasing one of length n + 1. Each index carries the length of the4-- longest increasing run and of the longest decreasing run ending there;5-- a later larger term lengthens the first label and a later smaller term6-- the second, so the label pairs are distinct, and there are only m·n of7-- them.8-- Part of Cumulus, the Grace17 mathematics library.9-- Copyright (c) 2026 Grant Passmore.10-- Released under the Apache License 2.0. See LICENSE in the repository root.11-- Authors: Grant Passmore1213module Grace.Cumulus.Combinatorics.ErdosSzekeres14import RamseyPigeonhole15import Lattice.Linear16import Nat.Least1718-- f increases, or decreases, along the index set S.19predicate IncreasingOn (P f S : Set) :=20  ∀ i ∈ S, ∀ j ∈ S, i < j → Le(P, f(i), f(j))2122predicate DecreasingOn (P f S : Set) :=23  ∀ i ∈ S, ∀ j ∈ S, i < j → Le(P, f(j), f(i))2425theorem Le.transitive_linear (P a b c : Set)26  requires order : LinearOrder(P)27  requires ha : a ∈ points(P)28  requires hb : b ∈ points(P)29  requires hc : c ∈ points(P)30  requires hab : Le(P, a, b)31  requires hbc : Le(P, b, c)32  shows Le(P, a, c)33proof34  have partial := LinearOrder.partial_order with order35  have preorder := PartialOrder.preorder_of with partial36  exact le_trans with *3738-- Decreasing along S is increasing in the dual order.39theorem DecreasingOn.dual (P f S : Set)40  requires values : ∀ i ∈ S, f(i) ∈ points(P)41  shows IncreasingOn(dual(P), f, S) ↔ DecreasingOn(P, f, S)42proof43  constructor44  . intros increasing i hi j hj ij45    have step := increasing with i, hi, j, hj, ij46    have related := Le.relates with step47    rw dual.le at related48    exact Le.of_relates with (converse.reflects with related)49  . intros decreasing i hi j hj ij50    have step := decreasing with i, hi, j, hj, ij51    have related := Le.relates with step52    have forward := converse.relates with53      (values with j, hj), (values with i, hi), related54    apply Le.of_relates55    rw dual.le56    exact forward5758-- A finite set has a subset of every smaller size.59theorem Finite.subset_of_size (k : Nat)60  shows ∀ A, Finite(A) → k ≤ cardinality(A) →61    ∃ T, T ⊆ A ∧ HasCardinality(T, k)62proof63  induction k64  | zero =>65    intros A finite le66    exact ⟨∅, empty.subset at A, HasCardinality.empty_set⟩67  | j + 1 using ih =>68    intros A finite le69    have natA := cardinality.nat with finite70    have jLe : j ≤ cardinality(A) by arith71    obtain ⟨T, subset, counted⟩ := ih with A, finite, jLe72    have sizeT := cardinality.eq_of_has with counted73    have fresh : ∃ a ∈ A, ¬a ∈ T74      by_contra none75      have cover : A ⊆ T76        intros a ha77        by_contra outside78        apply none79        exact ⟨a, ha, outside⟩80      have equal := Subset.antisymmetric with subset, cover81      rw [← equal, sizeT] at le82      arith83    obtain ⟨a, ha, outside⟩ := fresh84    have one : j + 1 = succ(j) := add.right_one with *85    have inserted := HasCardinality.insert_fresh with counted, outside86    rw ← one at inserted87    refine ⟨insert(a, T), ?_, inserted⟩88    intros x hx89    have split := insert.membership.forward with hx90    cases split with same | inT91    . rw same92      exact ha93    . exact subset with x, inT9495-- The greatest member of a nonempty finite set of naturals.9697def naturalBounds (S : Set) : Set := { b ∈ ℕ | S ⊆ succ(b) }9899-- A least bound of a nonempty set of naturals belongs to the set.100theorem naturalBounds.least_member (S u : Set)101  requires inhabited : Nonempty(S)102  requires bound : u ∈ naturalBounds(S)103  requires least : ∀ k ∈ naturalBounds(S), u ≤ k104  shows u ∈ S105proof106  obtain ⟨uOmega, uBound⟩ := naturalBounds.membership.forward with bound107  have uNat := nat.omega.backward with uOmega108  by_contra absent109  have below : S ⊆ u110    intros x hx111    have inNext := uBound with x, hx112    have split := membership.successor_forward{n := u} with inNext113    cases split with before | same114    . exact before115    . exfalso116      apply absent117      rw ← same118      exact hx119  have alternatives := natural.zero_or_successor at u120  cases alternatives with zero | successor121  . obtain ⟨x, hx⟩ := inhabited122    have inZero := below with x, hx123    rw [zero, nat.zero] at inZero124    exact set.empty with inZero125  . obtain ⟨k, kNat, shape⟩ := successor126    rw shape at below127    have kBound : k ∈ naturalBounds(S)128      apply naturalBounds.membership.backward129      exact ⟨nat.omega.forward with kNat, below⟩130    have le := least with k, kBound131    rw shape at le132    arith133134theorem Finite.greatest_natural (S : Set)135  requires inhabited : Nonempty(S)136  requires naturals : S ⊆ ℕ137  requires finite : Finite(S)138  shows ∃ n ∈ ℕ, n ∈ S ∧ S ⊆ succ(n)139proof140  obtain ⟨b, bNat, bounded⟩ := Finite.naturals_bounded with naturals, finite141  have bBound : b ∈ naturalBounds(S)142    apply naturalBounds.membership.backward143    have within : S ⊆ succ(b)144      intros y hy145      exact bounded with y, hy146    exact ⟨nat.omega.forward with bNat, within⟩147  have boundsInhabited : Nonempty(naturalBounds(S)) := ⟨b, bBound⟩148  have boundsNatural : naturalBounds(S) ⊆ ℕ149    intros x hx150    have parts := naturalBounds.membership.forward with hx151    exact parts.left152  have least := leastNatural.member with boundsInhabited, boundsNatural153  have minimal : ∀ k ∈ naturalBounds(S), leastNatural(naturalBounds(S)) ≤ k154    intros k hk155    have kNat := nat.omega.backward with (boundsNatural with k, hk)156    exact leastNatural.least with boundsInhabited, boundsNatural, hk157  have parts := naturalBounds.membership.forward with least158  have member := naturalBounds.least_member with inhabited, least, minimal159  refine ⟨leastNatural(naturalBounds(S)), parts.left, member, ?_⟩160  exact parts.right161162defunique greatestNatural (S : Set) (n ∈ ℕ) := n ∈ S ∧ S ⊆ succ(n)163requires inhabited : Nonempty(S)164requires naturals : S ⊆ ℕ165requires finite : Finite(S)166proof167  exact Finite.greatest_natural with inhabited, naturals, finite168uniqueness169  intros u hu first v hv second170  have uNat := nat.omega.backward with hu171  have vNat := nat.omega.backward with hv172  have uBelow : u ∈ succ(v) := second.right with u, first.left173  have vBelow : v ∈ succ(u) := first.right with v, second.left174  have uLess := Less.of_membership at u, succ(v)175  have vLess := Less.of_membership at v, succ(u)176  have uLe := Less.successor_upper with (uLess with uBelow)177  have vLe := Less.successor_upper with (vLess with vBelow)178  exact LessEqual.antisymmetric with uLe, vLe179180theorem greatestNatural.member (S : Set)181  requires inhabited : Nonempty(S)182  requires naturals : S ⊆ ℕ183  requires finite : Finite(S)184  shows greatestNatural(S) ∈ S185proof186  have selected := greatestNatural.selected at S with *187  exact selected.right.left188189theorem greatestNatural.greatest (S : Set, m : Nat)190  requires inhabited : Nonempty(S)191  requires naturals : S ⊆ ℕ192  requires finite : Finite(S)193  requires member : m ∈ S194  shows m ≤ greatestNatural(S)195proof196  have selected := greatestNatural.selected at S with *197  have natural := nat.omega.backward with selected.left198  have below : m ∈ succ(greatestNatural(S)) :=199    selected.right.right with m, member200  have less := Less.of_membership at m, succ(greatestNatural(S))201  exact Less.successor_upper with (less with below)202203-- The sizes of the index sets inside i + 1 that end at i and along which204-- f increases; the longest of them is the first label of i.205206def riseLengths (P f : Set, i : Nat) : Set :=207  { L ∈ ℕ | ∃ S ∈ 𝒫(i + 1),208      i ∈ S ∧ IncreasingOn(P, f, S) ∧ cardinality(S) = L }209210theorem riseLengths.naturals (P f : Set, i : Nat)211  shows riseLengths(P, f, i) ⊆ ℕ212proof213  intros L hL214  have parts := riseLengths.membership.forward with hL215  exact parts.left216217theorem IncreasingOn.singleton (P f : Set, i : Nat)218  shows IncreasingOn(P, f, {i})219proof220  intros x hx y hy xy221  have sameX := singleton.membership.forward with hx222  have sameY := singleton.membership.forward with hy223  rw [sameX, sameY] at xy224  exfalso225  exact Less.irreflexive at i with xy226227theorem riseLengths.one (P f : Set, i : Nat)228  shows 1 ∈ riseLengths(P, f, i)229proof230  apply riseLengths.membership.backward231  have oneNatural : Nat(1) by typecheck232  have oneOmega := nat.omega.forward with oneNatural233  have one : i + 1 = succ(i) := add.right_one with *234  have inPower : {i} ∈ 𝒫(i + 1)235    apply powerset.membership_iff.backward236    intros x hx237    have same := singleton.membership.forward with hx238    rw [same, one]239    exact membership.self_successor at i with *240  have increasing := IncreasingOn.singleton at P, f, i241  have size := cardinality.singleton at i242  refine ⟨oneOmega, {i}, inPower, singleton.self at i, increasing, size⟩243244theorem riseLengths.bounded (P f : Set, i : Nat)245  shows riseLengths(P, f, i) ⊆ succ(i + 1)246proof247  intros L hL248  obtain ⟨LOmega, S, inPower, hiS, increasing, size⟩ :=249    riseLengths.membership.forward with hL250  have LNat := nat.omega.backward with LOmega251  have subset := powerset.membership_iff.forward with inPower252  have bound := cardinality.monotone with (Finite.natural at i + 1), subset253  rw [size, cardinality.natural] at bound254  have succNat : Nat(succ(i + 1)) by typecheck255  have less : L < succ(i + 1) by arith256  have bridge := membership.of_Less at L, succ(i + 1) with LNat, succNat257  exact bridge with less258259theorem riseLengths.finite (P f : Set, i : Nat)260  shows Finite(riseLengths(P, f, i))261proof262  exact Finite.subset with (Finite.natural at succ(i + 1)),263    (riseLengths.bounded at P, f, i)264265theorem riseLengths.nonempty (P f : Set, i : Nat)266  shows Nonempty(riseLengths(P, f, i))267proof268  have one := riseLengths.one at P, f, i269  exact ⟨1, one⟩270271def rise (P f : Set, i : Nat) : Set := greatestNatural(riseLengths(P, f, i))272273theorem rise.value (P f : Set, i : Nat)274  shows rise(P, f, i) = greatestNatural(riseLengths(P, f, i))275proof276  simp [rise]277278theorem rise.member (P f : Set, i : Nat)279  shows rise(P, f, i) ∈ riseLengths(P, f, i)280proof281  rw rise.value282  exact greatestNatural.member with (riseLengths.nonempty at P, f, i),283    (riseLengths.naturals at P, f, i), (riseLengths.finite at P, f, i)284285theorem rise.natural (P f : Set, i : Nat)286  shows Nat(rise(P, f, i))287proof288  have parts := riseLengths.membership.forward with (rise.member at P, f, i)289  exact nat.omega.backward with parts.left290291theorem rise.witness (P f : Set, i : Nat)292  shows ∃ S ∈ 𝒫(i + 1), i ∈ S ∧ IncreasingOn(P, f, S) ∧293    cardinality(S) = rise(P, f, i)294proof295  have parts := riseLengths.membership.forward with (rise.member at P, f, i)296  exact parts.right297298theorem rise.greatest (P f : Set, i L : Nat)299  requires member : L ∈ riseLengths(P, f, i)300  shows L ≤ rise(P, f, i)301proof302  rw rise.value303  exact greatestNatural.greatest with (riseLengths.nonempty at P, f, i),304    (riseLengths.naturals at P, f, i), (riseLengths.finite at P, f, i), member305306theorem rise.positive (P f : Set, i : Nat)307  shows 1 ≤ rise(P, f, i)308proof309  exact rise.greatest with (riseLengths.one at P, f, i)310311-- A later, larger term extends every run ending at i: the label grows.312theorem rise.step (P f : Set, N i j : Nat)313  requires order : LinearOrder(P)314  requires function : f : N → points(P)315  requires hi : i ∈ N316  requires hj : j ∈ N317  requires below : i < j318  requires le : Le(P, f(i), f(j))319  shows rise(P, f, i) < rise(P, f, j)320proof321  obtain ⟨S, inPower, hiS, increasing, size⟩ := rise.witness at P, f, i322  have subset := powerset.membership_iff.forward with inPower323  have finiteS := Finite.subset with (Finite.natural at i + 1), subset324  have one : i + 1 = succ(i) := add.right_one with *325  have oneJ : j + 1 = succ(j) := add.right_one with *326  have NNat : Nat(N) by typecheck327  have succNat : Nat(succ(j)) by typecheck328  have indexNat : ∀ x ∈ S, Nat(x)329    intros x hx330    have inNext := subset with x, hx331    rw one at inNext332    exact natural.member at succ(i) with x, inNext333  have indexLe : ∀ x ∈ S, x ≤ i334    intros x hx335    have inNext := subset with x, hx336    rw one at inNext337    have xNat := indexNat with x, hx338    have less := Less.of_membership at x, succ(i)339    exact Less.successor_upper with (less with inNext)340  have indexIn : ∀ x ∈ S, x ∈ N341    intros x hx342    have xNat := indexNat with x, hx343    have xLe := indexLe with x, hx344    have xLess : x < N345      have jLess := Less.of_membership at j, N346      have jBelow := jLess with hj347      arith348    have bridge := membership.of_Less at x, N with xNat, NNat349    exact bridge with xLess350  have fresh : ¬j ∈ S351    intro inS352    have jLe := indexLe with j, inS353    arith354  have count := cardinality.insert_add_one with finiteS, fresh355  rw size at count356  have inPowerJ : insert(j, S) ∈ 𝒫(j + 1)357    apply powerset.membership_iff.backward358    intros x hx359    have split := insert.membership.forward with hx360    rw oneJ361    cases split with same | inS362    . rw same363      exact membership.self_successor at j with *364    . have xNat := indexNat with x, inS365      have xLe := indexLe with x, inS366      have xLess : x < succ(j) by arith367      have bridge := membership.of_Less at x, succ(j) with xNat, succNat368      exact bridge with xLess369  have fiIn := FunctionBetween.apply_closed with function, hi370  have fjIn := FunctionBetween.apply_closed with function, hj371  have increasingJ : IncreasingOn(P, f, insert(j, S))372    intros x hx y hy xy373    have splitX := insert.membership.forward with hx374    have splitY := insert.membership.forward with hy375    cases splitX with xIsJ | xInS376    . exfalso377      cases splitY with yIsJ | yInS378      . rw [xIsJ, yIsJ] at xy379        exact Less.irreflexive at j with xy380      . have yNat := indexNat with y, yInS381        have yLe := indexLe with y, yInS382        rw xIsJ at xy383        arith384    . cases splitY with yIsJ | yInS385      . rw yIsJ386        have xNat := indexNat with x, xInS387        have fxIn := FunctionBetween.apply_closed with function,388          (indexIn with x, xInS)389        have alternatives : x = i ∨ x ≠ i by tauto390        cases alternatives with same | different391        . rw same392          exact le393        . have xLe := indexLe with x, xInS394          have xLess := Less.of_LessEqual_ne with xLe, different395          have first := increasing with x, xInS, i, hiS, xLess396          exact Le.transitive_linear with order, fxIn, fiIn, fjIn, first, le397      . exact increasing with x, xInS, y, yInS, xy398  have finiteJ := Finite.insert at S, j with finiteS399  have natCount := cardinality.nat with finiteJ400  have inLengths : cardinality(insert(j, S)) ∈ riseLengths(P, f, j)401    apply riseLengths.membership.backward402    have countOmega := nat.omega.forward with natCount403    have jIn := insert.self at j, S404    refine ⟨countOmega, insert(j, S), inPowerJ, jIn, increasingJ, rfl⟩405  have bound := rise.greatest with inLengths406  rw count at bound407  have riseNat := rise.natural at P, f, i408  have riseNatJ := rise.natural at P, f, j409  arith410411-- Without an increasing run of length m + 1 inside N, every label is at412-- most m.413theorem rise.bounded (P f : Set, N i m : Nat)414  requires hi : i ∈ N415  requires none : ¬∃ S ∈ subsetsOfSize(N, m + 1), IncreasingOn(P, f, S)416  shows rise(P, f, i) ≤ m417proof418  by_contra above419  have riseNat := rise.natural at P, f, i420  have more : m + 1 ≤ rise(P, f, i)421    have less := Less.of_not_LessEqual with above422    exact Less.gap.forward with less423  obtain ⟨S, inPower, hiS, increasing, size⟩ := rise.witness at P, f, i424  have subset := powerset.membership_iff.forward with inPower425  have finiteS := Finite.subset with (Finite.natural at i + 1), subset426  rw ← size at more427  have all := Finite.subset_of_size at m + 1428  obtain ⟨T, inS, counted⟩ := all with S, finiteS, more429  apply none430  have inN : T ⊆ N431    have iLess := Less.of_membership at i, N432    have le : i + 1 ≤ N := Less.gap.forward with (iLess with hi)433    have nested := natural.subset_of_LessEqual at i + 1, N with le434    exact Subset.transitive with inS, (Subset.transitive with subset, nested)435  have member := subsetsOfSize.of_subset with inN, counted436  refine ⟨T, member, ?_⟩437  intros x hx y hy xy438  exact increasing with x, (inS with x, hx), y, (inS with y, hy), xy439440-- The labels 1, …, m.441442def positives (m : Nat) : Set := (m + 1) ∖ {0}443444theorem positives.membership (x : Set, m : Nat)445  shows x ∈ positives(m) ↔ x ∈ m + 1 ∧ x ≠ 0446proof447  simp [positives, difference.singleton_membership]448449theorem positives.of_bounds (x m : Nat)450  requires lower : 1 ≤ x451  requires upper : x ≤ m452  shows x ∈ positives(m)453proof454  apply positives.membership.backward455  have one : m + 1 = succ(m) := add.right_one with *456  have succNat : Nat(succ(m)) by typecheck457  constructor458  . rw one459    have less : x < succ(m) by arith460    have bridge := membership.of_Less at x, succ(m) with assumption, succNat461    exact bridge with less462  . intro zero463    rw zero at lower464    arith465466theorem positives.finite (m : Nat)467  shows Finite(positives(m))468proof469  unfold positives470  exact Finite.subset with (Finite.natural at m + 1),471    (difference.subset_left at m + 1, {0})472473theorem positives.count (m : Nat)474  shows cardinality(positives(m)) = m475proof476  have one : m + 1 = succ(m) := add.right_one with *477  have zeroNat : Nat(0) by typecheck478  have succNat : Nat(succ(m)) by typecheck479  have zeroIn : 0 ∈ m + 1480    rw one481    have less : 0 < succ(m) by arith482    have bridge := membership.of_Less at 0, succ(m) with zeroNat, succNat483    exact bridge with less484  have removed := cardinality.remove with (Finite.natural at m + 1), zeroIn485  rw [cardinality.natural, one] at removed486  have equal := Naturals.injective.succ with removed487  simp [positives]488489-- The pair of labels of an index: the longest increasing run and the490-- longest decreasing run ending there, the latter as a run of the dual491-- order. Without long runs both labels lie in 1, …, m and 1, …, n.492defgraph runLabel (P f : Set, m n : Nat) (i ∈ m * n + 1) :493    positives(m) × positives(n) :=494  (rise(P, f, i), rise(dual(P), f, i))495requires function : f : m * n + 1 → points(P)496requires noRise : ¬∃ S ∈ subsetsOfSize(m * n + 1, m + 1),497  IncreasingOn(P, f, S)498requires noFall : ¬∃ S ∈ subsetsOfSize(m * n + 1, n + 1),499  DecreasingOn(P, f, S)500proof501  have iNat := natural.member at m * n + 1 with i, member502  have noRiseDual : ¬∃ S ∈ subsetsOfSize(m * n + 1, n + 1),503      IncreasingOn(dual(P), f, S)504    intro some505    obtain ⟨S, hS, increasing⟩ := some506    apply noFall507    refine ⟨S, hS, ?_⟩508    have subset := subsetsOfSize.subset with hS509    have values : ∀ x ∈ S, f(x) ∈ points(P)510      intros x hx511      exact FunctionBetween.apply_closed with function, (subset with x, hx)512    have iff := DecreasingOn.dual with values513    exact iff.forward with increasing514  have riseLe := rise.bounded at P, f, m * n + 1, i, m with member, noRise515  have fallLe := rise.bounded at dual(P), f, m * n + 1, i, n with516    member, noRiseDual517  have riseNat := rise.natural at P, f, i518  have fallNat := rise.natural at dual(P), f, i519  apply product.pair520  . exact positives.of_bounds with (rise.positive at P, f, i), riseLe521  . exact positives.of_bounds with (rise.positive at dual(P), f, i), fallLe522523-- The Erdős–Szekeres theorem.524theorem erdos_szekeres (P f : Set) (m n : Nat)525  requires order : LinearOrder(P)526  requires distinct : InjectiveBetween(f, m * n + 1, points(P))527  shows (∃ S ∈ subsetsOfSize(m * n + 1, m + 1), IncreasingOn(P, f, S)) ∨528    (∃ S ∈ subsetsOfSize(m * n + 1, n + 1), DecreasingOn(P, f, S))529proof530  by_contra neither531  have noRise : ¬∃ S ∈ subsetsOfSize(m * n + 1, m + 1),532      IncreasingOn(P, f, S)533    intro some534    apply neither535    left536    exact some537  have noFall : ¬∃ S ∈ subsetsOfSize(m * n + 1, n + 1),538      DecreasingOn(P, f, S)539    intro some540    apply neither541    right542    exact some543  have function := Injective.function with distinct544  have labels := runLabel.function at P, f, m, n with function, noRise, noFall545  have dualOrder := LinearOrder.dual with order546  have dualFunction : f : m * n + 1 → points(dual(P))547    rw dual.points548    exact function549  have injective : InjectiveBetween(runLabel(P, f, m, n), m * n + 1,550      positives(m) × positives(n))551    apply Injective.of_pointwise with labels552    intros i hi j hj same553    have valueI := runLabel.value at P, f, m, n, i with554      function, noRise, noFall, hi555    have valueJ := runLabel.value at P, f, m, n, j with556      function, noRise, noFall, hj557    rw [valueI, valueJ] at same558    have coordinates := orderedPair.injective with same559    have iNat := natural.member at m * n + 1 with i, hi560    have jNat := natural.member at m * n + 1 with j, hj561    have fiIn := FunctionBetween.apply_closed with function, hi562    have fjIn := FunctionBetween.apply_closed with function, hj563    have riseNatI := rise.natural at P, f, i564    have riseNatJ := rise.natural at P, f, j565    have fallNatI := rise.natural at dual(P), f, i566    have fallNatJ := rise.natural at dual(P), f, j567    have dualOf : ∀ x ∈ points(P), ∀ y ∈ points(P), Le(P, y, x) →568        Le(dual(P), x, y)569      intros x hx y hy le570      apply Le.of_relates571      rw dual.le572      exact converse.relates with hy, hx, (Le.relates with le)573    by_contra different574    have separated := Injective.apply_ne with distinct, hi, hj, different575    have total : Le(P, f(i), f(j)) ∨ Le(P, f(j), f(i)) := le_total with *576    have alternatives := Less.trichotomy at i, j with *577    rcases alternatives with below | equal | above578    . cases total with forward | backward579      . have step := rise.step at P, f, m * n + 1, i, j with580          order, function, hi, hj, below, forward581        rw coordinates.left at step582        exact Less.irreflexive at rise(P, f, j) with step583      . have dualLe := dualOf with f(i), fiIn, f(j), fjIn, backward584        have step := rise.step at dual(P), f, m * n + 1, i, j with585          dualOrder, dualFunction, hi, hj, below, dualLe586        rw coordinates.right at step587        exact Less.irreflexive at rise(dual(P), f, j) with step588    . exact different with equal589    . cases total with forward | backward590      . have dualLe := dualOf with f(j), fjIn, f(i), fiIn, forward591        have step := rise.step at dual(P), f, m * n + 1, j, i with592          dualOrder, dualFunction, hj, hi, above, dualLe593        rw coordinates.right at step594        exact Less.irreflexive at rise(dual(P), f, j) with step595      . have step := rise.step at P, f, m * n + 1, j, i with596          order, function, hj, hi, above, backward597        rw coordinates.left at step598        exact Less.irreflexive at rise(P, f, j) with step599  have finiteLabels := Finite.product with (positives.finite at m),600    (positives.finite at n)601  have more : cardinality(positives(m) × positives(n)) < cardinality(m * n + 1)602    have count := cardinality.product_count with (positives.finite at m),603      (positives.finite at n)604    rw [count, positives.count, positives.count, cardinality.natural]605    arith606  exact pigeonhole.not_injective with labels, finiteLabels, more, injective607