Assuming countable choice, refuted: Lindelöfness is productive

For an open cover $\mathcal{U}$ of $S$, let $\mathcal{D}$ be all basic intervals $[a,b)$ lying in members of $\mathcal{U}$, and put $C=\bigcup \{(a,b):[a,b)\in \mathcal{D}\}$. For every rational pair $p<q$ for which $(p,q)\subseteq (a,b)$ for some $[a,b)\in \mathcal{D}$, use [A1] to select one such member of $\mathcal{D}$. The selected family is at most countable and covers $C$: every point of an interval $(a,b)$ lies in some rational interval $(p,q)\subseteq (a,b)$.

The antidiagonal $A=\{(x,-x):x\in \mathbb{R}\}$ is uncountable and discrete in $S^2$, because $[x,x+1)\times [-x,-x+1)$ meets $A$ only in $(x,-x)$.

The antidiagonal is closed: a point $(u,v)$ with $u+v\mathrm{\ne }0$ has a basic rectangle avoiding $A$, using $[u,u+1)\times [v,v+1)$ when $u+v>0$ and sufficiently short intervals ending before the sum reaches $0$ when $u+v<0$.

Fix an enumeration of $\mathbb{Q}$. If $x\mathrm{\notin }C$, some member of $\mathcal{D}$ containing $x$ must have left endpoint exactly $x$; otherwise $x$ would lie in its ordinary interior and hence in $C$. Let $r_x$ be the first rational in the fixed enumeration satisfying $x<r_x$ and $[x,r_x)\in \mathcal{D}$; such a rational exists by [L2]. If $x<y$ and $r_x=r_y$, then $y\in (x,r_x)\subseteq C$, a contradiction. Thus $x\mapsto r_x$ injects $\mathbb{R}\setminus C$ into $\mathbb{Q}$, so $\mathbb{R}\setminus C$ is at most countable.

The open cover consisting of $S^2\setminus A$ and one isolating basic rectangle for each point of $A$ has no at most countable subcover, so $S^2$ is not Lindelöf.

The selected basic intervals from step 1.1 together with the $[x,r_x)$ from step 2.1 form an at most countable basic cover of $S$. Using [A1], select for each of them a containing member of $\mathcal{U}$. The result is an at most countable subcover, so $S$ is Lindelöf.

Thus the Lindelöf space $S$ has a non-Lindelöf square, refuting productivity of Lindelöfness.