Does $|X|^m\cdot n^{|X|}\le (n+m)^{|X|}$ hold without choice? As we learned in this question, provably in $\mathsf{ZF}$, if $X$ is infinite then $|X|^n\le(n+1)^{|X|}$ for any natural number $n$, and this is optimal in the sense that, in general, $n+1$ cannot be replaced with $n$.
A naïve inductive attempt to show the inequality suggests that perhaps we can actually prove that $|X|\cdot n^{|X|}\le(n+1)^{|X|}$, although this ends up being not quite as easy as I had initially hoped for.

Suppose $n,m,k$ are natural numbers with $n>0$, and $X$ is an infinite set. Does $$k\cdot|X|^m\cdot n^{|X|}\le(n+m)^{|X|},$$ provably in $\mathsf{ZF}$?

I would expect that the method in the question referenced above (and its answer) should establish this, and in fact that this is optimal for $X$ strictly amorphous.
 A: The answer to your question is yes, in $\sf{ZF}$ we can prove that $k\cdot |X|^m\cdot n^{|X|}\leq (n+m)^{|X|}$, albeit with an exception: if we simultaneously have $k>1$ and $n>0$ and $m=0$, then our claim is unprovable
over $\sf{ZF}$. We'll return to the exceptions at the end, but for now we'll prove the claim while assuming $m>0$. We begin by constructing an injection $(k\times X^m\times n^{|X|})\to (k\times m^m\times n^m)\times (n+m)^{X}$, defined by sending the triplet $(t,f,p)\mapsto (t,g,h,q)$ where $g,h,q$ are defined as follows.
$$\begin{align}
q(x)&=\begin{cases} p(x) &: x\notin f[m] \\
n+\min\{j<m : f(j)=x\} &: x\in f[m]
\end{cases} \\
h(j)&=p(f(j)) \\
g(j)&=\min\{j<m : f(j)=x\}
\end{align}$$
To prove this map is an injection, we show that we can recover $(t,f,p)$ using only $(t,g,h,q)$. First we recover $f$ via $f(j)=q^{-1}(n+g(j))$. Despite that $q$ is not injective, this still works since we have $q(x)=n+g(j)$ if and only if $x=f(j)$. Indeed, if $x=f(j)$ then $q(x)=n+g(j)$ by definition of $q$, and conversely if $q(x)=n+g(j)$ then $q(x)\geq n$ so that $x\in f[m]$ and also $f(j)=f(g(j))=x$. After recovering $f$ it's easy to recover $p$, since we have $p(x)=q(x)$ whenever $x\notin f[m]$, and for $x\in f[m]$ we have $p(x)=h(j)$ for any $j<m$ obeying $f(j)=x$. The recoverability of $t$ is trivial, so we have an inverse map $(t,g,h,q)\mapsto (t,f,p)$, proving that our original map is injective. Letting $M=k\times m^m\times n^m$ and $b=(t,g,h)\in M$, we have an injection $k\times X^m\times n^X \to M\times (n+m)^X$ defined by $(t,f,p)\mapsto (b,q)$. This is useful, since $M$ is finite and doesn't depend on $(t,f,p)$.
The above strategy can be improved to remove the factor of $M$. To do this, first select $N\in\omega$ large enough so that $|M|\cdot n^{N+2}\leq (n+m)^N$. The existence of such $N$ follows from the assumption that $m>0$, since this implies the limit $(1+\frac{m}{n})^N \to \infty$ as $N\to\infty$, thus all sufficiently large $N$ will have $|M|\cdot n^2 \leq (1+\frac{m}{n})^N$ and consequently $|M|\cdot n^{N+2}\leq (n+m)^N$. Once we've selected such $N$, we then find an injection $\iota : (m+1)\times (N+2)\to X$, which is possible since $X$ is infinite. Now for each $j<m+1$, we define $B_j=\{\iota(j,i) : i<N\}$ and define $I_j=\{\iota(j,i) : N\leq i<N+2\}$. These $B_j$ and $I_j$ are all pairwise disjoint subsets of $X$, and they generally obey $|B_j|=N$ and $|I_j|=2$. Recall that $N$ was selected so that $|M|\cdot n^{N+2}\leq (n+m)^N$, thus for each $j<m+1$ we can find an injection $\alpha_j:M\times n^{(B_j\cup I_j)}\to (n+m)^{B_j}$. Using the same $(t,f,p)$ and $(b,q)$ defined previously, we finally define $r\in (n+m)^X$ as follows.
$$J:=\min\{j<m+1 : \forall(x\in I_j\cup B_j), q(x)<n\}$$
$$r(x):=\begin{cases} q(x) &: x\notin (I_J\cup B_J) \\ 
n &: x\in I_J \\
\alpha_J(b, q\restriction_{(I_J\cup B_J)})(x) &: x\in B_J\end{cases}$$
The selection of $J$ works because $|\{x\in X : q(x)\geq n\}|=|f[m]|\leq m$, so there must exist at least one $j<m+1$ for which all $x\in B_j\cup I_j$ have $q(x)\leq n$. By selecting $J$ in this way, the application of $\alpha_J$ works precisely because the restriction $q\restriction_{I_J\cup B_J}$ has codomain $n$, so $r$ is well defined. Taking the map $(t,f,p)\mapsto r$ gives us a function $k\times X^m\times n^X\to (n+m)^X$, and we prove our claim by showing that this map is injective. To do this, first we recover $J<m+1$ as the unique value which satisfies $r[I_j]=\{n\}$. This works because each $|I_j|=2$, meanwhile $q(x)=n$ for at most one $x$. Once we've recovered $J$, we then recover $(b, q\restriction_{(B_J\cup I_J)})=\alpha_J^{-1}(r\restriction_{B_J})$, which works because $\alpha_J$ is injective, so we recover the restriction $q\restriction_{(B_J\cup I_J)}$. Finally, we recover $q(x)=r(x)$ for $x\notin (B_J\cup I_J)$, and otherwise $q(x)=q\restriction_{(B_J\cup I_J)}(x)$. Because we can recover $(b,q)$ from $r$, and we know we can recover $(t,f,p)$ using only $(b,q)$, then our map $(t,f,p)\mapsto r$ is injective.
The intuition behind the strategy $(t,f,p)\mapsto (t,g,h,q)$ is that we assign each $x\in f[m]$ a unique numerical tag $q(x)$. This numbering can be used to convert the function $f:m\to X$ into a function $g:m\to m$. For all those $x\notin f[m]$, we can also use $q$ to preserve the information about $p(x)$, but we can't do this for $x\in f[m]$ since we're using that space already. That lost information about $p$ takes the form of a function $f[n]\to n$, but our numerical tags can convert this into a function $h:m\to n$, so no information is lost. This injection is inefficient because $|\{x\in X : q(x)\geq n\}|\leq m$, so despite the fact that the codomain is all of $n+m$, most values of $x$ will only have $q(x)<n$. This inefficiency is exploited to get our injection $(b,q)\mapsto r$. The intuition behind the improvement is that we select a block $B_J$ on which $q$ encodes information inefficiently, and we get $r$ by overwriting that section of $q$ with some additional information (about $b$). The indicator $I_J$ tells us where to look to recover that extra information, and the injection $\alpha_J$ tells us how to write that information on top of the old information, without also corrupting the old information.

