Motivated by this question I'm looking for a pair of Baire topological spaces whose product is not Baire and whose construction does not need the axiom of choice.
The example of such spaces I'm familiar with, which is due to Cohen, is to consider $\Bbb P_{S_1}\times\Bbb P_{S_2}$, where $S_1,S_2\subseteq\omega_1$ are disjoint stationary subsets of $\omega_1$ and $\Bbb P_{S_i}$ is the usual $\sigma$-distributive forcing that adds to $\omega_1$ a club contained in $S_i$, but this construction needs some choice.
I'm not too familiar with other examples of Baire spaces which are not productively Baire, but those that I could find in the literature all seemed to need some form of choice. Is there a construction in $\mathsf{ZF}$ of two Baire spaces $X,Y$ such that $X\times Y$ is not Baire? Or at the opposite, is it consistent with $\mathsf{ZF}$ that every finite product of Baire spaces is Baire?