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_1 G_1 : Functor.{v, v', u, u'} C D
F G A : Functor.{v, w, u, w + 1} C (Type w)
x : tensorObj (𝒞 := category) F A ⟶ G
⊢ (fun (a : F.HomObj G A) ↦
        ({
            app := fun (X : C) ↦
              ↾fun (x : (tensorObj (𝒞 := category) F A).obj X) ↦
                match (motive := (tensorObj (𝒞 := category) F A).obj X → G.obj X) x with
                | (x, y) =>
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X y) :
                      (a : (fun (X : Type w) ↦ X) (F.obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                    x,
            naturality := ⋯ } :
          NatTrans (tensorObj (𝒞 := category) F A) G))
      ((fun (a : tensorObj (𝒞 := category) F A ⟶ G) ↦
          ({
              app := fun (X : C) (y : A.obj X) ↦
                ↾fun (x : F.obj X) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X) :
                      (a : (fun (X : Type w) ↦ X) ((F ⊗ A).obj X)) → (fun (X : Type w) ↦ X) (G.obj X))
                    (x, y),
              naturality := ⋯ } :
            F.HomObj G A))
        x) =
    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
A : Functor.{v, w, u, w + 1} C (Type w)
f g : F.HomObj G A
h : f = g
X : C
a : A.obj X
subst : f.app X a = f.app X a
⊢ f.app X a = g.app X a

Tactic:
subst h
-- 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 : Functor.{v, w, u, w + 1} C (Type w)
f : F.HomObj G A
X : C
a : A.obj X
⊢ f.app X a = f.app X a

Tactic:
rfl
-- 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 A' : Functor.{v, w, u, w + 1} C (Type w)
f : A' ⟶ A
x : F.HomObj G A
Δ Δ' : C
φ : Δ ⟶ Δ'
a : A'.obj Δ
rw :
  F.map φ ≫
      x.app Δ'
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ') :
            (a : (fun (X : Type w) ↦ X) (A'.obj Δ')) → (fun (X : Type w) ↦ X) (A.obj Δ'))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (A'.map φ) :
                (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A'.obj Δ'))
              a :
            (fun (X : Type w) ↦ X) (A'.obj Δ'))) =
    F.map φ ≫
      x.app Δ'
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map φ) :
            (a : (fun (X : Type w) ↦ X) (A.obj Δ)) → (fun (X : Type w) ↦ X) (A.obj Δ'))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) :
                (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A.obj Δ))
              a :
            (fun (X : Type w) ↦ X) (A.obj Δ)))
rw₁ rw₂ :
  F.map φ ≫
      x.app Δ'
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map φ) : (a : A.obj Δ) → A.obj Δ')
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) : (a : A'.obj Δ) → A.obj Δ) a : A.obj Δ)) =
    F.map φ ≫
      x.app Δ'
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map φ) :
            (a : (fun (X : Type w) ↦ X) (A.obj Δ)) → (fun (X : Type w) ↦ X) (A.obj Δ'))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) :
                (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A.obj Δ))
              a :
            (fun (X : Type w) ↦ X) (A.obj Δ)))
⊢ F.map φ ≫
      x.app Δ'
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ') :
            (a : (fun (X : Type w) ↦ X) (A'.obj Δ')) → (fun (X : Type w) ↦ X) (A.obj Δ'))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (A'.map φ) :
                (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A'.obj Δ'))
              a :
            (fun (X : Type w) ↦ X) (A'.obj Δ'))) =
    x.app Δ
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Δ) :
            (a : (fun (X : Type w) ↦ X) (A'.obj Δ)) → (fun (X : Type w) ↦ X) (A.obj Δ))
          a) ≫
      G.map φ

Tactic:
rw [← x.naturality φ (f.app Δ a), f.naturality_apply φ a]

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.ConcreteCategory.hom, 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
A A' : (Functor.{v, w, u, w + 1} C (Type w))ᵒᵖ
f : A ⟶ A'
x : HomObj.{w, v', v, u, u'} F G (Opposite.unop A)
X Y : C
φ : X ⟶ Y
a : (Opposite.unop A').obj X
rw :
  F.map φ ≫
      x.app Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app Y) :
            (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A').map φ) :
                (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                  (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))
              a :
            (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))) =
    F.map φ ≫
      x.app Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A).map φ) :
            (a : (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app X) :
                (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                  (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X))
              a :
            (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)))
⊢ F.map φ ≫
      x.app Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app Y) :
            (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A').map φ) :
                (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                  (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))
              a :
            (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))) =
    x.app X
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app X) :
            (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X))
          a) ≫
      G.map φ

