-- 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 :
  F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    F₂.map k.hom ≫
      curry (f.app k.right) ≫
        Iso.inv
            (ρ_ (Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k)) ≫
          Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k ◁
              CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
                ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
                (enrichedHomπ C F₃ F₃' (Functor.obj (Under.forget j) k) ≫
                  NatTrans.app (pre (NatTrans.app (Iso.inv (Iso.refl (Under.forget j ⋙ F₃))) k))
                      (F₃'.obj (Functor.obj (Under.forget j) k)) ≫
                    Functor.map (ihom ((Under.forget j ⋙ F₃).obj k))
                      (NatTrans.app (Iso.hom (Iso.refl (Under.forget j ⋙ F₃'))) k)) ≫
            eComp C (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₃).obj k)
              ((Under.forget j ⋙ F₃').obj k)
⊢ Eq (α :=
    F₂.obj j ⟶ Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')) (Opposite.op k)) k)
    (CategoryStruct.comp (Y := end_ (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')))
      (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯)
      (end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')) k))
    (CategoryStruct.comp (Y := end_ (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')))
      (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯ ≫
        Iso.inv (ρ_ (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
              (enrichedHom C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))
            (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ◁
              CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
                ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
                (precompEnrichedHom C F₃ F₃' (Under.forget j)))
            (enrichedComp C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))
      (end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')) k))

Tactic:
rw [Category.assoc, Category.assoc, Category.assoc, end_.lift_π, enrichedComp_π,
    tensorHom_def, Category.assoc, whisker_exchange_assoc, whiskerRight_id_assoc,
    Iso.inv_hom_id_assoc, end_.lift_π_assoc, Category.assoc,
    ← MonoidalCategory.whiskerLeft_comp_assoc, Category.assoc, end_.lift_π,
    enrichedOrdinaryCategorySelf_eHomWhiskerRight,
    enrichedOrdinaryCategorySelf_eHomWhiskerLeft]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerRight, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Limits.end_.lift_π, CategoryTheory.Enriched.FunctorCategory.enrichedComp_π, CategoryTheory.MonoidalCategory.whiskerRight_id_assoc, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerLeft, CategoryTheory.Limits.end_.lift_π_assoc