Horseshoe lemma

Stream: Is there code for X?

[Edison Xie]

Has the Horseshoe lemma landed in mathlib yet? i.e given a short exact sequence and injective resolutions of first and last term, there exists an injective resolution of the second term such that the three injective resolutions form a short exact sequence.

[Edison Xie]

@Joël Riou do you know anything about this? :-)

[Joël Riou]

It was in some form in #12438 but it never made it into mathlib.
(Note that this will not be required for the long exact sequence of right derived functors: the derived category mechanisms will give connecting homomorphisms which do not depend on any choice of injective resolutions.)