-- 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
w :
  ∀ (k : Under.{v₃, u₃} j),
    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)
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ 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 ≫ g))
        (precompEnrichedHom V F₁ F₃ (Under.forget j)) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom 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₃))) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))

Tactic:
ext k