∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology i] [inst_3 : K.HasHomology j],
  CategoryTheory.Epi
    ((HomologicalComplex.HomologySequence.composableArrows₃ K i j).map' 2 3
      HomologicalComplex.HomologySequence.instEpiMap'ComposableArrows₃OfNatNat._proof_2
      HomologicalComplex.HomologySequence.instEpiMap'ComposableArrows₃OfNatNat._proof_3)