I am interested in the following innocent looking statement:
Let $A \leftarrow R \rightarrow B$ be two homomorphisms of commutative rings. Assume that their kernels consist of nilpotent elements. Then, the kernel of $R \to A \otimes_R B$ consists of nilpotent elements, too.
Geometrically, this means that if $X \to S$ and $Y \to S$ are two quasi-compact morphisms of schemes with dense image, then the image of $X \times_S Y \to S$ is dense, too.
We can prove this as follows (using the axiom of choice many times): It suffices to show that the kernel of $R \to A \otimes_R B$ is contained in any minimal prime ideal $P \subseteq R$. Since the kernel of $R \to A$ is contained in $P$, we have $A_P \neq 0$, and likewise $B_P \neq 0$. Choose prime ideals in these rings. Their preimages are prime ideals $I \subseteq A$, $J \subseteq B$ such that $I \cap R = P$ (since $I \cap R \subseteq P$ and $P$ is minimal) and $J \cap R = P$. The kernel of $R \to A \otimes_R B$ is contained in the kernel of $R \to Q(A/I) \otimes_{Q(R/P)} Q(B/J)$, which equals the kernel of $R \to Q(R/P)$, i.e. $P$, since $Q(R/P) \to Q(A/I) \otimes_{Q(R/P)} Q(B/J)$ is injective.
In fact, one can prove this statement in $\mathsf{ZF}$, i.e. the axiom of choice is not necessary. The trick is to use filtered colimits (or the explicit construction of the tensor product) to reduce to the case that $R$ is of finite type over $\mathbf{Z}$, hence countable, and to the case that $A,B$ are finite type over $R$, hence countable too. In Kostas Hatzikiriakou, "Minimal Prime Ideals and Arithmetic Comprehension", it is proven (in a fragment of $\mathsf{ZF}$) that every non-trivial countable commutative has a minimal prime ideal. Moreover, $\mathsf{ZF}$ proves that vector spaces are flat: Again, using filtered colimits, it suffices to prove this for finitely generated vector spaces, but these are free and hence flat. This proves in particular that the tensor product of two non-trivial vectors is a non-trivial vector. In particular, $Q(R/P) \to Q(A/I) \otimes_{Q(R/P)} Q(B/J)$ is injective.
The proof is still not very satisfying. We have a rather elementary statement about tensor products of algebras, do we really need prime ideals? Is it possible to simplify the proof further? Also notice that the proof above is not constructive, i.e., it uses the law of the excluded middle.
Question. Is there a constructive proof of the statement? If yes, how does it look like?
Notice that we may assume that $R,A,B$ are reduced. In that case, the question becomes: If $R \to A$ and $R \to B$ are injective, why is $R \to A \otimes_R B$ injective, too? The special case that $R$ is a field was already discussed above, and this part was constructive, I guess.
I have recently asked a similar yet broader question. I am not sure how to handle minimal prime ideals here. There is just a very short chapter about minimal prime ideals in the book by Lombardi and Quitté on constructive commutative algebra, and they "only" apply this to give a constructive proof of Traverso-Swan's theorem characterizing seminormal rings. But I would prefer a constructive proof of the statement which is really down-to-earth and can be therefore understood without any prerequisites on constructive mathematics (like the proof for the case that $R$ is a field).
Added 1. Using localization at some element in the kernel, it suffices to prove $A \otimes_R B = 0 \Rightarrow R = 0$ when $R \to A$, $R \to B$ are as above. Therefore, a related statement is the following: If $M,N$ are finitely generated $R$-modules, then it is known $\sqrt{\mathrm{Ann}(M \otimes_R N)} = \sqrt{\mathrm{Ann}(M)+\mathrm{Ann}(N)};$ this follows from $\mathrm{supp}(M \otimes_R N) = \mathrm{supp}(M) \cap \mathrm{supp}(N)$ as subsets of $\mathrm{Spec}(R)$. In particular, $\mathrm{Ann}(M) \subseteq \sqrt{0}$ and $\mathrm{Ann}(N) \subseteq \sqrt{0}$ imply $\mathrm{Ann}(M \otimes_R N) \subseteq \sqrt{0}$, thus $M \otimes_R N = 0 \Rightarrow R =0$. Again, I don't know a constructive proof. (But this probably won't help here since $A,B$ may just be assumed to be finitely generated $R$-algebras, not finitely generated $R$-modules).
Added 2. Here is a first simplification: We may assume that $R$ is reduced. Let $P$ be a minimal prime ideal of $R$. Then $R_P$ is a reduced zero-dimensional local ring, i.e. a field. The $R_P$-algebras $A_P$ and $B_P$ are non-trivial, hence $R_P \to A_P \otimes_{R_P} B_P$ is injective. It follows that the kernel of $R \to A \otimes_R B$ is contained in the kernel of $R \to R_P$, which is $P$. Now, Lombardi and Quitté write in their book in section XIII.7:
"It is a fact that the use of minimal prime ideals in a proof of classical mathematics can in general be made innocuous (i.e. constructive) by using $A_{\mathrm{min}}$".
Here, $A_{\mathrm{min}}$ denots a rather peculiar looking commutative ring constructed in Theorem 7.8. Does this mean that we can somehow prove that $R_{\mathrm{min}} \to A_{\mathrm{min}} \otimes_{R_{\mathrm{min}}} B_{\mathrm{min}}$ is injective? This would suffice since $R \to R_{\mathrm{min}}$ is injective when $R$ is reduced.
Added 3. Here is another proof, which seems to be more suitable for constructivization. We may assume that $A,B$ are of finite type over $R$ with $A \otimes_R B = 0$ and that $R$ is reduced, the goal is $R=0$. By generic freeness, there is some open dense subset $U \subseteq \mathrm{Spec}(R)$ such that $A_f$ is free over $R_f$ (hence, flat) for every $D(f) \subseteq U$. It follows that $A_f = A_f \otimes_{R_f} R_f$ injects into $A_f \otimes_{R_f} B_f = 0$, i.e. $A_f=0$. Since $R \to A$ is injective, this means $f=0$. This shows $U=\emptyset$, and therefore $R=0$. Theorem 2.45 in "Computational Methods in Commutative Algebra and Algebraic Geometry" by Wolmer Vasconcelos seems to be a constructive proof of Generic Flatness at least for Noetherian domains $R$. So we would have to generalize this to reduced commutative rings $R$, and avoid the usage of the prime spectrum.