A Lean Formalisation of Fermat's Last Theorem