-- Mathlib.Algebra.Homology.BifunctorAssociator
/-- The inclusion of a summand in `mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄`,
or zero.  -/
HomologicalComplex.mapBifunctor₂₃.ιOrZero : {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_10} →
                                                  {ι₂₃ : 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 ι₂₃) →
                                                                        (c₄ : ComplexShape ι₄) →
                                                                          [inst_15 : TotalComplexShape c₁ c₂ c₁₂] →
                                                                            [inst_16 : TotalComplexShape c₁₂ c₃ c₄] →
                                                                              [inst_17 : TotalComplexShape c₂ c₃ c₂₃] →
                                                                                [inst_18 :
                                                                                    TotalComplexShape c₁ c₂₃ c₄] →
                                                                                  [inst_19 :
                                                                                      K₂.HasMapBifunctor K₃ G₂₃ c₂₃] →
                                                                                    [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] →
                                                                                      [inst_21 : DecidableEq ι₂₃] →
                                                                                        [inst_22 :
                                                                                            K₁.HasMapBifunctor
                                                                                              (K₂.mapBifunctor K₃ G₂₃
                                                                                                c₂₃)
                                                                                              F c₄] →
                                                                                          (i₁ : ι₁) →
                                                                                            (i₂ : ι₂) →
                                                                                              (i₃ : ι₃) →
                                                                                                (j : ι₄) →
                                                                                                  (F.obj (K₁.X i₁)).obj
                                                                                                      ((G₂₃.obj
                                                                                                            (K₂.X
                                                                                                              i₂)).obj
                                                                                                        (K₃.X i₃)) ⟶
                                                                                                    ⋯.X j