A complete formalization of Fermat's Last Theorem for regular primes in Lean