LTE's "exact_seq"

Stream: homology

[Brendan Seamas Murphy]

Does mathlib have a version of the exact_seq type? This is a predicate on a list of arrows which say they are composable and form an exact sequence. I have a "four term right exact sequence" A -> B -> C -> D -> 0 showing up in the hypotheses/conclusion of a lemma and I'm not sure if I should just state everything componentwise or use an existing abstraction

[Joël Riou]

I have implemented this as docs#CategoryTheory.ComposableArrows.Exact, see for example PR #12649 and #12638 for examples of how to use it.

[Brendan Seamas Murphy]

Great, ty