-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- The action on graded objects of a trifunctor obtained by composition of two
bifunctors can be computed as a composition of the actions of these two bifunctors.  -/
CategoryTheory.GradedObject.mapBifunctorComp₁₂MapObjIso : {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₃] →
                                                [inst_7 :
                                                    ((((CategoryTheory.GradedObject.mapTrifunctor
                                                                      (CategoryTheory.bifunctorComp₁₂ F₁₂ G) I₁ I₂
                                                                      I₃).obj
                                                                  X₁).obj
                                                              X₂).obj
                                                          X₃).HasMap
                                                      r] →
                                                  CategoryTheory.GradedObject.mapTrifunctorMapObj
                                                      (CategoryTheory.bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ ≅
                                                    CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q
                                                      (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)
                                                      X₃