Diagonalisation, as in the textbook: a decider $H$ for $A_TM$ yields, by programming ($Nat.Partrec.Code.exists_code$), a machine $D$ that accepts the code of a machine $N$ exactly when $N$ does not accept its own code ($Acceptance.exists_flip_machine$ in the source); $D$ on its own code is a contradiction ($Acceptance.no_diagonal_machine$). The concept's definitions of machines, acceptance and $A_TM$ are the source's, so the source theorem is the statement.

Sipser, Introduction to the Theory of Computation, Theorem 4.11; Lean proof by Aristotle ($Acceptance.atm_not_turingDecidable$).