A non-mechanical way to get an infinite decidable subset of a Turing-recognizable language?
Let $\Sigma$ be an alphabet, let $\mathcal{R}$ be the collection of all recognizable subsets (languages) of $\Sigma^{*}$ and let $\mathcal{D}$ be the collection of all decidable subsets of $\Sigma^{*}$.

Say that $n \in \mathbb{N}$ is a code for $L \in \mathcal{R}$ if the Turing machine encoded by the number $n$ (via some Gödel encoding of Turing machines) recognizes $L$. Let us write $L_n$ for the set that is recognized by the $n$-th Turing machine.

Similarly, say that $n$ is a code of $D \in \mathcal{D}$ if the $n$-th Turing machine is the decider for $D$. If $n$ is the code of a decider (not every number is!) then we write $D_n$ for the set it decides.

Consider the statement: "For every infinite $L \in \mathcal{R}$ there is an infinite $D \in \mathcal{D}$ such that $D \subseteq L$."

You are asking whether we can prove the statement by giving an effective procedure which assigns to every $L$ a corresponding $D$ in such a way that $D$ does not depend on the choice of the code of $L$. (Clearly, we can do this inefectively by an application of the axiom of choice.) More precisely, the question seems to be whether there a computable map $f$ such that


if $n$ codes an infinite $L \in \mathcal{R}$ then $f(n)$ codes an infinite $D \in \mathcal{D}$ such that $D \subseteq L$, and
if $L_n = L_m$ then $D_{f(n)} = D_{f(m)}$.


The answer is no, there is no such map: you must appeal to a particular recognizer for $L$ and obtain a $D$ which depends on the recognizer.

To prove that this is really so we appeal to Rice's theorem. Suppose we had such an $f$. There exists $n, m, a \in \mathbb{N}$ such that $a \in D_n$ and $a \not \in D_m$. The subset $S \subseteq \mathcal{R}$ defined by
$$L \in S \iff \exists n \,.\, L = L_n \land a \in D_{f(n)}$$
is a non-trivial decidable subset of $\mathcal{R}$, which violates Rice's theorem.