-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
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
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)
⊢ 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)))

Tactic:
ext