-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
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₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_7 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
inst_8 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_9 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₄
j : J
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
          (enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))) ⟶
      enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₄))
    (Iso.inv
        (α_ (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
          (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
          (enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))) ≫
      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₄)))
        (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ▷
          enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))
        (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄)))
    (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₄)))
      (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ◁
        enrichedComp V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))
      (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₄)))
have w : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
      (tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
        (enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))) ⟶
    enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₄))
  (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₄)))
    (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ◁
      enrichedComp V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))
    (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₄)))
  (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₄)))
    (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ◁
      enrichedComp V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))
    (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₄)))
Tactic: rw [enriched_assoc]