-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- Constructor for morphisms from
`mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j`.  -/
CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorDesc : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₁₂ : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] →
                    {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} →
                      {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} →
                        {I₁ : Type u_7} →
                          {I₂ : Type u_8} →
                            {I₃ : Type u_9} →
                              {J : Type u_10} →
                                {r : I₁ × I₂ × I₃ → J} →
                                  {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r} →
                                    {X₁ : CategoryTheory.GradedObject I₁ C₁} →
                                      {X₂ : CategoryTheory.GradedObject I₂ C₂} →
                                        {X₃ : CategoryTheory.GradedObject I₃ C₃} →
                                          [inst_5 :
                                              (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj
                                                    X₂).HasMap
                                                ρ₁₂.p] →
                                            [inst_6 :
                                                (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
                                                          (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁
                                                            X₂)).obj
                                                      X₃).HasMap
                                                  ρ₁₂.q] →
                                              [H :
                                                  CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂
                                                    X₃] →
                                                {j : J} →
                                                  {A : C₄} →
                                                    ((i₁ : I₁) →
                                                        (i₂ : I₂) →
                                                          (i₃ : I₃) →
                                                            r (i₁, i₂, i₃) = j →
                                                              ((G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶
                                                                A)) →
                                                      (CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q
                                                          (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁
                                                            X₂)
                                                          X₃ j ⟶
                                                        A)