Add universe levels and use the more verbose pretty printer

[jasonrute]

Universe levels were added to the goal states and communicated to Lean. (The examples are now wrapped in section...end to keep the universes private to each example.

Ability to use imports also added.

Using a custom goal state which is more robust than what is pretty printed. It is essentially a cleaned up version of the pretty printer with set_option pp.all true.

A section on the current known issues was added.

Other small changes to the notebook were made, both to the code and the text.

[jasonrute]

@spolu See above for the new changes.

[spolu]

@jasonrute ack thanks 👍