awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
A : C ⥤ Type (max u v v')
φ : A ⟶ F.functorHom G
X : C
a : A.obj X
Y : C
f : X ⟶ Y
⊢ HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun (x : F.HomObj G A) ↦
                ({
                    app := fun (X : C) ↦
                      ↾fun (a : A.obj X) ↦
                        {
                          app := fun (Y : C) (f : obj (Opposite.unop (obj (Functor.rightOp coyoneda) X)) Y) ↦
                            x.app Y
                              ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
                                  (a :
                                      (fun (X : Type (max (max u v) v')) ↦ X) (A.obj (Opposite.unop (Opposite.op X)))) →
                                    (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y))
                                a),
                          naturality := ⋯ : F.HomObj G (Opposite.unop (obj (Functor.rightOp coyoneda) X)) },
                    naturality := ⋯ } :
                  NatTrans A (F.functorHom G)))
              ((fun (φ : A ⟶ F.functorHom G) ↦
                  ({
                      app := fun (X : C) (a : A.obj X) ↦
                        HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X) :
                              (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj X)) →
                                (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                            a)
                          X (𝟙 (Opposite.unop (Opposite.op X))),
                      naturality := ⋯ } :
                    F.HomObj G A))
                φ))
            X))
        a)
      Y f =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X)).toFun a).app Y f

Tactic:
exact (HomObj.congr_app (ConcreteCategory.congr_hom (φ.naturality f) a) Y (𝟙 _)).trans
      (congr_arg ((φ.app X a).app Y) (by simp))

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.id, congr_arg, CategoryTheory.Functor.HomObj.app, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Functor.HomObj.congr_app, DFunLike.coe, CategoryTheory.NatTrans.app, Eq.trans
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
A : C ⥤ Type (max u v v')
x : F.HomObj G A
⊢ (fun (φ : A ⟶ F.functorHom G) ↦
        ({
            app := fun (X : C) (a : A.obj X) ↦
              HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X) :
                    (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj X)) →
                      (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                  a)
                X (𝟙 (Opposite.unop (Opposite.op X))),
            naturality := ⋯ } :
          F.HomObj G A))
      ((fun (x : F.HomObj G A) ↦
          ({
              app := fun (X : C) ↦
                ↾fun (a : A.obj X) ↦
                  {
                    app := fun (Y : C) (f : obj (Opposite.unop (obj (Functor.rightOp coyoneda) X)) Y) ↦
                      x.app Y
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
                            (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj (Opposite.unop (Opposite.op X)))) →
                              (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y))
                          a),
                    naturality := ⋯ },
              naturality := ⋯ } :
            NatTrans A (F.functorHom G)))
        x) =
    x

Tactic:
simp [functorHom, homObjFunctor]

Premises used: CategoryTheory.Functor.functorHom, CategoryTheory.Functor.homObjFunctor
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G
X Y : C
φ : X ⟶ Y
rw :
  Eq (α := F.obj X ⟶ G.obj Y)
    (F.map φ ≫
      (fun (X : C) ↦
          (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                  (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                    (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                PUnit.unit)
              X (𝟙 (Opposite.unop (Opposite.op X))) :
            F.obj X ⟶ G.obj X))
        Y)
    (F.map φ ≫
      HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
            (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
              (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
          PUnit.unit)
        Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) φ) :
            (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj X)) →
              (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj Y))
          (𝟙 (Opposite.unop (Opposite.op X)))))
⊢ F.map φ ≫
      (fun (X : C) ↦
          (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                  (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                    (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                PUnit.unit)
              X (𝟙 (Opposite.unop (Opposite.op X))) :
            F.obj X ⟶ G.obj X))
        Y =
    (fun (X : C) ↦
          (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                  (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                    (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                PUnit.unit)
              X (𝟙 (Opposite.unop (Opposite.op X))) :
            F.obj X ⟶ G.obj X))
        X ≫
      G.map φ

Tactic:
rw [← (f.app X (PUnit.unit)).naturality φ]

Premises used: CategoryTheory.ConcreteCategory.hom, PUnit.unit, CategoryTheory.Functor.HomObj.naturality, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G
X Y : C
φ : X ⟶ Y
e_a :
  Eq.{v' + 1} (α := F.obj Y ⟶ G.obj Y)
    ((fun (X : C) ↦
        (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                  (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
              PUnit.unit)
            X (𝟙 (Opposite.unop (Opposite.op X))) :
          F.obj X ⟶ G.obj X))
      Y)
    (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
        PUnit.unit)
      Y
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) φ) :
          (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj X)) →
            (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj Y))
        (𝟙 (Opposite.unop (Opposite.op X)))))
