Yes — because there are many non-equivalent statements that are easier to prove.

So the Lean proves something and the question is whether that something is actually what we care about — or something similar, but ultimately not the question.