Formalizing a proof for $ \sum_{n=0}^\infty \sum_{k=n}^{\infty} a_k = \sum_{n=0}^{\infty} (n+1)a_n$

We can use the indicator function

$$\mathbf{1}_{\{k\geqslant n\}} = \begin{cases}1,&k \geqslant n \\0, &k < n\end{cases},$$

and nonnegativity of $a_k$ to obtain

$$\sum_{n = 0}^\infty\sum_{k=n}^\infty a_k = \sum_{n = 0}^\infty\sum_{k=0}^\infty \mathbf{1}_{\{k\geqslant n\}}a_k \,\underbrace{= \sum_{k = 0}^\infty\sum_{n=0}^\infty \mathbf{1}_{\{k\geqslant n\}}a_k }_{\text{applying Tonelli's theorem}} = \sum_{k = 0}^\infty a_k\sum_{n=0}^\infty \mathbf{1}_{\{k\geqslant n\}} \\ = \sum_{k = 0}^\infty a_k\sum_{n=0}^k (1) = \sum_{k=0}^\infty (k+1)a_k = \sum_{n=0}^\infty (n+1)a_n$$ Clearly, the last step is just replacing letter "k" with letter "n".