-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.FunctorHom (goal)
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
⊢ (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))
        φ) =
    φ
have 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 := sorry : F.HomObj G (Opposite.unop (obj (Functor.rightOp coyoneda) X)) },
                    naturality := sorry } :
                  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 := sorry } :
                    F.HomObj G A))
                φ))
            X))
        a)
      Y f =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (φ.app X)).toFun a).app Y f
Tactic: ext X a Y f