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
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₄
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
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
Y : C₄
j : J
inst_4 : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
φ φ' : mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
    ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ'
i₁ : I₁
i₂ : I₂
i₃ : I₃
hi : p (i₁, i₂, i₃) = j
⊢ ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p (i₁, i₂, i₃) j hi ≫ φ =
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p (i₁, i₂, i₃) j hi ≫ φ'

Tactic:
apply 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
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
h : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
⊢ (((mapTrifunctorObj F X₁ I₂ I₃).obj X₂).obj X₃).HasMap p

Tactic:
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
X₁ : GradedObject I₁ C₁
inst_6 :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
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 X₁ X₂ X₃ 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 (𝟙 X₁) (𝟙 X₂) (𝟙 X₃) j))
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
        (𝟙 (mapTrifunctorMapObj F p X₁ X₂ X₃) j))
⊢ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (𝟙 X₃) = 𝟙 (mapTrifunctorMapObj F p X₁ X₂ X₃)

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
X₁ : GradedObject I₁ C₁
inst_6 :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ : GradedObject I₂ C₂
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 X₁ X₂ X₃ 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 (𝟙 X₁) (𝟙 X₂) (𝟙 X₃) j))
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (𝟙 (mapTrifunctorMapObj F p X₁ X₂ X₃) j))

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

Premises used: CategoryTheory.GradedObject.categoryOfGradedObjects_id, CategoryTheory.Category.comp_id, 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₁ ⥤ 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
X₁ : GradedObject I₁ C₁
inst_6 :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ : GradedObject I₂ C₂
X₃ Y₃ Z₃ : GradedObject I₃ C₃
φ : X₃ ⟶ Y₃
ψ : Y₃ ⟶ Z₃
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 X₁ X₂ Z₃ 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 (𝟙 X₁) (𝟙 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₁ X₂ Y₃) (mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ)
          (mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) ψ) j))
⊢ Eq (α := mapTrifunctorMapObj F p X₁ X₂ X₃ ⟶ mapTrifunctorMapObj F p X₁ X₂ Z₃)
    (mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (φ ≫ ψ))
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ Y₃) (mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ)
      (mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) ψ))

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
X₁ : GradedObject I₁ C₁
inst_6 :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ : GradedObject I₂ C₂
X₃ Y₃ Z₃ : GradedObject I₃ C₃
φ : X₃ ⟶ Y₃
ψ : Y₃ ⟶ Z₃
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 X₁ X₂ Z₃ 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 (𝟙 X₁) (𝟙 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₁ X₂ Y₃) (mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ)
        (mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) ψ) j))

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GradedObject.categoryOfGradedObjects_id, CategoryTheory.GradedObject.ι_mapTrifunctorMapMap_assoc, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app, CategoryTheory.Functor.map_comp, CategoryTheory.GradedObject.categoryOfGradedObjects_comp, 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
X₁ : GradedObject I₁ C₁
inst_6 :
  ∀ (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₃
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 X₁ Y₂ 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 (𝟙 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₁ Y₂ X₃ j) (mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃) j)
        (mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) ψ j)))
⊢ Eq (α :=
    ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶
      Functor.obj
        { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Y₂ X₃,
          map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) φ, map_id := ⋯,
          map_comp := ⋯ }
        Y₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      ((Functor.map
            { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ X₂ X₃,
              map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ,
              map_id := ⋯, map_comp := ⋯ : GradedObject I₃ C₃ ⥤ GradedObject J C₄ }
            ψ ≫
          mapTrifunctorMapMap F p (𝟙 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 :=
        Functor.obj
          { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Y₂ X₃,
            map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) φ,
            map_id := ⋯, map_comp := ⋯ }
          X₃)
        (mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃))
        (Functor.map
          { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Y₂ X₃,
            map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) φ,
            map_id := ⋯, map_comp := ⋯ }
          ψ)
        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
X₁ : GradedObject I₁ C₁
inst_6 :
  ∀ (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₃
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 X₁ Y₂ 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 (𝟙 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₁ Y₂ X₃ j) (mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃) j)
        (mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) ψ 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
X₁ : GradedObject I₁ C₁
inst_6 :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ : GradedObject I₂ C₂
w :
  ∀ (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₃) ⟶
        Functor.obj
          { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ X₂ X₃,
            map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ,
            map_id := ⋯, map_comp := ⋯ }
          X₃ j)
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
        (NatTrans.app
          { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (𝟙 X₃), naturality := ⋯ } X₃
          j))
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
        (NatTrans.app
          (𝟙
            { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ X₂ X₃,
              map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ,
              map_id := ⋯, map_comp := ⋯ })
          X₃ j))
