awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
x : D
w : X_1.map (f ×ₘ 𝟙 x) ≫ T.app (X', x) = T.app (X, x) ≫ Y.map (f ×ₘ 𝟙 x)
⊢ 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

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 : C × D ⥤ E
T : X_1 ⟶ Y
X X' : C
f : X ⟶ X'
x : D
w w₁ : T.app (X, x) ≫ Y.map (f ×ₘ 𝟙 x) = T.app (X, x) ≫ Y.map (f ×ₘ 𝟙 x)
⊢ X_1.map (f ×ₘ 𝟙 x) ≫ T.app (X', x) = T.app (X, x) ≫ Y.map (f ×ₘ 𝟙 x)

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 × D ⥤ E
X₁ : C
X₂ : D
Y₁ : C
Y₂ : D
f₁ : (X₁, X₂).1 ⟶ (Y₁, Y₂).1
f₂ : (X₁, X₂).2 ⟶ (Y₁, Y₂).2
dsimp : (F.map (f₁ ×ₘ 𝟙 X₂) ≫ F.map (𝟙 Y₁ ×ₘ f₂)) ≫ 𝟙 (F.obj (Y₁, Y₂)) = 𝟙 (F.obj (X₁, X₂)) ≫ F.map (f₁, f₂)
⊢ (obj (curry ⋙ uncurry) F).map (f₁, f₂) ≫
      Iso.hom
        ((fun (x : C × D) ↦
            (Iso.refl ((obj (curry ⋙ uncurry) F).obj x) :
              (obj (curry ⋙ uncurry) F).obj x ≅ (obj (curry ⋙ uncurry) F).obj x))
          (Y₁, Y₂)) =
    Iso.hom
        ((fun (x : C × D) ↦
            (Iso.refl ((obj (curry ⋙ uncurry) F).obj x) :
              (obj (curry ⋙ uncurry) F).obj x ≅ (obj (curry ⋙ uncurry) F).obj x))
          (X₁, X₂)) ≫
      (obj (𝟭 (C × D ⥤ E)) F).map (f₁, f₂)

Tactic:
dsimp at f₁ f₂ ⊢
-- 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₂ : D
Y₁ : C
Y₂ : D
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
⊢ (F.map (f₁ ×ₘ 𝟙 X₂) ≫ F.map (𝟙 Y₁ ×ₘ f₂)) ≫ 𝟙 (F.obj (Y₁, Y₂)) = 𝟙 (F.obj (X₁, X₂)) ≫ F.map (f₁, f₂)

Tactic:
simp only [← F.map_comp, prod_comp, Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.prod_comp, CategoryTheory.Category.id_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
⊢ Full (C := C × D ⥤ E) curry

Tactic:
fullyFaithfulCurry.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.Functor.fullyFaithfulCurry
-- 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
⊢ Faithful (C := C × D ⥤ E) curry

Tactic:
fullyFaithfulCurry.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.Functor.fullyFaithfulCurry
-- 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
⊢ Full (C := C ⥤ Functor.{v₃, v₄, u₃, u₄} D E) uncurry

Tactic:
fullyFaithfulUncurry.full

Premises used: CategoryTheory.Functor.fullyFaithfulUncurry, CategoryTheory.Functor.FullyFaithful.full
-- 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
⊢ Faithful (C := C ⥤ Functor.{v₃, v₄, u₃, u₄} D E) uncurry

Tactic:
fullyFaithfulUncurry.faithful

Premises used: CategoryTheory.Functor.fullyFaithfulUncurry, CategoryTheory.Functor.FullyFaithful.faithful
-- 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
F : B × C ⥤ D
⊢ ∀ (X : B × C), (obj uncurry (obj curry F)).obj X = F.obj X

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
F : B × C ⥤ D
x x_1 : B × C
x₁ : B
x₂ : C
y₁ : B
y₂ : C
x_2 : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
dsimp : F.map (f₁ ×ₘ 𝟙 x₂) ≫ F.map (𝟙 y₁ ×ₘ f₂) = 𝟙 (F.obj (x₁, x₂)) ≫ F.map (f₁, f₂) ≫ 𝟙 (F.obj (y₁, y₂))
⊢ (obj uncurry (obj curry F)).map (f₁, f₂) = eqToHom ⋯ ≫ F.map (f₁, f₂) ≫ eqToHom ⋯

Tactic:
dsimp
-- 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
F : B × C ⥤ D
x x_1 : B × C
x₁ : B
x₂ : C
y₁ : B
y₂ : C
x_2 : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ F.map (f₁ ×ₘ 𝟙 x₂) ≫ F.map (𝟙 y₁ ×ₘ f₂) = 𝟙 (F.obj (x₁, x₂)) ≫ F.map (f₁, f₂) ≫ 𝟙 (F.obj (y₁, y₂))

Tactic:
simp only [← F.map_comp, Category.id_comp, Category.comp_id, prod_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.prod_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Functor.Currying
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₁ F₂ : C × D ⥤ E
h : obj curry F₁ = obj curry F₂
rw : obj uncurry (obj curry F₁) = F₂
rw₁ : obj uncurry (obj curry F₁) = obj uncurry (obj curry F₂)
rw₂ rw₃ : obj uncurry (obj curry F₂) = obj uncurry (obj curry F₂)
⊢ F₁ = F₂

Tactic:
rw [← uncurry_obj_curry_obj F₁, ← uncurry_obj_curry_obj F₂, h]

Premises used: CategoryTheory.Functor.uncurry_obj_curry_obj
-- 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
F : B ⥤ Functor.{v₂, v₃, u₂, u₃} C D
x : B
⊢ ∀ (X : C), ((obj curry (obj uncurry F)).obj x).obj X = (F.obj x).obj X

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
F : B ⥤ Functor.{v₂, v₃, u₂, u₃} C D
x : B
⊢ ∀ (X Y : C) (f : X ⟶ Y), ((obj curry (obj uncurry F)).obj x).map f = eqToHom ⋯ ≫ (F.obj x).map f ≫ eqToHom ⋯

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
F₁ F₂ : B ⥤ Functor.{v₂, v₃, u₂, u₃} C D
h : obj uncurry F₁ = obj uncurry F₂
rw : obj curry (obj uncurry F₁) = F₂
rw₁ : obj curry (obj uncurry F₁) = obj curry (obj uncurry F₂)
rw₂ rw₃ : obj curry (obj uncurry F₂) = obj curry (obj uncurry F₂)
⊢ F₁ = F₂

Tactic:
rw [← curry_obj_uncurry_obj F₁, ← curry_obj_uncurry_obj F₂, h]

Premises used: CategoryTheory.Functor.curry_obj_uncurry_obj
-- 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
F : B ⥤ Functor.{v₂, v₃, u₂, u₃} C D
⊢ F.flip.flip = F

Tactic:
rfl

Premises used: CategoryTheory.Functor.flip, rfl
-- 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
F₁ F₂ : B ⥤ Functor.{v₂, v₃, u₂, u₃} C D
h : F₁.flip = F₂.flip
rw : F₁.flip.flip = F₂
rw₁ : F₁.flip.flip = F₂.flip.flip
rw₂ rw₃ : F₂.flip.flip = F₂.flip.flip
⊢ F₁ = F₂

Tactic:
rw [← flip_flip F₁, ← flip_flip F₂, h]

Premises used: CategoryTheory.Functor.flip_flip
-- 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₁ : Functor.{v₁, v₂, u₁, u₂} B C
F₂ : Functor.{v₃, v₄, u₃, u₄} D E
G : C × E ⥤ H
⊢ ∀ (X : B × D), (obj uncurry (F₂ ⋙ (F₁ ⋙ obj curry G).flip).flip).obj X = (F₁.prod F₂ ⋙ G).obj X

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₁ : Functor.{v₁, v₂, u₁, u₂} B C
F₂ : Functor.{v₃, v₄, u₃, u₄} D E
G : C × E ⥤ H
x x_1 : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x_2 : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
dsimp :
  G.map (F₁.map f₁ ×ₘ 𝟙 (F₂.obj x₂)) ≫ G.map (𝟙 (F₁.obj y₁) ×ₘ F₂.map f₂) =
    𝟙 (G.obj (F₁.obj x₁, F₂.obj x₂)) ≫ G.map (F₁.map f₁ ×ₘ F₂.map f₂) ≫ 𝟙 (G.obj (F₁.obj y₁, F₂.obj y₂))
⊢ (obj uncurry (F₂ ⋙ (F₁ ⋙ obj curry G).flip).flip).map (f₁, f₂) = eqToHom ⋯ ≫ (F₁.prod F₂ ⋙ G).map (f₁, f₂) ≫ eqToHom ⋯

Tactic:
dsimp
-- 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₁ : Functor.{v₁, v₂, u₁, u₂} B C
F₂ : Functor.{v₃, v₄, u₃, u₄} D E
G : C × E ⥤ H
x x_1 : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x_2 : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
⊢ G.map (F₁.map f₁ ×ₘ 𝟙 (F₂.obj x₂)) ≫ G.map (𝟙 (F₁.obj y₁) ×ₘ F₂.map f₂) =
    𝟙 (G.obj (F₁.obj x₁, F₂.obj x₂)) ≫ G.map (F₁.map f₁ ×ₘ F₂.map f₂) ≫ 𝟙 (G.obj (F₁.obj y₁, F₂.obj y₂))

Tactic:
simp only [Category.id_comp, Category.comp_id, ← G.map_comp, prod_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp, CategoryTheory.prod_comp, CategoryTheory.Category.id_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₁ : Functor.{v₁, v₂, u₁, u₂} B C
F₂ : Functor.{v₃, v₄, u₃, u₄} D E
G : C × E ⥤ H
⊢ ∀ (X : B × D), (obj uncurry (F₁ ⋙ (F₂ ⋙ (obj curry G).flip).flip)).obj X = (F₁.prod F₂ ⋙ G).obj X

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₁ : Functor.{v₁, v₂, u₁, u₂} B C
F₂ : Functor.{v₃, v₄, u₃, u₄} D E
G : C × E ⥤ H
x x_1 : B × D
x₁ : B
x₂ : D
y₁ : B
y₂ : D
x_2 : (x₁, x₂) ⟶ (y₁, y₂)
f₁ : (x₁, x₂).1 ⟶ (y₁, y₂).1
f₂ : (x₁, x₂).2 ⟶ (y₁, y₂).2
dsimp :
  G.map (F₁.map f₁ ×ₘ 𝟙 (F₂.obj x₂)) ≫ G.map (𝟙 (F₁.obj y₁) ×ₘ F₂.map f₂) =
    𝟙 (G.obj (F₁.obj x₁, F₂.obj x₂)) ≫ G.map (F₁.map f₁ ×ₘ F₂.map f₂) ≫ 𝟙 (G.obj (F₁.obj y₁, F₂.obj y₂))
⊢ (obj uncurry (F₁ ⋙ (F₂ ⋙ (obj curry G).flip).flip)).map (f₁, f₂) =
    eqToHom ⋯ ≫ (F₁.prod F₂ ⋙ G).map (f₁, f₂) ≫ eqToHom ⋯

Tactic:
dsimp
-- 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
F : Functor.{v₁, v₃, u₁, u₃} B D
G : D ⥤ Functor.{v₂, v₄, u₂, u₄} C E
⊢ obj uncurry (F ⋙ G).flip = prod (𝟭 C) F ⋙ obj uncurry G.flip

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- 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
F : C × B ⥤ D
G : Functor.{v₃, v₄, u₃, u₄} D E
⊢ (obj curry (F ⋙ G)).flip = (obj curry F).flip ⋙ obj (whiskeringRight C D E) G

Tactic:
rfl

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerRight, rfl
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_4, u_3} C₁₂
inst_4 : Category.{v_5, u_5} C₂₃
inst_5 : Category.{v_6, u_6} D₁
inst_6 : Category.{v_7, u_7} D₂
inst_7 : Category.{v_8, u_8} D₃
inst_8 : Category.{v_9, u_9} E
⊢ Full (C := C₁ ⥤ C₂ ⥤ Functor.{v_3, v_9, u_4, u_9} C₃ E) uncurry₃

Tactic:
fullyFaithfulUncurry₃.full

Premises used: CategoryTheory.Functor.fullyFaithfulUncurry₃, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_4, u_3} C₁₂
inst_4 : Category.{v_5, u_5} C₂₃
inst_5 : Category.{v_6, u_6} D₁
inst_6 : Category.{v_7, u_7} D₂
inst_7 : Category.{v_8, u_8} D₃
inst_8 : Category.{v_9, u_9} E
⊢ Faithful (C := C₁ ⥤ C₂ ⥤ Functor.{v_3, v_9, u_4, u_9} C₃ E) uncurry₃

Tactic:
fullyFaithfulUncurry₃.faithful

Premises used: CategoryTheory.Functor.fullyFaithfulUncurry₃, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_4, u_3} C₁₂
inst_4 : Category.{v_5, u_5} C₂₃
inst_5 : Category.{v_6, u_6} D₁
inst_6 : Category.{v_7, u_7} D₂
inst_7 : Category.{v_8, u_8} D₃
inst_8 : Category.{v_9, u_9} E
⊢ Full (C := C₁ × C₂ × C₃ ⥤ E) curry₃

Tactic:
fullyFaithfulCurry₃.full

Premises used: CategoryTheory.Functor.fullyFaithfulCurry₃, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_4, u_3} C₁₂
inst_4 : Category.{v_5, u_5} C₂₃
inst_5 : Category.{v_6, u_6} D₁
inst_6 : Category.{v_7, u_7} D₂
inst_7 : Category.{v_8, u_8} D₃
inst_8 : Category.{v_9, u_9} E
⊢ Faithful (C := C₁ × C₂ × C₃ ⥤ E) curry₃

Tactic:
fullyFaithfulCurry₃.faithful

Premises used: CategoryTheory.Functor.fullyFaithfulCurry₃, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_4
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_9, u_9} E
F : C₁ × C₂ × C₃ ⥤ E
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ (((obj curry₃ F).map f).app X₂).app X₃ = F.map (f, 𝟙 X₂, 𝟙 X₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_4
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_9, u_9} E
F : C₁ × C₂ × C₃ ⥤ E
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (((obj curry₃ F).obj X₁).map f).app X₃ = F.map (𝟙 X₁, f, 𝟙 X₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_4
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_9, u_9} E
F : C₁ × C₂ × C₃ ⥤ E
X₁ : C₁
X₂ : C₂
X₃ Y₃ : C₃
f : X₃ ⟶ Y₃
⊢ (((obj curry₃ F).obj X₁).obj X₂).map f = F.map (𝟙 X₁, 𝟙 X₂, f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_4
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_9, u_9} E
F G : C₁ × C₂ × C₃ ⥤ E
f : F ⟶ G
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ Eq (α := (((obj curry₃ F).obj X₁).obj X₂).obj X₃ ⟶ (((obj curry₃ G).obj X₁).obj X₂).obj X₃)
    (NatTrans.app (NatTrans.app (NatTrans.app (map curry₃ f) X₁) X₂) X₃) (f.app (X₁, X₂, X₃))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_4
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_9, u_9} E
F : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_9, u_4, u_9} C₃ E
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ NatTrans.app (NatTrans.app (NatTrans.app (NatTrans.app (Iso.inv (Equivalence.unitIso currying₃)) F) X₁) X₂) X₃ =
    𝟙 ((((obj (Equivalence.functor currying₃ ⋙ Equivalence.inverse currying₃) F).obj X₁).obj X₂).obj X₃)

