-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Unitor (goal)
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₃
⊢ Eq (α := mapBifunctorMapObj G π X₁ X₃ ⟶ mapBifunctorMapObj G π X₁ X₃)
    (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₃)))))
    (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₃)))
have h : ∀ (j : J) (i₁ : I₁) (i₃ : I₃) (hj : π (i₁, i₃) = j),
  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₁₂ sorry 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₂₃ sorry 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₁₂ sorry X₁)) (𝟙 X₃))
        (mapBifunctorMapMap G π (Iso.hom (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ sorry X₁)) (𝟙 X₃)) j))
Tactic: ext j i₁ i₃ hj