Reviewing to make sure the proof is correct. Even the proof comes with lean, it could still proof the wrong thing.