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$.

You're trying to prove $$f:(\Bbb{Z}/12\Bbb{Z})^*\to(\Bbb{Z}/4\Bbb{Z})^*:[x]_{12}\mapsto[x]_4$$

So, you have to prove that this rule of assignment doesn't depend on the representative of the equivalence class. That is $$[x]_{12}=[y]_{12} \implies [x]_{4}=[y]_{4}$$

For example $[16]_{12}=[4]_{12}$ then $[16]_{4}=[4]_{4}$.

You also need to prove that $$ [x]_{12} \in (\Bbb{Z}/12\Bbb{Z})^* \implies [x]_{4} \in (\Bbb{Z}/4\Bbb{Z})^* $$

An option would be to resort to Relational Algebra, in a pointfree style.
A logic of relations was first proposed by Augustus de Morgan, in 1867.

Functions are just special cases of Relations (binary relations, for that matter).

Given types $A$ and $B$, we denote a relation $R$, from $A$ to $B$, as $B \xleftarrow{R} A$.
We write $b \, R \, a$, to denote $(b,a) \in R$.
In the particular case of functions, for a function $f$, writing $b \, f \, a$ simply means $b = f \, a$, since we expect $b$ to be unique.

Therefore, $b \, R \, a$ is a generalization of $b \, f \, a$.
This generalization applies in many ways. For instance, equality on functions, $f=g$, generalizes to inclusion on relations, $R \subseteq S$, meaning $R$ is (at most) $S$.

Besides inclusion, an important concept to have in mind is the converse of a relation.
The converse of $R$, $B \xleftarrow{R} A$, is $R^\circ$, $A \xleftarrow{R^\circ} B$ (just turn the arrows the other way around).

The converse of a function always exists, as a relation (sometimes, in special cases, as a function too).

Function composition, $f \cdot g$, also generalizes to relations, $R \cdot S$, in the same way.

So, what is it that really defines when a given relation is a function?$\vphantom{Some commands added; A.K.}\newcommand{\img}{\operatorname{img}}\newcommand{\id}{\mathrm{id}}$

Let's look at a special function, $\id$.
We have $b \, \id \, a \equiv b = a$. Not too hard.

Why does $id$ matter?

• $R$ is reflexive iff $\id \subseteq R$.
• $R$ is coreflexive iff $R \subseteq \id$.

We then define:

• Kernel of $R$ as $\ker R \doteq R^\circ \cdot R$.
• Image of $R$ as $\img R \doteq R \cdot R^\circ$.

Finally, we have the following facts:

• $\ker R$ is reflexive $\equiv$ $R$ is entire.
• $\ker R$ is coreflexive $\equiv$ $R$ is injective.
• $\img R$ is reflexive $\equiv$ $R$ is surjective.
• $\img R$ is coreflexive $\equiv$ $R$ is simple.

We say relation $f$ is a function iff $f$ is entire and $f$ is simple.
Put in another way, what you want to prove is:

• $\id \subseteq ker f$ (simplifies to $\id \subseteq f^\circ \cdot f$)
• $\img f \subseteq \id$ (simplifies to $f \cdot f^\circ \subseteq \id$)

Bonus facts:

• $\ker (R^\circ) = \img R$
• $\img (R^\circ) = \ker R$

For predictably wise words about this from Tim Gowers (that's Professor Sir Timothy Gowers to you ...), see

First, note that any function from $X$ to $Y$ defined by

$$ x \mapsto E $$

or by

$$ f(x) = E$$

is well-defined, where $x$ is an indeterminate variable that ranges over $X$ and $E$ is a (well-formed) Y-valued expression depending (only) on $x$. (to fix the edge cases, $1$ depends on $x$, albeit in a degenerate fashion)

However, this is not the only way we define functions. There are two ways of thinking about the common alternative:

The more set-theoretic viewpoint is that we can define $f$ by a relation. We might define a function on the rational numbers by thinking

$f$ relates $x/y$ with $(x+y)/y$

Of course, we would normally write it as $x/y \mapsto (x+y)/y$ or as $f(x/y) = (x+y)/y$. But we are thinking in terms of a relation.

To check that such a mapping is well-defined, we need to check that the relation passes the 'vertical line test': specifically, that set of values

$$ \left\{ \left(\frac{x}{y}, \frac{x+y}{y} \right) \mid x,y \in \mathbb{Q}, y \neq 0 \right\} $$

contains exactly one pair $(q, \square)$ for each $q \in \mathbb{Q}$.

A more algebraic viewpoint is that we define our mapping in terms of preimages. If we define functions $g : Z \to Y$ and $p : Z \to X$, then we think of defining $f$ as a mapping

$$ g(z) \mapsto p(z) $$

or by

$$f(g(z)) = p(z) $$

This is well-defined when we can prove

$$ g(z) = g(z') \implies p(z) = p(z') $$

This can be thought of as the third isomorphism theorem as applied to sets. An extremely natural example in this viewpoint is anything to do modular arithmetic. e.g. we can define "multiplication by 5" on $\mathbb{Z} / 2 \mathbb{Z} \to \mathbb{Z} / 10 \mathbb{Z}$ by

$$ [x]_2 \mapsto [5x]_{10} $$

In this case, the maps are

$$p(z) : \mathbb{Z} \to \mathbb{Z} / 2 \mathbb{Z} : x \mapsto [x]_2 $$ $$g(z) : \mathbb{Z} \to \mathbb{Z} / 10 \mathbb{Z} : x \mapsto [5x]_{10} $$

I've been wrestling with this for a whole semester, and today, while talking with the assistant professor, I think I came to a fairly easy way to understand if the function (or the map in question) is well defined if no element in the domain is mapped to more than one element in the codomain. It is probably not that simple, but I think for the purpose of my course (Algebra I), it is.