-- 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
W_1 : Type u''
inst_4 : Category.{v'', u''} W_1
inst_5 : MonoidalCategory.{v'', u''} W_1
F_1 : Functor.{v', v'', u', u''} V W_1
inst_6 : F_1.LaxMonoidal
W : Type u''
inst_7 : Category.{v'', u''} W
inst_8 : MonoidalCategory.{v'', u''} W
F : Functor.{v', v'', u', u''} V W
inst_9 : F.LaxMonoidal
D : Type u
inst_10 : EnrichedCategory.{v', u', u} V D
e :
  (v : V) →
    Equiv.{v' + 1, v'' + 1} (tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v) (tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
h :
  ∀ (v : V) (f : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v),
    Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      ((e v : (a : 𝟙_ V ⟶ v) → 𝟙_ W ⟶ F.obj v) f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
      (Functor.LaxMonoidal.ε F ≫ F.map f : tensorUnit.{v'', u''} W (𝒞 := inst_7) ⟶ F.obj v)
X Y Z : ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)
f : X ⟶ Y
g : Y ⟶ Z
e_f :
  Iso.inv (λ_ (tensorUnit.{v'', u''} W (𝒞 := inst_7))) ≫
      (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g) ≫
        Functor.LaxMonoidal.μ F (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y))
            (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
          F.map (eComp V (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) =
    CategoryStruct.comp (Y :=
      F.obj
        (tensorObj.{v', u'} (𝒞 := inst)
          (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y))
          (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z))))
      (CategoryStruct.comp (Y :=
        tensorObj.{v'', u''} (𝒞 := inst_7) (tensorUnit.{v'', u''} W (𝒞 := inst_7))
          (tensorUnit.{v'', u''} W (𝒞 := inst_7)))
        (Iso.inv (λ_ (tensorUnit.{v'', u''} W (𝒞 := inst_7))))
        ((CategoryStruct.comp (Y := F.obj (tensorUnit.{v', u'} V (𝒞 := inst))) (Functor.LaxMonoidal.ε F)
              (F.map
                ((Equiv.symm
                      (e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y))) :
                    (a : 𝟙_ W ⟶ F.obj (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W Y)) →
                      𝟙_ V ⟶ ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W Y)
                  (ForgetEnrichment.homTo W f))) ⊗ₘ
            CategoryStruct.comp (Y := F.obj (tensorUnit.{v', u'} V (𝒞 := inst))) (Functor.LaxMonoidal.ε F)
              (F.map
                ((Equiv.symm
                      (e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z))) :
                    (a : 𝟙_ W ⟶ F.obj (ForgetEnrichment.to W Y ⟶[V] ForgetEnrichment.to W Z)) →
                      𝟙_ V ⟶ ForgetEnrichment.to W Y ⟶[V] ForgetEnrichment.to W Z)
                  (ForgetEnrichment.homTo W g)))) ≫
          Functor.LaxMonoidal.μ F
            (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y))
            (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z))))
      (F.map (eComp V (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)))
⊢ Iso.inv (λ_ (tensorUnit.{v'', u''} W (𝒞 := inst_7))) ≫
      (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g) ≫
        Functor.LaxMonoidal.μ F (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y))
            (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
          F.map (eComp V (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) =
    Functor.LaxMonoidal.ε F ≫
      CategoryStruct.comp (Y :=
        F.obj (tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst)) (tensorUnit.{v', u'} V (𝒞 := inst))))
        (F.map (Iso.inv (λ_ (tensorUnit.{v', u'} V (𝒞 := inst)))))
        (CategoryStruct.comp (Y :=
          F.obj
            (tensorObj.{v', u'} (𝒞 := inst)
              (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y))
              (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z))))
          (F.map
            ((Equiv.symm (e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y))) :
                  (a : 𝟙_ W ⟶ F.obj (ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W Y)) →
                    𝟙_ V ⟶ ForgetEnrichment.to W X ⟶[V] ForgetEnrichment.to W Y)
                (ForgetEnrichment.homTo W f) ⊗ₘ
              (Equiv.symm (e (@Hom.{v', u', u} _ inst inst_1 _ _ (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z))) :
                  (a : 𝟙_ W ⟶ F.obj (ForgetEnrichment.to W Y ⟶[V] ForgetEnrichment.to W Z)) →
                    𝟙_ V ⟶ ForgetEnrichment.to W Y ⟶[V] ForgetEnrichment.to W Z)
                (ForgetEnrichment.homTo W g)))
          (F.map (eComp V (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z))))

Tactic:
slice_rhs 1 3 =>
      rw [← Functor.LaxMonoidal.left_unitality_inv, Category.assoc, Category.assoc,
        ← Functor.LaxMonoidal.μ_natural, ← leftUnitor_inv_comp_tensorHom_assoc,
        tensorHom_comp_tensorHom_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.leftUnitor_inv_comp_tensorHom_assoc, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc, CategoryTheory.Functor.LaxMonoidal.μ_natural, CategoryTheory.Functor.LaxMonoidal.left_unitality_inv