Prof Körner told us during the IB Metric and Topological Spaces course that the real meat of the course (indeed, its hardest theorem) was “a metric space is sequentially compact iff it is compact”. At the moment, all I remember of this result is that one direction requires Lebesgue’s lemma (whose statement I don’t remember) and that the other direction is quite easy. I’m going to try and discover a proof  I’ll be honest when I have to look things up.
Easy direction
I don’t remember which direction was the easy one. However, I do know that in Analysis we prove very early on that closed intervals are sequentially compact (that is, they have the BolzanoWeierstrass theorem), so I’m going to guess that that’s the easy direction.
Thought process
Suppose the space is compact. (Then for every open cover there is a finite subcover.) We want to show that every sequence has a convergent subsequence, so of course we’ll try a proof by contradiction, because the statement is so general.
Suppose the sequence has no convergent subsequence. That is, no subsequence of converges to , for any . We’re aiming for some kind of open cover, and we’re in a very general kind of metric space, so we’re going to have to generate our cover by considering balls around every point.
What does it mean for every subsequence of not to converge to ? It means that for every ball around , and for every subsequence, we can find arbitrarily many in the subsequence such that is outside that ball. My first thought is that we’ve made a sequence which might be useful  the outside balls of radius for  but it’s not obvious whether that will in fact be useful, because all we know about this sequence is that it doesn’t get near a particular point.
OK, let’s look at the “for every ” bit, because that’s bound to be where our cover comes from. We’re going to want a ball around each , so let’s say the ball is of radius . (We’ll delay stating what actually is in value, because I have no idea what it’s going to be.) Ah, then we know that for every subsequence, there are infinitely many which lie outside the ball .
What does our finite subcover look like? It’s a finite collection (say, many) of balls, and we know that there are infinitely many in any subsequence such that the are outside a given one of those balls. But this is a contradiction: take the subsequence of such that all of the in the subsequence lie outside ball 1. Then take a subsequence of that such that all the elements lie outside ball 2. Repeat: eventually we end up with a subsequence of such that all the elements lie in ball . This subsequence converges.
Proof
Suppose is a compact metric space, and take a sequence in . We show that there exists such that there is a subsequence of the such that .
Indeed, if the sequence gets arbitrarily close to then there is a subsequence of tending to (namely, let ; then pick such that ), so it is enough to show that there is some such that the sequence gets arbitrarily close to .
We show that this is true. Indeed, suppose not. Then for all there exists such that never gets within of (for all , some  the sequence might have started at , but we know it never returns after some point). Take a cover consisting of those ; by compactness, there is a finite subcover.
Now, we have that for the th ball in the cover, there exists such that never gets into the th ball for ; but there are only finitely many balls, so never gets into any of the balls for . But the finite collection of balls is a cover. That is, no is in , for  contradiction.
Postscript
That did indeed turn out to be the easier direction, then.
Hard direction
I’m not even going to begin attempting to find out what Lebesgue’s lemma is on my own, so I’ll just look it up and state it.
For a sequentially compact metric space , and an open cover , we have that there exists such that for all , there exists such that .
That is, “given any open cover, we can find a ballwidth such that for every point, a ball of that width lies entirely in some set in the cover”. It feels kind of related to Hausdorffness  while “metric spaces are Hausdorff” guarantees that we can wrap distinct points in nonoverlapping balls, Lebesgue’s lemma tells us that if our distinct points are not covered by the same set then we can separate them while remaining in those different sets in the cover.
OK, let’s go for a proof of this.
Proving Lebesgue’s lemma
Well, where can we start? To actually produce such a , it looks like we’d need to take some kind of minimum, and that would require a finite cover (which is assuming compactness). So that’s not a good place to start.
If we don’t know where to start, we contradict. Suppose there is no such that for all there exists such that . That is, for every there exists such that for all open sets in the cover, .
We’re in a sequentially compact space  we need a sequence, so that it can have a convergent subsequence. Mindlessly (nearly literally  I’m exhausted at the moment, having had an unusually long supervision since proving the easier direction), I’ll take and create a sequence such that is not wholly contained in any set of the cover. Then the has a convergent subsequence , say.
Picture pause. We’ve got our tending to , with everdecreasing balls around them. It seems sensible that at some point (since the position of the balls, the centre , is hardly changing, while the radius is getting smaller) the balls will get so small that they start being contained in some coverset.
That’s actually so close to a proof that I’ll write it up formally from this point.
Proof
Let be a sequentially compact metric space, and let be a cover (ranging over some indexing set). Assume for contradiction that for every there exists such that for all , .
Specialise to the sequence , and let be the corresponding . Then by sequential compactness, there exists a subsequence tending to some .
Now, for any . Also, because each is open, we have that for every such that there exists such that is wholly contained within .
Fix some such that , and let . Take such that (possible, because ). We have entirely contained in , because any point in the former ball is at most away from , which is itself at most away from ; hence any point in is at most away from . Picking (as well as such that ) ensures that .
But this is a contradiction: we have a ball entirely contained in some  namely  which contains a ball which is not entirely contained in  namely .
Proving the main theorem
OK, what do we have? We have that any open cover of a sequentially compact space allows us to draw a ball of predetermined width around each point, such that every ball is contained entirely in a set from the cover.
What do we want? We want every open cover of a sequentially compact space to have a finite subcover. ^{1}
OK, let’s do the only possible thing and take an open cover of a sequentially compact space. We might be able to build a finite subcover because of our predeterminedwidth balls, but I want a picture first.
Pictures (feel free to skip)
Let’s use and the cover where , and let’s suppose . (This clearly works as a in Lebesgue’s lemma.) Then a ball around any point remains in some set of the cover. The reason we have a finite subcover in this case is that the sets in the cover get smaller, so eventually we can just discard the ones which are too small to contain a ball. It turns out that wasn’t a great intuition guide  metric spaces can be a lot odder than that.
We want a space where the “balls get smaller” argument fails. Let’s use under the usual metric, and the cover along with some ball around . The reason this one works is because the ball around infinity makes sure we can throw out most of the sets of the cover, because they are contained in the ball around infinity. (A suitable is .)
End of pictures
Hmm, I don’t think I can easily come up with an example which explains exactly why the theorem is true. I slept on this, and got no further, so I looked up the next step: assume that it is not possible to cover the space with a finite number of . (This should perhaps have been suggested to me by my finite examples, in hindsight.) It turns out that this step makes it really easy.
Then for all finite sequences , there is a point such that is not in the cover; this forms a sequence which must have a convergent subsequence. Because the coveringballs are all of fixed width , we must have that eventually the points in the subsequence draw together enough to sit in the same ball.
Proof
Suppose is a sequentially compact metric space which is not compact, and fix an arbitrary open cover such that there is no finite subcover. Then by Lebesgue’s lemma, there is such that for all , there is such that .
Now, if it were possible to cover with a finite number of then we would have a finite subcover (namely, for each ). Hence it is impossible to cover with a finite number of . Take a sequence such that does not lie in any for (and where is arbitrary). Then there is a convergent subsequence , say; wlog let , for ease of notation (so the original sequence converged).
But this contradicts the requirement that always lies outside for : indeed, for sufficiently large , since convergent sequences are Cauchy.
Hence is compact.
Postscript
Ouch, that took a long time. There were three key ideas I ended up using.
 One direction is so easy that it’s one of the first theorems we prove in Analysis.
 Lebesgue’s lemma.
 Contradict ALL the things. (Every single major step in either direction of the proof is a contradiction, and everything just falls out.)

When do we want it? Now! ↩