I've tried to absorb several of the features of the Axiom of Choice, as well as its distinction between existential instantiation , but many deficits remain. The aim of this question is to address at least two of these deficits.
The implication
If $f: S \to T$ is a surjective function, then $f$ has a right inverse $g: T \to S$ such that $f \circ g = \text{Id}_T$, where $\text{Id}_T:=\{\langle t,t \rangle \ |\ t \in T\}$
requires the invocation of the Axiom of Choice (for the general case where $f$ is not also injective).
The need for the AoC occurs when we are trying to construct the function $g$ at the following stage:
Let $s$ be an element in $S$ such that $f(s)=t$. Let $X_s$ be the set of elements in $S$ that are mapped to $t$ through $f$. Equivalently, $f[X_s]=\{t\}$. Now, when it comes to determining how to construct $g$, we run into the issue of how to define $g(t)$ so that $f(g(t))=t$. Specifically, which $x \in X_s$ should $g(t)$ map to?
I believe there are two "bad scenarios" that need to be accounted for (but I have a question on the second scenario):
Firstly, let $X_s$ be uncountably infinite. Based on what I know, this is "bad" because $X_s$ can therefore not be related to the natural numbers $\omega$, which means I cannot select a minimum element in $X_s$. If I were able to select a minimal element from $X_s$, I would gain access to a definable rule (i.e. a rule that I could express using some finite combination of symbols) that I can use to describe $g$...thus necessarily circumventing the need for the Axiom of Choice.
Secondly, there are $3$ different possibilities when it comes to the number of $X_s$-like sets that arise in our function $f$. There could be
i) a finite number of $X_s$-like sets
ii) a countably infinite number of $X_s$-like sets
iii) an uncountably infinite number of $X_s$-like sets
For clarification, by "number of $X_s$-like sets", I mean the number of "instances of non-injectivity". Using "finite" as an example, suppose there are 4 elements in $T$ ($t_1,t_2,t_3, t_4$) that are "non-injectively mapped" into...i.e. $f[X']=\{t_1\}, f[X'']=\{t_2\}, f[X''']=\{t_3\}$, and $f[X'''']=\{t_4\}$.
I assume that any three of these possibilities (in conjunction with the first bad scenario) require the invocation of the Axiom of Choice...and perhaps the manner in which AoC is invoked is the same regardless of which three is encountered. Is this correct?
The equivalent variant of the Axiom of Choice that I have seen used in the above context of the surjectivity proof is the following:
Every relation contains a function having the same domain...symbolically: $\forall x \in T \exists y \in S \big[R(x,y)\big] \rightarrow \exists g \big[g:T \to S \land \forall x \in T [R(x,g(x))]\big]$
In essence, this is saying, "$f$ may not be injective, so $f^{-1}$ may not qualify as a function...but by AoC, we claim that there exists a function-variant of $f^{-1}$, call it $g$" (as a side note, this $g$ must be injective by default, because $f$ was defined as a function). Importantly, my understanding is that AoC does not give us a "rule" for the assignment choice $g$ makes when dealing with the $X_s$-like sets. This $g$ is then used to complete the surjectivity proof.
My confusion with this invocation of the AoC is that I cannot see why it is any different from the claim that the set $S^T$ exists. And thus, because $f:S \to T$ is surjective (which says something about the size of $T$ relative to $S$), there must necessarily be a $g \in S^T$ that satisfies our criteria for $f\circ g = \text{Id}_T$. In the same way as with the AoC, we are not given a "rule" for this $g$. But we know it exists.
So why do I need to Axiom of Choice here? Don't I effectively use the $g$ from $S^T$ as blindly as I do the $g$ from the AoC (blind in the sense that I do not know the specific assignment rule associated with $g$)?
First of all, you're falling into the naive pitfall of separating into cases, or at least the wrong cases, when that is not necessary. There's no need to distinguish between countable and uncountable cases. Finite and infinite cases are the correct distinction, and even that could be argued to be wrong.
The correct cases is "$\sf ZF$ proves the existence of a choice function" and its negation. And yes, this would depend on $S$ and $T$. So for example, if $S$ is well-ordered (which can be so much more than just $\omega$), then we can choose the minimum from each $X_s$. Or, if $T$ is finite, then we can prove by induction that a choice function exists.
Starting to break into cases is natural, it's a good approach of sorting out "what do I know is possible", but it's not always the right one, and it's easy to make mistakes that will just pull you deeper into this knot of not understanding.
The difference between using $\sf AC$ and using Existential Instantiation is obvious: EI can be used finitely many times. So if $T$ is not finite1, we cannot repeatedly use EI to exhaust the choices necessary for the inverse.
The axiom of choice, however, simply posits the existence of functions with the desired property: since $f$ is surjective, for all $t\in T$, $f^{-1}(t)$ is non-empty, so by $\sf AC$ a choice function from $\{f^{-1}(t)\mid t\in T\}$ exists. Now we use EI once and we have such a choice function in our hands.
Your question has been addressed before on the site. The existence of functions, or the existence of a relation $R\subseteq T\times S$ whose domain is $T$ (in this case, $f^{-1}$) is not enough to conclude that a function with the wanted properties exists. To prove it exists, you need to be able to use the axioms for a proof. The obvious candidate is Separation or Replacement. But to invoke those you need to have a defining property (which may or may not already be a functional one). So, what is that property?
If $S=\{x,y\}$ and $T=\{0\}$, consider $f(x)=f(y)=0$. Now to construct $g$ we need to choose an element for which $g$ maps $0$. Is it $x$? Is it $y$? Both options are good. But there's no preference for either one here, so we have to "leave it to chance": let the EI work its magic and choose one of them. But if we have to make infinitely many choices, how can you do that without already appealing to the axiom of choice?