-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
dsimp :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
          (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
            (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
              enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
                @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
                  ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
                  ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
            (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
              (NatTrans.app (pre (𝟙 (F₁.obj j'))) (F₃.obj j')) (eHomWhiskerLeft C (F₁.obj j') (𝟙 (F₃.obj j')))))
          (NatTrans.app (pre (F₁.map φ)) (F₃.obj j'))))
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
          (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
          (Functor.map (ihom (F₁.obj j)) (F₃.map φ))))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y :=
          Functor.obj
            (Functor.obj (diagram C (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) (Opposite.op (Under.mk (𝟙 j'))))
            (Under.mk (𝟙 j')))
          (CategoryStruct.comp (Y :=
            @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
              ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
              ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
            (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))))
            (CategoryStruct.comp (Y :=
              @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _ ((Under.forget j' ⋙ F₁).obj (Under.mk (𝟙 j')))
                ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
              (NatTrans.app
                (pre (NatTrans.app (Iso.inv (Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₁))) (Under.mk (𝟙 j'))))
                ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
              (eHomWhiskerLeft C ((Under.forget j' ⋙ F₁).obj (Under.mk (𝟙 j')))
                (NatTrans.app (Iso.hom (Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₃))) (Under.mk (𝟙 j'))))))
          (NatTrans.app (pre (F₁.map φ)) (F₃.obj j'))))
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
          (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
          (Functor.map (ihom (F₁.obj j)) (F₃.map φ))))

Tactic:
dsimp