Tactic:
rw [← HomObj.naturality]

Premises used: CategoryTheory.Functor.HomObj.naturality
-- 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 A' : (Functor.{v, w, u, w + 1} C (Type w))ᵒᵖ
f : A ⟶ A'
x : HomObj.{w, v', v, u, u'} F G (Opposite.unop A)
X Y : C
φ : X ⟶ Y
a : (Opposite.unop A').obj X
e_a :
  Eq (α := (Opposite.unop A).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app Y) :
          (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A').map φ) :
              (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))
            a :
          (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) :
      (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A).map φ) :
          (a : (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app X) :
              (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X))
            a :
          (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)) :
      (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
⊢ F.map φ ≫
      x.app Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app Y) :
            (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A').map φ) :
                (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                  (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))
              a :
            (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))) =
    F.map φ ≫
      x.app Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A).map φ) :
            (a : (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app X) :
                (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                  (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X))
              a :
            (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)))

Tactic:
congr 2
-- 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 A' : (Functor.{v, w, u, w + 1} C (Type w))ᵒᵖ
f : A ⟶ A'
x : HomObj.{w, v', v, u, u'} F G (Opposite.unop A)
X Y : C
φ : X ⟶ Y
a : (Opposite.unop A').obj X
⊢ Eq (α := (Opposite.unop A).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app Y) :
          (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A').map φ) :
              (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))
            a :
          (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) :
      (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A).map φ) :
          (a : (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app X) :
              (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X))
            a :
          (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)) :
      (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))

Tactic:
ConcreteCategory.congr_hom (f.unop.naturality φ) a

Premises used: Quiver.Hom.unop, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom
-- 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 A' : (Functor.{v, w, u, w + 1} C (Type w))ᵒᵖ
f : A ⟶ A'
x : HomObj.{w, v', v, u, u'} F G (Opposite.unop A)
X Y : C
φ : X ⟶ Y
a : (Opposite.unop A').obj X
⊢ Eq (α := (Opposite.unop A).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app Y) :
          (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A').map φ) :
              (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y))
            a :
          (fun (X : Type w) ↦ X) ((Opposite.unop A').obj Y)) :
      (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Opposite.unop A).map φ) :
          (a : (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)) → (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.unop.app X) :
              (a : (fun (X : Type w) ↦ X) ((Opposite.unop A').obj X)) →
                (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X))
            a :
          (fun (X : Type w) ↦ X) ((Opposite.unop A).obj X)) :
      (fun (X : Type w) ↦ X) ((Opposite.unop A).obj Y))

Tactic:
exact ConcreteCategory.congr_hom (f.unop.naturality φ) a

Premises used: Quiver.Hom.unop, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom
-- 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
X : C
x y : (F.functorHom G).obj X
h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f
h₁ : ∀ (x_1 : C) (x_2 : obj (Opposite.unop (obj (Functor.rightOp coyoneda) X)) x_1), x.app x_1 x_2 = y.app x_1 x_2
⊢ x.app = y.app

Tactic:
ext
-- 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
X : C
x y : (F.functorHom G).obj X
h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f
x_1 : C
x_2 : obj (Opposite.unop (obj (Functor.rightOp coyoneda) X)) x_1
⊢ x.app x_1 x_2 = y.app x_1 x_2

Tactic:
apply h
-- 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 Y : C
f : X ⟶ Y
a : A.obj X
rw :
  Eq (α := F.obj X ⟶ G.obj Y)
    (F.map f ≫
      HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Y) :
            (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y)) →
              (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
              (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj X)) →
                (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y))
            a))
        Y (𝟙 (Opposite.unop (Opposite.op Y))))
    (F.map f ≫
      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)
        Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) f) :
            (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 f ≫
      HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Y) :
            (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y)) →
              (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
              (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj X)) →
                (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y))
            a))
        Y (𝟙 (Opposite.unop (Opposite.op Y))) =
    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))) ≫
      G.map f

Tactic:
rw [← (φ.app X a).naturality f (𝟙 _)]

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.id, 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
A : C ⥤ Type (max u v v')
φ : A ⟶ F.functorHom G
X Y : C
f : X ⟶ Y
a : A.obj X
⊢ Eq.{v' + 1} (α := F.obj Y ⟶ G.obj Y)
    (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f ≫ φ.app Y) : (a : A.obj X) → (F.functorHom G).obj Y) a) Y
      (𝟙 (Opposite.unop (Opposite.op Y))))
    (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X ≫ (F.functorHom G).map f) :
          (a : A.obj X) → (F.functorHom G).obj Y)
        a)
      Y (𝟙 (Opposite.unop (Opposite.op Y))))

