Autogenerate LemmaDoc

[joneugster]

Add an Option to LemmaDoc (and DefinitionDoc) to automatically generate Information about a lemma that is in Mathlib. The automatically generated information could comprise:

• The lemma statement
• mathlib docs link.
• Full namespace
• Is it a simp-lemma

Information that needs to be added manually:

• The name the lemma appears under in the game.
• A supplementary short description (to explain the usage inside the game)

Lemmas that are not from Mathlib should also be marked as such somehow.

[joneugster]

The lemma-doc library is actually exploding quite quickly.

[joneugster]

Moreover, it would be nice to display in which level a lemma/def/tactic has been introduced.

[joneugster]

Could display mathlib docstring if one exists.