The theorem states:
Let $(h_n)_{n\in \mathbb{N}}$ be a sequence of positive harmonic functions on a domain $G$. Then either $h_n\to \infty$ locally uniformly or $h_n\to h$ locally uniformly where $h$ is harmonic on $G$.
So in the proof it is shown that $\log h_n$ is locally uniformly bounded. We then look at a countable dense subset $S\subseteq G$. The proof then claims that we can find a subsequence that is convergent for all $s\in S$ by the diagonal argument?
I think I got it pretty right, i.e: $h_n(s_1)$ is bounded $h_n(s_1)_j$ convergent, $h_n(s_2)_j$ bounded $h_n(s_2)_{j_{k}}$ convergent etc... How do I formally state that as a diagonal arguement? It's something like that n'th element evaluated in the n'th subsequence.
The formal way is going back to the definitions of sequence and subsequence:
a sequence is function $f:\Bbb N\to X$
a subsequence of $f$ is a sequence $g$ in the form $f\circ m$ for some strictly increasing $m:\Bbb N\to\Bbb N$
the $k$-th tail of a sequence $f$ is the subsequence $g_n=f_{n+k}$. This definition technically introduces a difference between a tail and the function $\left.f\right\rvert_{\Bbb N_{\ge k}}$. Said difference is as material as it looks like (sarcasm).
As per a long established notation, we shall denote $f(n)=f_n$ so that, when $X$ is a space of functions itself, $[f(n)](x)=f_n(x)$. Now, in your case there is a map $G:\{\text{sequences of functions}\}\times \Bbb N\to \{\text{sequences of functions}\}$ such that $G(f,n)$ is a subsequence of $f$ and $\lim_{k\to\infty} G(f,n)_k(s_n)$ exists. Therefore, you can define recursively a sequence of subsequences of $h$ such that $H^0=h$ and $H^{n+1}=G(H^n,n)$. Namely, $H^n$ is a subsequence of all the preceeding $H^i$-s such that $\lim_{k\to\infty}H^n_k(s_{n-1})$ exists. Finally, call the diagonal sequence is $\widetilde H_k=H^k_k$. The reason why $\lim_{k\to\infty}\widetilde H_k(s_n)$ converges for all $n$ is that the $n$-th tail of $\widetilde H$ is a subsequence of $H^n$. Now, consider striclty increasing functions $f^i$ such that $H^i=H^{i-1}\circ f^i$, so that \begin{align}\widetilde H_{n+k}&=H^{n+k}_{n+k}=(H^{n+k-1}\circ f^{n+k})_{n+k}=(H^{n+k-2}\circ f^{n+k-1}\circ f^{n+k})_{n+k}=\cdots\\\cdots&=(H^n\circ f^{n+1}\circ\cdots\circ f^{n+k})_{n+k}\end{align}
We'd like to prove that the function $g:\Bbb N\to\Bbb N$, $g(0)=0$, $g(k)=f^{n+1}(f^{n+2}(\cdots (f^{n+k}(k))\cdots))$ is strictly increasing. In order to do so, we need only prove that $g(m+1)>g(m)$ for all $m$. The essential ingredient is that, if $f:\Bbb N\to\Bbb N$ is strictly increasing, then $f(n)\ge n$. For $m\ge 1$, $$\begin{cases}g(m+1)=f^{n+1}(\cdots(f^{n+m}(f^{n+m+1}(m+1))\cdots)=\underbrace{[f^{n+1}\circ\cdots\circ f^{n+m}]}_{g^{n,m}}(f^{n+m+1}(m+1))\\f^{n+m+1}(m+1)\ge m+1>m\end{cases}$$ And since $g^{n,m}$ is a strictly increasing function, $$g(m+1)=g^{n,m}(f^{n+m+1}(m+1))>g^{n,m}(m)=g(m)$$ This proves that the $n$-th tail of $\widetilde H$ is the $n$-th tail of some subsequence of $H^n$ and, therefore, that the $n$-th tail of $\widetilde H$ is a subsequence of $H^n$.
I think that the generality of this procedure is sufficiently clear (if I do say so myself). A presentation for lectures that I, from a student's perspective, have found sufficiently effective is this one: $$\begin{matrix}\text{diagonal}\\&\searrow\\\text{original sequence}&\rightarrow &\boxed{h_0}&h_1& h_2 & h_3&\cdots\\ \text{converges on } s_0&\rightarrow&h_{f^1_0}&\boxed{h_{f^1_1}}& h_{f^1_2} & h_{f^1_3}&\cdots\\ \text{converges on } s_1&\rightarrow&h_{f^1_{f^2_0}}&h_{f^1_{f^2_1}}& \boxed{h_{f^1_{f^2_2}}} & h_{f^1_{f^2_3}}&\cdots\\ \text{converges on } s_2&\rightarrow&h_{f^1_{f^2_{f^3_0}}}&h_{f^1_{f^2_{f^3_1}}}& h_{f^1_{f^2_{f^3_2}}} & \boxed{h_{f^1_{f^2_{f^3_3}}}}&\cdots\\\vdots&\vdots&\vdots&\vdots&\vdots&\vdots&\ddots\end{matrix}$$