Comment by omnicognate

> If this file is correct and Lean kernel is correct, the proof is correct

There are two ifs in this sentence.