Related to: Löb's Theorem for implicit reasoning in natural language: Löbian party invitations

tl;dr: Löb's Theorem is much easier to grok if you separate the parts of the proof that use the assumption $\square p\to p$  from the parts that don't.  The parts that don't use $\square p\to p$ can be extracted as a stand-alone result, which I hereby dub "Löb's Lemma".

Here's how it works.

Key properties of $⊢$ and $\square$

Here is some standard notation.  In short, $⊢$ is our symbol for talking about what PA can prove, and $\square$ is shorthand for PA's symbols for talking about what (a copy of) PA can prove.

• "$⊢$ 1+1=2" means "Peano Arithmetic (PA) can prove that 1+1=2".  No parentheses are needed; the "$⊢$" applies to the whole line that follows it.  Also, $⊢$ does not stand for an expression in PA; it's a symbol we use to talk about what PA can prove.
• "$\square \left(\text{1+1=2}\right)$" basically means the same thing.  More precisely, it stands for a numerical expression within PA that can be translated as saying "$⊢$ 1+1=2".  This translation is possible because of something called a Gödel numbering which allows PA to talk about a (numerically encoded version of) itself. 
• "$\square X$ " is short for "$\square \left(X\right)$" in cases where "$X$" is just a single character of text.
• "$X⊢Y$" means "PA, along with X as an additional axiom/assumption, can prove Y". In this post we don't have any analogous notation for $\square$.

The proofs here will use the following standard properties of $⊢$ and $\square$ (source: Wikipedia), which respectively stand for provability and provability encoded within arithmetic.  

1. (necessitation) From $⊢A$, conclude $⊢\square A$.  Informally, this says that if A can be proven, then it can be proven that it can be proven (by just writing out and checking the proof within arithmetic).  Note that from $X⊢A$ we cannot conclude $X⊢\square A$, because $\square$ still means "PA can prove", and not "PA+X can prove".  
2. (internal necessitation) $⊢\square A\to \square \square A$ . If A is provable, then it is provable that it is provable (basically the same as the previous point).
3. (box distributivity) $⊢\square (A\to B)\to (\square A\to \square B)$. This rule allows one to apply modus ponens inside the provability operator. If it is provable that A implies B, and A is provable, then B is provable.
4. (deduction theorem) From $A⊢B$, conclude $⊢A\to B$: if assuming $A$ is enough to prove $B$, then it's possible to prove under no assumptions that $A\to B$. 

Point 4 is helpful and pretty intuitive, but for whatever reason isn't used in the main Wikipedia article on Löb's Theorem.

Löb's Lemma

Claim: Assume $\Psi$ and $p$ are any statements satisfying $⊢\Psi \leftrightarrow \square \Psi \to p$.  Then $⊢\square \Psi \leftrightarrow \square p$.

Intuition: By assumption, the sentence $\Psi$ is equivalent to saying "If this sentence is provable, then $p$".  Intuitively, $\Psi$ has very little content, except for the $p$ part at the end, so it makes sense that $\square \Psi$ boils down to nothing more than $\square p$ in terms of logical equivalence. 

Reminder: this does not use the assumption $\square p\to p$ from Löb's Theorem at all.

Proof:

Let's do the forward implication first:

1. $\square \Psi ⊢\square \square \Psi$                   by internal necessitation ($\square \Psi \to \square \square \Psi$).
2. $\square \Psi ⊢\square (\square \Psi \to p)$       using box distributivity on the assumption, 
                                            with $A=\Psi$ and $B=\square \Psi \to p$.
3. $\square \Psi ⊢\square p$                        from 1 and 2 by box distributivity.
4. $⊢\square \Psi \to \square p$                   from 3 by the deduction theorem.

Now for the backwards implication, which isn't needed for Löb's Theorem, but is handy anyway:

1. $⊢p\to (\square \Psi \to p)$              is a tautology.
2. $⊢\square p\to \square (\square \Psi \to p)$       by box distributivity on 1.
3. $⊢\square \Psi \leftrightarrow \square (\square \Psi \to p)$      by box distributivity on the assumption.
4. $⊢\square p\to \square \Psi$                       by 2 and 3.

I like this result because both directions of the proof are fairly short, it doesn't use the assumption $\square p\to p$ at all, and the conclusion itself is also fairly intuitive.  The statement $\Psi$ just turns out to have no content except for $p$ itself, from the perspective of writing proofs.

Löb's Theorem, now in just 6 lines

If you can remember Löb's Lemma, you can write a very straightforward proof of Löb's Theorem in just 6 lines:

Claim: If $p$ is any sentence such that $⊢\square p\to p$, then $⊢p$

Proof:

Let $\Psi$ be any sentence satisfying $⊢\Psi \leftrightarrow (\square \Psi \to p)$, which exists by the existence of modal fixed points (or by the Diagonal Lemma).

1. $⊢\square \Psi \to \square p$    by Löb's Lemma.
2. $⊢\square p\to p$         by assumption.
3. $⊢\square \Psi \to p$        by 1 and 2 combined.
4. $⊢\Psi$                    by 3 and the defining property of $\Psi$
5. $⊢\square \Psi$                 by necessitation.
6. $⊢p$                      by 3 and 5.

«mic drop»