awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
inst_6 :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ_1 : X₁ ⟶ Y₁
X₂ : GradedObject I₂ C₂
X₃ Y₃ : GradedObject I₃ C₃
φ : X₃ ⟶ Y₃
dsimp :
  ((mapTrifunctorMapFunctorObj F p X₁).obj X₂).map φ ≫ mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 Y₃) =
    mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 X₃) ≫ ((mapTrifunctorMapFunctorObj F p Y₁).obj X₂).map φ
⊢ ((mapTrifunctorMapFunctorObj F p X₁).obj X₂).map φ ≫ mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 Y₃) =
    mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 X₃) ≫ ((mapTrifunctorMapFunctorObj F p Y₁).obj X₂).map φ

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
inst_6 :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ_1 : X₁ ⟶ Y₁
X₂ : GradedObject I₂ C₂
X₃ Y₃ : GradedObject I₃ C₃
φ : X₃ ⟶ Y₃
h :
  ∀ (j : J) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
    Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ X₂ Y₃ j)
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
        ((((mapTrifunctorMapFunctorObj F p X₁).obj X₂).map φ ≫ mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 Y₃)) j))
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
        ((mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 X₃) ≫ ((mapTrifunctorMapFunctorObj F p Y₁).obj X₂).map φ) j))
⊢ ((mapTrifunctorMapFunctorObj F p X₁).obj X₂).map φ ≫ mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 Y₃) =
    mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 X₃) ≫ ((mapTrifunctorMapFunctorObj F p Y₁).obj X₂).map φ

Tactic:
ext j i₁ i₂ i₃ h
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
inst_6 :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ_1 : X₁ ⟶ Y₁
X₂ : GradedObject I₂ C₂
X₃ Y₃ : GradedObject I₃ C₃
φ : X₃ ⟶ Y₃
j : J
i₁ : I₁
i₂ : I₂
i₃ : I₃
h : p (i₁, i₂, i₃) = j
h₁ :
  Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ X₂ Y₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ Y₃ j) (mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ j)
        (mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 Y₃) j)))
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p Y₁ X₂ X₃ j) (mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 X₃) j)
        (mapTrifunctorMapMap F p (𝟙 Y₁) (𝟙 X₂) φ j)))
⊢ Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ X₂ Y₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      ((((mapTrifunctorMapFunctorObj F p X₁).obj X₂).map φ ≫ mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 Y₃)) j))
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      ((mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 X₃) ≫ ((mapTrifunctorMapFunctorObj F p Y₁).obj X₂).map φ) j))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
inst_6 :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ_1 : X₁ ⟶ Y₁
X₂ : GradedObject I₂ C₂
X₃ Y₃ : GradedObject I₃ C₃
φ : X₃ ⟶ Y₃
j : J
i₁ : I₁
i₂ : I₂
i₃ : I₃
h : p (i₁, i₂, i₃) = j
⊢ Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ X₂ Y₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ Y₃ j) (mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ j)
        (mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 Y₃) j)))
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p Y₁ X₂ X₃ j) (mapTrifunctorMapMap F p φ_1 (𝟙 X₂) (𝟙 X₃) j)
        (mapTrifunctorMapMap F p (𝟙 Y₁) (𝟙 X₂) φ j)))

Tactic:
simp only [ι_mapTrifunctorMapMap_assoc, categoryOfGradedObjects_id, Functor.map_id,
              NatTrans.id_app, ι_mapTrifunctorMapMap, id_comp, NatTrans.naturality_assoc]

Premises used: CategoryTheory.GradedObject.categoryOfGradedObjects_id, CategoryTheory.GradedObject.ι_mapTrifunctorMapMap_assoc, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Category.id_comp, CategoryTheory.GradedObject.ι_mapTrifunctorMapMap
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
inst_6 :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
w :
  ∀ (X₃ : GradedObject I₃ C₃) (j : J),
    Eq.{v_4 + 1}
      (NatTrans.app
        ((mapTrifunctorMapFunctorObj F p X₁).map ψ ≫
          { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃), naturality := ⋯ })
        X₃ j)
      (NatTrans.app
        ({ app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃), naturality := ⋯ :
            NatTrans ((mapTrifunctorMapFunctorObj F p X₁).obj X₂) ((mapTrifunctorMapFunctorObj F p Y₁).obj X₂) } ≫
          (mapTrifunctorMapFunctorObj F p Y₁).map ψ)
        X₃ j)
