Proving $\Box A \rightarrow \Box\Box A$ from $KG_r$ I'm trying to prove $\Box A\rightarrow \Box\Box A$ from $KG_r$ where $G_r$ is the axiom 
$$\Box[ \Box A \rightarrow A ] \rightarrow \Box A$$
I'm given the hint that 
$$ A \rightarrow ((\Box\Box A\land \Box A) \rightarrow (\Box A \land A))$$
is a theorem.  I know that in any normal system you can box any theorem but I haven't seen a way to turn that into something useful here.  In general that theorem just looks like a bunch of antecedent strengthening which doesn't seem useful but I don't know.
Because of the $KG_r$ axiom I know that $\Box[\Box \Box A\rightarrow \Box A]\rightarrow \Box \Box A$ so that if I could prove the antecedent of this from $\Box A$ I'd be done.  
I've also thought about the fact that $\Box A \rightarrow (\Box\Box A \rightarrow \Box A)$ is a theorem and therefore can get boxed, although already that seems like the wrong direction to head in.  But just to give it a go I try $\Box (\Box A \rightarrow (\Box\Box A \rightarrow \Box A))$ which by normalcy implies $\Box\Box A\rightarrow \Box(\Box\Box A\rightarrow \Box A)$.
I'm starting to get lost in all of my attempts so guidance at this point would be appreciated.
[Edit:  I also just derived the following possibly useful result.  Since $\Box A\rightarrow (\Box A\rightarrow A)$ is a theorem then $\Box(\Box A\rightarrow(\Box A\rightarrow A))$ is a theorem and due to $K$ we can infer $\Box\Box A\rightarrow \Box(\Box A\rightarrow A)$.  Then due to $KG_r$ directly we get $\Box(\Box A\rightarrow A) \rightarrow \Box A$ and so by transitivity of $\rightarrow$ we get $\Box\Box A\rightarrow \Box A$ which is the converse of what I'm trying to show.
... Never mind, realized $\Box A \rightarrow (\Box A \rightarrow A)$ isn't a theorem, $\Box A\rightarrow (A\rightarrow \Box A)$ is and that doesn't lead to anything.]
 A: What you are looking for is shown for example in Hughes&Cresswell A New Introduction to Modal Logic pp. 150, where $G_r$ is called $W$. (In other sources it is known as the Goedel-Loeb axiom $GL$; see also Wikipedia Kripke semantics or Loeb's theorem.) In case you don't have the book, here is the proof:
(1) $\:p\rightarrow ((q\land r)\rightarrow(p\land q))\quad$ Boolean tautology
(2) $\:p\rightarrow ((\Box p\land \Box\Box p) \rightarrow (p\land\Box p))\quad$ from (1) by substitution
(3) $\:p\rightarrow (\Box(p\land\Box p) \rightarrow (p\land\Box p))\quad$ from (2) by K-theorem $\Box(p\land q)\leftrightarrow(\Box p\land\Box q)$
(4) $\:\Box p\rightarrow \Box(\Box(p\land\Box p) \rightarrow (p\land\Box p))\quad$ from (3) by K-rule "from $\phi\rightarrow\psi$ infer $\Box \phi\rightarrow\Box \psi$"
(5) $\:\Box(\Box(p\land\Box p)\rightarrow(p\land\Box p))\rightarrow\Box(p\land\Box p)\quad$ from $W$ by substitution
(6) $\:\Box p\rightarrow \Box(p\land\Box p)\quad$ from (4) and (5) by hypothetical syllogism
(7) $\:\Box p\rightarrow (\Box p\land\Box\Box p)\quad$ from (6) by K-theorem $\Box(p\land q)\leftrightarrow(\Box p\land\Box q)$
(8) $\:\Box p\rightarrow\Box\Box p\quad$ from (7) by Boolean logic
Observe that even though the system KW is defined by an axiom of modal degree 2, the above proof uses formulas of modal degree 3. In fact, you can not prove this KW theorem using only formulas of modal degree 2. Here is the trick that was used, which is also applicable to other logics.
Consider a system S defined as K plus an axiom of modal degree 2. Let $f,g,h$ denote formulas of modal degree at most 1 in $p$ and $\sigma$ a substitution of modal degree 1 for $p$. What you can do is:
1) Choose a suitable formula $f(p)$ (typicaly not a theorem of S) and a suitable substitution $\sigma(p)$.
2) Find some $g(p)$ and $h(p)$ such that both the following are theorems of S:
    $g(p)\rightarrow f(\sigma(p))$
    $\Box f(p)\rightarrow h(p)$
3) From these derive the following modal degree 3 formulas respectively:
    $\Box g(p)\rightarrow \Box f(\sigma(p))$
    $\Box f(\sigma(p))\rightarrow h(\sigma(p))$
4) Then you can derive $\Box g(p)\rightarrow h(\sigma(p))$,
and you are back to modal degree 2.
This can be represented schematically as follows:
$$
\begin{align*}
\frac{g(p)\rightarrow f(\sigma(p))}{\Box g(p)\rightarrow \Box f(\sigma(p))} &
\qquad &
\frac{\Box f(p)\rightarrow h(p)}{\Box f(\sigma(p))\rightarrow h(\sigma(p))} \\
\\
\hline
\end{align*}
$$
$$\Box g(p)\rightarrow h(\sigma(p))$$
With suitable choices, the resulting theorem is stronger than what you can prove using only formulas of modal degree 2.
For the KW example above, take $f(p)=\Box p \rightarrow p$, $g(p)=p$, $h(p)=\Box p$ and $\sigma(p)=p\land\Box p$, then you get (7).
