-- 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 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₄
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
j : J
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄)) ⟶
      obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₄) (Opposite.op j)) j)
    (CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₄))
      (Iso.inv
          (α_ (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
            (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄)) ≫
        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₄))
          (enrichedComp V F₁ F₂ F₃ ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄) (enrichedComp V F₁ F₃ F₄))
      (end_.π (diagram V F₁ F₄) j))
    (CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₄))
      (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₄))
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄) (enrichedComp V F₁ F₂ F₄))
      (end_.π (diagram V F₁ F₄) j))
have h : Eq (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
      (tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄)) ⟶
    obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₄) (Opposite.op j)) j)
  ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
    Iso.inv
        (α_ (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j)
          (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₂ F₃) (Opposite.op j)) j)
          (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₃ F₄) (Opposite.op j)) j)) ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) ▷
          obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₃ F₄) (Opposite.op j)) j ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₃.obj j) (F₄.obj j))
  (CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₄))
    (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₄))
      (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄) (enrichedComp V F₁ F₂ F₄))
    (end_.π (diagram V F₁ F₄) j))
Tactic: conv_lhs =>
    rw [assoc, assoc, enrichedComp_π,
      tensorHom_def_assoc, ← comp_whiskerRight_assoc, enrichedComp_π,
      comp_whiskerRight_assoc, ← whisker_exchange_assoc,
      ← whisker_exchange_assoc, ← tensorHom_def'_assoc, ← associator_inv_naturality_assoc]