Tactic:
simp [currying₃, Equivalence.unitInv]

Premises used: CategoryTheory.Functor.currying₃, CategoryTheory.Equivalence.unitInv
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_4, u_3} C₁₂
inst_4 : Category.{v_5, u_5} C₂₃
inst_5 : Category.{v_6, u_6} D₁
inst_6 : Category.{v_7, u_7} D₂
inst_7 : Category.{v_8, u_8} D₃
inst_8 : Category.{v_9, u_9} E
X_1 Y_1 : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_9, u_4, u_9} C₃ E
f : X_1 ⟶ Y_1
X : C₃
Y : C₂
x x_1 : C₁
g : x ⟶ x_1
⊢ ((X_1.flip₁₃.obj X).obj Y).map g ≫ ((f.app x_1).app Y).app X =
    ((f.app x).app Y).app X ≫ ((Y_1.flip₁₃.obj X).obj Y).map g

Tactic:
simp [← NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_4, u_3} C₁₂
inst_4 : Category.{v_5, u_5} C₂₃
inst_5 : Category.{v_6, u_6} D₁
inst_6 : Category.{v_7, u_7} D₂
inst_7 : Category.{v_8, u_8} D₃
inst_8 : Category.{v_9, u_9} E
X_1 Y_1 : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_9, u_4, u_9} C₃ E
f : X_1 ⟶ Y_1
X : C₁
Y : C₃
x x_1 : C₂
g : x ⟶ x_1
⊢ ((X_1.flip₂₃.obj X).obj Y).map g ≫ ((f.app X).app x_1).app Y =
    ((f.app X).app x).app Y ≫ ((Y_1.flip₂₃.obj X).obj Y).map g

