-- 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₃ : 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
⊢ 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)
have 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))))
Tactic: rw [homEquiv_comp, assoc, assoc, assoc, assoc, assoc, end_.lift_π, enrichedComp_π]