doc-gen: Explorability of theories

[hargoniX]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Making.20mathlib.20more.20readable.20.28was.3A.20Improving.20the.20mathlib.20.2E.2E.2E/near/291460564

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Making.20mathlib.20more.20readable.20.28was.3A.20Improving.20the.20mathlib.20.2E.2E.2E/near/291485777

Implementation idea:

1. The individual JSON of each module contains:

• A list of used theorems per theorem
• A map from theorem names to a counter for how often this name was used

2. In the index step this information is accumulated into the final JSON in such a way that the following things can be calculated in JS with little runtime:

• The list of theorems a certain theorem used, sorted by use counter, the theorem with the least use counter first. This is so theorems that are special for this declaration show up first
• The list of theorems that use a certain theorem, sorted by use counter, here the theorem with the highest counter first. This is so the significant results can be visited quickly.

[hargoniX]

Addressed by tools like blueprint and David's docs.