Eric Wieser

Note that this was merged in a fork already

> What is the story for the *.lean files here? Are these installed as well? No, not yet - but the python code doesn't use these at all yet.

The bmp is now 1660854 bytes, and loads in half a second on my machine - I think it was 15mB before compression before, so the file extension change definitely...

#deploy

This seems not to work

I think Google only respects the meta tag if it finds it on the homepage at the root of the URL

#deploy

> This PR has been successfully deployed at http://leanprover-community.github.io/mathlib_docs_demo! [Citation needed](https://github.com/leanprover-community/mathlib_docs_demo/runs/4494496859)

#deploy

> I thought MathJax was smart enough to do this, it handles `