∀ {A : Type u_4} {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) {X Y : A} (f : X ⟶ Y) [inst_2 : ι.Full] [inst_3 : ι.Faithful]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (Λ.chainComplexXOneIso X).hom
        (CategoryTheory.CategoryStruct.comp
          (Λ.F.map (CategoryTheory.Limits.kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯))
          (Λ.chainComplexXOneIso Y).inv))
      ((Λ.chainComplex Y).d 1 0) =
    CategoryTheory.CategoryStruct.comp ((Λ.chainComplex X).d 1 0)
      (CategoryTheory.CategoryStruct.comp (Λ.chainComplexXZeroIso X).hom
        (CategoryTheory.CategoryStruct.comp (Λ.F.map f) (Λ.chainComplexXZeroIso Y).inv))