Rigour leading to insight
András, as you probably know, there are so many examples of what you're talking about that it's almost impossible to know where to start!  However, I think this question can actually be a good one, if people give examples from their own experience where the proof of a widely-believed conjecture in their subarea led to new insights.

When I was an undergrad, the first real TCS problem I tackled was this: what's the fastest quantum algorithm to evaluate an OR of &radic;n ANDs of &radic;n Boolean variables each?  It was painfully obvious to me and everyone else I talked to that the best you could do would be to apply Grover's algorithm recursively, both to the OR and to the ANDs.  This gave an O(&radic;n log(n)) upper bound.  (Actually you can shave off the log factor, but let's ignore that for now.)

To my enormous frustration, though, I was unable to prove any lower bound better than the trivial &Omega;(n1/4).  "Going physicist" and "handwaving the answer" never looked more appealing! :-D

But then, a few months later, Andris Ambainis came out with his quantum adversary method, whose main application at first was a &Omega;(&radic;n) lower bound for the OR-of-ANDs.  To prove this result, Andris imagined feeding a quantum algorithm a superposition of different inputs; he then studied how the entanglement between the inputs and the algorithm increased with each query the algorithm made.  He showed how this approach let you lower-bound quantum query complexity even for "messy," non-symmetric problems, by using only very general combinatorial properties of the function f that the quantum algorithm was trying to compute.

Far from just confirming that the quantum query complexity of one annoying problem was what everyone expected it to be, these techniques turned out to represent one of the biggest advances in quantum computing theory since Shor's and Grover's algorithms.  They've since been used to prove dozens of other quantum lower bounds, and were even repurposed to obtain new classical lower bounds.

Of course, this is "just another day in the wonderful world of math and TCS."  Even if everyone "already knows" X is true, proving X very often requires inventing new techniques that then get applied far beyond X, and in particular to problems for which the right answer was much less obvious a priori.