-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic (goal)
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'
⊢ 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 φ))))
have 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 φ))))
Tactic: dsimp