Note: Large Mathlib imports can take forever on the main EC2. If you are confident in your proof and want it in the Hall of Fame, click the green GCloud button, which will queue it at a compiler service that will submit it, if correct, in reasonable time.
Lean InfoView
Run Check Proof to see output (wait time approx 30 seconds)