⊢ Eq (α :=
    Quiver.Hom (V := GradedObject I₃ C₃ ⥤ GradedObject J C₄)
      { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ X₂ X₃,
        map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ, map_id := ⋯,
        map_comp := ⋯ }
      { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ X₂ X₃,
        map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ, map_id := ⋯,
        map_comp := ⋯ })
    { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (𝟙 X₃), naturality := ⋯ }
    (𝟙
      { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ X₂ X₃,
        map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ, map_id := ⋯,
        map_comp := ⋯ })

Tactic:
ext X₃ 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
X₁ : GradedObject I₁ C₁
inst_6 :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ : GradedObject I₂ C₂
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₃) ⟶
      Functor.obj
        { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ X₂ X₃,
          map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ, map_id := ⋯,
          map_comp := ⋯ }
        X₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (NatTrans.app
        { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (𝟙 X₃), naturality := ⋯ } X₃ j))
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (NatTrans.app
        (𝟙
          { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ X₂ X₃,
            map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ,
            map_id := ⋯, map_comp := ⋯ })
        X₃ j))

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

Premises used: CategoryTheory.GradedObject.categoryOfGradedObjects_id, CategoryTheory.Category.comp_id, 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₁ ⥤ 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
X₁ : GradedObject I₁ C₁
inst_6 :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ Y₂ Z₂ : GradedObject I₂ C₂
φ : X₂ ⟶ Y₂
ψ : Y₂ ⟶ Z₂
w :
  ∀ (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₃) ⟶
        Functor.obj
          { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Z₂ X₃,
            map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Z₂) φ,
            map_id := ⋯, map_comp := ⋯ }
          X₃ j)
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
        (NatTrans.app
          { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (φ ≫ ψ) (𝟙 X₃), naturality := ⋯ } X₃
          j))
      (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
        (NatTrans.app
          (CategoryStruct.comp (Y :=
            { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Y₂ X₃,
              map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) φ,
              map_id := ⋯, map_comp := ⋯ })
            { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃), naturality := ⋯ }
            { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃), naturality := ⋯ })
          X₃ j))
⊢ Eq (α :=
    Quiver.Hom (V := GradedObject I₃ C₃ ⥤ GradedObject J C₄)
      { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ X₂ X₃,
        map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ, map_id := ⋯,
        map_comp := ⋯ }
      { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Z₂ X₃,
        map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Z₂) φ, map_id := ⋯,
        map_comp := ⋯ })
    { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (φ ≫ ψ) (𝟙 X₃), naturality := ⋯ }
    (CategoryStruct.comp (Y :=
      { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Y₂ X₃,
        map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) φ, map_id := ⋯,
        map_comp := ⋯ })
      { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃), naturality := ⋯ }
      { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃), naturality := ⋯ })

Tactic:
ext X₃ j i₁ i₂ 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₁ ⥤ 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
X₁ : GradedObject I₁ C₁
inst_6 :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ Y₂ Z₂ : GradedObject I₂ C₂
φ : X₂ ⟶ Y₂
ψ : Y₂ ⟶ Z₂
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₃) ⟶
      Functor.obj
        { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Z₂ X₃,
          map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Z₂) φ, map_id := ⋯,
          map_comp := ⋯ }
        X₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (NatTrans.app
        { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (φ ≫ ψ) (𝟙 X₃), naturality := ⋯ } X₃ j))
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          { obj := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapObj F p X₁ Y₂ X₃,
            map := fun {x x_1 : GradedObject I₃ C₃} (φ : x ⟶ x_1) ↦ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 Y₂) φ,
            map_id := ⋯, map_comp := ⋯ })
          { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃), naturality := ⋯ }
          { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃), naturality := ⋯ })
        X₃ j))

Tactic:
simp only [ι_mapTrifunctorMapMap, categoryOfGradedObjects_id, Functor.map_id,
      NatTrans.id_app, categoryOfGradedObjects_comp, Functor.map_comp, NatTrans.comp_app,
      id_comp, assoc, ι_mapTrifunctorMapMap_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.GradedObject.categoryOfGradedObjects_id, CategoryTheory.GradedObject.ι_mapTrifunctorMapMap_assoc, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.GradedObject.categoryOfGradedObjects_comp, CategoryTheory.Category.id_comp, CategoryTheory.GradedObject.ι_mapTrifunctorMapMap