-- 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)
    ((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))
have h : Eq.{v₁ + 1} (α :=
  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))
  ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) 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) ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj j))
Tactic: conv_rhs =>
    rw [assoc, enrichedComp_π, tensorHom_def'_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
      enrichedComp_π, MonoidalCategory.whiskerLeft_comp_assoc, whisker_exchange_assoc,
      whisker_exchange_assoc, ← tensorHom_def_assoc]