-- 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
w :
  ∀ (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
⊢ (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)))
      ((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))
        φ) =
    φ

Tactic:
ext X a Y f