<s>[INST] AC^2 Algebraic simplifications Suppose I know that:
$AB^2=DF^2+CF^2$;
$AD^2=BE^2+CE^2$;
$AC^2=AE^2+CE^2$;
$AC^2=AF^2+CF^2$
And also: 
$DF=AF-AD$ and $BE=AE-AB$
How can I prove that $AB * AE + AD * AF = AC^2$?
I start like this, but then I get stucked: 
$AB*AE + AD*AF = AB*(BE+AB) + AD*(DF+AD) =
AB*BE + AB^2 + AD*DF + AD^2 =
AB*BE + AB^2 + AD*DF + BE^2 + CE^2 =
(AE - BE)*BE + AB^2 + AD*DF + BE^2 + CE^2 =
AE*BE - BE^2 + AB^2 + AD*DF + BE^2 + CE^2 =
AE*BE + AB^2 + AD*DF + CE^2 =
AE*(AE - AB) + AB^2 + AD*DF + CE^2 =
AE^2 - AE*AB + AB^2 + AD*DF + CE^2...$
Can anyone give a hint how to continue?
Thanks!
 [/INST] Let $AB=x$, $BE=y$, $AD=p$, $DF=q$, now from the first $4$ equations we have
\begin{eqnarray*}
p^2+(x+y)^2=y^2+CE^2+(x+y)^2=y^2+AC^2 \\=y^2+(p+q)^2+CF^2=y^2+p^2+2pq+x^2
\end{eqnarray*}
and so $xy=pq$.
Now
\begin{eqnarray*}
AB \times AE+ AD \times AF = x(x+y)+p(p+q)
\end{eqnarray*}
and 
\begin{eqnarray*}
AC^2 = (x+y)^2+CE^2=(x+y)^2+p^2-y^2
\end{eqnarray*}
and thus $\color{red}{AB \times AE+ AD \times AF =AC^2}$.
</s>