Comment by sebzim4500

No one is disputing the correctness of the lean proof, the problem is that they did a bad job converting it to natural language.