Tactic:
simp [← NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_4, u_3} C₁₂
inst_4 : Category.{v_5, u_5} C₂₃
inst_5 : Category.{v_6, u_6} D₁
inst_6 : Category.{v_7, u_7} D₂
inst_7 : Category.{v_8, u_8} D₃
inst_8 : Category.{v_9, u_9} E
X Y : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_9, u_4, u_9} C₃ E
f : X ⟶ Y
x x_1 : C₁
g : x ⟶ x_1
w :
  ∀ (x_2 : C₃) (x_3 : C₂),
    ((X.flip₂₃.map g ≫
                {
                  app := fun (Y_1 : C₃) ↦
                    { app := fun (Z : C₂) ↦ ((f.app x_1).app Z).app Y_1, naturality := ⋯ :
                      NatTrans ((X.flip₂₃.obj x_1).obj Y_1) ((Y.flip₂₃.obj x_1).obj Y_1) },
                  naturality := ⋯ : NatTrans (X.flip₂₃.obj x_1) (Y.flip₂₃.obj x_1) }).app
            x_2).app
        x_3 =
      NatTrans.app
        (NatTrans.app
          ({
              app := fun (Y_1 : C₃) ↦
                { app := fun (Z : C₂) ↦ ((f.app x).app Z).app Y_1, naturality := ⋯ :
                  NatTrans ((X.flip₂₃.obj x).obj Y_1) ((Y.flip₂₃.obj x).obj Y_1) },
              naturality := ⋯ : NatTrans (X.flip₂₃.obj x) (Y.flip₂₃.obj x) } ≫
            Y.flip₂₃.map g)
          x_2)
        x_3
