Here is a cute application of Baire category theorem that is in the spirit of your examples.

Assume that $f: {\mathbb{R}}^{\mathbb{N}} \rightarrow \mathbb{R}$ is a Borel measurable function with the property that if $x \sim y$, then $f(x)=f(y)$, where $x \sim y$ if and only if $\{x_n: n \in \mathbb{N}\}=\{y_n: n \in \mathbb{N}\}$ for $x,y \in {\mathbb{R}}^{\mathbb{N}}$. Then, there exists $x \in {\mathbb{R}}^{\mathbb{N}}$ such that $f(x)=x_k$ for some $k \in \mathbb{N}$.

We can consider Cantor's diagonalization argument as a Borel map taking a sequence of reals and producing a real different than any element in the list. This theorem tells you that there is no Borel way to do diagonalization in a "uniform" way. "Uniform" here means that the sequences consisting of the same elements are diagonalized with the same element.

This is the most basic version of Friedman's Borel diagonalization theorem. In On the necessary use of abstract set theory, Advances in Mathematics, 41 (1981), 209-280, Harvey Friedman proves this result (Proposition C, p. 229) using a forcing argument. Though, in the appendix of the same paper, he gives another proof based on Baire category theorem.

Here is a cute application of Baire category theorem that is in the spirit of your examples.

Assume that $f: {\mathbb{R}}^{\mathbb{N}} \rightarrow \mathbb{R}$ is a Borel measurable function with the property that if $x =^+ y$, then $f(x)=f(y)$, where $x =^+ y$ if and only if $\{x_n: n \in \mathbb{N}\}=\{y_n: n \in \mathbb{N}\}$ for $x,y \in {\mathbb{R}}^{\mathbb{N}}$. Then, there exists $x \in {\mathbb{R}}^{\mathbb{N}}$ such that $f(x)=x_k$ for some $k \in \mathbb{N}$.

We can consider Cantor's diagonalization argument as a Borel map taking a sequence of reals and producing a real different than any element in the sequence. This theorem tells you that there is no Borel way to do diagonalization in a "uniform" way. "Uniform" here means that the sequences consisting of the same elements are diagonalized with the same element.

This is the most basic version of Friedman's Borel diagonalization theorem. In On the necessary use of abstract set theory, Advances in Mathematics, 41 (1981), 209-280, Harvey Friedman proves this result (Proposition C, p. 229) using a forcing argument. Though, in the appendix of the same paper, he gives another proof based on the Baire category theorem. An unusual feature of this proof is that you pass to a different space and apply Baire category to ${\mathbb{R}}^{\mathbb{N}}$ where $\mathbb{R}$ is endowed with the discrete topology.

Here is a cute application of Baire category theorem that is in the spirit of your examples.

Assume that $f: {\mathbb{R}}^{\mathbb{N}} \rightarrow \mathbb{R}$ is a Borel measurable function with the property that if $x \sim y$, then $f(x)=f(y)$, where $x \sim y$ if and only if $\{x_n: n \in \mathbb{N}\}=\{y_n: n \in \mathbb{N}\}$ for $x,y \in {\mathbb{R}}^{\mathbb{N}}$. Then, there exists $x \in {\mathbb{R}}^{\mathbb{N}}$ such that $f(x)=x_k$ for some $k \in \mathbb{N}$.

In other words, there is no Borel way to do Cantor's diagonalization argument in a "uniform" way. "Uniform" here means that the sequences consisting of same elements are diagonalized with the same element.

This is the most basic version of Friedman's Borel diagonalization theorem. In On the necessary use of abstract set theory, Advances in Mathematics, 41 (1981), 209-280, Harvey Friedman proves this result (Proposition C, p. 229) using a forcing argument. Though, in the appendix of the same paper, he gives another proof based on Baire category theorem.

Here is a cute application of Baire category theorem that is in the spirit of your examples.

Assume that $f: {\mathbb{R}}^{\mathbb{N}} \rightarrow \mathbb{R}$ is a Borel measurable function with the property that if $x \sim y$, then $f(x)=f(y)$, where $x \sim y$ if and only if $\{x_n: n \in \mathbb{N}\}=\{y_n: n \in \mathbb{N}\}$ for $x,y \in {\mathbb{R}}^{\mathbb{N}}$. Then, there exists $x \in {\mathbb{R}}^{\mathbb{N}}$ such that $f(x)=x_k$ for some $k \in \mathbb{N}$.

We can consider Cantor's diagonalization argument as a Borel map taking a sequence of reals and producing a real different than any element in the list. This theorem tells you that there is no Borel way to do diagonalization in a "uniform" way. "Uniform" here means that the sequences consisting of the same elements are diagonalized with the same element.

This is the most basic version of Friedman's Borel diagonalization theorem. In On the necessary use of abstract set theory, Advances in Mathematics, 41 (1981), 209-280, Harvey Friedman proves this result (Proposition C, p. 229) using a forcing argument. Though, in the appendix of the same paper, he gives another proof based on Baire category theorem.