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\ne0$ 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\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.