When learning mathematics should one prove everything one learns?
Solution 1:
You think you didn't get any particular new insights. This is probably true for the present, but no longer true for the future. When you will learn about the completion of a metric space using Cauchy sequences, you will just know the contruction already. And if go further on to study the completion of a uniform space using Cauchy filters, you will be pleased to see this is an abstract version of the construction on which you spent 9 hours.
Conclusion. The answer to your question heavily depends on your goals. If you just want to pass an exam and then forget about math, you probably don't need to worry about any single proof. Now if you want to become a mathematician, going deeper is a good idea in the long run.
Solution 2:
Knowing when to go through all the steps in detail belongs to that mysterious quality called mathematical maturity.
It doesn't sound like your instructor required you to write out all the details; you just felt the need, but regretted the time spent afterwards. Is this right?
Sometimes a book or paper will alert the reader, e.g., "after two pages of unenlightening computation, we find..." Other times you'll need to make your own call.
Perhaps after verifying the commutative law of addition for real numbers (defined via Cauchy sequences), you said to yourself, "OK, it's going to go the same way for the other algebraic laws: associative law for addition, commutative and associative laws for multiplication, etc." Your instinct would have been right.
On the other hand, good instincts would probably tell you, "I have to see how the completeness of the reals follows from the construction." Also the fact that the operations are well-defined, i.e., don't depend on the choice of representatives. (But it's enough to check for one operation.)
Two further thoughts.
Back in the day, mathematicians like Euler and Gauss did reams of calculations. You might wonder, "How did they ever come up with that theorem?" Part of the answer seems to be, they worked out tons of examples and noticed patterns. Nowadays we have software to shoulder much of the burden, but I've heard it suggested that something is lost by not being so "close to the metal".
There are some famous cases where people's intuition tripped them up. One incorrect "proof" of Fermat's last theorem simply assumed that unique factorization held for all algebraic number fields (Lamé, 1847). Not true!
Solution 3:
I'm afraid you can't get away without proving things in mathematics (although you certainly don't have to verify every detail of every proof that you read). You have a good point that the usual constructions of the real numbers are often presented as if the verification of the required properties is an easy exercise, whereas the very readable and detailed account in Landau's Foundations of Analysis (using Dedekind sections) occupies over 90 pages. To quote John H. Conway (On Numbers and Games p. 26):
In practice the main problem is to avoid tedious case discussions. [Nobody. can seriously pretend that he has ever discussed even eight cases in such a theorem [the construction of $\Bbb{R}$ from $\Bbb{Q}$ via Dedekind sections or Cauchy sequences] - yet I have seen a presentation in which one theorem has 64 cases.]
On the other hand, many people (myself included) have carried out complete formal verifications of such constructions with some computer assistance, in systems such as HOL. But even with machine support, it is good to use nicer methods than crude case analysis. One simple observation is that once you have shown that the additive structure $(\Bbb{R}, 0, +, <)$ is a complete totally ordered abelian group, you can define and verify the multiplicative structure by studying the order-preserving homomorphisms of $(\Bbb{R}, 0, +, <)$, which is both more interesting and less error-prone than working directly with Cauchy sequences or Dedekind sections.
Schanuel's Eudoxus Reals provide another entertaining alternative construction of the real numbers involving an interesting investigation of self-mappings of the integers that aren't quite additive homomorphisms.
Solution 4:
There is a trend toward excessive formalism in mathematics which is why you spent the 9 hours to begin with. Surely rigor is an important part of mathematics, but the learning of mathematics is a more mysterious process that does not follow the "axiom-definition-theorem-proof" pattern. I suggest you read up on some excellent pedagogues we have out there, like Polya and Freudenthal. It may save you a lot of time in the long run.