Transporting the kernel of a short exact complex

noncomputable def CategoryTheory.ShortComplex.sourceIsoKernelOfShortExactCompIso {C : Type u} [Category.{v, u} C] [Abelian C] (S : ShortComplex C) (hS : S.ShortExact) {Y : C} (g : S.X₂ ⟶ Y) (e : S.X₃ ≅ Y) (h : CategoryStruct.comp S.g e.hom = g) : S.X₁ ≅ Limits.kernel g

If a short exact complex's second map is transported across an isomorphism of its target, its source remains a kernel of the transported map.