-- 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₃
j : J
i₁ : I₁
i₃ : I₃
hj : π (i₁, i₃) = j
⊢ 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₃ ⋯))
        ((G.map (𝟙 (X₁ i₁))).app (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 π 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))
have 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₃) ≫
    (G.obj (X₁ i₁)).map (NatTrans.app (F₂.map (Iso.hom (singleObjApplyIso 0 X₂))) (X₃ i₃) ≫ e₂.hom.app (X₃ i₃)) ≫
      ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j sorry)
  (NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.hom (singleObjApplyIso 0 X₂)) ≫ e₁.hom.app (X₁ i₁))) (X₃ i₃) ≫
    ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj)
Tactic: rw [Functor.map_id, NatTrans.id_app, id_comp,
    ← Functor.map_comp_assoc, ← NatTrans.comp_app_assoc, ← Functor.map_comp,
    ι_mapBifunctorLeftUnitor_hom_apply F₂ X₂ e₂ τ.p₂₃ τ.h₃ X₃ i₃,
    ι_mapBifunctorRightUnitor_hom_apply F₁ X₂ e₁ τ.p₁₂ τ.h₁ X₁ i₁]