As above, we've proven $k\cdot |X|^m\cdot n^{|X|}\leq (n+m)^{|X|}$ for all infinte $X$ and all $k,m,n\in\omega$ so long as $m>0$. Ignoring the trivial cases where either $n=0$ or $k=0$, this solution is moreover optimal, we cannot replace $n+m$ with $n+m-1$. Indeed, as proven in this answer to the question you linked, we can prove $|X|^{n-1}\leq n^{|X|}$ and thus $|X|^{m+n-1}\leq k\cdot |X|^m\cdot n^{|X|}$, but we cannot prove $|X|^{m+n-1}\leq (n+m-1)^{|X|}$, so we also cannot prove $k\cdot |X|^m\cdot n^{|X|}\leq (m+n-1)^{|X|}$.
Focusing on the case where $m=0$ now, our claim is equivalent to $k\cdot n^{|X|}\leq n^{|X|}$. In case $k=0$ or $k=1$, this is trivially true, and likewise it's trivially true when $n=0$. The remaining cases have $k>1$ and $n>0$ and $m=0$, which we asserted in our introduction would be unprovable cases. The case where $n=1$ is trivially false, since then $k\cdot n^{|X|}=k>1=n^{|X|}$. Finally in the case $n>1$, our claim logically implies $2\cdot n^{|X|}\leq n^{|X|}$, and thus it implies $n^X$ is dedekind infinite. This is unprovable over $\sf{ZF}$ however, and in particular it's false whenever $X$ is an amorphous set.
Theorem: If $X$ is an amorphous set, and $n\in\omega$, then $n^X$ is dedekind finite.
proof: Suppose we have a sequence $\{p_j\}_{j\in\omega}$ of functions $p_j:X\to n$. As proven in lemma 2 of the previously linked answer, there's a finite set $D(p_j)\subseteq X$ outside of which $p_j(x)=L(p_j)$ is constant. Proven as the second lemma to this other answer, we know that $[X]^{<\omega}$ is dedekind finite, so the sequence $\{D(p_j)\}_{j\in\omega}$ must have finite image. It follows that the union $Y=\bigcup\{D(p_j) : j\in\omega\}$ is a finite union of finite sets, which is finite. Now though, the set $\{p_j : j\in\omega\}$ has a natural injection to the set $n\times n^Y$ defined by $p_j\mapsto (L(p_j), p\restriction_Y)$. Since the set $n\times n^Y$ is finite, then our $p_j$ sequence had finite image, proving that $n^X$ is dedekind finite. $\Box$
