Mouseover doesn't match comment

Stream: new members

[tris]

image.png
Why doesn't the mouseover text match what the comment claims it will be? I understand that both mean the same thing.

[Chris Bailey]

What is the source of the comment, is there some reason why the printed output should match? The output and the actual declaration for cons match, surely that's more important?

[tris]

This was from Theorem Proving in Lean 4. It implied that the comments were showing the result of #check, but I guess it didn't explicitly say that. It was just a bit confusing to see something different, especially when it happened earlier on before it explained that they mean the same thing.