-- 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 X' : C
f : X ⟶ X'
Y Z : C
rw :
  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) (tensorUnit.{v', u'} V (𝒞 := inst))
          (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)))
        (Iso.inv
          (λ_
            (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)
              (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))))
        ((eHomEquiv V : (a : X ⟶ X') → 𝟙_ V ⟶ X ⟶[V] X') f ▷
            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 X' ◁ eComp V X' Y Z ≫ eComp V X X' 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))
    (CategoryStruct.comp (Y :=
            tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
              (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y))
            (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)))
            ((eHomEquiv V : (a : X ⟶ X') → 𝟙_ V ⟶ X ⟶[V] X') f ▷
                @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y ≫
              eComp V X X' 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))
⊢ 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))
    (eComp V X' Y Z ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Z))
        (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Z)))
        ((eHomEquiv V : (a : X ⟶ X') → 𝟙_ V ⟶ X ⟶[V] X') f ▷ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Z ≫
          eComp V X X' Z))
    (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y))
          (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)))
          ((eHomEquiv V : (a : X ⟶ X') → 𝟙_ V ⟶ X ⟶[V] X') f ▷
              @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y ≫
            eComp V X X' Y) ▷
        @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
      eComp V X Y Z)

Tactic:
rw [leftUnitor_inv_naturality_assoc, whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality_assoc