Let $A$ denote a finite set, equipped with the discrete topology, and consider the product topology on $A^{\mathbb N}$, i.e. the set of all infinite sequences over $A$. Denote by $\pi_i : A^{\mathbb N} \to A$ the projection onto the $i$-te coordinate, then finite intersection of sets of inverse images of these projection maps are called cylinder sets, i.e. $C$ is a cylinder set iff the set $\{ i \in \mathbb N : \pi_i(C) \ne A \}$ is finite. Now a set $B \subseteq A^{\mathbb N}$ is clopen iff it is a finite intersection of cylinder sets.
I am looking for a proof of this fact using König's Lemma. I have an intuitive idea, namely that $A^{\mathbb N}$ is a finite branching, infinite and complete tree. Now consider a clopen set $B$, then we have $$ B = \bigcup_{i\in I} C_i $$ where the $C_i$ are cylinder sets. Now for a cylinder set $C$ let $ind(C)$ be the maximal index such that $\pi_i(C) \ne A$ and denote by $N(C, n) = \{ (a_1, \ldots, a_n) \in C \}$ the set of all finite sequences up to $n$ which build up initial segments in $C$, then with $n = ind(C)$ we can write each cylinder set as a finite union $$ C = \bigcup_{(a_1, \ldots, a_n) \in N(C, n)} \{ a_1 \} \times \cdots \times \{ a_n \} \times A \times A \times A \times \cdots $$ and therefore each set $B$ could be written as a union of such "initial segment" cylinder sets. Now the sets off all such initial segments in $B$ describes also a finite branching subtree of $A^{\mathbb N}$ as the set of all vertexes that are reachable. Here I guess I have to select a minimal set such that no initial segment is the prefix of another, and if this set is finite then I get, by König's Lemma, some limit point that is not in $B$. But I have difficulty in making this argument formal.
Let me give an example, consider the set $$ B = \{ 1 \} \times A^{\mathbb N} \cup \{ 0 \} \times \{ 1 \} \times A^{\mathbb N} \cup\{ 0 \}\times \{0\}\times \{1\} \times A^{\mathbb N} \cup \ldots $$ then the initial segments $1,01,001,0001,\ldots$ are in some sense minimal that none could be taken away or the union could be written with lesser sets, then by König an infinite path in the tree described by them is $(0,0,0,0,0,\ldots) \in A^{\mathbb N}$. So here I am stuck in making this formal, as this set lies in no base set by which the $B$ is formed, also the interplay between finite sequences and infinite sequences, how could this be made formal so that a beautiful proof results?
A proof by a direct compactness argument is given here, but I am specifically looking for a proof using König's Lemma.
For $n\in\Bbb N$ and $\sigma=\langle a_0,\ldots,a_{n-1}\rangle\in A^n$ let
$$B(\sigma)=\left\{x\in A^{\Bbb N}:x_k=a_k\text{ for all }k<n\right\}\;;$$
$B(\sigma)$ is a cylinder set. Let $\mathscr{B}_n=\{B(\sigma):\sigma\in A^n\}$, and let $\mathscr{B}=\bigcup_{n\in\Bbb N}\mathscr{B}_n$. Then $\mathscr{B}$ is a base of cylinder sets for $A^{\Bbb N}$, $\langle\mathscr{B},\supseteq\rangle$ is a tree, the sets $\mathscr{B}_n$ are the levels of the $\mathscr{B}$, and each of these levels is finite. It’s easy to check that every cylinder set is a finite union of members of $\mathscr{B}$.
Suppose that $U\subseteq A^{\Bbb N}$ is open but not a finite union of cylinder sets. Let
$$\mathscr{T}=\{B\in\mathscr{B}:B\cap U\ne\varnothing\ne B\setminus U\}\;;$$
$\mathscr{T}$ is a subtree of $\mathscr{B}$. If $\mathscr{T}\cap\mathscr{B}_n=\varnothing$ for some $n\in\Bbb N$, then
$$U=\bigcup\{B\in\mathscr{B}_n:B\subseteq U\}$$
is a finite union of cylinder sets, so $\mathscr{T}$ meets every level of $\mathscr{B}$ and is therefore infinite. By König’s lemma there is a branch $\mathscr{C}$ through $\mathscr{T}$. There is then an $x\in A^{\Bbb N}$ such that
$$\mathscr{C}=\{B(x\upharpoonright n):n\in\Bbb N\}\;,$$
and clearly $\bigcap\mathscr{C}=\{x\}$. $\mathscr{C}$ is a local base at $x$, so $x\in(\operatorname{cl}U)\cap\operatorname{cl}(A^{\Bbb N}\setminus U)$, and $U$ is not clopen.