-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
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₂
τ : F₁ ⟶ F₂
i j : J
f : i ⟶ j
trans :
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op i)) j)
    ((fun (j : J) ↦
          ((eHomEquiv V :
                (a : Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶ F₂.obj j) →
                  𝟙_ V ⟶ Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶[V] F₂.obj j)
              (τ.app j) :
            tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
              @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (Opposite.unop (F₁.op.obj (Opposite.op j)))
                (F₂.obj j)))
        i ≫
      map (obj (diagram V F₁ F₂) (Opposite.op i)) f)
    ((eHomEquiv V :
        (a : Opposite.unop (F₁.op.obj (Opposite.op i)) ⟶ F₂.obj j) →
          𝟙_ V ⟶ Opposite.unop (F₁.op.obj (Opposite.op i)) ⟶[V] F₂.obj j)
      (τ.app i ≫ F₂.map f))
trans₁ :
  Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj j))
    ((eHomEquiv V :
          (a : Opposite.unop (F₁.op.obj (Opposite.op i)) ⟶ F₂.obj j) →
            𝟙_ V ⟶ Opposite.unop (F₁.op.obj (Opposite.op i)) ⟶[V] F₂.obj j)
        (τ.app i ≫ F₂.map f) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj j))
    ((fun (j : J) ↦
            ((eHomEquiv V :
                  (a : Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶ F₂.obj j) →
                    𝟙_ V ⟶ Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶[V] F₂.obj j)
                (τ.app j) :
              tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
                @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (Opposite.unop (F₁.op.obj (Opposite.op j)))
                  (F₂.obj j)))
          j ≫
        NatTrans.app (map (diagram V F₁ F₂) f.op) j :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op i)) j)
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op i)) j)
    ((fun (j : J) ↦
          ((eHomEquiv V :
                (a : Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶ F₂.obj j) →
                  𝟙_ V ⟶ Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶[V] F₂.obj j)
              (τ.app j) :
            tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
              @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (Opposite.unop (F₁.op.obj (Opposite.op j)))
                (F₂.obj j)))
        i ≫
      map (obj (diagram V F₁ F₂) (Opposite.op i)) f)
    ((fun (j : J) ↦
          ((eHomEquiv V :
                (a : Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶ F₂.obj j) →
                  𝟙_ V ⟶ Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶[V] F₂.obj j)
              (τ.app j) :
            tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
              @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (Opposite.unop (F₁.op.obj (Opposite.op j)))
                (F₂.obj j)))
        j ≫
      NatTrans.app (map (diagram V F₁ F₂) f.op) j)

Tactic:
trans eHomEquiv V (τ.app i ≫ F₂.map f)

Premises used: CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, DFunLike.coe, CategoryTheory.NatTrans.app, CategoryTheory.eHomEquiv