Mathlib have errors?

Stream: new members

[Hbz]

In Mathlib's file mathlib4/Mathlib/Algebra/AddConstMap/Basic.lean, I found an error in the theorem rel_map_of_Icc on line 239.
Is it just my problem?
https://github.com/leanprover-community/mathlib4/blob/00335dd967b5e65901b802d67118172f536d2f48/Mathlib/Algebra/AddConstMap/Basic.lean

[Kenny Lau]

@Hbz it's impossible to have a compilation error in any released version of mathlib

[Aaron Liu]

what error are you experiencing?

[Kenny Lau]

you're likely viewing mathlib with an outdated mathlib version

[Kenny Lau]

note that you can copy the whole file into live.lean-lang.org and see that there is no error

[Hbz]

ok :thinking: