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

Tactic:
rw [rightUnitor_inv_naturality_assoc, ← whisker_exchange_assoc]

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