It's not a proof. You check that the mathematical ideas expressed in the claimed statement are the same as the mathematical ideas expressed by the Lean repository.