-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y Y₁ Z : C
α : Y ≅ Y₁
simp :
  Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (CategoryStruct.comp (Y :=
            tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
              (tensorUnit.{v', u'} V (𝒞 := inst)))
            (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)))
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y ◁
                (eHomEquiv V : (a : Y ⟶ Y₁) → 𝟙_ V ⟶ Y ⟶[V] Y₁) α.hom ≫
              eComp V X Y Y₁) ▷
          @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst)
            (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁)
              (tensorUnit.{v', u'} V (𝒞 := inst)))
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
          (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁)) ▷
            @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)
          ((@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁ ◁
                (eHomEquiv V : (a : Y₁ ⟶ Y) → 𝟙_ V ⟶ Y₁ ⟶[V] Y) α.inv) ▷
              @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
            eComp V X Y₁ Y ▷ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫ eComp V X Y Z)) :
      Quiver.Hom.{v', u'} (V := V)
        (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (eComp V X Y Z :
      Quiver.Hom.{v', u'} (V := V)
        (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (CategoryStruct.comp (Y :=
            tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
              (tensorUnit.{v', u'} V (𝒞 := inst)))
            (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)))
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y ◁
                (eHomEquiv V : (a : Y ⟶ Y₁) → 𝟙_ V ⟶ Y ⟶[V] Y₁) α.hom ≫
              eComp V X Y Y₁) ▷
          @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁ ◁
            CategoryStruct.comp (Y :=
              tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
                (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
              (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)))
              ((eHomEquiv V : (a : Y₁ ⟶ Y) → 𝟙_ V ⟶ Y₁ ⟶[V] Y) α.inv ▷
                  @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
                eComp V Y₁ Y Z) ≫
          eComp V X Y₁ Z) :
      Quiver.Hom.{v', u'} (V := V)
        (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (eComp V X Y Z :
      Quiver.Hom.{v', u'} (V := V)
        (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))

Tactic:
simp only [MonoidalCategory.whiskerLeft_comp_assoc, whisker_assoc_symm,
    triangle_assoc_comp_left_inv_assoc, e_assoc', assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.triangle_assoc_comp_left_inv_assoc, CategoryTheory.e_assoc', CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.MonoidalCategory.whisker_assoc_symm