-- Mathlib.Algebra.Homology.BifunctorAssociator
/-- Constructor for morphisms from
`(mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄).X j`.  -/
HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc : {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₄] →
                                                                                [HomologicalComplex.HasGoodTrifunctor₁₂Obj
                                                                                      F₁₂ G K₁ K₂ K₃ c₁₂ c₄] →
                                                                                  {j : ι₄} →
                                                                                    {A : C₄} →
                                                                                      ((i₁ : ι₁) →
                                                                                          (i₂ : ι₂) →
                                                                                            (i₃ : ι₃) →
                                                                                              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₃) ⟶
                                                                                                  A)) →
                                                                                        (((K₁.mapBifunctor K₂ F₁₂
                                                                                                    c₁₂).mapBifunctor
                                                                                                K₃ G c₄).X
                                                                                            j ⟶
                                                                                          A)