awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.Category
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
H : Functor.{v₃, v₁, u₃, u₁} E C
α : F ⟶ G
X : E
⊢ (𝟙 H ◫ α).app X = α.app (H.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Category
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F G H : Functor.{v₁, v₂, u₁, u₂} C D
I J K : Functor.{v₂, v₃, u₂, u₃} D E
α : F ⟶ G
β : G ⟶ H
γ : I ⟶ J
δ : J ⟶ K
w w₁ w₂ w₃ : ∀ (x : C), ((α ≫ β) ◫ (γ ≫ δ)).app x = ((α ◫ γ) ≫ β ◫ δ).app x
⊢ (α ≫ β) ◫ (γ ≫ δ) = (α ◫ γ) ≫ β ◫ δ

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Functor.Category
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : C ⥤ Functor.{v₂, v₃, u₂, u₃} D E
d d' : D
f : d ⟶ d'
c : C
⊢ (F.flip.map f).app c = (F.obj c).map f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.Category
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
H : Functor.{v₃, v₄, u₃, u₄} E E'
⊢ (F ⋙ G) ⋙ H = F ⋙ G ⋙ H

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Functor.Category
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
X Y : C
e : X ≅ Y
F : C ⥤ Functor.{v₂, v₃, u₂, u₃} D E
Z : D
⊢ (F.map e.hom).app Z ≫ (F.map e.inv).app Z = 𝟙 ((F.obj X).obj Z)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Functor.Category
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
X Y : C
e : X ≅ Y
F : C ⥤ Functor.{v₂, v₃, u₂, u₃} D E
Z : D
⊢ (F.map e.inv).app Z ≫ (F.map e.hom).app Z = 𝟙 ((F.obj Y).obj Z)

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Functor.Const
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
X : Cᵒᵖ
j : Jᵒᵖ
⊢ NatTrans.app (Iso.hom (opObjUnop X)) j = 𝟙 (obj.{v₁, v₂, u₁, u₂} (obj (const Jᵒᵖ) (unop X)) j)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.Const
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
X : Cᵒᵖ
j : Jᵒᵖ
⊢ NatTrans.app (Iso.inv (opObjUnop X)) j = 𝟙 (obj.{v₁, v₂, u₁, u₂} (Functor.leftOp (obj (const J) X)) j)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.Const
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
X : Cᵒᵖ
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ Eq.{v₂ + 1} (α :=
    obj.{v₁, v₂, u₁, u₂} (unop (obj (Functor.op (const J)) X)) j₁ ⟶
      obj.{v₁, v₂, u₁, u₂} (unop (obj (Functor.op (const J)) X)) j₂)
    (map (unop (obj (Functor.op (const J)) X)) f) (𝟙 (unop X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.Const
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
F : Functor.{v₂, v₃, u₂, u₃} C D
X : C
⊢ ∀ {X_1 Y : J} (f : X_1 ⟶ Y),
    Eq (α :=
      obj.{v₁, v₃, u₁, u₃} (obj (F ⋙ const J) X) X_1 ⟶
        obj.{v₁, v₃, u₁, u₃} (obj (const J ⋙ obj (whiskeringRight J C D) F) X) Y)
      (map (obj (F ⋙ const J) X) f ≫
        Iso.hom
          ((fun (x : J) ↦
              (Iso.refl (obj.{v₁, v₃, u₁, u₃} (obj (F ⋙ const J) X) x) :
                obj.{v₁, v₃, u₁, u₃} (obj (F ⋙ const J) X) x ≅ obj.{v₁, v₃, u₁, u₃} (obj (F ⋙ const J) X) x))
            Y))
      (Iso.hom
          ((fun (x : J) ↦
              (Iso.refl (obj.{v₁, v₃, u₁, u₃} (obj (F ⋙ const J) X) x) :
                obj.{v₁, v₃, u₁, u₃} (obj (F ⋙ const J) X) x ≅ obj.{v₁, v₃, u₁, u₃} (obj (F ⋙ const J) X) x))
            X_1) ≫
        map (obj (const J ⋙ obj (whiskeringRight J C D) F) X) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
X Y Z : C × D
f : X ⟶ Y
g : Y ⟶ Z
simp :
  (F.map f.1).app X.2 ≫ (F.map g.1).app X.2 ≫ (F.obj Z.1).map f.2 ≫ (F.obj Z.1).map g.2 =
    (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2
⊢ (F.map (f ≫ g).1).app X.2 ≫ (F.obj Z.1).map (f ≫ g).2 =
    ((F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2) ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2

Tactic:
simp only [prod_comp_fst, prod_comp_snd, Functor.map_comp, NatTrans.comp_app,
          Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.prod_comp_fst, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.prod_comp_snd
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
X Y Z : C × D
f : X ⟶ Y
g : Y ⟶ Z
a : (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2
| (F.map g.1).app X.2 ≫ (F.obj Z.1).map f.2

Tactic:
rw [← NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
X Y Z : C × D
f : X ⟶ Y
g : Y ⟶ Z
slice_lhs :
  (F.map f.1).app X.2 ≫ ((F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2) ≫ (F.obj Z.1).map g.2 =
    (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2
⊢ (F.map f.1).app X.2 ≫ (F.map g.1).app X.2 ≫ (F.obj Z.1).map f.2 ≫ (F.obj Z.1).map g.2 =
    (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2

Tactic:
slice_lhs 2 3 => rw [← NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
X Y Z : C × D
f : X ⟶ Y
g : Y ⟶ Z
rw rw₁ :
  (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2 =
    (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2
⊢ (F.map f.1).app X.2 ≫ ((F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2) ≫ (F.obj Z.1).map g.2 =
    (F.map f.1).app X.2 ≫ (F.obj Y.1).map f.2 ≫ (F.map g.1).app Y.2 ≫ (F.obj Z.1).map g.2

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
T : X_1 ⟶ Y_1
X Y : C × D
f : X ⟶ Y
simp :
  (X_1.map f.1).app X.2 ≫ (X_1.obj Y.1).map f.2 ≫ NatTrans.app (T.app Y.1) Y.2 =
    NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2
⊢ Eq.{v₄ + 1} (α :=
    Quiver.Hom.{v₄, u₄} (V := E)
      (obj
        { obj := fun (X : C × D) ↦ (X_1.obj X.1).obj X.2,
          map := fun {X Y : C × D} (f : X ⟶ Y) ↦ (X_1.map f.1).app X.2 ≫ (X_1.obj Y.1).map f.2, map_id := ⋯,
          map_comp := ⋯ }
        X)
      (obj
        { obj := fun (X : C × D) ↦ (Y_1.obj X.1).obj X.2,
          map := fun {X Y : C × D} (f : X ⟶ Y) ↦ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2, map_id := ⋯,
          map_comp := ⋯ }
        Y))
    (map
        { obj := fun (X : C × D) ↦ (X_1.obj X.1).obj X.2,
          map := fun {X Y : C × D} (f : X ⟶ Y) ↦ (X_1.map f.1).app X.2 ≫ (X_1.obj Y.1).map f.2, map_id := ⋯,
          map_comp := ⋯ : C × D ⥤ E }
        f ≫
      NatTrans.app (T.app Y.1) Y.2)
    (NatTrans.app (T.app X.1) X.2 ≫
      map
        { obj := fun (X : C × D) ↦ (Y_1.obj X.1).obj X.2,
          map := fun {X Y : C × D} (f : X ⟶ Y) ↦ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2, map_id := ⋯,
          map_comp := ⋯ }
        f)

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
T : X_1 ⟶ Y_1
X Y : C × D
f : X ⟶ Y
a : NatTrans.app (T.app Y.1) X.2 ≫ (Y_1.obj Y.1).map f.2
| (X_1.obj Y.1).map f.2 ≫ NatTrans.app (T.app Y.1) Y.2

Tactic:
rw [NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
T : X_1 ⟶ Y_1
X Y : C × D
f : X ⟶ Y
slice_lhs :
  (X_1.map f.1).app X.2 ≫ NatTrans.app (T.app Y.1) X.2 ≫ (Y_1.obj Y.1).map f.2 =
    NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2
⊢ (X_1.map f.1).app X.2 ≫ (X_1.obj Y.1).map f.2 ≫ NatTrans.app (T.app Y.1) Y.2 =
    NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2

Tactic:
slice_lhs 2 3 => rw [NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
T : X_1 ⟶ Y_1
X Y : C × D
f : X ⟶ Y
a : NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2
| (X_1.map f.1).app X.2 ≫ NatTrans.app (T.app Y.1) X.2

Tactic:
rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
T : X_1 ⟶ Y_1
X Y : C × D
f : X ⟶ Y
slice_lhs :
  (NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2) ≫ (Y_1.obj Y.1).map f.2 =
    NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2
⊢ (X_1.map f.1).app X.2 ≫ NatTrans.app (T.app Y.1) X.2 ≫ (Y_1.obj Y.1).map f.2 =
    NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2

Tactic:
slice_lhs 1 2 => rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C ⥤ Functor.{v₃, v₄, u₃, u₄} D E
T : X_1 ⟶ Y_1
X Y : C × D
f : X ⟶ Y
rw rw₁ :
  NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2 =
    NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2
⊢ (NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2) ≫ (Y_1.obj Y.1).map f.2 =
    NatTrans.app (T.app X.1) X.2 ≫ (Y_1.map f.1).app X.2 ≫ (Y_1.obj Y.1).map f.2

Tactic:
rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X : C
Y : D
rw : F.map (𝟙 (X, Y)) = 𝟙 (F.obj (X, Y))
⊢ F.map (𝟙 X ×ₘ 𝟙 Y) = 𝟙 (F.obj (X, Y))

Tactic:
rw [← prod_id]

Premises used: CategoryTheory.prod_id
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X : C
Y : D
⊢ F.map (𝟙 (X, Y)) = 𝟙 (F.obj (X, Y))

Tactic:
F.map_id ⟨X,Y⟩

Premises used: Prod.mk, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X : C
Y : D
⊢ F.map (𝟙 (X, Y)) = 𝟙 (F.obj (X, Y))

Tactic:
exact F.map_id ⟨X,Y⟩

Premises used: Prod.mk, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X : C
X_1 Y Z : D
f : X_1 ⟶ Y
g : Y ⟶ Z
⊢ F.map (𝟙 X ×ₘ f ≫ g) = F.map (𝟙 X ×ₘ f) ≫ F.map (𝟙 X ×ₘ g)

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X Y_1 : C
f : X ⟶ Y_1
Y Y' : D
g : Y ⟶ Y'
⊢ Eq.{v₄ + 1} (α :=
    Quiver.Hom.{v₄, u₄} (V := E)
      (obj.{v₃, v₄, u₃, u₄}
        { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
          map_comp := ⋯ }
        Y)
      (obj.{v₃, v₄, u₃, u₄}
        { obj := fun (Y : D) ↦ F.obj (Y_1, Y), map := fun {X Y : D} (g : X ⟶ Y) ↦ F.map (𝟙 Y_1 ×ₘ g), map_id := ⋯,
          map_comp := ⋯ }
        Y'))
    (map
        { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
          map_comp := ⋯ }
        g ≫
      F.map (f ×ₘ 𝟙 Y'))
    (F.map (f ×ₘ 𝟙 Y) ≫
      map
        { obj := fun (Y : D) ↦ F.obj (Y_1, Y), map := fun {X Y : D} (g : X ⟶ Y) ↦ F.map (𝟙 Y_1 ×ₘ g), map_id := ⋯,
          map_comp := ⋯ }
        g)

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X : C
w :
  ∀ (Y : D),
    Eq.{v₄ + 1} (α :=
      Quiver.Hom.{v₄, u₄} (V := E)
        (obj.{v₃, v₄, u₃, u₄}
          { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
            map_comp := ⋯ }
          Y)
        (obj.{v₃, v₄, u₃, u₄}
          { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
            map_comp := ⋯ }
          Y))
      (NatTrans.app { app := fun (Y : D) ↦ F.map (𝟙 X ×ₘ 𝟙 Y), naturality := ⋯ } Y)
      (NatTrans.app
        (𝟙
          { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
            map_comp := ⋯ })
        Y)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₃, v₄, u₃, u₄} D E)
      { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
        map_comp := ⋯ }
      { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
        map_comp := ⋯ })
    { app := fun (Y : D) ↦ F.map (𝟙 X ×ₘ 𝟙 Y), naturality := ⋯ }
    (𝟙
      { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
        map_comp := ⋯ })

Tactic:
ext Y
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X : C
Y : D
⊢ Eq.{v₄ + 1} (α :=
    Quiver.Hom.{v₄, u₄} (V := E)
      (obj.{v₃, v₄, u₃, u₄}
        { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
          map_comp := ⋯ }
        Y)
      (obj.{v₃, v₄, u₃, u₄}
        { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
          map_comp := ⋯ }
        Y))
    (NatTrans.app { app := fun (Y : D) ↦ F.map (𝟙 X ×ₘ 𝟙 Y), naturality := ⋯ } Y)
    (NatTrans.app
      (𝟙
        { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
          map_comp := ⋯ })
      Y)

Tactic:
F.map_id _

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X : C
Y : D
⊢ Eq.{v₄ + 1} (α :=
    Quiver.Hom.{v₄, u₄} (V := E)
      (obj.{v₃, v₄, u₃, u₄}
        { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
          map_comp := ⋯ }
        Y)
      (obj.{v₃, v₄, u₃, u₄}
        { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
          map_comp := ⋯ }
        Y))
    (NatTrans.app { app := fun (Y : D) ↦ F.map (𝟙 X ×ₘ 𝟙 Y), naturality := ⋯ } Y)
    (NatTrans.app
      (𝟙
        { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
          map_comp := ⋯ })
      Y)

Tactic:
exact F.map_id _

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w :
  ∀ (Y_1 : D),
    Eq.{v₄ + 1} (α :=
      Quiver.Hom.{v₄, u₄} (V := E)
        (obj.{v₃, v₄, u₃, u₄}
          { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
            map_comp := ⋯ }
          Y_1)
        (obj.{v₃, v₄, u₃, u₄}
          { obj := fun (Y : D) ↦ F.obj (Z, Y), map := fun {X Y : D} (g : X ⟶ Y) ↦ F.map (𝟙 Z ×ₘ g), map_id := ⋯,
            map_comp := ⋯ }
          Y_1))
      (NatTrans.app { app := fun (Y_2 : D) ↦ F.map (f ≫ g ×ₘ 𝟙 Y_2), naturality := ⋯ } Y_1)
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          { obj := fun (Y_2 : D) ↦ F.obj (Y, Y_2), map := fun {X Y_2 : D} (g : X ⟶ Y_2) ↦ F.map (𝟙 Y ×ₘ g), map_id := ⋯,
            map_comp := ⋯ })
          { app := fun (Y_2 : D) ↦ F.map (f ×ₘ 𝟙 Y_2), naturality := ⋯ }
          { app := fun (Y_2 : D) ↦ F.map (g ×ₘ 𝟙 Y_2), naturality := ⋯ })
        Y_1)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₃, v₄, u₃, u₄} D E)
      { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
        map_comp := ⋯ }
      { obj := fun (Y : D) ↦ F.obj (Z, Y), map := fun {X Y : D} (g : X ⟶ Y) ↦ F.map (𝟙 Z ×ₘ g), map_id := ⋯,
        map_comp := ⋯ })
    { app := fun (Y_1 : D) ↦ F.map (f ≫ g ×ₘ 𝟙 Y_1), naturality := ⋯ }
    (CategoryStruct.comp (Y :=
      { obj := fun (Y_1 : D) ↦ F.obj (Y, Y_1), map := fun {X Y_1 : D} (g : X ⟶ Y_1) ↦ F.map (𝟙 Y ×ₘ g), map_id := ⋯,
        map_comp := ⋯ })
      { app := fun (Y_1 : D) ↦ F.map (f ×ₘ 𝟙 Y_1), naturality := ⋯ }
      { app := fun (Y_1 : D) ↦ F.map (g ×ₘ 𝟙 Y_1), naturality := ⋯ })

Tactic:
ext Y
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
F : C × D ⥤ E
X Y_1 Z : C
f : X ⟶ Y_1
g : Y_1 ⟶ Z
Y : D
⊢ Eq.{v₄ + 1} (α :=
    Quiver.Hom.{v₄, u₄} (V := E)
      (obj.{v₃, v₄, u₃, u₄}
        { obj := fun (Y : D) ↦ F.obj (X, Y), map := fun {X_1 Y : D} (g : X_1 ⟶ Y) ↦ F.map (𝟙 X ×ₘ g), map_id := ⋯,
          map_comp := ⋯ }
        Y)
      (obj.{v₃, v₄, u₃, u₄}
        { obj := fun (Y : D) ↦ F.obj (Z, Y), map := fun {X Y : D} (g : X ⟶ Y) ↦ F.map (𝟙 Z ×ₘ g), map_id := ⋯,
          map_comp := ⋯ }
        Y))
    (NatTrans.app { app := fun (Y : D) ↦ F.map (f ≫ g ×ₘ 𝟙 Y), naturality := ⋯ } Y)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        { obj := fun (Y : D) ↦ F.obj (Y_1, Y), map := fun {X Y : D} (g : X ⟶ Y) ↦ F.map (𝟙 Y_1 ×ₘ g), map_id := ⋯,
          map_comp := ⋯ })
        { app := fun (Y : D) ↦ F.map (f ×ₘ 𝟙 Y), naturality := ⋯ }
        { app := fun (Y : D) ↦ F.map (g ×ₘ 𝟙 Y), naturality := ⋯ })
      Y)

Tactic:
simp [← F.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C × D ⥤ E
T : X_1 ⟶ Y_1
X : C
Y Y' : D
g : Y ⟶ Y'
dsimp : X_1.map (𝟙 X ×ₘ g) ≫ T.app (X, Y') = T.app (X, Y) ≫ Y_1.map (𝟙 X ×ₘ g)
⊢ (X_1.curryObj.obj X).map g ≫ T.app (X, Y') = T.app (X, Y) ≫ (Y_1.curryObj.obj X).map g

Tactic:
dsimp [curryObj]

Premises used: CategoryTheory.Functor.curryObj
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y_1 : C × D ⥤ E
T : X_1 ⟶ Y_1
X : C
Y Y' : D
g : Y ⟶ Y'
rw rw₁ : T.app (X, Y) ≫ Y_1.map (𝟙 X ×ₘ g) = T.app (X, Y) ≫ Y_1.map (𝟙 X ×ₘ g)
⊢ X_1.map (𝟙 X ×ₘ g) ≫ T.app (X, Y') = T.app (X, Y) ≫ Y_1.map (𝟙 X ×ₘ g)

Tactic:
rw [NatTrans.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Functor.Currying
Goal:
B : Type u₁
inst : Category.{v₁, u₁} B
C : Type u₂
inst_1 : Category.{v₂, u₂} C
D : Type u₃
inst_2 : Category.{v₃, u₃} D
E : Type u₄
inst_3 : Category.{v₄, u₄} E
H : Type u₅
inst_4 : Category.{v₅, u₅} H
X_1 Y : C × D ⥤ E
T : X_1 ⟶ Y
X X' : C
f : X ⟶ X'
w :
  ∀ (x : D),
    NatTrans.app (X_1.curryObj.map f ≫ { app := fun (Y_1 : D) ↦ T.app (X', Y_1), naturality := ⋯ }) x =
      NatTrans.app
        ({ app := fun (Y_1 : D) ↦ T.app (X, Y_1), naturality := ⋯ : NatTrans (X_1.curryObj.obj X) (Y.curryObj.obj X) } ≫
          Y.curryObj.map f)
        x
⊢ X_1.curryObj.map f ≫ { app := fun (Y_1 : D) ↦ T.app (X', Y_1), naturality := ⋯ } =
    { app := fun (Y_1 : D) ↦ T.app (X, Y_1), naturality := ⋯ : NatTrans (X_1.curryObj.obj X) (Y.curryObj.obj X) } ≫
      Y.curryObj.map f

Tactic:
ext