-- 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₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under.{v₂, u₂} j
w :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃'.obj k.right))
    (F₂.map k.hom ≫ curry (f.app k.right) ≫ Functor.map (ihom (F₁.obj k.right)) (f₃.app k.right))
    (F₂.map k.hom ≫
      curry (f.app k.right) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
            (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
          (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
              (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
            (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
              (eHomEquiv C : (a : F₃.obj k.right ⟶ F₃'.obj k.right) → 𝟙_ C ⟶ F₃.obj k.right ⟶[C] F₃'.obj k.right)
                (f₃.app k.right))
            (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right))))
⊢ Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃'.obj k.right))
    (F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right))
    (F₂.map k.hom ≫
      curry (f.app k.right) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
            (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
          (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
              (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
            (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
              CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
                ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
                (enrichedHomπ C F₃ F₃' k.right ≫
                  NatTrans.app (pre (𝟙 (F₃.obj k.right))) (F₃'.obj k.right) ≫
                    Functor.map (ihom (F₃.obj k.right)) (𝟙 (F₃'.obj k.right))))
            (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right))))

Tactic:
rw [pre_id, NatTrans.id_app, Functor.map_id, Category.comp_id,
    Category.comp_id, homEquiv_apply_π, curry_natural_right]

Premises used: CategoryTheory.Enriched.FunctorCategory.homEquiv_apply_π, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalClosed.pre_id, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app, CategoryTheory.MonoidalClosed.curry_natural_right