⊢ X.flip₂₃.map g ≫
      {
        app := fun (Y_1 : C₃) ↦
          { app := fun (Z : C₂) ↦ ((f.app x_1).app Z).app Y_1, naturality := ⋯ :
            NatTrans ((X.flip₂₃.obj x_1).obj Y_1) ((Y.flip₂₃.obj x_1).obj Y_1) },
        naturality := ⋯ : NatTrans (X.flip₂₃.obj x_1) (Y.flip₂₃.obj x_1) } =
    {
        app := fun (Y_1 : C₃) ↦
          { app := fun (Z : C₂) ↦ ((f.app x).app Z).app Y_1, naturality := ⋯ :
            NatTrans ((X.flip₂₃.obj x).obj Y_1) ((Y.flip₂₃.obj x).obj Y_1) },
        naturality := ⋯ : NatTrans (X.flip₂₃.obj x) (Y.flip₂₃.obj x) } ≫
      Y.flip₂₃.map g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_4, u_3} C₁₂
inst_4 : Category.{v_5, u_5} C₂₃
inst_5 : Category.{v_6, u_6} D₁
inst_6 : Category.{v_7, u_7} D₂
inst_7 : Category.{v_8, u_8} D₃
inst_8 : Category.{v_9, u_9} E
X Y : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_9, u_4, u_9} C₃ E
f : X ⟶ Y
x x_1 : C₁
g : x ⟶ x_1
x_2 : C₃
x_3 : C₂
w :
  ((X.map g).app x_3).app x_2 ≫ ((f.app x_1).app x_3).app x_2 =
    ((f.app x).app x_3).app x_2 ≫ ((Y.map g).app x_3).app x_2