⊢ (mapTrifunctorMapFunctorObj F p X₁).map ψ ≫
      { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃), naturality := ⋯ } =
    { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃), naturality := ⋯ :
        NatTrans ((mapTrifunctorMapFunctorObj F p X₁).obj X₂) ((mapTrifunctorMapFunctorObj F p Y₁).obj X₂) } ≫
      (mapTrifunctorMapFunctorObj F p Y₁).map ψ

Tactic:
ext X₃ j
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
inst_6 :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
j : J
w :
  Eq (α := mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ mapTrifunctorMapObj F p Y₁ Y₂ X₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ Y₂ X₃ j) (mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃) j)
      (mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃) j))
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p Y₁ X₂ X₃ j) (mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃) j)
      (mapTrifunctorMapMap F p (𝟙 Y₁) ψ (𝟙 X₃) j))
⊢ Eq.{v_4 + 1}
    (NatTrans.app
      ((mapTrifunctorMapFunctorObj F p X₁).map ψ ≫
        { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃), naturality := ⋯ })
      X₃ j)
    (NatTrans.app
      ({ app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃), naturality := ⋯ :
          NatTrans ((mapTrifunctorMapFunctorObj F p X₁).obj X₂) ((mapTrifunctorMapFunctorObj F p Y₁).obj X₂) } ≫
        (mapTrifunctorMapFunctorObj F p Y₁).map ψ)
      X₃ j)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
inst_6 :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
j : J
w :
  ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
    Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ X₃ j)
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
        (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ Y₂ X₃ j) (mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃) j)
          (mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃) j)))
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
        (CategoryStruct.comp (Y := mapTrifunctorMapObj F p Y₁ X₂ X₃ j) (mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃) j)
          (mapTrifunctorMapMap F p (𝟙 Y₁) ψ (𝟙 X₃) j)))
⊢ Eq (α := mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ mapTrifunctorMapObj F p Y₁ Y₂ X₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ Y₂ X₃ j) (mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃) j)
      (mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃) j))
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p Y₁ X₂ X₃ j) (mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃) j)
      (mapTrifunctorMapMap F p (𝟙 Y₁) ψ (𝟙 X₃) j))

Tactic:
ext i₁ i₂ i₃ h
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
inst_6 :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
j : J
i₁ : I₁
i₂ : I₂
i₃ : I₃
h : p (i₁, i₂, i₃) = j
⊢ Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ X₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ Y₂ X₃ j) (mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃) j)
        (mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃) j)))
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p Y₁ X₂ X₃ j) (mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃) j)
        (mapTrifunctorMapMap F p (𝟙 Y₁) ψ (𝟙 X₃) j)))

Tactic:
simp only [ι_mapTrifunctorMapMap_assoc, categoryOfGradedObjects_id, Functor.map_id,
          NatTrans.id_app, ι_mapTrifunctorMapMap, id_comp,
          NatTrans.naturality_app_assoc]

Premises used: CategoryTheory.GradedObject.categoryOfGradedObjects_id, CategoryTheory.GradedObject.ι_mapTrifunctorMapMap_assoc, CategoryTheory.NatTrans.naturality_app_assoc, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app, CategoryTheory.Category.id_comp, CategoryTheory.GradedObject.ι_mapTrifunctorMapMap
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_6 : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst_7 : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
rw : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = r (i₁, i₂, i₃)
rw₁ rw₂ : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = ρ₁₂.q (ρ₁₂.p ((i₁, i₂, i₃).1, (i₁, i₂, i₃).2.1), (i₁, i₂, i₃).2.2)
⊢ ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = j

Tactic:
rw [← h, ← ρ₁₂.hpq]

