-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
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 : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D
inst_4 : Zero I₂
inst_5 : DecidableEq I₂
inst_6 : HasInitial.{v_2, u_2} C₂
F₁ : C₁ ⥤ Functor.{v_2, v_1, u_2, u_1} C₂ C₁
F₂ : C₂ ⥤ Functor.{v_3, v_3, u_3, u_3} C₃ C₃
G : C₁ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ D
associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂
X₂ : C₂
e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁
e₂ : F₂.obj X₂ ≅ 𝟭 C₃
inst_7 : ∀ (X₁ : C₁), PreservesColimit (Functor.empty C₂) (F₁.obj X₁)
inst_8 : ∀ (X₃ : C₃), PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
X₁ : GradedObject I₁ C₁
X₃ : GradedObject I₃ C₃
inst_9 : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj (Functor.obj (single₀ I₂) X₂)).HasMap τ.p₁₂
inst_10 : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂))).obj X₃).HasMap π
inst_11 : (((mapBifunctor F₂ I₂ I₃).obj (Functor.obj (single₀ I₂) X₂)).obj X₃).HasMap τ.p₂₃
inst_12 : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ (Functor.obj (single₀ I₂) X₂) X₃)).HasMap π
inst_13 : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ (Functor.obj (single₀ I₂) X₂) X₃
inst_14 : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ (Functor.obj (single₀ I₂) X₂) X₃
inst_15 : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π
triangle :
  ∀ (X₁ : C₁) (X₃ : C₃),
    ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃
j : J
i₁ : I₁
i₃ : I₃
hj : π (i₁, i₃) = j
h :
  Eq (α := (G.obj (X₁ i₁)).obj (X₃ i₃) ⟶ mapBifunctorMapObj G π X₁ X₃ j)
    (NatTrans.app (G.map (e₁.inv.app (X₁ i₁))) (X₃ i₃) ≫
      CategoryStruct.comp (Y := (G.obj ((F₁.obj (X₁ i₁)).obj (Functor.obj (single 0) X₂ 0))).obj (X₃ i₃))
        (NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.inv (singleObjApplyIso 0 X₂)))) (X₃ i₃))
        (CategoryStruct.comp (Y :=
          (G.obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂) i₁)).obj (X₃ i₃))
          (NatTrans.app (G.map (ιMapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂) i₁ 0 i₁ ⋯)) (X₃ i₃))
          (CategoryStruct.comp (Y :=
            mapBifunctorMapObj G π (mapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂)) X₃ j)
            (ιMapBifunctorMapObj G π (mapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂)) X₃ i₁ i₃ j hj)
            (CategoryStruct.comp (Y :=
              mapBifunctorMapObj G π X₁ (mapBifunctorMapObj F₂ τ.p₂₃ (Functor.obj (single₀ I₂) X₂) X₃) j)
              (Iso.hom (mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁ (Functor.obj (single₀ I₂) X₂) X₃) j)
              (mapBifunctorMapMap G π (𝟙 X₁) (Iso.hom (mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃)) j)))))
    (NatTrans.app (G.map (e₁.inv.app (X₁ i₁))) (X₃ i₃) ≫
      CategoryStruct.comp (Y := (G.obj ((F₁.obj (X₁ i₁)).obj (Functor.obj (single 0) X₂ 0))).obj (X₃ i₃))
        (NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.inv (singleObjApplyIso 0 X₂)))) (X₃ i₃))
        (CategoryStruct.comp (Y :=
          (G.obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂) i₁)).obj (X₃ i₃))
          (NatTrans.app (G.map (ιMapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂) i₁ 0 i₁ ⋯)) (X₃ i₃))
          (NatTrans.app (G.map (Iso.hom (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁) i₁)) (X₃ i₃) ≫
            ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj)))
⊢ Eq (α := (G.obj (X₁ i₁)).obj (X₃ i₃) ⟶ mapBifunctorMapObj G π X₁ X₃ j)
    (CategoryStruct.comp (Y := mapBifunctorMapObj G π X₁ X₃ j) (ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj)
      (CategoryStruct.comp (Y :=
        mapBifunctorMapObj G π (mapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂)) X₃)
        (mapBifunctorMapMap G π (Iso.inv (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁)) (𝟙 X₃))
        (CategoryStruct.comp (Y :=
          mapBifunctorMapObj G τ.ρ₂₃.q X₁ (mapBifunctorMapObj F₂ τ.ρ₂₃.p (Functor.obj (single₀ I₂) X₂) X₃))
          (Iso.hom (mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁ (Functor.obj (single₀ I₂) X₂) X₃))
          (mapBifunctorMapMap G π (𝟙 X₁) (Iso.hom (mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃))))
        j))
    (CategoryStruct.comp (Y := mapBifunctorMapObj G π X₁ X₃ j) (ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj)
      (CategoryStruct.comp (Y :=
        mapBifunctorMapObj G π (mapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂)) X₃)
        (mapBifunctorMapMap G π (Iso.inv (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁)) (𝟙 X₃))
        (mapBifunctorMapMap G π (Iso.hom (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁)) (𝟙 X₃)) j))

Tactic:
simp only [categoryOfGradedObjects_comp, ι_mapBifunctorMapMap_assoc,
    mapBifunctorRightUnitor_inv_apply, Functor.id_obj, Functor.flip_obj_obj, Functor.map_comp,
    NatTrans.comp_app, categoryOfGradedObjects_id, Functor.map_id, id_comp, assoc,
    ι_mapBifunctorMapMap]

Premises used: CategoryTheory.GradedObject.ι_mapBifunctorMapMap, CategoryTheory.Category.assoc, CategoryTheory.GradedObject.categoryOfGradedObjects_id, CategoryTheory.GradedObject.mapBifunctorRightUnitor_inv_apply, CategoryTheory.GradedObject.ι_mapBifunctorMapMap_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.flip_obj_obj, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.GradedObject.categoryOfGradedObjects_comp, CategoryTheory.Category.id_comp