-- Mathlib.Algebra.Homology.BifunctorAssociator
/-- The first differential on `mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄`.  -/
HomologicalComplex.mapBifunctor₂₃.D₁ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₂₃ : Type u_4} →
      {C₃ : Type u_5} →
        {C₄ : Type u_6} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] →
                    [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                      [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                        [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃] →
                          [inst_8 : CategoryTheory.Preadditive C₂₃] →
                            [inst_9 : CategoryTheory.Preadditive C₄] →
                              (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) →
                                (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) →
                                  [inst_10 : G₂₃.PreservesZeroMorphisms] →
                                    [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] →
                                      [inst_12 : F.PreservesZeroMorphisms] →
                                        [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] →
                                          {ι₁ : Type u_7} →
                                            {ι₂ : Type u_8} →
                                              {ι₃ : Type u_9} →
                                                {ι₂₃ : Type u_11} →
                                                  {ι₄ : Type u_12} →
                                                    [inst_14 : DecidableEq ι₄] →
                                                      {c₁ : ComplexShape ι₁} →
                                                        {c₂ : ComplexShape ι₂} →
                                                          {c₃ : ComplexShape ι₃} →
                                                            (K₁ : HomologicalComplex C₁ c₁) →
                                                              (K₂ : HomologicalComplex C₂ c₂) →
                                                                (K₃ : HomologicalComplex C₃ c₃) →
                                                                  (c₂₃ : ComplexShape ι₂₃) →
                                                                    (c₄ : ComplexShape ι₄) →
                                                                      [inst_15 : TotalComplexShape c₂ c₃ c₂₃] →
                                                                        [inst_16 : TotalComplexShape c₁ c₂₃ c₄] →
                                                                          [inst_17 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃] →
                                                                            [inst_18 : DecidableEq ι₂₃] →
                                                                              [inst_19 :
                                                                                  K₁.HasMapBifunctor
                                                                                    (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] →
                                                                                (j j' : ι₄) →
                                                                                  (K₁.mapBifunctor
                                                                                          (K₂.mapBifunctor K₃ G₂₃ c₂₃) F
                                                                                          c₄).X
                                                                                      j ⟶
                                                                                    (K₁.mapBifunctor
                                                                                          (K₂.mapBifunctor K₃ G₂₃ c₂₃) F
                                                                                          c₄).X
                                                                                      j'