I need to prove the following lemma, let ~ be an equivalence relation on $X$, and let $\pi: X\rightarrow X/$~ be the quotient map. Let $f:X\rightarrow Y $ be an application. Then:
$f(x)=f(y) \; \forall \;x $ ~ $y$ if and only if $\exists$ unique $g:X/$~ $\rightarrow Y $ such that $f=g\circ\pi$
My attempt: Suppose such $g$ exists, then if $x$ ~ $y$ we have: $\pi(x)=\pi(y) \implies g(\pi(x))=g(\pi(y)) \implies f(x)=f(y) \;\forall\; x$ ~ $y$
which should give our inverse implication.
Suppose now that $f(x)=f(y) \; \forall \;x $ ~ $y$ then $f(x)=f(y) \iff \pi(x)=\pi(y)$ at this point I got kinda stuck, also I figured out I should at least assume I proved the existence of such application and therefore it would be worth a shot to try proving it's uniqueness.
For the uniqueness I just wrote suppose there exist another $h: X/$~ $\rightarrow Y $ then we have for the same initial reasoning $x$ ~ $y \implies f(x)=h(\pi(x))=h(\pi(y))=f(y)$ hence $f(x)=g(\pi(x))=h(\pi(x))$ for all $x$ having at least one equivalent element $y \in X$. (which seems to be close to what I wanted...)
I don't know whether or not my "proof" is correct, it's without any doubt incomplete, anyway, please be aware that I just read two pages about equivalences on my textbook, I know pretty much nothing about them so feel free to correct me and I would appreciate a "base level" explaination for the missing part of my "proof"...
The first part of the proof (existence of $g$ implies $f(x)=f(y) \ \forall x \sim y$) seems okay.
There is a mistake worth pointing out at the start of the next part: $f(x)=f(y) \not\Leftrightarrow \pi(x)=\pi(y)$. Only the implication pointing to the left was assumed, so it's not an "if and only if".
For every equivalence class $[z] \in X/\sim$, the image $f([z])$ is a single element of $Y$. That is to say, $f(x)=f(y) \ \forall x,y\in [z]$. We'll call this value just $f([z])$. Therefore, we can construct $g: X/\sim \longrightarrow Y$ which maps an equivalence class $[z]$ to the previously defined value $f([z])$. This $g$ satisfies the conditions we wanted (you can check that for yourself, but feel free to ask if it isn't clear!)
As for the uniqueness of the function $g$, what you wrote seems right, but you might want to refine it a bit further. $\pi(x)$ is surjective, and as such, $g \circ \pi = h \circ \pi$ implies that $g=h$.