feat: update the glossary to Lean 4 (#728)

Go through the glossary, remove references to Lean 3, update links and
make small fixes.

I split apart the entries for environment/code linters (the distinction
was introduced in Lean 4) and added a few entries:
"definitional"/"syntactic equality" and "Lean 3".

This is the last main page that needs updating to Lean 4, the remaining
one is the tactic writing guide (which I think we should replace or
throw away completely).

---------

Co-authored-by: Floris van Doorn <[email protected]>
Co-authored-by: Michael Rothgang <[email protected]>

Author: 3 people