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?