Proof of Brzozowski's algorithm for DFA minimization?
The proof of Brzozowski's result is technical, but not very complicated.
In fact we only have to consider one sequence of reversal-determinization, to obtain the minimality result we want. (The first sequence of reversal determination leads to a deterministic FSA for the reversal of the original language; the minimality proof is for the second reversal-determinization.)

First one needs some good view of the different automata involved. 
And nerves of steel.

The construction of Brzozowski.
Let $A = (Q, \Sigma, \delta, q_0, F)$ be a deterministic automaton for the language $L=L(A)$. We assume that all states of $Q$ are reachable from the initial state $q_0$.

In the first step one reverses the automaton: all edges are inverted, and inital and final states are swapped. Informally we get the automaton $\mathrm{rev}(A) = (Q, \Sigma, \delta^{-1}, F, q_0)$.

In the second step one determinizes the automaton so obtained, by the standard construction, but keeping only reachable states. We get $A'= \mathrm{det}(\mathrm{rev}(A)) = (Q', \Sigma, \delta', q'_0, F')$. 
The states of $A'$ are sets of states for $\mathrm{rev}(A)$: $Q'\subseteq 2^Q$; 
the initial state consists of the initial states for $\mathrm{rev}(A)$, which are final states in $Q$: $q'_0 = F$;
the final states in $A'$ are the states that contain a final state for $\mathrm{rev}(A)$: $U\in F'$ iff $q_0\in U$. 

The key of the proof is the following important relation between automata $A$ and $A'$.




  Basic Observation: $q\in \delta'(X,w^R)$ iff $\delta(q,w) \in X$.


Proof (one side only). $q\in \delta'(X,w^R)$ iff there exists a state $p$ in $X$ and a path from $p$ to $q$ in $\mathrm{rev}(A)$ with label $w^R$. But that means there is a path from $q$ to $p$ with label $w$ in $A$, or $\delta(q,w) = p$; thus $\delta(q,w) \in X$. end-of-proof.

As announced, this is used to prove the essential property we need.


  Property: $A'$ is minimal (and deterministic for $L^R$).


Proof. Let $U$ and $V$ be two states in $A'$ that cannot be distinguished. This means that for any string $w^R$ we have $\delta'(U,w^R) \in F'$ iff $\delta'(V,w^R) \in F'$. We show that now $U$ and $V$ are equal.

By the construction of $F'$ we can rephrase indistinguishability as $\delta'(U,w^R) \ni q_0$ iff $\delta'(V,w^R) \ni q_0$. 

Apply the Basic Observation, and we have $\delta(q_0,w) \in U$ iff $\delta(q_0,w) \in V$.

From this equality $U=V$ follows, as all states in $Q$ are assumed to be reachable, thus for any state $p$ in $U$ or $V$ there is a string $w$ such that $p = \delta(q_0,w)$.
end-of-proof.

But even after proving, the result is still real magic!