-- 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₂
g : tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
i j : J
f : i ⟶ j
conv_lhs :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₁.obj j))
          (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
        ((eHomEquiv V : (a : F₁.obj i ⟶ F₁.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₁.obj j) (F₁.map f) ⊗ₘ
          g ≫ end_.π (diagram V F₁ F₂) j)
        (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    (Iso.hom (ρ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
        g ≫
          enrichedHomπ V F₁ F₂ j ≫
            CategoryStruct.comp (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst))
                (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
              (Iso.inv (λ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))))
              (CategoryStruct.comp (Y :=
                tensorObj.{v₁, u₁} (𝒞 := inst)
                  (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₁.obj j))
                  (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
                ((eHomEquiv V : (a : F₁.obj i ⟶ F₁.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₁.obj j) (F₁.map f) ▷
                  @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
                (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j))) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
conv_lhs₁ :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    (Iso.hom (ρ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
      g ≫
        end_.π (diagram V F₁ F₂) j ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst))
              (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
            (Iso.inv (λ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))))
            (CategoryStruct.comp (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst)
                (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₁.obj j))
                (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
              ((eHomEquiv V : (a : F₁.obj i ⟶ F₁.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₁.obj j) (F₁.map f) ▷
                @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
              (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j))))
    (Iso.hom (ρ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
      g ≫
        enrichedHomπ V F₁ F₂ j ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst))
              (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
            (Iso.inv (λ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))))
            (CategoryStruct.comp (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst)
                (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₁.obj j))
                (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
              ((eHomEquiv V : (a : F₁.obj i ⟶ F₁.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₁.obj j) (F₁.map f) ▷
                @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
              (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j))))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₁.obj j))
          (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
        ((eHomEquiv V : (a : F₁.obj i ⟶ F₁.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₁.obj j) (F₁.map f) ⊗ₘ
          g ≫ end_.π (diagram V F₁ F₂) j)
        (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    (Iso.hom (ρ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
        g ≫
          enrichedHomπ V F₁ F₂ j ≫
            CategoryStruct.comp (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst))
                (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
              (Iso.inv (λ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))))
              (CategoryStruct.comp (Y :=
                tensorObj.{v₁, u₁} (𝒞 := inst)
                  (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₁.obj j))
                  (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
                ((eHomEquiv V : (a : F₁.obj i ⟶ F₁.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₁.obj j) (F₁.map f) ▷
                  @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
                (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j))) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))

Tactic:
conv_lhs =>
          rw [tensorHom_def'_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
            id_whiskerLeft_assoc, id_whiskerLeft_assoc, Iso.inv_hom_id_assoc, unitors_equal]

Premises used: CategoryTheory.MonoidalCategory.unitors_equal, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.id_whiskerLeft_assoc, CategoryTheory.MonoidalCategory.tensorHom_def'_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc