Comment by adrianN

You carefully check that the problem is formalized correctly and then trust the Lean machinery to check the proof.