awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.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₄
X₁ Y₁ : C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
ψ : X₂ ⟶ Y₂
X₃ : C₃
⊢ (G.map ((F₁₂.obj X₁).map ψ)).app X₃ ≫ (G.map ((F₁₂.map φ).app Y₂)).app X₃ =
    (G.map ((F₁₂.map φ).app X₂)).app X₃ ≫ (G.map ((F₁₂.obj Y₁).map ψ)).app X₃

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

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.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 G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
φ : G ⟶ G'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
w :
  ∀ (X₃ : C₃),
    (((bifunctorComp₁₂ F₁₂ G).obj X₁).map f ≫
            { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj Y₂)) X₃, naturality := ⋯ :
              NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj Y₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj Y₂) }).app
        X₃ =
      NatTrans.app
        ({ app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃, naturality := ⋯ :
            NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj X₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj X₂) } ≫
          ((bifunctorComp₁₂ F₁₂ G').obj X₁).map f)
        X₃
⊢ ((bifunctorComp₁₂ F₁₂ G).obj X₁).map f ≫
      { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj Y₂)) X₃, naturality := ⋯ :
        NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj Y₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj Y₂) } =
    { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃, naturality := ⋯ :
        NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj X₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj X₂) } ≫
      ((bifunctorComp₁₂ F₁₂ G').obj X₁).map f

Tactic:
ext X₃
-- Module: Mathlib.CategoryTheory.Functor.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 G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
φ : G ⟶ G'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
w :
  (G.map ((F₁₂.obj X₁).map f)).app X₃ ≫ NatTrans.app (φ.app ((F₁₂.obj X₁).obj Y₂)) X₃ =
    NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃ ≫ (G'.map ((F₁₂.obj X₁).map f)).app X₃
⊢ (((bifunctorComp₁₂ F₁₂ G).obj X₁).map f ≫
          { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj Y₂)) X₃, naturality := ⋯ :
            NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj Y₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj Y₂) }).app
      X₃ =
    NatTrans.app
      ({ app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃, naturality := ⋯ :
          NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj X₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj X₂) } ≫
        ((bifunctorComp₁₂ F₁₂ G').obj X₁).map f)
      X₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Functor.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 G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
φ : G ⟶ G'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (G.map ((F₁₂.obj X₁).map f)).app X₃ ≫ NatTrans.app (φ.app ((F₁₂.obj X₁).obj Y₂)) X₃ =
    NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃ ≫ (G'.map ((F₁₂.obj X₁).map f)).app X₃

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

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.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 G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
φ : G ⟶ G'
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
w :
  ∀ (X₂ : C₂) (X₃ : C₃),
    NatTrans.app
        (NatTrans.app
          ((bifunctorComp₁₂ F₁₂ G).map f ≫
            {
              app := fun (X₂ : C₂) ↦
                { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj Y₁).obj X₂)) X₃, naturality := ⋯ },
              naturality := ⋯ })
          X₂)
        X₃ =
      NatTrans.app
        (NatTrans.app
          ({
              app := fun (X₂ : C₂) ↦
                { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃, naturality := ⋯ :
                  NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj X₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj X₂) },
              naturality := ⋯ : NatTrans ((bifunctorComp₁₂ F₁₂ G).obj X₁) ((bifunctorComp₁₂ F₁₂ G').obj X₁) } ≫
            (bifunctorComp₁₂ F₁₂ G').map f)
          X₂)
        X₃
⊢ (bifunctorComp₁₂ F₁₂ G).map f ≫
      {
        app := fun (X₂ : C₂) ↦
          { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj Y₁).obj X₂)) X₃, naturality := ⋯ },
        naturality := ⋯ } =
    {
        app := fun (X₂ : C₂) ↦
          { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃, naturality := ⋯ :
            NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj X₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj X₂) },
        naturality := ⋯ : NatTrans ((bifunctorComp₁₂ F₁₂ G).obj X₁) ((bifunctorComp₁₂ F₁₂ G').obj X₁) } ≫
      (bifunctorComp₁₂ F₁₂ G').map f

Tactic:
ext X₂ X₃
-- Module: Mathlib.CategoryTheory.Functor.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 G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
φ : G ⟶ G'
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
w :
  (G.map ((F₁₂.map f).app X₂)).app X₃ ≫ NatTrans.app (φ.app ((F₁₂.obj Y₁).obj X₂)) X₃ =
    NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃ ≫ (G'.map ((F₁₂.map f).app X₂)).app X₃
⊢ NatTrans.app
      (NatTrans.app
        ((bifunctorComp₁₂ F₁₂ G).map f ≫
          {
            app := fun (X₂ : C₂) ↦
              { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj Y₁).obj X₂)) X₃, naturality := ⋯ },
            naturality := ⋯ })
        X₂)
      X₃ =
    NatTrans.app
      (NatTrans.app
        ({
            app := fun (X₂ : C₂) ↦
              { app := fun (X₃ : C₃) ↦ NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃, naturality := ⋯ :
                NatTrans (((bifunctorComp₁₂ F₁₂ G).obj X₁).obj X₂) (((bifunctorComp₁₂ F₁₂ G').obj X₁).obj X₂) },
            naturality := ⋯ : NatTrans ((bifunctorComp₁₂ F₁₂ G).obj X₁) ((bifunctorComp₁₂ F₁₂ G').obj X₁) } ≫
          (bifunctorComp₁₂ F₁₂ G').map f)
        X₂)
      X₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Functor.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 G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
φ : G ⟶ G'
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ (G.map ((F₁₂.map f).app X₂)).app X₃ ≫ NatTrans.app (φ.app ((F₁₂.obj Y₁).obj X₂)) X₃ =
    NatTrans.app (φ.app ((F₁₂.obj X₁).obj X₂)) X₃ ≫ (G'.map ((F₁₂.map f).app X₂)).app X₃

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

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
w :
  ∀ (X₃ : C₃),
    (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).map f ≫
            { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app Y₂)).app X₃, naturality := ⋯ :
              NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj Y₂)
                (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj Y₂) }).app
        X₃ =
      NatTrans.app
        ({ app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ :
            NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂)
              (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj X₂) } ≫
          ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).map f)
        X₃
⊢ ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).map f ≫
      { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app Y₂)).app X₃, naturality := ⋯ :
        NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj Y₂)
          (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj Y₂) } =
    { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ :
        NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂)
          (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj X₂) } ≫
      ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).map f

