Proof in Lean of Fermat Last Theorem for exponent 3