Difficulty in proving $A[x]/(f)\otimes_A B\simeq B[x]/(f)$? Suppose $A\subset B$ are rings. I'm trying to justify that $A[x]/(f)\otimes_A B\simeq B[x]/(f)$ as algebras by defining inverse morphisms.
I defined $\varphi\colon A[x]/(f)\otimes_A B\to B[x]/(f)$ by 
$$
\left(a(x)+(f)\right)\otimes b\mapsto ba(x)+(f).
$$
The inverse map $\psi\colon B[x]/(f)\to A[x]/(f)\otimes_A B$ should be given by
$$
\sum_i b_ix^i+(f)\mapsto\sum_i ((x^i+(f))\otimes b_i).
$$
The only difficulty I'm having is showing that $\psi$ is well-defined. Does anyone know how to check this detail? Assuming $\sum b_ix^i-\sum c_ix^i=\sum (b_i-c_i)x^i\in (f)$, I'd want $\sum_i ((x^i+(f))\otimes b_i-c_i)=0$ but it's eluding me.
If there's a nice proof using universal properties, I wouldn't mind scrapping this in favor of that.
 A: The question was already answered in the comments, but you also asked for a nice proof using universal properties. Assuming rings are defined to be commutative, there is a relatively painless argument using universal properties in the form of natural bijections between Hom-sets. 
For any $A$-algebra $Y$ we let $Z_f(Y)$ be zero set of $f$ in $Y$. This defines a functor from the category of $A$-algebras to the category of sets. The key observation now is that if $C$ is another $A$-algebra, then giving a $A$-algebra morphism $C[x]/(f) \to Y$ is the same as giving a morphism from $C$ to $Y$ and choosing a point in $Z_f(Y)$ to send $x$ to. Hence, we have a bijection of sets
$$\textrm{Hom}_A(\,{C[x]}/{(f)},\, Y) \cong \textrm{Hom}_A(C, Y) \times Z_f(Y)$$
which is natural in $Y$. 
Using this observation and the fact that the tensor product is the coproduct in the category of commutative $A$-algebras we get
\begin{align}
\textrm{Hom}_A\big(A[x]/(f)\otimes_A B,\,\, Y\big) 
&\cong \textrm{Hom}_A\big(A[x]/(f),\,\, Y\big) \times \textrm{Hom}_A(B,\,\, Y) \\
&\cong \textrm{Hom}_A(A,\,\, Y) \times Z_f(Y) \times \textrm{Hom}_A(B,\,\, Y) \\
&\cong Z_f(Y) \times \textrm{Hom}_A(B,\,\, Y) \\
&\cong \textrm{Hom}_A\big(B[x]/(f), \,\,Y\big)
\end{align}
These bijections are all natural in $Y$. Hence the $A$-algebras $A[x]/(f) \otimes_A B$ and $B[x]/(f)$ represent the same functor, and are therefore isomorphic as $A$-algebras and in particular as rings. 
Notice by the way that this argument does not depend on the ideal $(f)$ being principal: the same argument applies for any ideal $I \triangleleft A[x]$ if we interpret $Z_I(Y)$ as $\{y \in Y: \forall f \in I: f(y)\}$, i.e. as the common zero set of all elements of $I$. Similarly, we can also immidiately generalize to the case of multiple variables, if we reinterpret $Z_I(Y)$ as a subset of $Y^n$, where $n$ is the number of variables. So without any extra work, we also get an isomorphism $A[x_1, \ldots, x_n]/I \otimes _A B \cong B[x_1, \ldots, x_n]/(I)$, where $(I)$ denotes the ideal generated by $I$ in $B[x_1, \ldots, x_n]$. 
If the rings are not assumed to be commutative, then above considerations do not hold. Perhaps a similar derivation will work in that case, but I don't know enough about tensor products of non-commutative rings to say much about that. 
