How do I prove that a function is well defined?

When we write $f\colon X\to Y$ we say three things:

1. $f\subseteq X\times Y$.
2. The domain of $f$ is $X$.
3. Whenever $\langle x,y_1\rangle,\langle x,y_2\rangle\in f$ then $y_1=y_2$. In this case whenever $\langle x,y\rangle\in f$ we denote $y$ by $f(x)$.

So to say that something is well-defined is to say that all three things are true. If we know some of these we only need to verify the rest, for example if we know that $f$ has the third property (so it is a function) we need to verify its domain is $X$ and the range is a subset of $Y$. If we know those things we need to verify the third condition.

But, and that's important, if we do not know that $f$ satisfies the third condition we cannot write $f(x)$ because that term assumes that there is a unique definition for that element of $Y$.

Okay, I'm trying to answer my own question here. This is how a function is defined in "Reading, Writing, and Proving: A Closer Look at Mathematics".

Recall that a relation $f$ from $X$ to $Y$ is a subset of $X\times Y$, and therefore the elements of $f$ are ordered pairs $(x,y)$.

A function $f:X\to Y$ is a relation $f$ from $X$ to $Y$ satisfying:
i). $\forall x\in X ,\exists y\in Y :(x,y)\in f $
ii). $\forall x\in X,\forall y_1,y_2 \in Y : (x,y_1),(x,y_2)\in f\implies y_1=y_2$

An function is often called an map or a mapping. The set is $X$ is called the domain and denoted by $\text{dom}(f)$, and the set $Y$ is called the codomain and denoted by $\text{cod}(f)$. When we know what these two sets are and the two conditions are satisfied, we say that $f$ is a well defined function.

Condition i) makes sure that each element in $X$ is related to some element of $Y$, while condition ii) makes sure that no element in $X$ is related to more than one element of $Y$. Note that it may be the case that an element of $Y$ has no element in $X$ to which it is related; or an element of $Y$ could be related to more than one element of $X$.

Therefore, like Asaf Karagila mentioned, if you want to prove that $f$ is a well defined funciton, and the domain $X$ and codomain $Y$ are given, then you need to show that:

1. $f$ is a relation from $X$ to $Y$
   $f\subseteq X\times Y$

2. The domain of $f$ is $X$, every element in $X$ is related to some element of $Y$ $\forall x\in X ,\exists y\in Y :(x,y)\in f $

3. No element of $X$ is related to more than one element of $Y$ $\forall x\in X,\forall y_1,y_2 \in Y : (x,y_1),(x,y_2)\in f\implies y_1=y_2$

The issue here is that $[x]_{12}$ means an equivalence class of elements of $\def\Z{\mathbb Z}\Z$, specifically the class of all $y$ such that $x-y$ is a multiple of 12. You have some procedure that says you are given one of these equivalence classes, $[x]_{12}$, and you are calculating a value by selecting a representative element, say $y$, from $[x]_{12}$, and then doing something to that representative to get the answer, in this case the object $[y]_4$. But this does not make sense—it is not "well defined"—if the value you get for the given class $[x]_{12}$ depends on which representative $y$ you selected from $[x]_{12}$.

So your job here is to show that the result you get does not depend on which $y$ you pick as a representative of $[x]_{12}$.

As a counterexample, let's consider the "function" that says that $f\left(\frac ab\right) = a+ b$. So for example $f\left(\frac 12\right) = 3$, simple. But no, wait. $\frac12$ is actually an equivalence class; it is the class $\left[\frac12\right]_\mathbb Q$, which contains not only $\frac12$ but also $\frac24$, $\frac36$, and $\frac{576}{288}$. And with the definition given, the value of $f$ does depend on which representative of $\left[\frac12\right]_\mathbb Q$ you chose. $\frac12 = \frac 24$, but if you use $\frac24$ to calculate $f\left(\frac 12\right)$ you get 6 instead of 3. So this is not a well-defined function; it's not a function at all.

In your example you need to show that if you are given a class, say $[x]_{12}$, and you select an element $y$ from it (which could be any integer at all, as long as $y-x\equiv 0\pmod{12}$), and then you consider the equivalence class $[y]_4$, the class you get does not depend on which $y$ you chose from $[x]_{12}$. If it does, then this $f$ operation is an meaningless as the one in the previous paragraph that claimed to have $f\left(\frac ab\right) = a+b$.