-- 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
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)
have w : Eq (α := F.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).1
  (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).1
Tactic: apply Prod.ext