Historical block moved losslessly from the former monolithic index.
lake build +Mathlib:docs or consult the
doc-gen4 README.
The CI job is commented out in
.github/workflows/lean_action_ci.yml with a note on how to
re-enable.tex/proof-guide.tex)