The point GP is making, is that everyday mathematics is not done in Lean, but in a language that's more like JavaScript, where equals doesn't always mean equals

The point GP is making, is that everyday mathematics is not done in Lean, but in a language that's more like JavaScript, where equals doesn't always mean equals, + and • mean whatever seems convenient at the time, and objects sometimes change type without notice.