⊢ Eq (α := F.obj X ⟶ G.obj Y)
    (F.map φ ≫
      (fun (X : C) ↦
          (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                  (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                    (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                PUnit.unit)
              X (𝟙 (Opposite.unop (Opposite.op X))) :
            F.obj X ⟶ G.obj X))
        Y)
    (F.map φ ≫
      HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
            (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
              (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
          PUnit.unit)
        Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) φ) :
            (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj X)) →
              (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj Y))
          (𝟙 (Opposite.unop (Opposite.op X)))))

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G
X Y : C
φ : X ⟶ Y
⊢ Eq.{v' + 1} (α := F.obj Y ⟶ G.obj Y)
    (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (map ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) φ ≫ f.app Y) :
          (a : (𝟙_ (C ⥤ Type (max v' v u))).obj X) → (F.functorHom G).obj Y)
        PUnit.unit)
      Y (𝟙 Y))
    (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X ≫ (F.functorHom G).map φ) :
          (a : (𝟙_ (C ⥤ Type (max v' v u))).obj X) → (F.functorHom G).obj Y)
        PUnit.unit)
      Y (𝟙 Y))

Tactic:
have := HomObj.congr_app (ConcreteCategory.congr_hom (f.naturality φ) PUnit.unit) Y (𝟙 Y)
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G
X Y : C
φ : X ⟶ Y
this :
  Eq.{v' + 1} (α := F.obj Y ⟶ G.obj Y)
    (HomObj.app (A := obj coyoneda (Opposite.op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : 𝟙_ (Type (max v' v u))) → F.HomObj G (coyoneda.obj (Opposite.op Y)))
        PUnit.unit)
      Y (𝟙 Y))
    (HomObj.app (A := obj coyoneda (Opposite.op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : 𝟙_ (Type (max v' v u))) → F.HomObj G (coyoneda.obj (Opposite.op X)))
        PUnit.unit)
      Y (φ ≫ 𝟙 Y))
⊢ Eq.{v' + 1} (α := F.obj Y ⟶ G.obj Y)
    ((fun (X : C) ↦
        (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                  (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
              PUnit.unit)
            X (𝟙 (Opposite.unop (Opposite.op X))) :
          F.obj X ⟶ G.obj X))
      Y)
    (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
            (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
        PUnit.unit)
      Y
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) φ) :
          (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj X)) →
            (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj Y))
        (𝟙 (Opposite.unop (Opposite.op X)))))

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G
w :
  ∀ (X : C) (a : obj ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) X) (Y : C) (φ : X ⟶ Y),
    HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              ((fun (f : F ⟶ G) ↦
                  {
                    app := fun (x : C) ↦
                      ↾fun (x_1 : obj ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) x) ↦ HomObj.ofNatTrans f,
                    naturality := ⋯ : NatTrans ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) (F.functorHom G) })
                ((fun (f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G) ↦
                    {
                      app := fun (X : C) ↦
                        HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                              (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                                (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                            PUnit.unit)
                          X (𝟙 (Opposite.unop (Opposite.op X))),
                      naturality := ⋯ : NatTrans F G })
                  f))
              X))
          a)
        Y φ =
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun a).app Y φ
⊢ (fun (f : F ⟶ G) ↦
        { app := fun (x : C) ↦ ↾fun (x_1 : obj ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) x) ↦ HomObj.ofNatTrans f,
          naturality := ⋯ : NatTrans ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) (F.functorHom G) })
      ((fun (f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G) ↦
          {
            app := fun (X : C) ↦
              HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                    (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                      (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                  PUnit.unit)
                X (𝟙 (Opposite.unop (Opposite.op X))),
            naturality := ⋯ : NatTrans F G })
        f) =
    f

Tactic:
ext X a Y φ
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G
X : C
a : obj ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) X
Y : C
φ : X ⟶ Y
this :
  Eq.{v' + 1} (α := F.obj Y ⟶ G.obj Y)
    (HomObj.app (A := obj coyoneda (Opposite.op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : 𝟙_ (Type (max v' v u))) → F.HomObj G (coyoneda.obj (Opposite.op Y)))
        PUnit.unit)
      Y (𝟙 Y))
    (HomObj.app (A := obj coyoneda (Opposite.op X))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : 𝟙_ (Type (max v' v u))) → F.HomObj G (coyoneda.obj (Opposite.op X)))
        PUnit.unit)
      Y (φ ≫ 𝟙 Y))
⊢ HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun (f : F ⟶ G) ↦
                {
                  app := fun (x : C) ↦
                    ↾fun (x_1 : obj ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) x) ↦ HomObj.ofNatTrans f,
                  naturality := ⋯ : NatTrans ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) (F.functorHom G) })
              ((fun (f : (𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category) ⟶ F.functorHom G) ↦
                  {
                    app := fun (X : C) ↦
                      HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) X))
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                            (a : (fun (X : Type (max (max u v) v')) ↦ X) ((𝟙_ (C ⥤ Type (max v' v u))).obj X)) →
                              (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj X))
                          PUnit.unit)
                        X (𝟙 (Opposite.unop (Opposite.op X))),
                    naturality := ⋯ : NatTrans F G })
                f))
            X))
        a)
      Y φ =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun a).app Y φ

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G : Functor.{v, v', u, u'} C D
f : F ⟶ G
X : C
a : obj ((𝟙_ (C ⥤ Type (max v' v u))) (𝒞 := category)) X
Y : C
φ : X ⟶ Y
⊢ HomObj.app (A := obj coyoneda (Opposite.op X))
      (({ toFun := fun (x : (𝟙_ (Type (max v' v u))) (𝒞 := types)) ↦ HomObj.ofNatTrans f } :
          (a : 𝟙_ (Type (max v' v u))) → F.HomObj G (coyoneda.obj (Opposite.op X)))
        a)
      Y φ =
    f.app Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
K L : Functor.{v, v', u, u'} C D
X : C
f : K ⟶ K
x : tensorObj (𝒞 := types) ((𝟙_ (Type (max (max u v) v'))) (𝒞 := types)) ((K.functorHom L).obj X)
⊢ Eq (α :=
    tensorObj (𝒞 := types) (K.HomObj K (obj coyoneda (Opposite.op X))) (K.HomObj L (obj coyoneda (Opposite.op X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾fun (x : (𝟙_ (Type (max v' v u))) (𝒞 := types)) ↦ HomObj.ofNatTrans f) ▷
              K.HomObj L (obj coyoneda (Opposite.op X))) :
          (a : 𝟙_ (Type (max v' v u)) ⊗ K.HomObj L (coyoneda.obj (Opposite.op X))) →
            K.HomObj K (coyoneda.obj (Opposite.op X)) ⊗ K.HomObj L (coyoneda.obj (Opposite.op X)))
        x :
      tensorObj (𝒞 := types) (K.HomObj K (obj coyoneda (Opposite.op X))) (K.HomObj L (obj coyoneda (Opposite.op X))))
    ((HomObj.ofNatTrans f, x.2) : K.HomObj K (obj coyoneda (Opposite.op X)) × K.HomObj L (obj coyoneda (Opposite.op X)))

Tactic:
rfl

Premises used: CategoryTheory.Functor.HomObj.ofNatTrans, rfl
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
K L : Functor.{v, v', u, u'} C D
X : C
f : L ⟶ L
x : tensorObj (𝒞 := types) ((K.functorHom L).obj X) ((𝟙_ (Type (max (max u v) v'))) (𝒞 := types))
⊢ Eq (α :=
    tensorObj (𝒞 := types) (K.HomObj L (obj coyoneda (Opposite.op X))) (L.HomObj L (obj coyoneda (Opposite.op X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (K.HomObj L (obj coyoneda (Opposite.op X)) ◁
              ↾fun (x : (𝟙_ (Type (max v' v u))) (𝒞 := types)) ↦ HomObj.ofNatTrans f) :
          (a : K.HomObj L (coyoneda.obj (Opposite.op X)) ⊗ 𝟙_ (Type (max v' v u))) →
            K.HomObj L (coyoneda.obj (Opposite.op X)) ⊗ L.HomObj L (coyoneda.obj (Opposite.op X)))
        x :
      tensorObj (𝒞 := types) (K.HomObj L (obj coyoneda (Opposite.op X))) (L.HomObj L (obj coyoneda (Opposite.op X))))
    ((x.1, HomObj.ofNatTrans f) : K.HomObj L (obj coyoneda (Opposite.op X)) × L.HomObj L (obj coyoneda (Opposite.op X)))

Tactic:
rfl

Premises used: CategoryTheory.Functor.HomObj.ofNatTrans, rfl
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
K L M N : Functor.{v, v', u, u'} C D
g : tensorObj (𝒞 := category) (L.functorHom M) (M.functorHom N) ⟶ L.functorHom N
X : C
a : (tensorObj (𝒞 := category) (K.functorHom L) (tensorObj (𝒞 := category) (L.functorHom M) (M.functorHom N))).obj X
⊢ Eq (α :=
    tensorObj (𝒞 := types) (K.HomObj L (obj coyoneda (Opposite.op X))) (L.HomObj N (obj coyoneda (Opposite.op X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (K.HomObj L (obj coyoneda (Opposite.op X)) ◁ g.app X) :
          (a :
              K.HomObj L (coyoneda.obj (Opposite.op X)) ⊗
                L.HomObj M (coyoneda.obj (Opposite.op X)) ⊗ M.HomObj N (coyoneda.obj (Opposite.op X))) →
            K.HomObj L (coyoneda.obj (Opposite.op X)) ⊗ L.HomObj N (coyoneda.obj (Opposite.op X)))
        a :
      tensorObj (𝒞 := types) (K.HomObj L (obj coyoneda (Opposite.op X))) (L.HomObj N (obj coyoneda (Opposite.op X))))
    ((a.1,
        (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app X) :
            (a : L.HomObj M (coyoneda.obj (Opposite.op X)) ⊗ M.HomObj N (coyoneda.obj (Opposite.op X))) →
              L.HomObj N (coyoneda.obj (Opposite.op X)))
          a.2) :
      K.HomObj L (obj coyoneda (Opposite.op X)) × L.HomObj N (obj coyoneda (Opposite.op X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
K L M N : Functor.{v, v', u, u'} C D
f : tensorObj (𝒞 := category) (K.functorHom L) (L.functorHom M) ⟶ K.functorHom M
X : C
a : (tensorObj (𝒞 := category) (tensorObj (𝒞 := category) (K.functorHom L) (L.functorHom M)) (M.functorHom N)).obj X
⊢ Eq (α :=
    tensorObj (𝒞 := types) (K.HomObj M (obj coyoneda (Opposite.op X))) (M.HomObj N (obj coyoneda (Opposite.op X))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X ▷ M.HomObj N (obj coyoneda (Opposite.op X))) :
          (a :
              (K.HomObj L (coyoneda.obj (Opposite.op X)) ⊗ L.HomObj M (coyoneda.obj (Opposite.op X))) ⊗
                M.HomObj N (coyoneda.obj (Opposite.op X))) →
            K.HomObj M (coyoneda.obj (Opposite.op X)) ⊗ M.HomObj N (coyoneda.obj (Opposite.op X)))
        a :
      tensorObj (𝒞 := types) (K.HomObj M (obj coyoneda (Opposite.op X))) (M.HomObj N (obj coyoneda (Opposite.op X))))
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
            (a : K.HomObj L (coyoneda.obj (Opposite.op X)) ⊗ L.HomObj M (coyoneda.obj (Opposite.op X))) →
              K.HomObj M (coyoneda.obj (Opposite.op X)))
          a.1,
        a.2) :
      K.HomObj M (obj coyoneda (Opposite.op X)) × M.HomObj N (obj coyoneda (Opposite.op X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Functor.FunctorHom
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
K L M N : Functor.{v, v', u, u'} C D
X : C
x : (tensorObj (𝒞 := category) (K.functorHom L) (tensorObj (𝒞 := category) (L.functorHom M) (M.functorHom N))).obj X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.inv
            (α_ (K.HomObj L (obj coyoneda (Opposite.op X))) (L.HomObj M (obj coyoneda (Opposite.op X)))
              (M.HomObj N (obj coyoneda (Opposite.op X))))) :
        (a :
            K.HomObj L (coyoneda.obj (Opposite.op X)) ⊗
              L.HomObj M (coyoneda.obj (Opposite.op X)) ⊗ M.HomObj N (coyoneda.obj (Opposite.op X))) →
          (K.HomObj L (coyoneda.obj (Opposite.op X)) ⊗ L.HomObj M (coyoneda.obj (Opposite.op X))) ⊗
            M.HomObj N (coyoneda.obj (Opposite.op X)))
      x =
    ((x.1, x.2.1), x.2.2)

Tactic:
rfl

Premises used: rfl