Very simple question: if we're asked to prove that $a=b$, do we start with $a$ and then find $b$ from $a$? Does going the other way around count as a formal proof? The exercise in question is this:
Prove that $$\mbox{arctanh}\left[ \frac{1}{\cosh \left( 2x \right)} \right]=\log \left[ \coth \left( x \right) \right]\; ,\; \; x>0$$
I want to be as formal as possible
Your question stems, unfortunately, from a serious misunderstanding in the logical nature of equality. We say "$x = y$" to mean "$x$ is the same as $y$". We are thus allowed to write down "$x = x$" for any object $x$. Also, given that $x = y$ we can substitute "$x$" in place of any occurrence of "$y$" in any true statement to produce another true statement.
An important result of these rules is that, given $x = y$ and $y = z$, we get $x = z$ by substituting $x$ in place of $y$ in the second statement. This logical fact of equality is called transitivity of equality. This means that when asked to prove a statement of the form $A = Z$, it is perfectly fine to first prove a whole chain of equalities such as $B = C$ and $D = C$ and $D = E$ and $A = B$ and $Z = E$, and after that you can then use transitivity of equality a few times to obtain $A = Z$.
Also, I should add that in practice when asked to prove something of the form "$A = B$", it is often helpful to first prove $A = A'$ and $B = B'$ where "$A'$" and "$B'$" are as simple expressions as possible, and only after that to try to prove $A' = B'$.
You may even prove $a=c$ and $b=c$ and deduce $a=b$ from the fact that equality is symetric ($c=b$) and transitive.
