-- 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 : 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₃
i j : J
f : i ⟶ j
trans :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj j))
    (((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i)) ≫
      eHomWhiskerLeft V (F₁.obj i) (F₃.map f))
    ((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      Iso.inv (ρ_ (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op i)) i)) ▷
          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 i)) i ◁
              (eHomEquiv V : (a : F₂.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₂.obj i ⟶[V] F₂.obj j) (F₂.map f)) ▷
            obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₂ F₃) (Opposite.op j)) j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj i) (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 i))) (F₂.obj j) (F₃.obj j))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj j))
    (((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i)) ≫
      eHomWhiskerLeft V (F₁.obj i) (F₃.map f))
    (((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫
      eHomWhiskerRight V (F₁.map f) (F₃.obj j))
have trans₁ : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
      (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃) ⟶
    @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj j))
  ((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
    Iso.inv (ρ_ (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op i)) i)) ▷
        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 i)) i ◁
            (eHomEquiv V : (a : F₂.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₂.obj i ⟶[V] F₂.obj j) (F₂.map f)) ▷
          obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₂ F₃) (Opposite.op j)) j ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj i) (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 i))) (F₂.obj j) (F₃.obj j))
  (((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫
    eHomWhiskerRight V (F₁.map f) (F₃.obj j))
Tactic: trans (end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      (ρ_ _).inv ▷ _ ≫ (_ ◁ (eHomEquiv V (F₂.map f))) ▷ _ ≫ eComp V _ (F₂.obj i) _ ▷ _ ≫
        eComp V _ (F₂.obj j) _