Inner product on the tensor product of Hilbert spaces

Let $H_1$ and $H_2$ be Hilbert spaces with inner products $\langle\cdot,\cdot\rangle_1$ and $\langle\cdot,\cdot\rangle_2$, respectively. Then $H_1\otimes H_2$ is at least a pre-Hilbert space (we are not concerned with completeness here).
On this tensor product we can define an inner product by setting $$\langle v_1\otimes v_2,w_1\otimes w_2\rangle:=\langle v_1,w_1\rangle_1 \langle v_2,w_2\rangle_2$$ for $v_1,w_1\in H_1,\;v_2,w_2\in H_2$. This is how all textbooks define it.

However, I do not understand why this product is bilinear. To prove bilinearity, we would consider something like $$\langle \lambda u_1\otimes u_2+ v_1\otimes v_2,w_1\otimes w_2\rangle,$$ but in general it is not possible to write the sum $\lambda u_1\otimes u_2+ v_1\otimes v_2$ as one pure tensor product. Therefore it would not be possible to write this in the form of the definition which formally does not permit sums of tensor products.

In the literature on this topic, the above definition is the only information on the new inner product, so my question is: Are the textbooks missing the fact that bilinearity does not follow from the above definition (i.e. bilinearity should be part of the definition in order to get an inner product) or did I miss something and bilinearity is already clear from the definition?

The map $b:(v_1,v_2,w_1,w_2)\in (H_1\times H_2)\times (H_1\times H_2)\to \langle v_1,w_1\rangle_1\langle v_2,w_2\rangle_2\in\mathbb R$ is multinear.
So it factors through $$\begin{array}{cc}\otimes\times\otimes:&(H_1\times H_2)\times (H_1\times H_2)\to (H_1\otimes H_2)\times (H_1\otimes H_2)\\&(v_1,v_2,w_1,w_2)\mapsto(v_1\otimes v_2,w_1\otimes w_2)\end{array}$$ and a bilinear form $\langle\cdot,\cdot\rangle:(H_1\otimes H_2)\times (H_1\otimes H_2)\to\mathbb R.$
The latter is precisely your product.

The statement you cited does provide enough information to completely determine the function $\langle \cdot, \cdot \rangle$. Sesquilinearity follows from the clause stating that it's an inner product, and any sesquilinear map is completely determined by its values on pairs of basis elements.

The challenge isn't to prove it's sesquilinear, but to prove it's well-defined.

In general, definitions aren't of the form

<thing to be defined> := <thing it is defined as>

it is rather more common to implicitly define it by providing sufficient information to uniquely determine it. It may help to digest this fact by noting that defining the function $f$ by

$$ f(x) = x^2 + 2x + 1$$

is actually an implicit definition for $f$ -- you aren't defining $f$ directly, but instead you are providing an equation involving the evaluation operator applied to $f$ (and $x$).