The following deduction can be found from the Boolos - The Logic of Provability in the page 59. It is in the proof for arithmetical soundness theorem.
Let's assign
\begin{align*} &B = \square ( \square A \rightarrow A)\\ &C = \square A\\ &D = B \rightarrow C = \square ( \square A \rightarrow A) \rightarrow \square A \end{align*}
Then \begin{align*} K4 &\vdash \square (B \rightarrow C) \rightarrow (\square B \rightarrow \square C) &&\text{Distribution axiom}\\ K4 &\vdash B \rightarrow (\square C \rightarrow C) && \text{Distribution axiom}\\ K4 &\vdash B \rightarrow \square B && \text{transitivity / 4}\\ K4 &\vdash \square (B \rightarrow C) \rightarrow (B \rightarrow C) && \text{???}\\ \end{align*}
I know the last line should be a tautological consequence of the three lines above. I suppose it's something pretty straight forward, but I just don't get it. Thank you for helping.
Let us show that $\square D \rightarrow D$ follows truth-functionally from (and so is a tautological consequence of) the three formulae above it.
From the hypotheses $H_1 =\square D \rightarrow (\square B \rightarrow \square C), H_2 = B \rightarrow (\square C \rightarrow C), H_3 = B \rightarrow \square B\ $ we need to deduce $\square D \rightarrow D$. So from $H_1, H_2, H_3$ and $\square D$ we need to deduce $D$, that is $B \rightarrow C$. Hence from $H_1, H_2, H_3, \square D$ and $B$ we need to deduce $C$.
From $H_1$ and $\square D$ we get $\square B \rightarrow \square C$. From $H_3$ and $B$ we get $\square B$. From $\square B$ and $\square B \rightarrow \square C$ we get $\square C$. Now, from $H_2$ and $B$ we get $\square C \rightarrow C$. Finally, from $\square C$ and $\square C \rightarrow C$ we get $C$.
The above shows that whenver all $H_1, H_2, H_3$ are true, so is $\square D \rightarrow D$, hence by the completeness theorem for propositional calculus $\square D \rightarrow D$ is a tautological consequence of these hypotheses. Also if you need an actual proof in propositional calculus, the argument above can be transformed into such a proof by appealing to the deduction theorem.