-- Mathlib/CategoryTheory/GradedObject/Unitor.lean
lemma mapBifunctor_triangle
    (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₃) :
    (mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃).hom ≫
    mapBifunctorMapMap G π (𝟙 X₁) (mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ τ.h₃ X₃).hom =
      mapBifunctorMapMap G π (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ τ.h₁ X₁).hom (𝟙 X₃)

Proof state:
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.{u_12, u_1} C₁
inst✝¹⁴ : Category.{u_11, u_2} C₂
inst✝¹³ : Category.{u_10, u_3} C₃
inst✝¹² : Category.{u_9, u_4} D
inst✝¹¹ : Zero I₂
inst✝¹⁰ : DecidableEq I₂
inst✝⁹ : HasInitial C₂
F₁ : C₁ ⥤ C₂ ⥤ C₁
F₂ : C₂ ⥤ C₃ ⥤ C₃
G : C₁ ⥤ C₃ ⥤ D
associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂
X₂ : C₂
e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁
e₂ : F₂.obj X₂ ≅ 𝟭 C₃
inst✝⁸ : ∀ (X₁ : C₁), PreservesColimit (Functor.empty C₂) (F₁.obj X₁)
inst✝⁷ : ∀ (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✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂
inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π
inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃
inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π
inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃
inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃
inst✝ : (((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
⊢ r (i₁, 0, i₃) = j

Tactic:
rw [τ.r_zero, hj]

Result:
no goals

Proof state:
case h.h.e_a.e_a
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.{u_12, u_1} C₁
inst✝¹⁴ : Category.{u_11, u_2} C₂
inst✝¹³ : Category.{u_10, u_3} C₃
inst✝¹² : Category.{u_9, u_4} D
inst✝¹¹ : Zero I₂
inst✝¹⁰ : DecidableEq I₂
inst✝⁹ : HasInitial C₂
F₁ : C₁ ⥤ C₂ ⥤ C₁
F₂ : C₂ ⥤ C₃ ⥤ C₃
G : C₁ ⥤ C₃ ⥤ D
associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂
X₂ : C₂
e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁
e₂ : F₂.obj X₂ ≅ 𝟭 C₃
inst✝⁸ : ∀ (X₁ : C₁), PreservesColimit (Functor.empty C₂) (F₁.obj X₁)
inst✝⁷ : ∀ (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✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂
inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π
inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃
inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π
inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃
inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃
inst✝ : (((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
⊢ (G.map (ιMapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂) i₁ 0 i₁ ⋯)).app (X₃ i₃) ≫
      ιMapBifunctorMapObj G π (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂)) X₃ i₁ i₃ j hj ≫
        (mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃).hom j ≫
          mapBifunctorMapMap G π (𝟙 X₁) (mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom j =
    (G.map (ιMapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂) i₁ 0 i₁ ⋯)).app (X₃ i₃) ≫
      (G.map ((mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom i₁)).app (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]

Result:
case h.h.e_a.e_a
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.{u_12, u_1} C₁
inst✝¹⁴ : Category.{u_11, u_2} C₂
inst✝¹³ : Category.{u_10, u_3} C₃
inst✝¹² : Category.{u_9, u_4} D
inst✝¹¹ : Zero I₂
inst✝¹⁰ : DecidableEq I₂
inst✝⁹ : HasInitial C₂
F₁ : C₁ ⥤ C₂ ⥤ C₁
F₂ : C₂ ⥤ C₃ ⥤ C₃
G : C₁ ⥤ C₃ ⥤ D
associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂
X₂ : C₂
e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁
e₂ : F₂.obj X₂ ≅ 𝟭 C₃
inst✝⁸ : ∀ (X₁ : C₁), PreservesColimit (Functor.empty C₂) (F₁.obj X₁)
inst✝⁷ : ∀ (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✝⁶ : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj ((single₀ I₂).obj X₂)).HasMap τ.p₁₂
inst✝⁵ : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂))).obj X₃).HasMap π
inst✝⁴ : (((mapBifunctor F₂ I₂ I₃).obj ((single₀ I₂).obj X₂)).obj X₃).HasMap τ.p₂₃
inst✝³ : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ ((single₀ I₂).obj X₂) X₃)).HasMap π
inst✝² : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ ((single₀ I₂).obj X₂) X₃
inst✝¹ : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃
inst✝ : (((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
⊢ ((associator.hom.app (X₁ i₁)).app ((single₀ I₂).obj X₂ 0)).app (X₃ i₃) ≫
      (G.obj (X₁ i₁)).map (ιMapBifunctorMapObj F₂ τ.ρ₂₃.p ((single₀ I₂).obj X₂) X₃ 0 i₃ i₃ ⋯) ≫
        (G.map (𝟙 X₁ i₁)).app (mapBifunctorMapObj F₂ τ.ρ₂₃.p ((single₀ I₂).obj X₂) X₃ i₃) ≫
          (G.obj (X₁ i₁)).map ((mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ ⋯ X₃).hom i₃) ≫
            ιMapBifunctorMapObj G τ.ρ₂₃.q X₁ X₃ i₁ i₃ j ⋯ =
    (G.map (ιMapBifunctorMapObj F₁ τ.p₁₂ X₁ ((single₀ I₂).obj X₂) i₁ 0 i₁ ⋯)).app (X₃ i₃) ≫
      (G.map ((mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ ⋯ X₁).hom i₁)).app (X₃ i₃) ≫
        ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj