[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => (F.obj X.fst).obj X.snd,
          map := fun {X Y} f => NatTrans.app (F.map f.fst) X.snd ≫ (F.obj Y.fst).map f.snd }.map
      (f ≫ g) =
    { obj := fun X => (F.obj X.fst).obj X.snd,
            map := fun {X Y} f => NatTrans.app (F.map f.fst) X.snd ≫ (F.obj Y.fst).map f.snd }.map
        f ≫
      { obj := fun X => (F.obj X.fst).obj X.snd,
            map := fun {X Y} f => NatTrans.app (F.map f.fst) X.snd ≫ (F.obj Y.fst).map f.snd }.map
        g
[PROOFSTEP]
simp only [prod_comp_fst, prod_comp_snd, Functor.map_comp, NatTrans.comp_app, Category.assoc]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ NatTrans.app (F.map f.fst) X✝.snd ≫
      NatTrans.app (F.map g.fst) X✝.snd ≫ (F.obj Z✝.fst).map f.snd ≫ (F.obj Z✝.fst).map g.snd =
    NatTrans.app (F.map f.fst) X✝.snd ≫
      (F.obj Y✝.fst).map f.snd ≫ NatTrans.app (F.map g.fst) Y✝.snd ≫ (F.obj Z✝.fst).map g.snd
[PROOFSTEP]
slice_lhs 2 3 => rw [← NatTrans.naturality]
[GOAL]
case a.a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| NatTrans.app (F.map g.fst) X✝.snd ≫ (F.obj Z✝.fst).map f.snd
case a.a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| (F.obj Z✝.fst).map g.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| NatTrans.app (F.map f.fst) X✝.snd
[PROOFSTEP]
rw [← NatTrans.naturality]
[GOAL]
case a.a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| NatTrans.app (F.map g.fst) X✝.snd ≫ (F.obj Z✝.fst).map f.snd
case a.a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| (F.obj Z✝.fst).map g.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| NatTrans.app (F.map f.fst) X✝.snd
[PROOFSTEP]
rw [← NatTrans.naturality]
[GOAL]
case a.a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| NatTrans.app (F.map g.fst) X✝.snd ≫ (F.obj Z✝.fst).map f.snd
case a.a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| (F.obj Z✝.fst).map g.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
| NatTrans.app (F.map f.fst) X✝.snd
[PROOFSTEP]
rw [← NatTrans.naturality]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C ⥤ D ⥤ E
X✝ Y✝ Z✝ : C × D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ NatTrans.app (F.map f.fst) X✝.snd ≫
      ((F.obj Y✝.fst).map f.snd ≫ NatTrans.app (F.map g.fst) Y✝.snd) ≫ (F.obj Z✝.fst).map g.snd =
    NatTrans.app (F.map f.fst) X✝.snd ≫
      (F.obj Y✝.fst).map f.snd ≫ NatTrans.app (F.map g.fst) Y✝.snd ≫ (F.obj Z✝.fst).map g.snd
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
⊢ ((fun F =>
              Functor.mk
                { obj := fun X => (F.obj X.fst).obj X.snd,
                  map := fun {X Y} f => NatTrans.app (F.map f.fst) X.snd ≫ (F.obj Y.fst).map f.snd })
            X✝).map
        f ≫
      (fun X => NatTrans.app (NatTrans.app T X.fst) X.snd) Y =
    (fun X => NatTrans.app (NatTrans.app T X.fst) X.snd) X ≫
      ((fun F =>
              Functor.mk
                { obj := fun X => (F.obj X.fst).obj X.snd,
                  map := fun {X Y} f => NatTrans.app (F.map f.fst) X.snd ≫ (F.obj Y.fst).map f.snd })
            Y✝).map
        f
[PROOFSTEP]
simp only [prod_comp_fst, prod_comp_snd, Category.comp_id, Category.assoc, Functor.map_id, Functor.map_comp,
  NatTrans.id_app, NatTrans.comp_app]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
⊢ NatTrans.app (X✝.map f.fst) X.snd ≫ (X✝.obj Y.fst).map f.snd ≫ NatTrans.app (NatTrans.app T Y.fst) Y.snd =
    NatTrans.app (NatTrans.app T X.fst) X.snd ≫ NatTrans.app (Y✝.map f.fst) X.snd ≫ (Y✝.obj Y.fst).map f.snd
[PROOFSTEP]
slice_lhs 2 3 => rw [NatTrans.naturality]
[GOAL]
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (X✝.obj Y.fst).map f.snd ≫ NatTrans.app (NatTrans.app T Y.fst) Y.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| NatTrans.app (X✝.map f.fst) X.snd
[PROOFSTEP]
rw [NatTrans.naturality]
[GOAL]
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (X✝.obj Y.fst).map f.snd ≫ NatTrans.app (NatTrans.app T Y.fst) Y.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| NatTrans.app (X✝.map f.fst) X.snd
[PROOFSTEP]
rw [NatTrans.naturality]
[GOAL]
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (X✝.obj Y.fst).map f.snd ≫ NatTrans.app (NatTrans.app T Y.fst) Y.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| NatTrans.app (X✝.map f.fst) X.snd
[PROOFSTEP]
rw [NatTrans.naturality]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
⊢ NatTrans.app (X✝.map f.fst) X.snd ≫ NatTrans.app (NatTrans.app T Y.fst) X.snd ≫ (Y✝.obj Y.fst).map f.snd =
    NatTrans.app (NatTrans.app T X.fst) X.snd ≫ NatTrans.app (Y✝.map f.fst) X.snd ≫ (Y✝.obj Y.fst).map f.snd
[PROOFSTEP]
slice_lhs 1 2 => rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]
[GOAL]
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| NatTrans.app (X✝.map f.fst) X.snd ≫ NatTrans.app (NatTrans.app T Y.fst) X.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (Y✝.obj Y.fst).map f.snd
[PROOFSTEP]
rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]
[GOAL]
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| NatTrans.app (X✝.map f.fst) X.snd ≫ NatTrans.app (NatTrans.app T Y.fst) X.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (Y✝.obj Y.fst).map f.snd
[PROOFSTEP]
rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]
[GOAL]
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| NatTrans.app (X✝.map f.fst) X.snd ≫ NatTrans.app (NatTrans.app T Y.fst) X.snd
case a
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (Y✝.obj Y.fst).map f.snd
[PROOFSTEP]
rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
⊢ (NatTrans.app (NatTrans.app T X.fst) X.snd ≫ NatTrans.app (Y✝.map f.fst) X.snd) ≫ (Y✝.obj Y.fst).map f.snd =
    NatTrans.app (NatTrans.app T X.fst) X.snd ≫ NatTrans.app (Y✝.map f.fst) X.snd ≫ (Y✝.obj Y.fst).map f.snd
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C
Y : D
⊢ { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }.map (𝟙 Y) =
    𝟙 ({ obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }.obj Y)
[PROOFSTEP]
simp only [F.map_id]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C
Y : D
⊢ F.map (𝟙 X, 𝟙 Y) = 𝟙 (F.obj (X, Y))
[PROOFSTEP]
rw [← prod_id]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C
Y : D
⊢ F.map (𝟙 (X, Y)) = 𝟙 (F.obj (X, Y))
[PROOFSTEP]
exact F.map_id ⟨X, Y⟩
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C
X✝ Y✝ Z✝ : D
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }.map (f ≫ g) =
    { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }.map f ≫
      { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }.map g
[PROOFSTEP]
simp [← F.map_comp]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X✝ Y✝ : C
f : X✝ ⟶ Y✝
Y Y' : D
g : Y ⟶ Y'
⊢ ((fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }) X✝).map g ≫
      (fun Y => F.map (f, 𝟙 Y)) Y' =
    (fun Y => F.map (f, 𝟙 Y)) Y ≫
      ((fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) }) Y✝).map g
[PROOFSTEP]
simp [← F.map_comp]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C
⊢ { obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
          map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
            map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.obj
        X)
[PROOFSTEP]
ext Y
[GOAL]
case w.h
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C
Y : D
⊢ NatTrans.app
      ({ obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
            map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
        (𝟙 X))
      Y =
    NatTrans.app
      (𝟙
        ({ obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
              map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.obj
          X))
      Y
[PROOFSTEP]
exact F.map_id _
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
          map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
      (f ≫ g) =
    { obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
            map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
        f ≫
      { obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
            map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
        g
[PROOFSTEP]
ext Y
[GOAL]
case w.h
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
Y : D
⊢ NatTrans.app
      ({ obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
            map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
        (f ≫ g))
      Y =
    NatTrans.app
      ({ obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
              map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
          f ≫
        { obj := fun X => Functor.mk { obj := fun Y => F.obj (X, Y), map := fun {X_1 Y} g => F.map (𝟙 X, g) },
              map := fun {X Y} f => NatTrans.mk fun Y_1 => F.map (f, 𝟙 Y_1) }.map
          g)
      Y
[PROOFSTEP]
dsimp
[GOAL]
case w.h
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
Y : D
⊢ F.map (f ≫ g, 𝟙 Y) = F.map (f, 𝟙 Y) ≫ F.map (g, 𝟙 Y)
[PROOFSTEP]
simp [← F.map_comp]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X : C
Y Y' : D
g : Y ⟶ Y'
⊢ (((fun F => curryObj F) X✝).obj X).map g ≫ (fun Y => NatTrans.app T (X, Y)) Y' =
    (fun Y => NatTrans.app T (X, Y)) Y ≫ (((fun F => curryObj F) Y✝).obj X).map g
[PROOFSTEP]
dsimp [curryObj]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X : C
Y Y' : D
g : Y ⟶ Y'
⊢ X✝.map (𝟙 X, g) ≫ NatTrans.app T (X, Y') = NatTrans.app T (X, Y) ≫ Y✝.map (𝟙 X, g)
[PROOFSTEP]
rw [NatTrans.naturality]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X X' : C
f : X ⟶ X'
⊢ ((fun F => curryObj F) X✝).map f ≫ (fun X => NatTrans.mk fun Y => NatTrans.app T (X, Y)) X' =
    (fun X => NatTrans.mk fun Y => NatTrans.app T (X, Y)) X ≫ ((fun F => curryObj F) Y✝).map f
[PROOFSTEP]
ext
[GOAL]
case w.h
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X X' : C
f : X ⟶ X'
x✝ : D
⊢ NatTrans.app (((fun F => curryObj F) X✝).map f ≫ (fun X => NatTrans.mk fun Y => NatTrans.app T (X, Y)) X') x✝ =
    NatTrans.app ((fun X => NatTrans.mk fun Y => NatTrans.app T (X, Y)) X ≫ ((fun F => curryObj F) Y✝).map f) x✝
[PROOFSTEP]
dsimp [curryObj]
[GOAL]
case w.h
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
X✝ Y✝ : C × D ⥤ E
T : X✝ ⟶ Y✝
X X' : C
f : X ⟶ X'
x✝ : D
⊢ X✝.map (f, 𝟙 x✝) ≫ NatTrans.app T (X', x✝) = NatTrans.app T (X, x✝) ≫ Y✝.map (f, 𝟙 x✝)
[PROOFSTEP]
rw [NatTrans.naturality]
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X : C × D
⊢ ((curry ⋙ uncurry).obj F).obj X = ((𝟭 (C × D ⥤ E)).obj F).obj X
[PROOFSTEP]
simp
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
⊢ ∀ {X Y : C × D} (f : X ⟶ Y),
    ((curry ⋙ uncurry).obj F).map f ≫ ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) Y).hom =
      ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) X).hom ≫ ((𝟭 (C × D ⥤ E)).obj F).map f
[PROOFSTEP]
intros X Y f
[GOAL]
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
X Y : C × D
f : X ⟶ Y
⊢ ((curry ⋙ uncurry).obj F).map f ≫ ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) Y).hom =
    ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) X).hom ≫ ((𝟭 (C × D ⥤ E)).obj F).map f
[PROOFSTEP]
cases X
[GOAL]
case mk
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
Y : C × D
fst✝ : C
snd✝ : D
f : (fst✝, snd✝) ⟶ Y
⊢ ((curry ⋙ uncurry).obj F).map f ≫ ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) Y).hom =
    ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) (fst✝, snd✝)).hom ≫ ((𝟭 (C × D ⥤ E)).obj F).map f
[PROOFSTEP]
cases Y
[GOAL]
case mk.mk
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
fst✝¹ : C
snd✝¹ : D
fst✝ : C
snd✝ : D
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ ((curry ⋙ uncurry).obj F).map f ≫ ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) (fst✝, snd✝)).hom =
    ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) (fst✝¹, snd✝¹)).hom ≫ ((𝟭 (C × D ⥤ E)).obj F).map f
[PROOFSTEP]
cases f
[GOAL]
case mk.mk.mk
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
fst✝² : C
snd✝² : D
fst✝¹ : C
snd✝¹ : D
fst✝ : (fst✝², snd✝²).fst ⟶ (fst✝¹, snd✝¹).fst
snd✝ : (fst✝², snd✝²).snd ⟶ (fst✝¹, snd✝¹).snd
⊢ ((curry ⋙ uncurry).obj F).map (fst✝, snd✝) ≫
      ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) (fst✝¹, snd✝¹)).hom =
    ((fun X => eqToIso (_ : F.obj (X.fst, X.snd) = F.obj X)) (fst✝², snd✝²)).hom ≫
      ((𝟭 (C × D ⥤ E)).obj F).map (fst✝, snd✝)
[PROOFSTEP]
dsimp at *
[GOAL]
case mk.mk.mk
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
fst✝² : C
snd✝² : D
fst✝¹ : C
snd✝¹ : D
fst✝ : (fst✝², snd✝²).fst ⟶ (fst✝¹, snd✝¹).fst
snd✝ : (fst✝², snd✝²).snd ⟶ (fst✝¹, snd✝¹).snd
⊢ (F.map (fst✝, 𝟙 snd✝²) ≫ F.map (𝟙 fst✝¹, snd✝)) ≫ 𝟙 (F.obj (fst✝¹, snd✝¹)) =
    𝟙 (F.obj (fst✝², snd✝²)) ≫ F.map (fst✝, snd✝)
[PROOFSTEP]
rw [← F.map_comp]
[GOAL]
case mk.mk.mk
B : Type u₁
inst✝³ : Category.{v₁, u₁} B
C : Type u₂
inst✝² : Category.{v₂, u₂} C
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
E : Type u₄
inst✝ : Category.{v₄, u₄} E
F : C × D ⥤ E
fst✝² : C
snd✝² : D
fst✝¹ : C
snd✝¹ : D
fst✝ : (fst✝², snd✝²).fst ⟶ (fst✝¹, snd✝¹).fst
snd✝ : (fst✝², snd✝²).snd ⟶ (fst✝¹, snd✝¹).snd
⊢ F.map ((fst✝, 𝟙 snd✝²) ≫ (𝟙 fst✝¹, snd✝)) ≫ 𝟙 (F.obj (fst✝¹, snd✝¹)) = 𝟙 (F.obj (fst✝², snd✝²)) ≫ F.map (fst✝, snd✝)
[PROOFSTEP]
simp
