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 F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
α : F ⟶ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ : GradedObject I₁ C₁
X₂ Y₂ : GradedObject I₂ C₂
φ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
w :
  Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ ((F'.obj (X₁ i₁)).obj (Y₂ i₂)).obj (X₃ i₃))
    (((F.obj (X₁ i₁)).map (φ i₂)).app (X₃ i₃) ≫ NatTrans.app (NatTrans.app (α.app (X₁ i₁)) (Y₂ i₂)) (X₃ i₃))
    (NatTrans.app (NatTrans.app (α.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫ ((F'.obj (X₁ i₁)).map (φ i₂)).app (X₃ i₃))
⊢ Eq.{v_4 + 1}
    (NatTrans.app
      (((mapTrifunctor F I₁ I₂ I₃).obj X₁).map φ ≫
        {
          app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
            NatTrans.app (NatTrans.app (α.app (X₁ x_1.1)) (Y₂ x_1.2.1)) (x x_1.2.2),
          naturality := ⋯ })
      X₃ (i₁, i₂, i₃))
    (NatTrans.app
      ({
          app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
            NatTrans.app (NatTrans.app (α.app (X₁ x_1.1)) (X₂ x_1.2.1)) (x x_1.2.2),
          naturality := ⋯ :
          NatTrans (((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂) (((mapTrifunctor F' I₁ I₂ I₃).obj X₁).obj X₂) } ≫
        ((mapTrifunctor F' I₁ I₂ I₃).obj X₁).map φ)
      X₃ (i₁, i₂, i₃))

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 F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
α : F ⟶ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ : GradedObject I₁ C₁
X₂ Y₂ : GradedObject I₂ C₂
φ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ ((F'.obj (X₁ i₁)).obj (Y₂ i₂)).obj (X₃ i₃))
    (((F.obj (X₁ i₁)).map (φ i₂)).app (X₃ i₃) ≫ NatTrans.app (NatTrans.app (α.app (X₁ i₁)) (Y₂ i₂)) (X₃ i₃))
    (NatTrans.app (NatTrans.app (α.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫ ((F'.obj (X₁ i₁)).map (φ i₂)).app (X₃ i₃))

Tactic:
simp only [← NatTrans.comp_app, NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.comp_app
-- 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 F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
α : F ⟶ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
w :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
    Eq.{v_4 + 1}
      (NatTrans.app
        (NatTrans.app
          ((mapTrifunctor F I₁ I₂ I₃).map φ ≫
            {
              app := fun (X₂ : GradedObject I₂ C₂) ↦
                {
                  app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
                    NatTrans.app (NatTrans.app (α.app (Y₁ x_1.1)) (X₂ x_1.2.1)) (x x_1.2.2),
                  naturality := ⋯ },
              naturality := ⋯ })
          X₂)
        X₃ (i₁, i₂, i₃))
      (NatTrans.app
        (NatTrans.app
          ({
              app := fun (X₂ : GradedObject I₂ C₂) ↦
                {
                  app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
                    NatTrans.app (NatTrans.app (α.app (X₁ x_1.1)) (X₂ x_1.2.1)) (x x_1.2.2),
                  naturality := ⋯ :
                  NatTrans (((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂) (((mapTrifunctor F' I₁ I₂ I₃).obj X₁).obj X₂) },
              naturality := ⋯ : NatTrans ((mapTrifunctor F I₁ I₂ I₃).obj X₁) ((mapTrifunctor F' I₁ I₂ I₃).obj X₁) } ≫
            (mapTrifunctor F' I₁ I₂ I₃).map φ)
          X₂)
        X₃ (i₁, i₂, i₃))
⊢ (mapTrifunctor F I₁ I₂ I₃).map φ ≫
      {
        app := fun (X₂ : GradedObject I₂ C₂) ↦
          {
            app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
              NatTrans.app (NatTrans.app (α.app (Y₁ x_1.1)) (X₂ x_1.2.1)) (x x_1.2.2),
            naturality := ⋯ },
        naturality := ⋯ } =
    {
        app := fun (X₂ : GradedObject I₂ C₂) ↦
          {
            app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
              NatTrans.app (NatTrans.app (α.app (X₁ x_1.1)) (X₂ x_1.2.1)) (x x_1.2.2),
            naturality := ⋯ :
            NatTrans (((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂) (((mapTrifunctor F' I₁ I₂ I₃).obj X₁).obj X₂) },
        naturality := ⋯ : NatTrans ((mapTrifunctor F I₁ I₂ I₃).obj X₁) ((mapTrifunctor F' I₁ I₂ I₃).obj X₁) } ≫
      (mapTrifunctor F' I₁ I₂ I₃).map φ

Tactic:
ext X₂ X₃ ⟨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 F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
α : F ⟶ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
w :
  Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ ((F'.obj (Y₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃))
    (NatTrans.app ((F.map (φ i₁)).app (X₂ i₂)) (X₃ i₃) ≫ NatTrans.app (NatTrans.app (α.app (Y₁ i₁)) (X₂ i₂)) (X₃ i₃))
    (NatTrans.app (NatTrans.app (α.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫ NatTrans.app ((F'.map (φ i₁)).app (X₂ i₂)) (X₃ i₃))
⊢ Eq.{v_4 + 1}
    (NatTrans.app
      (NatTrans.app
        ((mapTrifunctor F I₁ I₂ I₃).map φ ≫
          {
            app := fun (X₂ : GradedObject I₂ C₂) ↦
              {
                app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
                  NatTrans.app (NatTrans.app (α.app (Y₁ x_1.1)) (X₂ x_1.2.1)) (x x_1.2.2),
                naturality := ⋯ },
            naturality := ⋯ })
        X₂)
      X₃ (i₁, i₂, i₃))
    (NatTrans.app
      (NatTrans.app
        ({
            app := fun (X₂ : GradedObject I₂ C₂) ↦
              {
                app := fun (x : GradedObject I₃ C₃) (x_1 : I₁ × I₂ × I₃) ↦
                  NatTrans.app (NatTrans.app (α.app (X₁ x_1.1)) (X₂ x_1.2.1)) (x x_1.2.2),
                naturality := ⋯ :
                NatTrans (((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂) (((mapTrifunctor F' I₁ I₂ I₃).obj X₁).obj X₂) },
            naturality := ⋯ : NatTrans ((mapTrifunctor F I₁ I₂ I₃).obj X₁) ((mapTrifunctor F' I₁ I₂ I₃).obj X₁) } ≫
          (mapTrifunctor F' I₁ I₂ I₃).map φ)
        X₂)
      X₃ (i₁, i₂, i₃))

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 F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
α : F ⟶ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ ((F'.obj (Y₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃))
    (NatTrans.app ((F.map (φ i₁)).app (X₂ i₂)) (X₃ i₃) ≫ NatTrans.app (NatTrans.app (α.app (Y₁ i₁)) (X₂ i₂)) (X₃ i₃))
    (NatTrans.app (NatTrans.app (α.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫ NatTrans.app ((F'.map (φ i₁)).app (X₂ i₂)) (X₃ i₃))

Tactic:
simp only [← NatTrans.comp_app, NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.comp_app
-- 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 F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
e : F ≅ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
w :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
    (((mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃).app X₁).app X₂).app X₃
        (i₁, i₂, i₃) =
      ((NatTrans.app (𝟙 (mapTrifunctor F I₁ I₂ I₃)) X₁).app X₂).app X₃ (i₁, i₂, i₃)
⊢ mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃ = 𝟙 (mapTrifunctor F I₁ I₂ I₃)

Tactic:
ext X₁ X₂ X₃ ⟨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 F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
e : F ≅ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
w :
  NatTrans.app (NatTrans.app (e.hom.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫
      NatTrans.app (NatTrans.app (e.inv.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) =
    𝟙 (((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃))
⊢ (((mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃).app X₁).app X₂).app X₃
      (i₁, i₂, i₃) =
    ((NatTrans.app (𝟙 (mapTrifunctor F I₁ I₂ I₃)) X₁).app X₂).app X₃ (i₁, i₂, i₃)

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 F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
e : F ≅ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ NatTrans.app (NatTrans.app (e.hom.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫
      NatTrans.app (NatTrans.app (e.inv.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) =
    𝟙 (((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃))

Tactic:
simp only [← NatTrans.comp_app, e.hom_inv_id, NatTrans.id_app]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.NatTrans.id_app, CategoryTheory.NatTrans.comp_app
-- 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 F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
e : F ≅ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
w :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃) (i₁ : I₁) (i₂ : I₂) (i₃ : I₃),
    (((mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃).app X₁).app X₂).app X₃
        (i₁, i₂, i₃) =
      ((NatTrans.app (𝟙 (mapTrifunctor F' I₁ I₂ I₃)) X₁).app X₂).app X₃ (i₁, i₂, i₃)
⊢ mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃ = 𝟙 (mapTrifunctor F' I₁ I₂ I₃)

Tactic:
ext X₁ X₂ X₃ ⟨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 F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
e : F ≅ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
w :
  NatTrans.app (NatTrans.app (e.inv.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫
      NatTrans.app (NatTrans.app (e.hom.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) =
    𝟙 (((F'.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃))
⊢ (((mapTrifunctorMapNatTrans e.inv I₁ I₂ I₃ ≫ mapTrifunctorMapNatTrans e.hom I₁ I₂ I₃).app X₁).app X₂).app X₃
      (i₁, i₂, i₃) =
    ((NatTrans.app (𝟙 (mapTrifunctor F' I₁ I₂ I₃)) X₁).app X₂).app X₃ (i₁, i₂, i₃)

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 F' : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
e : F ≅ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ NatTrans.app (NatTrans.app (e.inv.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) ≫
      NatTrans.app (NatTrans.app (e.hom.app (X₁ i₁)) (X₂ i₂)) (X₃ i₃) =
    𝟙 (((F'.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃))

Tactic:
simp only [← NatTrans.comp_app, e.inv_hom_id, NatTrans.id_app]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.NatTrans.id_app, CategoryTheory.NatTrans.comp_app
-- 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₁ 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
dsimp :
  Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j)
      (((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p (i₁, i₂, i₃) j h)
      (mapMap
        ((((mapTrifunctor F I₁ I₂ I₃).map f₁).app X₂).app X₃ ≫
          (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).map f₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).map f₃)
        p 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₃) ≫
          ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).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)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j) (ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h)
      (mapTrifunctorMapMap F p f₁ f₂ f₃ 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₃) ≫ ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h)

Tactic:
dsimp only [ιMapTrifunctorMapObj, mapTrifunctorMapMap]

Premises used: CategoryTheory.GradedObject.mapTrifunctorMapMap, CategoryTheory.GradedObject.ιMapTrifunctorMapObj
-- 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₁ 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.{v_4 + 1} (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
    (((((mapTrifunctor F I₁ I₂ I₃).map f₁).app X₂).app X₃ ≫
            (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).map f₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).map f₃)
          (i₁, i₂, i₃) ≫
        ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h :
      (((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃ (i₁, i₂, i₃) ⟶
        ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).mapObj p 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₃) ≫
            ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h :
      ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
⊢ Eq (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
    (CategoryStruct.comp (Y := mapTrifunctorMapObj F p X₁ X₂ X₃ j)
      (((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p (i₁, i₂, i₃) j h)
      (mapMap
        ((((mapTrifunctor F I₁ I₂ I₃).map f₁).app X₂).app X₃ ≫
          (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).map f₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).map f₃)
        p 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₃) ≫
          ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h)

Tactic:
rw [ι_mapMap]

Premises used: CategoryTheory.GradedObject.ι_mapMap
-- 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₁ 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
dsimp :
  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.{v_4 + 1} (α := ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ j)
    (((((mapTrifunctor F I₁ I₂ I₃).map f₁).app X₂).app X₃ ≫
            (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).map f₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).map f₃)
          (i₁, i₂, i₃) ≫
        ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h :
      (((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃ (i₁, i₂, i₃) ⟶
        ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).mapObj p 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₃) ≫
            ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h :
      ((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p Y₁ Y₂ Y₃ 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
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)
rw₁ 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)

Tactic:
rw [assoc, assoc]

Premises used: CategoryTheory.Category.assoc
-- 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 ≫ φ'
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

Premises used: CategoryTheory.GradedObject.mapObj_ext