awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Zero I
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
F : D ⥤ Functor.{v_1, v_2, u_1, u_2} C D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst_5 : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
inst_6 : (((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).HasMap p
inst_7 : (((mapBifunctor F J I).obj X').obj (Functor.obj (single₀ I) Y)).HasMap p
j : J
h :
  Eq (α := X j ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j)
    (φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (Iso.inv (singleObjApplyIso 0 Y)) ≫
          ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯)
    (e.inv.app (X j) ≫
      CategoryStruct.comp (Y := (F.obj (X j)).obj (Functor.obj (single 0) Y 0))
        ((F.obj (X j)).map (Iso.inv (singleObjApplyIso 0 Y)))
        ((F.map (φ j)).app (Functor.obj (single₀ I) Y 0) ≫
          (F.obj (X' j)).map (𝟙 (Functor.obj (single₀ I) Y 0)) ≫
            ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯))
⊢ Eq (α := X j ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j)
    (φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (Iso.inv (singleObjApplyIso 0 Y)) ≫
          ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯)
    (e.inv.app (X j) ≫
      CategoryStruct.comp (Y := (F.obj (X j)).obj (Functor.obj (single 0) Y 0))
        ((F.obj (X j)).map (Iso.inv (singleObjApplyIso 0 Y)))
        ((F.map (φ j)).app (Functor.obj (single₀ I) Y 0) ≫
          (F.obj (X' j)).map (𝟙 (Functor.obj (single₀ I) Y) 0) ≫
            ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Zero I
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
F : D ⥤ Functor.{v_1, v_2, u_1, u_2} C D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst_5 : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
inst_6 : (((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).HasMap p
inst_7 : (((mapBifunctor F J I).obj X').obj (Functor.obj (single₀ I) Y)).HasMap p
j : J
h :
  Eq (α := X j ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j)
    (φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (Iso.inv (singleObjApplyIso 0 Y)) ≫
          ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯)
    (e.inv.app (X j) ≫
      (F.map (φ j)).app Y ≫
        (F.obj (X' j)).map (Iso.inv (singleObjApplyIso 0 Y)) ≫
          ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯)
⊢ Eq (α := X j ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j)
    (φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (Iso.inv (singleObjApplyIso 0 Y)) ≫
          ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯)
    (e.inv.app (X j) ≫
      CategoryStruct.comp (Y := (F.obj (X j)).obj (Functor.obj (single 0) Y 0))
        ((F.obj (X j)).map (Iso.inv (singleObjApplyIso 0 Y)))
        ((F.map (φ j)).app (Functor.obj (single₀ I) Y 0) ≫
          (F.obj (X' j)).map (𝟙 (Functor.obj (single₀ I) Y 0)) ≫
            ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯))

Tactic:
rw [Functor.map_id, id_comp, NatTrans.naturality_assoc]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Zero I
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
F : D ⥤ Functor.{v_1, v_2, u_1, u_2} C D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst_5 : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
inst_6 : (((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).HasMap p
inst_7 : (((mapBifunctor F J I).obj X').obj (Functor.obj (single₀ I) Y)).HasMap p
j : J
h :
  Eq (α := X j ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j)
    (φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (Iso.inv (singleObjApplyIso 0 Y)) ≫
          ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯)
    (Functor.map (𝟭 D) (φ j) ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (Iso.inv (singleObjApplyIso 0 Y)) ≫
          ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯)
⊢ Eq (α := X j ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j)
    (φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (Iso.inv (singleObjApplyIso 0 Y)) ≫
          ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯)
    (e.inv.app (X j) ≫
      (F.map (φ j)).app Y ≫
        (F.obj (X' j)).map (Iso.inv (singleObjApplyIso 0 Y)) ≫
          ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯)

Tactic:
erw [← NatTrans.naturality_assoc e.inv]

Premises used: CategoryTheory.Iso.inv, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Zero I
inst_3 : DecidableEq I
inst_4 : HasInitial.{v_1, u_1} C
F : D ⥤ Functor.{v_1, v_2, u_1, u_2} C D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst_5 : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
inst_6 : (((mapBifunctor F J I).obj X).obj (Functor.obj (single₀ I) Y)).HasMap p
inst_7 : (((mapBifunctor F J I).obj X').obj (Functor.obj (single₀ I) Y)).HasMap p
j : J
⊢ Eq (α := X j ⟶ mapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j)
    (φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (Iso.inv (singleObjApplyIso 0 Y)) ≫
          ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯)
    (Functor.map (𝟭 D) (φ j) ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (Iso.inv (singleObjApplyIso 0 Y)) ≫
          ιMapBifunctorMapObj F p X' (Functor.obj (single₀ I) Y) j 0 j ⋯)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
J : Type u_4
inst : Zero I₂
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
i₁ : I₁
i₃ : I₃
rw : π ((i₁, 0, i₃).1, τ.p₂₃ (i₁, 0, i₃).2) = π (i₁, i₃)
rw₁ rw₂ : π ((i₁, 0, i₃).1, i₃) = π (i₁, i₃)
⊢ r (i₁, 0, i₃) = π (i₁, i₃)

Tactic:
rw [← τ.hp₂₃, τ.h₃ i₃]

Premises used: CategoryTheory.GradedObject.TriangleIndexData.h₃, CategoryTheory.GradedObject.TriangleIndexData.hp₂₃
-- 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 rw : π (i₁, i₃) = j
rw₁ rw₂ : j = j
⊢ r (i₁, 0, i₃) = j

Tactic:
rw [τ.r_zero, hj]

Premises used: CategoryTheory.GradedObject.TriangleIndexData.r_zero
-- 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
⊢ τ.ρ₁₂.p (i₁, 0) = i₁

Tactic:
simp
-- 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
⊢ τ.ρ₂₃.p (0, i₃) = i₃

Tactic:
simp
-- 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₃) ≫
      (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 ⋯)
    (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)
⊢ 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 ⋯)
    (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:
dsimp
-- 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₃) ≫
          (G.obj (X₁ i₁)).map (NatTrans.app (F₂.map (Iso.hom (singleObjApplyIso 0 X₂))) (X₃ i₃))) ≫
        (G.obj (X₁ i₁)).map (e₂.hom.app (X₃ i₃))) ≫
      ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j ⋯)
    (((NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.hom (singleObjApplyIso 0 X₂)))) (X₃ i₃) ≫
          NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) X₂) (X₃ i₃)) ≫
        (G.obj (X₁ i₁)).map (e₂.hom.app (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)
    (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 ⋯)
    (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:
simp only [Functor.map_comp, NatTrans.comp_app, ← triangle (X₁ i₁) (X₃ i₃), ← assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app
-- 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₀ I₂) X₂ 0))).obj (X₃ i₃) ⟶
      (G.obj (X₁ i₁)).obj ((F₂.obj X₂).obj (X₃ i₃)))
    (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₃)))
    (NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.hom (singleObjApplyIso 0 X₂)))) (X₃ i₃) ≫
      NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) X₂) (X₃ i₃))
⊢ 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₃))) ≫
        (G.obj (X₁ i₁)).map (e₂.hom.app (X₃ i₃))) ≫
      ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j ⋯)
    (((NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.hom (singleObjApplyIso 0 X₂)))) (X₃ i₃) ≫
          NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) X₂) (X₃ i₃)) ≫
        (G.obj (X₁ i₁)).map (e₂.hom.app (X₃ i₃))) ≫
      ιMapBifunctorMapObj G π X₁ X₃ i₁ i₃ j hj)

Tactic:
congr 2
-- 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₀ I₂) X₂ 0))).obj (X₃ i₃) ⟶
      (G.obj (X₁ i₁)).obj ((F₂.obj X₂).obj (X₃ i₃)))
    (NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.hom (singleObjApplyIso 0 X₂)))) (X₃ i₃) ≫
      NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) X₂) (X₃ i₃))
    (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₃)))
⊢ Eq (α :=
    (G.obj ((F₁.obj (X₁ i₁)).obj (Functor.obj (single₀ I₂) X₂ 0))).obj (X₃ i₃) ⟶
      (G.obj (X₁ i₁)).obj ((F₂.obj X₂).obj (X₃ i₃)))
    (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₃)))
    (NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.hom (singleObjApplyIso 0 X₂)))) (X₃ i₃) ≫
      NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) X₂) (X₃ i₃))

Tactic:
symm