-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x : C
x_1 : (obj (𝟭 (C ⥤ Type (max w v u))) G).obj x
⊢ Eq (α := F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app
                (f ≫
                  (Equiv.symm (functorHomEquiv.{w, v, u} F H (tensorObj (𝒞 := category) F H)) :
                      (a : F ⊗ H ⟶ F ⊗ H) → H ⟶ F.functorHom (F ⊗ H))
                    (𝟙 (tensorObj (𝒞 := category) F H)))
                x) :
            TypeCat.Fun (G.obj x) (F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))) :
          (a : G.obj x) → F.HomObj (F ⊗ H) (coyoneda.obj (Opposite.op x)))
        x_1 :
      F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app
                ((Equiv.symm (functorHomEquiv.{w, v, u} F G (tensorObj (𝒞 := category) F G)) :
                      (a : F ⊗ G ⟶ F ⊗ G) → G ⟶ F.functorHom (F ⊗ G))
                    (𝟙 (tensorObj (𝒞 := category) F G)) ≫
                  (rightAdj.{w, v, u} F).map (F ◁ f))
                x) :
            TypeCat.Fun (G.obj x) (F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))) :
          (a : G.obj x) → F.HomObj (F ⊗ H) (coyoneda.obj (Opposite.op x)))
        x_1 :
      F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))
have w : ∀ (x_2 : C) (x_3 : obj (obj coyoneda (Opposite.op x)) x_2) (x_4 : F.obj x_2),
  Eq (α := (tensorObj (𝒞 := category) F H).obj x_2)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (HomObj.app
          (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                  (NatTrans.app
                    (f ≫
                      (Equiv.symm (functorHomEquiv.{w, v, u} F H (tensorObj (𝒞 := category) F H)) :
                          (a : F ⊗ H ⟶ F ⊗ H) → H ⟶ F.functorHom (F ⊗ H))
                        (𝟙 (tensorObj (𝒞 := category) F H)))
                    x) :
                TypeCat.Fun (G.obj x) (F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))) :
              (a : G.obj x) → F.HomObj (F ⊗ H) (coyoneda.obj (Opposite.op x)))
            x_1)
          x_2 x_3))
      x_4)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (HomObj.app
          (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                  (NatTrans.app
                    ((Equiv.symm (functorHomEquiv.{w, v, u} F G (tensorObj (𝒞 := category) F G)) :
                          (a : F ⊗ G ⟶ F ⊗ G) → G ⟶ F.functorHom (F ⊗ G))
                        (𝟙 (tensorObj (𝒞 := category) F G)) ≫
                      (rightAdj.{w, v, u} F).map (F ◁ f))
                    x) :
                TypeCat.Fun (G.obj x) (F.HomObj (tensorObj (𝒞 := category) F H) (obj coyoneda (Opposite.op x)))) :
              (a : G.obj x) → F.HomObj (F ⊗ H) (coyoneda.obj (Opposite.op x)))
            x_1)
          x_2 x_3))
      x_4)
Tactic: ext