Why König's lemma isn't "obvious"?

I keep facing König's lemma "Every finitely branching infinite tree over $\mathbb{N}$ has infinite branch". Why it is not taken "obvious" but needs a careful proof?

It seems somewhat obvious, but I guess I overlook something.

If you mean take König's Lemma as almost an axiom of set theory, then you are on sketchy ground. While it is an intuitively obvious statement, note that at first glance so, too, is the following statement:

If $T$ is a tree of height $\omega_1$ in which all levels are countable, then there is a cofinal branch through $T$.

Unfortunately, the above is false, as the existence of Aronszajn trees immediately implies.

Lest you think that the heart of the difference is between $\omega$ and $\omega_1$ is that the former is closed under the (cardinal) exponential function $\lambda \mapsto 2^\lambda$ while the latter is not, note that even if we assume that $\kappa$ is an inaccessible cardinal, the statement

If $T$ is a tree of height $\kappa$ in which all levels have cardinality $< \kappa$, then there is a cofinal branch through $T$

is only true if, in addition, $\kappa$ is weakly compact.

We should be very careful when we ascribe the adjective obvious. We can prove König's Lemma carefully from the usual axioms, and so there is no harm in requiring that we do so.

Note, however, that a weak form of König's Lemma is taken as a basic axiom in certain important subsystems of second-order arithmetic, and many mathematically interesting theorems have been shown to be equivalent to this axiom over even weaker subsystems.

Two of the answers indicate how naive analogues of the result fail at larger cardinals. One test of obviousness of a result is how malleable it is, and these failures indicate that there are subtle obstructions.

An additional issue that the previous answers have not addressed is that even if a finite branching infinite tree is very easy to describe, this does not mean that any of its branches are. For an example of this issue see this answer, and for more refined versions, see the section on "computability aspects" in the Wikipedia entry for König's lemma.

Informally, we tend to say that a result stating the existence of an object is obvious, if the object can be easily computed from the data. In the present case, we can make this informal claim precise in the context of computability theory, and we have precise results showing that it fails. The harder it is to exhibit a branch, the less convincing our claim of obviousness. (And we can go further and combine both tests, seeing how much harder it is to exhibit a branch when we relax the assumption that the tree is finite branching: There are computable trees over $\mathbb N$ with branches but without hyperarithmetical branches.)

Yet a third test of obviousness lies in the ("direct") consequences of a principle, though this test perhaps carries less weight than the others. König's lemma for trees over $\mathbb N$ is equivalent over the weak theory $\mathsf{RCA}_0$ to the infinite Ramsey theorem for triples: Fix a finite set of colors, and assign a color to each $3$-sized set of natural numbers. Then there is an infinite subset of $\mathbb N$ all of whose $3$-sized subsets have the same color. (For $\mathsf{RCA}_0$ and reverse mathematics, see here.) Again, it is "computationally demanding" to exhibit such an infinite homogeneous set, even in cases where the coloring is very easy to describe. For a direct proof of the equivalence of these principles, see here. Ramsey's theorem for triples trivially implies the corresponding result for pairs. In his book Linear orderings, Joseph Rosenstein presents the following nice example of a simple coloring of the $2$-sized sets without simple infinite homogeneous sets: Linearly order the $2$-sized sets of natural numbers by saying that $\{a,b\}<\{c,d\}$ iff $a+b<c+d$ or ($a+b=c+d$ but $\min\{a,b\}<\min\{c,d\}$). This order begins $$\{0,1\}<\{0,2\}<\{0,3\}<\{1,2\}<\{0,4\}<\{1,3\}<\{0,5\}<\dots$$ Now color red those pairs $\{a,b\}$ that appear in even places in this enumeration, and color blue those that appear in odd places.

It might be instructive to see that Kőnig's lemma is false (and why it fails) in a computable setting. See this very clear exposition by Andrej Bauer and in particular theorem 3.5.

Look at an informal proof of König's Lemma (I mean a proof/proof[s] for the simple case[s] that interest you -- as others have already remarked, things quickly get hairier for trees of larger cardinality).

Look again carefully. Does it involve at some point appeal to a choice principle (some version of the Axiom of Choice)? If so, which version? If a version of Choice is appealed to, is that choice principle "obvious"? Why? And even if you would say that that choice principle is "obvious" too, shouldn't it be noted that we are appealing to a version of Choice?

I agree that out of context this lemma seems so trivial that it does not justify any discussion. In a slightly broader context, the non-triviality emerges, in (at least) two ways. First, there is the issue of what choice principle is required for the result. The result does seem very obvious but it does require a form of the axiom of choice, so (at least for logicians) it is no longer a trivial result.

Secondly, there is the natural question of extending the result to entertain larger cardinalities, than (surprisingly?) the situation is not so obvious at all (see Aronszajn tree). So, the special case of paths of countable cardinalities is true, but depends on some axiom of choice. But for higher cardinalities the situation is not so obvious. To me it seems the Lemma is less of a triviality then.