Diagonalization is a poor example -- though I don't think Cantor's logic was widely accepted until the early 20th century -- but I think there are examples of proofs where mathematicians will accept the logic, but argue with it none the less:

The Banach-Tarski paradox comes to mind first. I don't think anyone argues that the proof is wrong, but you'll easily find people to argue that that very fact means that the full axiom of choice should be held in deep suspicion.

The 4-color map coloring theorem is more interesting in this thread, though; I think it's the best known example of a proof that offers little to no insight into why the theorem is true. I don't think any solution that requires breaking a problem into 1,936 special cases, and then mechanically checking each one of those cases, will ever lead to an understanding that makes the theorem "obvious".

I think once you understand the proof of 5 color theorem and believe the fact that the proof of 4 color theorem is more or less the same, but more hardcore, then it is as much insight as you can get.

Looking for insight is what many people do in mathematics, but nonetheless believing that every true fact is true for a reason is naive, just as naive as believing that every problem has to have a solution. So far, most of the time we succeed in explaining why true things are true, but it may be the case that some facts are true merely by combinatorics, and not for human-imaginable reason.

Sure, I would like to believe that there is a crucial observation we haven't made yet that makes 4 color theorem easy, just as it is for 6 color theorem. Nevertheless, I accept the fact that there may be no such thing and 4 color theorem holds just because the constraints force it to be.

I didn't mean to defend the idea that every fact is true for a reason.

I remember reading something of Chaitin's a couple of years ago that drove home the point that most mathematical facts are, in some fairly-well defined sense, true for no reason at all.

(Alas, I don't remember the argument well enough to re-cap it here.)

The axiom of choice also allows you to prove the existence of a strategy that allows near perfect predictive accuracy given a function and a set of all past points. The reals themselves admit many far out properties such as virtually all reals being "inaccessible" or the existence of a know it all number.

No, the problem that those who dislike the axiom of choice have is not inherent with the axiom but more the law of excluded middle. Constructivism has no rooms for such imaginings hence those who follow it are not happy with existential proofs. This more practical viewpoint will prove more profound IMHO just as bayesianism is winning the day. Just too many things connected.. types and terms in programs, intuitionistic logic, parts of physics, topoi, CCC.

You could apply the Lowenheim-Skolem theorem to the ZFC theory to obtain a countable model of set theory, but the object representing the set of real numbers in this model would still be "uncountable" inside of the model, altough clearly countable for us outside of it.