⊢ ((X.flip₂₃.map g ≫
              {
                app := fun (Y_1 : C₃) ↦
                  { app := fun (Z : C₂) ↦ ((f.app x_1).app Z).app Y_1, naturality := ⋯ :
                    NatTrans ((X.flip₂₃.obj x_1).obj Y_1) ((Y.flip₂₃.obj x_1).obj Y_1) },
                naturality := ⋯ : NatTrans (X.flip₂₃.obj x_1) (Y.flip₂₃.obj x_1) }).app
          x_2).app
      x_3 =
    NatTrans.app
      (NatTrans.app
        ({
            app := fun (Y_1 : C₃) ↦
              { app := fun (Z : C₂) ↦ ((f.app x).app Z).app Y_1, naturality := ⋯ :
                NatTrans ((X.flip₂₃.obj x).obj Y_1) ((Y.flip₂₃.obj x).obj Y_1) },
            naturality := ⋯ : NatTrans (X.flip₂₃.obj x) (Y.flip₂₃.obj x) } ≫
          Y.flip₂₃.map g)
        x_2)
      x_3

Tactic:
simp only [flip₂₃_obj_obj_obj, NatTrans.comp_app, flip₂₃_map_app_app]

Premises used: CategoryTheory.Functor.flip₂₃_obj_obj_obj, CategoryTheory.Functor.flip₂₃_map_app_app, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Functor.CurryingThree
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_4} C₃
inst_3 : Category.{v_4, u_3} C₁₂
inst_4 : Category.{v_5, u_5} C₂₃
inst_5 : Category.{v_6, u_6} D₁
inst_6 : Category.{v_7, u_7} D₂
inst_7 : Category.{v_8, u_8} D₃
inst_8 : Category.{v_9, u_9} E
X Y : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_9, u_4, u_9} C₃ E
f : X ⟶ Y
x x_1 : C₁
g : x ⟶ x_1
x_2 : C₃
x_3 : C₂
⊢ ((X.map g).app x_3).app x_2 ≫ ((f.app x_1).app x_3).app x_2 =
    ((f.app x).app x_3).app x_2 ≫ ((Y.map g).app x_3).app x_2

Tactic:
simp [← NatTrans.comp_app]

Premises used: CategoryTheory.NatTrans.comp_app