$\varphi(1)+\varphi(p)+\varphi(p^2)+\dots+\varphi(p^\alpha)=p^\alpha$

This is Problem 4.133 of N. B. Alfutova and A. V. Ustinov, Algebra and Number Theory (MCCME, 2002), Chapter 4, §4 “Theorems of Fermat and Euler”. The problem asks for the value of the sum $\varphi(1)+\varphi(p)+\varphi(p^2)+\dots+\varphi(p^\alpha)$, where $\varphi$ is Euler's function, $p$ is a prime (as in the preceding Problem 4.132) and $\alpha$ is a natural number. The book's answer is $p^{\alpha}$.

Theorem. For every prime $p$ and every $\alpha\in\mathbb N$,

This is the prime-power case of Gauss's identity $\sum_{d\mid n}\varphi(d)=n$.

Formalization Note Euler's function is Nat.totient. The statement is proved for all $\alpha\in\mathbb N$, including $\alpha=0$ (where it reads $\varphi(1)=1$), which contains the book's case $\alpha\ge 1$.