Tactic:
have := HomObj.congr_app (ConcreteCategory.congr_hom (φ.naturality f) 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
A : C ⥤ Type (max u v v')
φ : A ⟶ F.functorHom G
X Y : C
f : X ⟶ Y
a : A.obj X
this :
  Eq.{v' + 1} (α := F.obj Y ⟶ G.obj Y)
    (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f ≫ φ.app Y) : (a : A.obj X) → (F.functorHom G).obj Y) a) Y
      (𝟙 (Opposite.unop (Opposite.op Y))))
    (HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X ≫ (F.functorHom G).map f) :
          (a : A.obj X) → (F.functorHom G).obj Y)
        a)
      Y (𝟙 (Opposite.unop (Opposite.op Y))))
⊢ Eq (α := F.obj X ⟶ G.obj Y)
    (F.map f ≫
      HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app Y) :
            (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y)) →
              (fun (X : Type (max (max u v) v')) ↦ X) ((F.functorHom G).obj Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
              (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj X)) →
                (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y))
            a))
        Y (𝟙 (Opposite.unop (Opposite.op Y))))
    (F.map f ≫
      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)
        Y
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (Opposite.unop (obj (Functor.rightOp coyoneda) X)) f) :
            (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:
simp_all [-NatTrans.naturality, functorHom, homObjFunctor]

Premises used: CategoryTheory.Functor.functorHom, CategoryTheory.Functor.homObjFunctor, CategoryTheory.NatTrans.naturality
-- 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
X Y : C
f : X ⟶ Y
h :
  ∀ (x_1 : A.obj X) (Y_1 : C) (f_1 : Y ⟶ Y_1),
    HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (A.map f ≫
              ↾fun (a : A.obj Y) ↦
                {
                  app := fun (Y_2 : C) (f : obj (Opposite.unop (obj (Functor.rightOp coyoneda) Y)) Y_2) ↦
                    x.app Y_2
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
                          (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj (Opposite.unop (Opposite.op Y)))) →
                            (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y_2))
                        a),
                  naturality := ⋯ : F.HomObj G (Opposite.unop (obj (Functor.rightOp coyoneda) Y)) }))
          x_1)
        Y_1 f_1 =
      (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              ((↾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)) }) ≫
                (F.functorHom G).map f))
            x_1).app
        Y_1 f_1
⊢ (A.map f ≫
      ↾fun (a : A.obj Y) ↦
        {
          app := fun (Y_1 : C) (f : obj (Opposite.unop (obj (Functor.rightOp coyoneda) Y)) Y_1) ↦
            x.app Y_1
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
                  (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj (Opposite.unop (Opposite.op Y)))) →
                    (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y_1))
                a),
          naturality := ⋯ }) =
    (↾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)) }) ≫
      (F.functorHom G).map f

Tactic:
ext
-- 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
X Y : C
f : X ⟶ Y
x_1 : A.obj X
Y_1 : C
f_1 : Y ⟶ Y_1
⊢ HomObj.app (A := Opposite.unop (obj (Functor.rightOp coyoneda) Y))
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (A.map f ≫
            ↾fun (a : A.obj Y) ↦
              {
                app := fun (Y_2 : C) (f : obj (Opposite.unop (obj (Functor.rightOp coyoneda) Y)) Y_2) ↦
                  x.app Y_2
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f) :
                        (a : (fun (X : Type (max (max u v) v')) ↦ X) (A.obj (Opposite.unop (Opposite.op Y)))) →
                          (fun (X : Type (max (max u v) v')) ↦ X) (A.obj Y_2))
                      a),
                naturality := ⋯ : F.HomObj G (Opposite.unop (obj (Functor.rightOp coyoneda) Y)) }))
        x_1)
      Y_1 f_1 =
    (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾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)) }) ≫
              (F.functorHom G).map f))
          x_1).app
      Y_1 f_1

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
A : C ⥤ Type (max u v v')
φ : A ⟶ F.functorHom G
X : C
a : A.obj X
Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Quiver.Hom.unop (map (Functor.rightOp coyoneda) f)) Y) :
        (a : (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj Y)).obj Y)) →
          (fun (X : Type v) ↦ X) ((Opposite.unop (coyoneda.rightOp.obj X)).obj Y))
      (𝟙 (Opposite.unop (Opposite.op Y))) =
    f

Tactic:
simp