The boundary and horn product has a finite horn attachment

Description of the complement. Put $S=(\mathrm{\partial }\mathrm{\Delta }[m]\times \mathrm{\Delta }[n])\cup (\mathrm{\Delta }[m]\times {\mathrm{\Lambda }}^k[n])$, so the target of the pushout product is $\mathrm{\Delta }[m]\times \mathrm{\Delta }[n]$ and $S$ is its subcomplex generated by the boundary in the first factor and the horn in the second. A nondegenerate chain $(i_0,j_0)<\cdots <(i_r,j_r)$ lies outside $S$ exactly when its first-coordinate image is all of $\{0,\dots ,m\}$ and its second-coordinate image contains every $0\le j\le n$ except possibly $k$; in particular, for $k<n$ it contains a vertex of second coordinate $k+1$, and for $k=n$ it contains a vertex of second coordinate $n-1$.

Pivot matching for $k<n$. In an outside chain let $(a,k+1)$ be the first vertex above second coordinate $k$. If the pivot $(a,k)$ is present, remove it; if it is absent, insert it immediately before $(a,k+1)$. The insertion keeps the chain strictly increasing, because every preceding vertex has second coordinate $\le k$ and first coordinate $\le a$, and the following vertex is $(a,k+1)$; it creates no duplicate by the assumption that the pivot is absent. Removal preserves the required projection values, because $(a,k+1)$ still supplies the first coordinate $a$ and $k$ is not a required second-coordinate value. The anchor $(a,k+1)$ and hence $a$ are unchanged. This pairs every outside chain uniquely with a lower chain $\sigma$ (without the pivot) and an upper chain $\tau$ (with the pivot), so the subcomplex generated by $S$ and the $\tau$'s is obtained from $S$ by attaching each $\tau$ along the horn omitting its pivot-deletion face $\sigma$.

Pivot matching for $k=n$. Use the last vertex below $n$, necessarily $(a,n-1)$, and insert or remove the pivot $(a,n)$ immediately after it; the same arguments as step 2.1 give a unique lower/upper pairing.

Attachment order. Order the pairs: for $k<n$ by increasing dimension of $\tau$ and then by decreasing $a$; for $k=n$ by increasing dimension and then increasing $a$. Finitely many pairs occur, since $[m]\times [n]$ is finite. Attach the simplex $\tau$ along the horn omitting its pivot-deletion face $\sigma$. Every other codimension-one face of $\tau$ is already present: a face losing a required projection value is in $S$; deleting a vertex other than pivot or anchor retains both and yields the upper simplex of a pair of smaller dimension; deleting the anchor either loses its required second-coordinate value (landing in $S$) or moves the anchor to a strictly larger first coordinate for $k<n$, respectively strictly smaller for $k=n$, and then the face lacks the new pivot and is the lower face of a pair of the same upper dimension but earlier in the chosen order.

The omitted face is new. The face $\sigma$ lies outside $S$ and is a lower, not an upper, simplex. A smaller-dimensional upper simplex cannot contain it; an upper simplex of the same dimension containing it either is $\tau$ itself (if the inserted vertex is its own pivot) or has an anchor moved in the direction that makes it later in the order. Higher-dimensional upper simplices occur later by dimension. Therefore each attachment adds exactly $\sigma$ and $\tau$ with all other faces already present, which is precisely a pushout of a horn inclusion ${\mathrm{\Lambda }}^p[\dim \tau ]\subset \mathrm{\Delta }[\dim \tau ]$; induction over the finitely many pairs attaches all outside chains and proves that the pushout product is anodyne.

General monomorphisms and products. A simplicial monomorphism $K\to L$ has a skeletal cell decomposition obtained by attaching simplices along their boundaries (the boundary-cell construction), and the simplicial product preserves colimits in each variable; hence $(K\to L)\mathrm{\square }({\mathrm{\Lambda }}^k[n]\to \mathrm{\Delta }[n])$ is a composite of pushouts of the cases just proved and is anodyne. The argument is symmetric in the two factors. Finally, the pushout product of two monomorphisms is a monomorphism because in each degree it is the inclusion $(K\times L^{\mathrm{\prime }})\cup (L\times K^{\mathrm{\prime }})\subseteq L\times L^{\mathrm{\prime }}$ of a union inside a product of sets. No Kan-Quillen model axiom or general weak-equivalence theorem is invoked; AC is used only for the arbitrary cell and lift choices in the general monomorphism case.