found a few issues about tutorial HOT 2 CLOSED

8.3 Opaque Definitions

Spelling mistake; defiend should be defined:

The idea is that we can prove theorems about an opaque constant in the module in which it is defiend, but in other modules, we can only rely on these theorems.

from tutorial.

8.6 Sections and Contexts [0]

The the should be that in:

Notice the Lean is consistent when it comes to providing alternative syntax for Prop-valued variants of declarations:

8.6 Sections and Contexts [1]

I think once should be one in:

Their scope is the entire namespace in which the section resides, and when another module imports the once containing the section and opens the relevant namespace, all these objects are available.

from tutorial.