awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₁ Y₁ : GradedObject I₁ C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : GradedObject I₃ C₃
f₃ : X₃ ⟶ Y₃
inst_4 : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
inst_5 : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : p (i₁, i₂, i₃) = j
⊢ Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
    ((NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃)) ≫
      (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
    (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
          (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
have rw : Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
  (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
    (((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃)) ≫
      (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
  (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
    ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
        (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
Tactic: rw [assoc, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₁ Y₁ : GradedObject I₁ C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : GradedObject I₃ C₃
f₃ : X₃ ⟶ Y₃
inst_4 : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
inst_5 : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : p (i₁, i₂, i₃) = j
rw :
  Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
    (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
      (((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃)) ≫
        (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
    (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
          (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
⊢ Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
    ((NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃)) ≫
      (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
    (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
          (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
have rw₁ : Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
  (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
    ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
        (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
  (NatTrans.app ((F.map (f₁ i₁)).app (X₂ i₂)) (X₃ i₃) ≫
    ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
        (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)
Tactic: rw [assoc, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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 ≫ φ'
⊢ φ = φ'
have hfg : ∀ (i : I₁ × I₂ × I₃) (hij : p i = j),
  ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p i j hij ≫ φ =
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p i j hij ≫ φ'
Tactic: apply mapObj_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₃
⊢ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (𝟙 X₃) = 𝟙 (mapTrifunctorMapObj F p X₁ X₂ X₃)
have 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))
Tactic: ext j i₁ i₂ i₃ h
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₃
⊢ 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₂) ψ))
have 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))
Tactic: ext j i₁ i₂ i₃ h
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₃) ⟶
      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))
have 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)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₂
⊢ 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 := ⋯ })
have 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 := sorry,
          map_comp := sorry }
        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 := sorry } 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 := sorry, map_comp := sorry })
        X₃ j))
Tactic: ext X₃ j i₁ i₂ i₃ h
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₂
⊢ 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 := ⋯ })
have 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 := sorry,
          map_comp := sorry }
        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 := sorry } 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 := sorry, map_comp := sorry })
          { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃), naturality := sorry }
          { app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃), naturality := sorry })
        X₃ j))
Tactic: ext X₃ j i₁ i₂ i₃
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₃
⊢ ((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 φ
have 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 φ
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₃
⊢ ((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 φ
have 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))
Tactic: ext j i₁ i₂ i₃ h
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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)
      ((((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))
have 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)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.GradedObject.Trifunctor (goal)
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₂
⊢ (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 ψ
have 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 := sorry })
      X₃ j)
    (NatTrans.app
      ({ app := fun (X₃ : GradedObject I₃ C₃) ↦ mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃), naturality := sorry :
          NatTrans ((mapTrifunctorMapFunctorObj F p X₁).obj X₂) ((mapTrifunctorMapFunctorObj F p Y₁).obj X₂) } ≫
        (mapTrifunctorMapFunctorObj F p Y₁).map ψ)
      X₃ j)
Tactic: ext X₃ j