information returned by repl is inconsistent with the information returned by lean info.

[tsuki8]

In the REPL, this constitutes an erroneous proof; however, judging from the information returned by Lean Info, there appears to be no issue with it.My version of Lean is v4.18.0.

[RexWzh]

You need to make sure the REPL version (4.17.0-rc1) matches your mathlib version (4.18.0)

[tsuki8]

I saw that you have updated the toolchain to v4.18.0?

[tsuki8]

I found that as long as I add import Mathlib, this problem occurs, but if I don't add it, there is no problem.

[RexWzh]

Have you tried following the guidelines in the README?

cd /path/to/your/mathlib-project
echo '...' | lake env /path/to/repl/.lake/build/bin/repl