Premises used: CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.hpq
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_6 : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst_7 : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₁₂ : ρ₁₂.I₁₂
h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂
rw : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = j
rw₁ : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = r (i₁, i₂, i₃)
rw₂ rw₃ : ρ₁₂.q (ρ₁₂.p (i₁, i₂), i₃) = ρ₁₂.q (ρ₁₂.p ((i₁, i₂, i₃).1, (i₁, i₂, i₃).2.1), (i₁, i₂, i₃).2.2)
⊢ ρ₁₂.q (i₁₂, i₃) = j

Tactic:
rw [← h₁₂, ← h, ← ρ₁₂.hpq]

Premises used: CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.hpq
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_5 : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst_6 : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
i₁₂ : ρ₁₂.I₁₂
h₁₂ : ρ₁₂.p (i₁, i₂) = i₁₂
subst :
  Eq (α :=
    (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶
      mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j)
    (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
    (NatTrans.app (G.map (ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ (ρ₁₂.p (i₁, i₂)) ⋯)) (X₃ i₃) ≫
      ιMapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ (ρ₁₂.p (i₁, i₂)) i₃ j ⋯)
⊢ Eq (α :=
    (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶
      mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j)
    (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
    (NatTrans.app (G.map (ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)) (X₃ i₃) ≫
      ιMapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j ⋯)

Tactic:
subst h₁₂
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_5 : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst_6 : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ Eq (α :=
    (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶
      mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j)
    (ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
    (NatTrans.app (G.map (ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ (ρ₁₂.p (i₁, i₂)) ⋯)) (X₃ i₃) ≫
      ιMapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ (ρ₁₂.p (i₁, i₂)) i₃ j ⋯)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_6 : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst_7 : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun (i₁₂ : ρ₁₂.I₁₂) ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
have :
  (h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)) → IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
⊢ IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)

Tactic:
have h₁₂ : ∀ i₁₂, IsColimit (c₁₂ i₁₂) := fun i₁₂ =>
    (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).isColimitCofanMapObj ρ₁₂.p i₁₂
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_6 : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst_7 : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun (i₁₂ : ρ₁₂.I₁₂) ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
c : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).CofanMapObjFun ρ₁₂.q j :=
  ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j
have : (hc : IsColimit c) → IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
⊢ IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)

Tactic:
have hc : IsColimit c := (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj
    (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).isColimitCofanMapObj ρ₁₂.q j
-- Module: Mathlib.CategoryTheory.GradedObject.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
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} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData.{u_7, u_8, u_9, u_10, u_11} r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst_6 : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst_7 : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun (i₁₂ : ρ₁₂.I₁₂) ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
c : ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).CofanMapObjFun ρ₁₂.q j :=
  ((Functor.obj (mapBifunctor G ρ₁₂.I₁₂ I₃) (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j
hc : IsColimit c
c₁₂' : (i : (↑(ρ₁₂.q ⁻¹' {j}) : Type (max u_9 u_11))) →
  Cocone (J := Discrete (↑(ρ₁₂.p ⁻¹' {(↑i : ρ₁₂.I₁₂ × I₃).1}) : Type (max u_7 u_8)))
    (Discrete.functor ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p (↑i : ρ₁₂.I₁₂ × I₃).1) ⋙
      G.flip.obj (X₃ (↑i : ρ₁₂.I₁₂ × I₃).2)) :=
  fun (i : (↑(ρ₁₂.q ⁻¹' {j}) : Type (max u_9 u_11))) ↦
    (G.flip.obj (X₃ (↑i : ρ₁₂.I₁₂ × I₃).2)).mapCocone (c₁₂ (↑i : ρ₁₂.I₁₂ × I₃).1)
have :
  (hc₁₂' : (i : (↑(ρ₁₂.q ⁻¹' {j}) : Type (max u_9 u_11))) → IsColimit (c₁₂' i)) →
    IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
⊢ IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)

Tactic:
have hc₁₂' : ∀ i, IsColimit (c₁₂' i) := fun i => isColimitOfPreserves _ (h₁₂ i.1.1)