∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    ∀ (n : ℕ),
      CategoryTheory.HasInjectiveDimensionLT S.X₂ n →
        CategoryTheory.HasInjectiveDimensionLT S.X₁ (n + 1) → CategoryTheory.HasInjectiveDimensionLT S.X₃ n