As a contrast to Bram28's answer, instead of understanding anything, you can think like a machine. The outermost connective is $\to$, so (ignoring cut) we need $\to$-introduction, then we have $\forall$ twice, so use $\forall$-introduction. We now have $$x_0, y_0; \exists x.\forall y.x = y\vdash x_0 = y_0$$ Now the only option is $\exists$-elimination, giving $$x_0, y_0, x_1; \forall y.x_1 = y\vdash x_0 = y_0$$ Now the only thing we can do is use $\forall$-elimination which only gives us two additional facts: $$x_0, y_0, x_1; x_1 = y_0, x_1 = x_0\vdash x_0 = y_0$$ Now we can apply $=$-elimination producing: $$x_0, y_0; x_0 = y_0\vdash x_0 = y_0$$
And we're done.
If we ignore cut, then at each step in the proof there are relatively few options, often only one. Actually writing this out in typical natural deduction style is a bit awkward because natural deduction proofs proceed from the top and bottom simultaneously to the middle. The sequent calculus avoids this by being strictly bottom-up. In particular, doing the $\forall$-eliminations will produce two floating branches that will be connected to the "trunk" of the proof with the $=$-elimination. Anyway, to reiterate, regardless of the exact rules of your system, for many proofs of simple logical facts there will be only a few (or possibly only one) way of continuing the proof making even brute-force search often quite effective. Obviously, adding a bit of intuition to guide the search when there is more than one option can avoid wasting time on dead-ends.