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