-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctor_triangle : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D : Type u_4} {I₁ : Type u_5} {I₂ : Type u_6} {I₃ : Type u_7}
  {J : Type u_8} [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} D] [inst_4 : Zero I₂]
  [inst_5 : DecidableEq I₂] [inst_6 : CategoryTheory.Limits.HasInitial C₂]
  {F₁ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁)}
  {F₂ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₃)}
  {G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₃ D)}
  (associator : CategoryTheory.bifunctorComp₁₂ F₁ G ≅ CategoryTheory.bifunctorComp₂₃ G F₂) (X₂ : C₂)
  (e₁ : F₁.flip.obj X₂ ≅ CategoryTheory.Functor.id C₁) (e₂ : F₂.obj X₂ ≅ CategoryTheory.Functor.id C₃)
  [inst_7 : ∀ (X₁ : C₁), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C₂) (F₁.obj X₁)]
  [inst_8 : ∀ (X₃ : C₃), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C₂) (F₂.flip.obj X₃)]
  {r : I₁ × I₂ × I₃ → J} {π : I₁ × I₃ → J} (τ : CategoryTheory.GradedObject.TriangleIndexData r π)
  (X₁ : CategoryTheory.GradedObject I₁ C₁) (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_9 :
    (((CategoryTheory.GradedObject.mapBifunctor F₁ I₁ I₂).obj X₁).obj
          ((CategoryTheory.GradedObject.single₀ I₂).obj X₂)).HasMap
      τ.p₁₂]
  [inst_10 :
    (((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁ τ.p₁₂ X₁
                ((CategoryTheory.GradedObject.single₀ I₂).obj X₂))).obj
          X₃).HasMap
      π]
  [inst_11 :
    (((CategoryTheory.GradedObject.mapBifunctor F₂ I₂ I₃).obj ((CategoryTheory.GradedObject.single₀ I₂).obj X₂)).obj
          X₃).HasMap
      τ.p₂₃]
  [inst_12 :
    (((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj F₂ τ.p₂₃ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂)
            X₃)).HasMap
      π]
  [inst_13 :
    CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂)
      X₃]
  [inst_14 :
    CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((CategoryTheory.GradedObject.single₀ I₂).obj X₂)
      X₃]
  [inst_15 : (((CategoryTheory.GradedObject.mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π],
  (∀ (X₁ : C₁) (X₃ : C₃),
      CategoryTheory.CategoryStruct.comp (((associator.hom.app X₁).app X₂).app X₃) ((G.obj X₁).map (e₂.hom.app X₃)) =
        (G.map (e₁.hom.app X₁)).app X₃) →
    CategoryTheory.CategoryStruct.comp
        (CategoryTheory.GradedObject.mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁
            ((CategoryTheory.GradedObject.single₀ I₂).obj X₂) X₃).hom
        (CategoryTheory.GradedObject.mapBifunctorMapMap G π (CategoryTheory.CategoryStruct.id X₁)
          (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom) =
      CategoryTheory.GradedObject.mapBifunctorMapMap G π
        (CategoryTheory.GradedObject.mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom
        (CategoryTheory.CategoryStruct.id X₃)