-- 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
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
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₃
j j' : J
f : j ⟶ j'
k : Under.{v₃, u₃} j'
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
        (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj k.right) (F₃.obj k.right))
    (CategoryStruct.comp (Y := end_ (diagram 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₃)))
        (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
            (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂)) ⊗ₘ
          precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂))
            (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)))
        (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))
    (CategoryStruct.comp (Y := end_ (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)))
      (CategoryStruct.comp (Y := enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
        (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
        (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃))))
      (end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) k))
have h : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
      (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) ⟶
    @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj k.right) (F₃.obj k.right))
  (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₃)))
    (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂)) ⊗ₘ
      precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂))
        (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)))
    ((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)))
  (CategoryStruct.comp (Y := 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 := end_ (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)))
      (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)))
      (end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) k)))
Tactic: rw [assoc, assoc, enrichedComp_π]