Proving undecidability of HALT_tm by reduction Sipser in his book introduction to the theory of computation provided a proof of undecidability of $HALT_{TM}$. He uses a contradiction, he assumed that $HALT_{TM}$ is decidable, and built a decider for $A_{TM}$, and since $A_{TM}$ is already proved by digonalization method to be undecidable, thus the contradiction occurs and $HALT_{TM}$ is undecidable. The Turing Machine is simple and straightforward and I'm not going to talk about its details.

What makes me confused is this sentence


  We prove the undecidability of $HALT_{TM}$ by a reduction from $A_{TM}$ to $HALT_{TM}$


and I would like to know in which part of the proof reduction actually occurs?

From what we know of the concept of reduction, reducing $A$ to $B$ means: we have two problems $A$ and $B$ and we know how to solve $B$ but we stuck in $A$, then if we reduce $A$ to $B$, it means solving an instance of $B$ will cause solving an instance of $A$.

let's get back to the proof, Sipser says


  We prove the undecidability of $HALT_{TM}$ by a reduction from $A_{TM}$ to $HALT_{TM}$


thus $A = A_{TM}$ and $B = HALT_{TM}$. We don't know how to solve $HALT_{TM}$ and actually this is the problem in hand, furthermore the strategy of the proof is based on contradiction, something that is completely irrelevant to the concept of reduction. Then why Sipser uses the term reduction in this proof?
Sipser reduces $A_{\mathit{TM}}$ to $\mathit{HALT}_{\mathit{TM}}$. Since $A_{\mathit{TM}}$ is uncomputable, it follows that $\mathit{HALT}_{\mathit{TM}}$ has to be uncomputable. He is using the following general statement:


  If $A$ reduces to $B$ and $B$ is uncomputable, then so is $A$.


You are right that this general statement itself is proved by contradiction. A proof which uses this general statement to prove that a particular problem is undecidable is a proof by reduction – in your case, you prove the undecidability $\mathit{HALT}_{\mathit{TM}}$ by reducing a problem you already know is undecidable to $\mathit{HALT}_{\mathit{TM}}$. In contrast, Sipser's proof that $A_{\mathit{TM}}$ uses a different technique, diagonalization.