Tactic:
ext X₃
-- Module: Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
w :
  (G.map ((F₁₂.obj X₁).map f)).app X₃ ≫ (G.map ((φ.app X₁).app Y₂)).app X₃ =
    (G.map ((φ.app X₁).app X₂)).app X₃ ≫ (G.map ((F₁₂'.obj X₁).map f)).app X₃
⊢ (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).map f ≫
          { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app Y₂)).app X₃, naturality := ⋯ :
            NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj Y₂)
              (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj Y₂) }).app
      X₃ =
    NatTrans.app
      ({ app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ :
          NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂)
            (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj X₂) } ≫
        ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).map f)
      X₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (G.map ((F₁₂.obj X₁).map f)).app X₃ ≫ (G.map ((φ.app X₁).app Y₂)).app X₃ =
    (G.map ((φ.app X₁).app X₂)).app X₃ ≫ (G.map ((F₁₂'.obj X₁).map f)).app X₃

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

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
w :
  ∀ (X₂ : C₂) (X₃ : C₃),
    NatTrans.app
        (NatTrans.app
          ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).map f ≫
            { app := fun (X₂ : C₂) ↦ { app := fun (X₃ : C₃) ↦ (G.map ((φ.app Y₁).app X₂)).app X₃, naturality := ⋯ },
              naturality := ⋯ })
          X₂)
        X₃ =
      NatTrans.app
        (NatTrans.app
          ({
              app := fun (X₂ : C₂) ↦
                { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ :
                  NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂)
                    (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj X₂) },
              naturality := ⋯ :
              NatTrans ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁)
                ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁) } ≫
            (Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).map f)
          X₂)
        X₃
