tactic for string diagram?

Stream: new members

[Shanghe Chen]

Hi recently I learned some basic language in string diagram and read the proof https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Equivalence.html#CategoryTheory.Equivalence.unit_inverse_comp and found that the proof in fact same as lemma 3.2 in https://ncatlab.org/nlab/show/adjoint+equivalence . I found the language is powerful and intuitive. Nevertheless the proof still has to be translated to use more basic tactics. Is it possible to have a direct string_diagram tactic?

[Joël Riou]

@Yuma Mizuno is developing a widget for string diagrams #10581

[Shanghe Chen]

Ah it is awesome :tada: