Proof if $g$ is surjective, then $g\circ f=I_X$.

Let $x \in X$ be random.

Do not use the term "random" unless you're dealing with probability. It has a precise meaning. Instead, say "Consider some arbitrary $x \in X$."

Assuming $g$ is surjective,

We should assume $g$ is surjective before taking our arbitrary $x$ if we're being extremely formal.

therefore for all $x \in X$ we have a $y \in Y$, such that $x = g(y)$

You've just introduced a new bound variable $x$ which is different from the variable $x$ that you introduced earlier.

Therefore $g(y) = x$

We have not picked any specific $y$ such that $g(y) = x$. We have only asserted that $\forall x \in X \exists y \in Y (x = g(y))$.

The more precise way to prove this is:

Suppose $g$ is surjective. We wish to show that $g \circ f = I_X$; by function extensionality, it suffices to show that for all $x \in X$, $(g \circ f)(x) = I_X(x)$.

Now consider an arbitrary $x \in X$. Since we assumed $g$ is surjective, we can take some $y \in Y$ such that $x = g(y)$. Then we see that

$\begin{equation} \begin{split} (g \circ f)(x) &= g(f(x)) \\ &= g(f(g(y))) \\ &= g((f \circ g)(y)) \\ &= g(I_Y(y)) \\ &= g(y) \\ &= x \\ &= I_X(x) \end{split} \end{equation}$

which is the very thing we sought to show. $\square$