∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Y ⟶ Z)
  (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (P.complex.d 1 0) (CategoryTheory.ProjectiveResolution.liftFZero f P Q))
      { X₁ := Q.complex.X 1, X₂ := Q.complex.X 0, X₃ := ((ChainComplex.single₀ C).obj Z).X 0, f := Q.complex.d 1 0,
          g := Q.π.f 0, zero := ⋯ }.g =
    0