Let $f : X \to Y$ be surjective. Show that there exists an injection $h : Y \to X$ such that $f \circ h = \operatorname{id}_Y$
This was my attempted solution.
My Proof: Restrict the domain of $X$ to $X'$ so that the restriction of $f$ to $X'$ (which I'll call $f' : X' \to Y$) is one-to-one. Now define $h : Y \to X$ by $h(y) = h(f'(x)) = x$. We can do this because $f$ is bijective, so $h(y)$ is well-defined.
Then $f \circ h : Y \to Y$ is given by $f(h(y)) = f(h(f'(x))) = f(x) = y$. To see why this is true, since $y \in Y$ and $f'$ is bijective from $X' \to Y$ there exists a unique $x \in X'$ such that $y = f'(x)$, then by well-definedness of $h$ we have $h(f'(x)) = x$ and since $f'(x) = y$ we must have $f(x) = y$ (since $f$ is a function). Hence $f \circ h = \operatorname{id}_Y$. $\square$
I'm not too happy with how rigorous my proof is. Is it rigorous enough? Do I need to constructively define $X'$?
By that I mean should I pick $y \in Y$ and then consider $f^{-1}[\{y\}]$, then taking the union of all preimages of $y$, we get $X$, which means $\bigcup_{y \in Y} f^{-1}[\{y\}] = X$.
Then we'd need to define a choice function (which relies on axiom of choice) (we can do this because $f$ is surjective and $\emptyset \not\in \{f^{-1}[\{y\}]\}_{y \in Y}$, in words since $f$ is surjective, the preimage of any $y \in Y$ is always nonempty). The choice function $\phi : \left\{f^{-1}[\{y\}]\right\}_{y \in Y} \to \left\{f^{-1}[\{y\}]\right\}_{y \in Y}$ is then defined on $X$ to be $\phi([f^{-1}[y]]) = x_y$ for some $x_y \in X$.
Then we define $X'$ to be the image of the choice function $\phi\left[\left\{f^{-1}[\{y\}]\right\}_{y \in Y}\right]$, that is $X' = \phi\left[\left\{f^{-1}[\{y\}]\right\}_{y \in Y}\right]$.
One can then define $f' : X \to Y$ and check that it's one to one and follow the proof as outlined above.
My lecturer did the following proof in class and I wasn't too happy with how rigorous it was either,
Lecturer's Proof:
Surjectivity of $f$ implies that for any $y \in $Y $f^{-1}[\{y\}] \neq \emptyset$. We define $h : Y \to X$ by $$h(y) = \text{some element of $f^{-1}[\{y\}]$}$$ and claim that $h$ is injective. Take $y_1 \neq y_2 \in Y$ then $f^{-1}[\{y_1\}] \cap f^{-1}[\{y_2\}] = \emptyset \implies h(y_1) \neq h(y_2)$.
Then $(f \circ h)(y) = f(h(y)) = f\left(\text{some element of $f^{-1}[\{y\}]$}\right) = y$. Hence $(f \circ h)(y) = y \implies f \circ h = \operatorname{id}_Y$. $\square$
My lecturer also makes subtle use of Axiom of Choice when he says "$\text{some element of $f^{-1}[\{y\}]$}$" because he needs a choice function to do just that.
My lecturer's proof may or may not have been a sketch of a proof, but is it rigorous enough? Is my proof rigorous enough?
Which of the two proofs would you think is better to write up as a proof of this theorem and why? (The reason I ask this is because I want to be rigorous in my proof writing but avoid being too pedantic)
Also out of curiosity is there any way to prove this without using Axiom of Choice? Because this seems like a really basic theorem from set theory which needs Axiom of Choice.