The mathematical content is the ported $Lax14Proofs.TupleCore.tupleRamseyAtSize$. That development first proves Ramsey for strict-monotone tuples by the Erdős–Rado chain-building induction on the arity: for arity $m + 1$ one repeatedly extracts the minimum $v$ of the current set, applies the arity-$m$ statement to the colouring $b ↦ c (v ::ᵥ b)$ on the rest, and thereby colours the elements of a long chain by the colour their tuples receive; a pigeonhole on that colouring of elements produces the homogeneous set. An arbitrary tuple is then factored as $a = e ∘ σ$ with $σ : Fin ℓ → Fin m$ surjective (its rank pattern, determined by the order type) and $e$ strict-monotone, and the strict-monotone statement is applied once per shape $(m, σ)$ — a finite type — shrinking the set each time. The resulting set is homogeneous for every shape at once, so the colour of a tuple is read off its shape alone.

Two bridges lead from there to the submitted statement. The ground set is taken to be all of $Fin n$, so the ported hypothesis $Nfin ≤ S.card$ becomes $Nfin ≤ n$ and the returned $Finset$ is coerced to a $Set$ with $Set.ncard_coe_finset$. And the ported statement concludes with a function $f$ from $Ordering$-valued order types to colours through which the colouring factors, while the submitted statement says instead that tuples with equal $Prop$-valued order types get equal colours. The lemma $otp_eq_of_orderType_eq$ closes that gap in the direction needed: if the strict-order patterns of two tuples agree then so do their $Ordering$-valued patterns, because in a linear order $a i = a j$ holds exactly when neither $a i < a j$ nor $a j < a i$ does. Both colours are then rewritten through $f$ and coincide.

The submitted statement carries no positivity hypothesis on the number of colours, whereas the ported one needs one to have a default colour available. The case $k = 0$ is split off first and closed outright: with $N := 1$ the carrier $Fin n$ is nonempty, so the assumed colouring applied to the constant tuple produces an element of $Fin 0$, which is absurd.

The proof is ported from the proof package of the submission Monadic dependence and neighborhood complexity ($Lax5Proofs/TupleRamsey.lean$). The theorem is due to Erdős and Rado, Combinatorial theorems on classifications of subsets of a given set (Proc. London Math. Soc. 1952); the order-type formulation followed here is the one of Mählmann, Monadically stable and monadically dependent graph classes (PhD thesis, TU Wien 2024), Section 4.