∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)),
  S.Exact ↔
    ∀ (x₂ : ↑S.X₂),
      (CategoryTheory.ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (CategoryTheory.ConcreteCategory.hom S.f) x₁ = x₂