⊢ (Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).map f ≫
      { app := fun (X₂ : C₂) ↦ { app := fun (X₃ : C₃) ↦ (G.map ((φ.app Y₁).app X₂)).app X₃, naturality := ⋯ },
        naturality := ⋯ } =
    {
        app := fun (X₂ : C₂) ↦
          { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ :
            NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂)
              (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj X₂) },
        naturality := ⋯ :
        NatTrans ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁)
          ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁) } ≫
      (Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).map f

Tactic:
ext X₂ X₃
-- Module: Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
w :
  (G.map ((F₁₂.map f).app X₂)).app X₃ ≫ (G.map ((φ.app Y₁).app X₂)).app X₃ =
    (G.map ((φ.app X₁).app X₂)).app X₃ ≫ (G.map ((F₁₂'.map f).app X₂)).app X₃
⊢ NatTrans.app
      (NatTrans.app
        ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).map f ≫
          { app := fun (X₂ : C₂) ↦ { app := fun (X₃ : C₃) ↦ (G.map ((φ.app Y₁).app X₂)).app X₃, naturality := ⋯ },
            naturality := ⋯ })
        X₂)
      X₃ =
    NatTrans.app
      (NatTrans.app
        ({
            app := fun (X₂ : C₂) ↦
              { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ :
                NatTrans (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂)
                  (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁).obj X₂) },
            naturality := ⋯ :
            NatTrans ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁)
              ((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).obj X₁) } ≫
          (Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G).map f)
        X₂)
      X₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ (G.map ((F₁₂.map f).app X₂)).app X₃ ≫ (G.map ((φ.app Y₁).app X₂)).app X₃ =
    (G.map ((φ.app X₁).app X₂)).app X₃ ≫ (G.map ((F₁₂'.map f).app X₂)).app X₃

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

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
f : G ⟶ G'
w :
  ∀ (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
    Eq (α :=
      (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂).obj X₃ ⟶
        (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G').obj X₁).obj X₂).obj X₃)
      (NatTrans.app
        (NatTrans.app
          (NatTrans.app
            (Functor.map (bifunctorComp₁₂FunctorObj F₁₂) f ≫
              {
                app := fun (X₁ : C₁) ↦
                  {
                    app := fun (X₂ : C₂) ↦
                      { app := fun (X₃ : C₃) ↦ (G'.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ },
                    naturality := ⋯ },
                naturality := ⋯ })
            X₁)
          X₂)
        X₃)
      (NatTrans.app
        (NatTrans.app
          (NatTrans.app
            ({
                app := fun (X₁ : C₁) ↦
                  {
                    app := fun (X₂ : C₂) ↦
                      { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ },
                    naturality := ⋯ },
                naturality := ⋯ } ≫
              Functor.map (bifunctorComp₁₂FunctorObj F₁₂') f)
            X₁)
          X₂)
        X₃)
⊢ Eq (α := Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G ⟶ Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G')
    (Functor.map (bifunctorComp₁₂FunctorObj F₁₂) f ≫
      {
        app := fun (X₁ : C₁) ↦
          { app := fun (X₂ : C₂) ↦ { app := fun (X₃ : C₃) ↦ (G'.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ },
            naturality := ⋯ },
        naturality := ⋯ })
    ({
        app := fun (X₁ : C₁) ↦
          { app := fun (X₂ : C₂) ↦ { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ },
            naturality := ⋯ },
        naturality := ⋯ } ≫
      Functor.map (bifunctorComp₁₂FunctorObj F₁₂') f)

Tactic:
ext X₁ X₂ X₃
-- Module: Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
f : G ⟶ G'
X₁ : C₁
X₂ : C₂
X₃ : C₃
w :
  NatTrans.app (f.app ((F₁₂.obj X₁).obj X₂)) X₃ ≫ (G'.map ((φ.app X₁).app X₂)).app X₃ =
    (G.map ((φ.app X₁).app X₂)).app X₃ ≫ NatTrans.app (f.app ((F₁₂'.obj X₁).obj X₂)) X₃
⊢ Eq (α :=
    (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂) G).obj X₁).obj X₂).obj X₃ ⟶
      (((Functor.obj (bifunctorComp₁₂FunctorObj F₁₂') G').obj X₁).obj X₂).obj X₃)
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app
          (Functor.map (bifunctorComp₁₂FunctorObj F₁₂) f ≫
            {
              app := fun (X₁ : C₁) ↦
                {
                  app := fun (X₂ : C₂) ↦
                    { app := fun (X₃ : C₃) ↦ (G'.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ },
                  naturality := ⋯ },
              naturality := ⋯ })
          X₁)
        X₂)
      X₃)
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app
          ({
              app := fun (X₁ : C₁) ↦
                { app := fun (X₂ : C₂) ↦ { app := fun (X₃ : C₃) ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ },
                  naturality := ⋯ },
              naturality := ⋯ } ≫
            Functor.map (bifunctorComp₁₂FunctorObj F₁₂') f)
          X₁)
        X₂)
      X₃)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Functor.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₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
φ : F₁₂ ⟶ F₁₂'
G G' : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
f : G ⟶ G'
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ NatTrans.app (f.app ((F₁₂.obj X₁).obj X₂)) X₃ ≫ (G'.map ((φ.app X₁).app X₂)).app X₃ =
    (G.map ((φ.app X₁).app X₂)).app X₃ ≫ NatTrans.app (f.app ((F₁₂'.obj X₁).obj X₂)) X₃

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

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.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_6, v_4, u_6, u_4} C₂₃ C₄
G₂₃ : C₂ ⥤ Functor.{v_3, v_6, u_3, u_6} C₃ C₂₃
X₁ : C₁
X₂ Y₂ : C₂
φ_1 : X₂ ⟶ Y₂
X₃ Y₃ : C₃
φ : X₃ ⟶ Y₃
dsimp :
  (F.obj X₁).map ((G₂₃.obj X₂).map φ) ≫ (F.obj X₁).map ((G₂₃.map φ_1).app Y₃) =
    (F.obj X₁).map ((G₂₃.map φ_1).app X₃) ≫ (F.obj X₁).map ((G₂₃.obj Y₂).map φ)
⊢ Eq.{v_4 + 1} (α :=
    Quiver.Hom.{v_4, u_4} (V := C₄)
      (Functor.obj.{v_3, v_4, u_3, u_4}
        { obj := fun (X₃ : C₃) ↦ (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃),
          map := fun {X Y : C₃} (φ : X ⟶ Y) ↦ (F.obj X₁).map ((G₂₃.obj X₂).map φ), map_id := ⋯, map_comp := ⋯ }
        X₃)
      (Functor.obj.{v_3, v_4, u_3, u_4}
        { obj := fun (X₃ : C₃) ↦ (F.obj X₁).obj ((G₂₃.obj Y₂).obj X₃),
          map := fun {X Y : C₃} (φ : X ⟶ Y) ↦ (F.obj X₁).map ((G₂₃.obj Y₂).map φ), map_id := ⋯, map_comp := ⋯ }
        Y₃))
    (Functor.map
        { obj := fun (X₃ : C₃) ↦ (F.obj X₁).obj ((G₂₃.obj X₂).obj X₃),
          map := fun {X Y : C₃} (φ : X ⟶ Y) ↦ (F.obj X₁).map ((G₂₃.obj X₂).map φ), map_id := ⋯, map_comp := ⋯ }
        φ ≫
      (F.obj X₁).map ((G₂₃.map φ_1).app Y₃))
    ((F.obj X₁).map ((G₂₃.map φ_1).app X₃) ≫
      Functor.map
        { obj := fun (X₃ : C₃) ↦ (F.obj X₁).obj ((G₂₃.obj Y₂).obj X₃),
          map := fun {X Y : C₃} (φ : X ⟶ Y) ↦ (F.obj X₁).map ((G₂₃.obj Y₂).map φ), map_id := ⋯, map_comp := ⋯ }
        φ)

Tactic:
dsimp