[proofplan]
The proof is a direct application of [Lagrange's Theorem](/theorems/???) from group theory to the unit group $(\mathbb{Z}/n\mathbb{Z})^\times$. We first verify that the residue class of $a$ is a well-defined element of this group by invoking [Units in $\mathbb{Z}/n\mathbb{Z}$](/theorems/1699), which characterises units as residue classes of integers coprime to $n$. We then identify the order of the group as $\varphi(n)$ by definition of the Euler totient. Lagrange's theorem forces the order of any element to divide the group order, yielding $\bar{a}^{\varphi(n)} = \bar{1}$ — which is the congruence $a^{\varphi(n)} \equiv 1 \pmod n$.
[/proofplan]
[step:Identify the multiplicative group $(\mathbb{Z}/n\mathbb{Z})^\times$ and verify $\bar{a}$ lies in it]
Define the unit group
\begin{align*}
(\mathbb{Z}/n\mathbb{Z})^\times &:= \{\bar{x} \in \mathbb{Z}/n\mathbb{Z} : \exists\, \bar{y} \in \mathbb{Z}/n\mathbb{Z} \text{ with } \bar{x}\bar{y} = \bar{1}\},
\end{align*}
the set of multiplicatively invertible residue classes. Standard arithmetic in $\mathbb{Z}/n\mathbb{Z}$ shows $(\mathbb{Z}/n\mathbb{Z})^\times$ is a group under multiplication, with identity $\bar{1}$.
Let $\bar{a}$ denote the residue class of $a$ modulo $n$. By hypothesis $\gcd(a, n) = 1$, so by [Units in $\mathbb{Z}/n\mathbb{Z}$](/theorems/1699) the class $\bar{a}$ has a multiplicative inverse mod $n$. Therefore
\begin{align*}
\bar{a} &\in (\mathbb{Z}/n\mathbb{Z})^\times.
\end{align*}
[/step]
[step:Identify the order of $(\mathbb{Z}/n\mathbb{Z})^\times$ as $\varphi(n)$]
By definition, the Euler totient $\varphi(n)$ counts the integers in $\{1, 2, \dots, n\}$ coprime to $n$, which is the same as the number of residue classes in $\mathbb{Z}/n\mathbb{Z}$ represented by an integer coprime to $n$. By [Units in $\mathbb{Z}/n\mathbb{Z}$](/theorems/1699), these are exactly the elements of $(\mathbb{Z}/n\mathbb{Z})^\times$. Hence
\begin{align*}
\bigl| (\mathbb{Z}/n\mathbb{Z})^\times \bigr| &= \varphi(n).
\end{align*}
[guided]
We want to pin down the size of the multiplicative group $(\mathbb{Z}/n\mathbb{Z})^\times$. Two perspectives need to be reconciled:
(a) the Euler totient $\varphi(n)$ is defined as the number of integers $k$ with $1 \leq k \leq n$ and $\gcd(k, n) = 1$;
(b) the group $(\mathbb{Z}/n\mathbb{Z})^\times$ consists of residue classes admitting a multiplicative inverse mod $n$.
These are the same count. Each residue class in $\mathbb{Z}/n\mathbb{Z}$ has a unique representative in $\{1, 2, \dots, n\}$ (using $n$ for the class of $0$, or equivalently $\{0, 1, \dots, n-1\}$), so counting residue classes coprime to $n$ is the same as counting integers in $\{1, \dots, n\}$ coprime to $n$ — namely $\varphi(n)$.
By [Units in $\mathbb{Z}/n\mathbb{Z}$](/theorems/1699), the residue classes coprime to $n$ coincide with the multiplicatively invertible classes, i.e., the elements of $(\mathbb{Z}/n\mathbb{Z})^\times$. Therefore
\begin{align*}
\bigl|(\mathbb{Z}/n\mathbb{Z})^\times\bigr| &= \#\{\bar{k} : 1 \leq k \leq n,\; \gcd(k, n) = 1\} = \varphi(n).
\end{align*}
[/guided]
[/step]
[step:Apply Lagrange's theorem to $\bar{a} \in (\mathbb{Z}/n\mathbb{Z})^\times$]
Since $(\mathbb{Z}/n\mathbb{Z})^\times$ is a finite group of order $\varphi(n)$ by Step 2, and $\bar{a}$ is an element of this group by Step 1, [Lagrange's Theorem](/theorems/???) — which states that the order of any element of a finite group divides the order of the group — yields: for every $g \in (\mathbb{Z}/n\mathbb{Z})^\times$,
\begin{align*}
g^{\varphi(n)} &= \bar{1}.
\end{align*}
Specialising to $g = \bar{a}$,
\begin{align*}
\bar{a}^{\varphi(n)} &= \bar{1}.
\end{align*}
Unfolding the quotient, $\bar{a}^{\varphi(n)} = \overline{a^{\varphi(n)}}$, so $\overline{a^{\varphi(n)}} = \bar{1}$ means
\begin{align*}
a^{\varphi(n)} &\equiv 1 \pmod{n},
\end{align*}
which is the conclusion of the theorem.
[guided]
We have all the ingredients to apply Lagrange's theorem. Lagrange's theorem states: if $G$ is a finite group and $g \in G$, then the order of $g$ — the smallest positive integer $m$ with $g^m = e$ — divides $|G|$. A direct corollary is that $g^{|G|} = e$ for every $g \in G$, since if $m = \operatorname{ord}(g)$ divides $|G|$, writing $|G| = mq$ we have $g^{|G|} = (g^m)^q = e^q = e$.
We apply this to $G = (\mathbb{Z}/n\mathbb{Z})^\times$. Verifying the hypotheses of Lagrange's theorem: $G$ is a finite group — it is a subset of the finite set $\mathbb{Z}/n\mathbb{Z}$, and it is closed under multiplication and taking inverses by definition of a unit group; $|G| = \varphi(n)$ by Step 2; and $\bar{a} \in G$ by Step 1. The corollary above yields
\begin{align*}
\bar{a}^{\varphi(n)} &= \bar{1}.
\end{align*}
Unwinding the quotient notation: powers in $\mathbb{Z}/n\mathbb{Z}$ are defined by repeated multiplication, and the multiplication on residue classes is induced from multiplication on $\mathbb{Z}$, so $\bar{a}^{\varphi(n)} = \overline{a^{\varphi(n)}}$. The equation $\overline{a^{\varphi(n)}} = \bar{1}$ in $\mathbb{Z}/n\mathbb{Z}$ says exactly that $n \mid (a^{\varphi(n)} - 1)$, i.e.,
\begin{align*}
a^{\varphi(n)} &\equiv 1 \pmod n,
\end{align*}
which is the Euler–Fermat congruence.
A remark on hypotheses. The hypothesis $\gcd(a, n) = 1$ was consumed in exactly one place: in Step 1, to ensure $\bar{a}$ lies in the unit group $(\mathbb{Z}/n\mathbb{Z})^\times$ rather than in the larger ring $\mathbb{Z}/n\mathbb{Z}$, where non-units need not have any power equal to $\bar{1}$ (e.g., $\bar{2}^k = \bar{2^k}$ in $\mathbb{Z}/4\mathbb{Z}$ never equals $\bar{1}$).
[/guided]
[/step]