  We formalise the proof of the first case of Fermat's Last Theorem for regular
primes using the \emph{Lean} theorem prover and its mathematical library
\emph{mathlib}. This is an important 19th century result that motivated the
development of modern algebraic number theory. Besides explaining the
mathematics behind this result, we analyze in this paper the difficulties we
faced in the formalisation process and how we solved them. For example, we had
to deal with a diamond about characteristic zero fields and problems arising
from multiple nested coercions related to number fields. We also explain how we
integrated our work to \emph{mathlib}.
