∀ {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 ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] {X Y Z : A} (x : X ⟶ Y) (x_1 : Y ⟶ Z),
  { f := Λ.F.map (CategoryTheory.CategoryStruct.comp x x_1) - Λ.F.map 0, comm := ⋯ } =
    CategoryTheory.CategoryStruct.comp { f := Λ.F.map x - Λ.F.map 0, comm := ⋯ }
      { f := Λ.F.map x_1 - Λ.F.map 0, comm := ⋯ }