The orbit-stabilizer theorem is completely encoded by the equation
$$|G| = |\operatorname{Orb}(x)||\operatorname{Stab_G}(x)| $$
Most books/online presentations I am reading jump straight into this equation after the definitions are introduced.
Note that Lagrange Theorem tells us
$$|G| = [G: \operatorname{Stab}_G(x) ]|\operatorname{Stab}_G(x)|$$
So what prompts us to suggest $[G:\operatorname{Stab}_G(x)]$ is bijective with $|\operatorname{Orb}(x)|$?
Is it observed via a few examples and conjectured later?
Note I am not asking for the proof
Best Answer
I'm going to answer what I think is the literal question; if I've misunderstood the question, perhaps you can correct me.
I believe what you are asking is: How can a mathematician discover this theorem, knowing nothing about it beforehand?
Well, the answer is that they can't. That's not what happens. Just learning the abstract definition of a group, and maybe the definition of a group action, and maybe the definition of orbits, and then expecting that anyone can just say "Hey, here's a theorem!"... well... that's not how any mathematical theorems ever get discovered.
Instead, someone learns about actual groups, and actual group actions. They learn examples. They observe patterns. They stumble upon this particular pattern, noticing that it holds in a few different examples: the order of the group is the size of an orbit times the size if a stabilizer of a point in that orbit. They think "Huh... is this just a coincidence?" They might look for more examples to bolster the point, they might look (unsuccessfully) for counterexamples, which bolsters the point even more.
They become more and more convinced that the pattern is true.
And when a mathematician becomes convinced that something is true, then they are very motivated to prove that it is true.
And fortunately, the proof is easy.
I really don't think there's much more than that to say.