-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- Constructor for morphisms from
`mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j`.  -/
CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃Desc : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {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_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_6, u_6} 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 G₂₃ I₂ I₃).obj X₂).obj
                                                    X₃).HasMap
                                                ρ₂₃.p] →
                                            [inst_6 :
                                                (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
                                                      (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂
                                                        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 →
                                                              ((F.obj (X₁ i₁)).obj ((G₂₃.obj (X₂ i₂)).obj (X₃ i₃)) ⟶
                                                                A)) →
                                                      (CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
                                                          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂
                                                            X₃)
                                                          j ⟶
                                                        A)