Convert goals to latex?

Stream: new members

[Shanghe Chen]

Hi I am following some theorem in mathlib4 (namely https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Equivalence.html#CategoryTheory.Equivalence.unit_inverse_comp)

[Shanghe Chen]

The intermediate goals are kind of hard to follow. Is it possible to convert them to latex formulas similar in a textbook?

[Patrick Massot]

This is work in (very slow) progress.

[Shanghe Chen]

Ah Thank you very much. I find some thread related in https://proofassistants.stackexchange.com/questions/62/is-there-software-for-interfacing-lean-code-with-latex too