-- Mathlib.Algebra.Homology.BifunctorAssociator
/-- The inclusion of a summand in `mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄`.  -/
HomologicalComplex.mapBifunctor₁₂.ι : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₁₂ : Type u_3} →
      {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_5, u_3} 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 : F₁₂.PreservesZeroMorphisms] →
                                    [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] →
                                      [inst_12 : G.Additive] →
                                        [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] →
                                          {ι₁ : Type u_7} →
                                            {ι₂ : Type u_8} →
                                              {ι₃ : Type u_9} →
                                                {ι₁₂ : Type u_10} →
                                                  {ι₄ : 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₂ F₁₂ c₁₂] →
                                                                            [inst_18 : DecidableEq ι₁₂] →
                                                                              [inst_19 :
                                                                                  (K₁.mapBifunctor K₂ F₁₂
                                                                                        c₁₂).HasMapBifunctor
                                                                                    K₃ G c₄] →
                                                                                (i₁ : ι₁) →
                                                                                  (i₂ : ι₂) →
                                                                                    (i₃ : ι₃) →
                                                                                      (j : ι₄) →
                                                                                        c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) =
                                                                                            j →
                                                                                          ((G.obj
                                                                                                  ((F₁₂.obj
                                                                                                        (K₁.X i₁)).obj
                                                                                                    (K₂.X i₂))).obj
                                                                                              (K₃.X i₃) ⟶
                                                                                            ((K₁.mapBifunctor K₂ F₁₂
                                                                                                      c₁₂).mapBifunctor
                                                                                                  K₃ G c₄).X
                                                                                              j)