Proving the existence of a left-inverse for every injective function Trying to prove the theorem that for every injective function there exists a left-inverse of that function, I have conjured up the following proof:
Assume that $f$ indeed, is a function, chance, from $A$ to $B$; and that $f$ is injective. From this I am trying to prove the existence of a function, chance, $g$ from $B$ to $A$ such that $g\circ f(x) = x$. The existence of this function could be shown with a constructive proof. We may construct our left-inverse $g$ by defining its mapping such that if $y$ is an element of $B$, and $y$ belongs to $ranf$, then $g(y) = f^{-1}(y)$; and else, if $y$ does not belong to $ranf$ then $g(y) = a$ where $a$ is some arbitrary value in $A$. Therefore we have constructively defined the existence of this function $g$ for when $f$ is injective. Notice that that is all I needed for I have no intention in proving the converse (namely that the existence of the left-inverse proves that $f$ is injective).
Now I have three concerns pertaining to this proof. The first of which is if this proof is even valid. I ask of this for I am still new to formulating proofs, hence I require affirmation from those more advanced. Second, in constructing this function $g$, I have defined a part of it using $f^{-1}$. How is this permissable since I have not proved the existence of $f^{-1}$ in the first place; and so how am I using it to define but another function? Thirdly, is this kind of proof considered as a "constructive proof" as I have been calling it so far? Since I assumed we're proving the existence of a mathematical object by providing a construction for it, I have been calling it so. And would you also care to explain why this type of proof is valid (in addition to my first question) since all we have done is provided a way to construct this function $g$. Does the ability of being able to construct it properly prove its existence?
Thank you in advance
 A: Given a function $f\colon A\to B$, this function induces two functions, the direct image function, $\underline{f}\colon P(A)\to P(B)$ (where $P(X)$ is the power set of $X$, the set of all subsets of $X$), and the inverse image function, $\overline{f}\colon P(B)\to P(A)$, defined by:
$$\begin{align*}
\underline{f}(X) &= \{f(x)\mid x\in X\}\\
\overline{f}(Y) &= \{a\in A\mid f(a)\in Y\}.
\end{align*}$$
One can formalize the part of your argument that uses $f^{-1}$ by instead saying:

For $y\in\mathrm{ran}(f)$, let $g(y)$ be the unique element of $\overline{f}(\{y\})$,

by proving that because $f$ is injective, then $\overline{f}(\{y\})$ is a singleton, so "the unique element of $\overline{f}(\{y\})$" makes sense.
That said:
It is common to abuse notation and denote the inverse image function by $f$ (same as the original function), relying on the fact that one will usually be able to tell whether the input is an element of $X$ or a subset of $X$, so we will know if we mean the value of $f$, or the direct image of the set.
Likewise, it is common to again abuse notation and use $f^{-1}$ to denote the inverse image function, again relying on the hope that one will normally be able to tell whether we are applying it to a subset of $Y$ or to an element of $Y$. So one would write $f^{-1}(\{y\})$.
However, it is also common to further abuse notation and just write $f^{-1}(y)$ to mean $f^{-1}(\{y\})$, which really means $\overline{f}(\{y\})$. This seldom leads to problems. But when this causes confusing, then one should switch to one of the less abusive notations.

Now, as to your argument, there is a fly in the ointment: the "arbitrary value $a$". You can do this provided that $A$ is nonempty: just start by using existential instantiation to select an element of $A$ (ahead of time, once and for all), and proceed as you do.
But if $A$ is empty, then the only function $A\to B$ (for any set $B$) is the empty function (which consists of no ordered pairs). This functin is injective (by vacuity); but if $B\neq\varnothing$, then it has no left inverse, because there do not exist any functions $B\to\varnothing$ at all.
So what you stated as a theorem is actually false. The correct statement is:

Every injective function with non-empty domain has a left inverse.

(In fact, the converse is true with no qualifications: a function with a left inverse is necessarily injective.)

Finally, yes. A correct construction of an object proves the existence of the object. Usually the philosophical objections run the other way. Of course this requires an explicit construction which can be formalized in whatever logical system you are working in. Here, once you use the direct and inverse image functions, one can easily construct the inverse function explicitly, as the set
$$g = \left(\bigcup_{y\in\underline{f}(A)} \overline{f}(y)\times\{y\}\right)\cup \left( \{a\}\times (B\setminus \underline{f}(A))\right)$$
which is easily verified to be a function (defined as a set of ordered pairs) with the desired property, and which is definable in Set Theory.
