Why isn't the orbit-stabilizer theorem obvious?
Are you missing some mathematical subtlety by thinking that the Orbit-Stabilizer Theorem is very easy to prove? No, I don't think so: your proof is correct. Moreover, I skimmed Gowers's blog post and I don't think he says or intends to say that OST is in some way deep or nonobvious. In fact I think the goal of the post is essentially the opposite: to convince a beginner in abstract algebra that OST is, if not completely obvious, then quite easy: easy enough for someone to fully understand and remember the proof for ever after.
Gowers gives several different proofs (or maybe more accurately, several different expositions of a proof) of OST. Some of them take only a few lines. The fact that his whole discussion is rather lengthy is because he is trying to teach the obviousness of OST to someone who is not very comfortable or familiar with algebraic arguments. That is, by the way, a truly high-level teaching maneuver: it would be so much easier just to write down a three line proof and leave the task of interpreting it to the student.
Here is one big difference between OST and FTA: the statement of FTA is incredibly easy and familiar, using only concepts that are truly well known to most educated people. Moreover, since most people learn about factoring numbers in school, the level of experience with the conclusion of FTA is essentially maximal. That's not true for OST: how much time passes between most students' learning the definition of a group action and learning the statement of OST: a week? Less? It's a much different situation: modern mathematics has to be taught carefully so as not to be a sequence of answers to questions that no one has thought (or been given the chance to think) to ask.
OST is one of those theorems for which finding the statement is much more of an achievement than finding the proof. Such theorems are not inherently less useful than "deeper" theorems.
Let me take things a step further: what you state (which is what Gowers states) as OST is not what I think of as OST but rather a corollary of it. What I think of OST is a slightly more complicated statement that has the proof built into it to a larger degree. Namely:
Orbit Stabilizer Theorem: Let $G$ be a group acting on a set $X$. For $x \in X$, let $H_x$ be the stabilizer of $x$. Then there is a well-defined $G$-set isomorphism $\Phi: G/H_x \stackrel{\sim}{\rightarrow} G x$, $gH_x \mapsto gx$.
Notice that if you combine this with Lagrange's Theorem -- for a subgroup $H$ of a group we have $(\# H)(\# G/H) = \# G$ -- then we get the earlier statement of OST. But because we've put more into the statement (my statement is more "categorified" than yours, but let's not get into that here), it really is obvious. Or more precisely it is as obvious as it could possibly be: you need to know the meanings of all the terms involved, which for a beginner at algebra is hard work (which I think is why Gowers did not choose to state OST this way). If you know all the lingo, here is the proof:
$\bullet$ $\Phi$ is well-defined: if $gH_x = g' H_x$, then $ g^{-1}g' \in H_x$, so $g x = g (g^{-1} g' x) = g' x$.
$\bullet$ $\Phi$ is surjective: yes, it is!
$\bullet$ $\Phi$ is injective: If $\Phi(g H_x) = \Phi(g' H_x)$ then $gx = g' x$ so $g^{-1} g' x = x$, so $g^{-1} g' \in H_x$, so $g H_x = g' H_x$.
$\bullet$ $\Phi$ is a $G$-map: if $g \in G$ and $z = g' H_x \in G/H_x$, then $g\Phi(z) = g\Phi(g'H_x) = g(g'x) = (gg')x = \Phi((gg') H_x) = \Phi(g(g'H_x)) = \Phi(gz)$.
Note that in the above, I didn't try to write things as briefly as possible. On the contrary, I gave every detail (perhaps even obnoxiously so, in the last line). Whether something is "obvious" should not (I think) be measured in how many lines it takes to express the formal verification that you have in your head, but in how long it takes you to find the formal verification.
I would say that the theorem is pretty obvious.
However, if you look at Gowers's post, he is trying to do a bit more than just prove the theorem:
Firstly, he is not proceeding via quoting Lagrange's theorem, but is rather building the proof of this particular case of Lagrange's theorem into his argument.
Secondly, he is furthermore interpeting the cosets of $S_x$ as being precisely the elements of $G$ that take $x$ to some other element $y$. In other words, he is exhibiting the bijection $G/S_x \cong X$, in a fairly concrete way.
Finally, he is writing for beginners, and trying to put all his thoughts down on the page. The goal isn't to find the most succinct proof, but to try to make things clear to a motivated beginner who's willing to read the discussion carefully.
Conclusion: I don't think you're missing anything about the mathematics, but perhaps viewing Gowers's post through the prism of the most efficient proof is not quite the right thing to do.
I guess it's not obvious because you could conceive of one element of the set having a small stabilizer, but having a large number of group elements that send it to the same thing, or, more generally, having a different number of group elements sending one element to each of the other elements. Of course, if you know how a group action works, it is sort of trvial to see why this is impossible.