-- 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 ((F₁.obj (X₁ i₁)).obj (Functor.obj (single 0) X₂ 0))).obj (X₃ i₃) ⟶ mapBifunctorMapObj G π X₁ X₃ j)
    (NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) (Functor.obj (single₀ I₂) X₂ 0)) (X₃ i₃) ≫
      CategoryStruct.comp (Y := (G.obj (X₁ i₁)).obj (mapBifunctorMapObj F₂ τ.ρ₂₃.p (Functor.obj (single₀ I₂) X₂) X₃ i₃))
        ((G.obj (X₁ i₁)).map (ιMapBifunctorMapObj F₂ τ.ρ₂₃.p (Functor.obj (single₀ I₂) X₂) X₃ 0 i₃ i₃ ⋯))
        (NatTrans.app (G.map (𝟙 X₁ i₁)) (mapBifunctorMapObj F₂ τ.ρ₂₃.p (Functor.obj (single₀ I₂) X₂) X₃ i₃) ≫
          (G.obj (X₁ i₁)).map (Iso.hom (mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃) i₃) ≫
            ιMapBifunctorMapObj G τ.ρ₂₃.q X₁ X₃ i₁ i₃ j ⋯))
    (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 ((F₁.obj (X₁ i₁)).obj (Functor.obj (single 0) X₂ 0))).obj (X₃ i₃) ⟶ mapBifunctorMapObj G π X₁ X₃ j)
    (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))))
    (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))

Tactic:
rw [← ιMapBifunctor₁₂BifunctorMapObj_eq_assoc F₁ G τ.ρ₁₂ _ _ _ i₁ 0 i₃ j
    (by rw [τ.r_zero, hj]) i₁ (by simp), ι_mapBifunctorAssociator_hom_assoc,
    ιMapBifunctorBifunctor₂₃MapObj_eq_assoc G F₂ τ.ρ₂₃ _ _ _ i₁ 0 i₃ j
    (by rw [τ.r_zero, hj]) i₃ (by simp), ι_mapBifunctorMapMap]

Premises used: CategoryTheory.GradedObject.ι_mapBifunctorMapMap, CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj_eq_assoc, CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj_eq_assoc, CategoryTheory.GradedObject.ι_mapBifunctorAssociator_hom_assoc, CategoryTheory.GradedObject.TriangleIndexData.ρ₂₃, OfNat.ofNat, CategoryTheory.GradedObject.TriangleIndexData.ρ₁₂