You mentioned König's Tree Lemma in the question. There is a very useful refinement that is often usedcommon in computability theory and related areas:
Every computable infinite subtree of $\{0,1\}^{<\infty}$ has an infinite branch with a low Turing degree.
A set $A$ has low Turing degree if the halting problem relative to $A$ has the same Turing degree as the (unrelativized) halting problem. In particular, a set that has low Turing degree is incomplete (does not compute the halting set). Thus, the Low Basis Theorem is often used to show that a particular problem has a solution which has strictly lower complexity than the halting problem.
Another interesting feature of the Low Basis Theorem is that it is iterable. Indeed, the therorem relativizes very easily. Since being low relative to a low degree is the same as being plainly low, the theorem can be applied multiple times in a row to achieve the same outcome.
Also note that it is very important that the tree be a subtree of $\{0,1\}^{<\infty}$ (or, more generally, that the tree is computably bounded). Indeed, there are computable finitely branching subtrees of $\mathbb{N}^{<\infty}$ all of whose infinite branches compute the halting set. However, the Kreisel Basis Theorem guarantees that every computable finitely branching subtree of $\mathbb{N}^{<\infty}$ with infinite height has an infinite branch which is computable from the halting set.
An interesting application of the Low Basis Theorem is that Peano Arithmetic (PA), Zermelo-Fraenkel set theory (ZF), and all other consistent axiomatizable theories have completions that have low degree, and hence do not compute the halting set.