We've defined relations and equivalence relations a few days ago at university.
I tried to look at them a bit more abstract and came up with two lemmata. I am going to write them down with my proofs and it would be nice to let me know what you think of them.
Are they useful/useless, are the proofs right/wrong etc...
Lemma 1: Be $Z$ a set and be $\sim$ an equivalence relation on a set $M$. Be $f$ a function with $f: M \rightarrow Z$ and be $g$ a function with $g: M \rightarrow M$
$f$ and $g$ also fulfill the following: \begin{align} &\forall x,y \in M: f(x) = f(y) \implies g(x) = g(y)\\ &\forall x \in M: x \sim g(x) \end{align}
It follows: $$\forall x,y \in M: f(x) = f(y) \implies x \sim y$$
Proof. Be $x,y \in M$ and be $f(x) = f(y)$. It follows $g(x) = g(y)$ and because $\sim$ is an equivalence relation it holds: $$x \sim g(x) \sim g(y) \sim y \quad \square$$
Lemma 2: Be $Z$ a set and be $\sim$ an equivalence relation on a set $M$. Be $f$ a (surjective) function with $f: M \rightarrow Z$. Be also $X \subseteq M$ and be $f \mid_X$ bijective. $f$ also fulfills the following: $$\forall x,y \in M: x \sim y \Longleftrightarrow f(x) = f(y)$$
It follows: $$M/_\sim = \{[a]_\sim \mid a \in X\}$$ and $$\forall x,y \in X: x \sim y \implies x=y$$
Proof. $M/_\sim \supseteq \{[a]_\sim \mid a \in X\}$ is trivial. Be $x \in M/_\sim$ and be $x' \in x$. It holds $f(x') \in Z$. $f \mid_X$ is surjective, hence there is a $y \in X$ with: $$f(y) = f(x')$$ Hence $y \sim x'$, which yields $[y]_\sim = [x']_\sim$. Finally: $$M/_\sim \subseteq \{[a]_\sim \mid a \in X\}$$
Be now $x,y \in X$ and be $x \sim y$. It follows $f(x) = f(y)$ and since $f \mid_X$ is injective, we get: $$x=y \quad \square$$
Intro:
Every function $h:X\rightarrow Z$ induces an equivalence relation $\sim_{h}$ on set $X$. This by $u\sim_{h}v\iff h\left(u\right)=h\left(v\right)$. Let $\left[x\right]_{h}$ denote the equivalence class represented by $x\in X$. Then $\left[x\right]_{h}=h^{-1}\left(\left\{ h\left(x\right)\right\} \right)$.
Conversely if $\sim$ is some equivalence relation on $X$ then $\sim=\sim_{\nu}$ where $\nu:X\rightarrow X/\sim$ is the natural map that send $x$ to the equivalence class that contains $x$.
If $P$ denotes a partition of $X$ then the relation $\sim$ on $X$ defined by $$u\sim v\iff u,v\text{ belong to the same element of }P$$ is an equivalence relation and its equivalence classes are the elements of $P$.
In that sense there is a strong relation between functions, equivalence relations and partitions.
It is a very good custom to keep this connection in mind.
Your lemma1 in this light.
In your first lemma we have $f\left(x\right)=f\left(y\right)\implies g\left(x\right)=g\left(y\right)$. This is sometimes expressed as: "function $g$ respects function $f$". It means exactly that $\left[x\right]_{f}\subseteq\left[x\right]_{g}$ for each $x\in X$. In fact the partition induced by function $f$ is finer than the partition induced by function $g$.
This will be the case if and only if: $$g=h\circ f\text { for some function }h$$ It is easy to prove that this condition is sufficient. Conversely we can prescribe such function $h$ by stating that $h\left(z\right):=f\left(x\right)$ when $f\left(x\right)=z$. If no such $x$ can be found then for $h\left(z\right)$ we can take any element in $M$. Exactly the fact that $g$ respects $f$ guarantees that $h$ is well defined. If $f$ is surjective then $h$ is unique :for each $z\in Z$ we can find an $x$ with $z=f(x)$ and $h(z)=g(x)$.
Prescribing $\nu:M\rightarrow M/\sim$ by $x\mapsto\left[x\right]_{\sim}$ the statement $\forall x\in M\left[x\sim g\left(x\right)\right]$ is the same as $\nu=\nu\circ g$. Combined with $g=h\circ f$ we find: $\nu=\nu\circ\left(h\circ f\right)=\left(\nu\circ h\right)\circ f$. So $\nu$ respects $f$ wich means exactly that $f\left(x\right)=f\left(y\right)\implies x\sim y$.
Your lemma2 in this light.
Let me first say that your lemma is okay again. Defined like this we have $\sim=\sim_{f}$. The injectivity of $f\upharpoonleft X$ ensures that $\left[x\right]_{f}\cap X=\left\{ x\right\} $ for each $x\in X$ (so that $x\sim y\implies x=y$ for $x,y\in X$ ). The surjectivity of $f\upharpoonleft X$ ensures that collection $\left\{ \left[x\right]_{f}:x\in X\right\} $ is a partition of $M$ (so that $\left\{ \left[x\right]_{f}:x\in X\right\} =\left\{ \left[x\right]_{f}:x\in M\right\} $ ).
Sidenote:
For every $z\in Z$ there is a unique $x\in X\subseteq M$ with $f\left(x\right)=z$. This enables us to define a function $s:Z\rightarrow M$ that sends each $z\in Z$ to this unique $x$. Then $f\circ s=1_{Z}$. Let $r:=s\circ f$. Then $r$ respects $f$. But also we have $f=1_{Z}\circ f=f\circ s\circ f=f\circ r$ wich means that conversely $f$ respects $r$. This means exactly that $\sim_{r}=\sim_{f}$. Characteristic for function $r:M\rightarrow M$ is the property $r\circ r=r$. For every partition $P$ on set $X$ you can easily construct such a function. In each $p\in P$ select some representant $x_{p}\in p$ and prescribe the function by stating that elements of $p\subset X$ are sent to $x_{p}$.