-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
k : Under.{v₃, u₃} j
w :
  Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
      obj (obj (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k)
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
      (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃))
        ((homEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ V ⟶ enrichedHom V F₁ F₂) f ⊗ₘ
          (homEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₂ F₃) g)
        (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃) (enrichedComp V F₁ F₂ F₃)
          (enrichedHomπ V F₁ F₃ (obj (Under.forget j) k) ≫
            eHomWhiskerRight V (NatTrans.app (Iso.inv (Iso.refl (Under.forget j ⋙ F₁))) k)
                (F₃.obj (obj (Under.forget j) k)) ≫
              eHomWhiskerLeft V ((Under.forget j ⋙ F₁).obj k)
                (NatTrans.app (Iso.hom (Iso.refl (Under.forget j ⋙ F₃))) k)))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
      (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
          (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)))
        (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
            ((homEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ V ⟶ enrichedHom V F₁ F₂) f)
            (precompEnrichedHom V F₁ F₂ (Under.forget j)) ⊗ₘ
          CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
            ((homEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₂ F₃) g) (precompEnrichedHom V F₂ F₃ (Under.forget j)))
        ((end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k ⊗ₘ
            end_.π (diagram V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) k) ≫
          eComp V (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₂).obj k)
            ((Under.forget j ⋙ F₃).obj k))))
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
      obj (obj (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k)
    (CategoryStruct.comp (Y := end_ (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)))
        (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃)
          ((homEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₁ F₃) (f ≫ g))
          (precompEnrichedHom V F₁ F₃ (Under.forget j)))
        (end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
        obj (obj (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k)
    (CategoryStruct.comp (Y := end_ (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
          (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
              (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)))
            (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
                ((homEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ V ⟶ enrichedHom V F₁ F₂) f)
                (precompEnrichedHom V F₁ F₂ (Under.forget j)) ⊗ₘ
              CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
                ((homEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₂ F₃) g)
                (precompEnrichedHom V F₂ F₃ (Under.forget j)))
            (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))))
        (end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
        obj (obj (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k)

Tactic:
rw [homEquiv_comp, assoc, assoc, assoc, assoc, assoc, end_.lift_π, enrichedComp_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Enriched.FunctorCategory.homEquiv_comp, CategoryTheory.Limits.end_.lift_π, CategoryTheory.Enriched.FunctorCategory.enrichedComp_π