> not at the Lean code, since I know very little of the actual usage of Lean, and that code was enormous

Dismissing results on the basis that Lean code is too long disqualifies this opinion. It is not hard at all to read the Lean result statement, even with very superficial Lean knowledge.