-- 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 : Type u''
inst_4 : Category.{v'', u''} W
inst_5 : MonoidalCategory.{v'', u''} W
F : Functor.{v', v'', u', u''} V W
inst_6 : F.LaxMonoidal
e :
  (v : V) →
    Equiv.{v' + 1, v'' + 1} (tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v) (tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj v)
h :
  ∀ (v : V) (f : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ v),
    Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj v)
      ((e v : (a : 𝟙_ V ⟶ v) → 𝟙_ W ⟶ F.obj v) f : tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj v)
      (Functor.LaxMonoidal.ε F ≫ F.map f : tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj v)
X Y Z : TransportEnrichment F C
f : X ⟶ Y
g : Y ⟶ Z
dsimp :
  Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    ((e (@Hom.{v', u', u} _ inst inst_1 _ _ X Z) : (a : 𝟙_ V ⟶ X ⟶[V] Z) → 𝟙_ W ⟶ F.obj (X ⟶[V] Z))
        ((eHomEquiv V : (a : X ⟶ Z) → 𝟙_ V ⟶ X ⟶[V] Z) (f ≫ g)) :
      tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (CategoryStruct.comp (Y :=
        tensorObj.{v'', u''} (𝒞 := inst_4) (tensorUnit.{v'', u''} W (𝒞 := inst_4))
          (tensorUnit.{v'', u''} W (𝒞 := inst_4)))
        (Iso.inv (λ_ (tensorUnit.{v'', u''} W (𝒞 := inst_4))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v'', u''} (𝒞 := inst_4) (F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ X Y))
            (F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ Y Z)))
          ((e (@Hom.{v', u', u} _ inst inst_1 _ _ X Y) : (a : 𝟙_ V ⟶ X ⟶[V] Y) → 𝟙_ W ⟶ F.obj (X ⟶[V] Y))
              ((eHomEquiv V : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f) ⊗ₘ
            (e (@Hom.{v', u', u} _ inst inst_1 _ _ Y Z) : (a : 𝟙_ V ⟶ Y ⟶[V] Z) → 𝟙_ W ⟶ F.obj (Y ⟶[V] Z))
              ((eHomEquiv V : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g))
          (eComp W X Y Z)) :
      tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ F.obj (@Hom.{v', u', u} _ inst inst_1 _ _ X Z))
⊢ Eq.{v'' + 1} (α := tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ @Hom.{v'', u'', u} _ inst_4 inst_5 _ _ X Z)
    ((Equiv.trans (eHomEquiv V) (e (@Hom.{v', u', u} _ inst inst_1 _ _ X Z)) : (a : X ⟶ Z) → 𝟙_ W ⟶ X ⟶[W] Z) (f ≫ g) :
      tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ @Hom.{v'', u'', u} _ inst_4 inst_5 _ _ X Z)
    (CategoryStruct.comp (Y :=
        tensorObj.{v'', u''} (𝒞 := inst_4) (tensorUnit.{v'', u''} W (𝒞 := inst_4))
          (tensorUnit.{v'', u''} W (𝒞 := inst_4)))
        (Iso.inv (λ_ (tensorUnit.{v'', u''} W (𝒞 := inst_4))))
        (((Equiv.trans (eHomEquiv V) (e (@Hom.{v', u', u} _ inst inst_1 _ _ X Y)) : (a : X ⟶ Y) → 𝟙_ W ⟶ X ⟶[W] Y) f ⊗ₘ
            (Equiv.trans (eHomEquiv V) (e (@Hom.{v', u', u} _ inst inst_1 _ _ Y Z)) : (a : Y ⟶ Z) → 𝟙_ W ⟶ Y ⟶[W] Z)
              g) ≫
          eComp W X Y Z) :
      tensorUnit.{v'', u''} W (𝒞 := inst_4) ⟶ @Hom.{v'', u'', u} _ inst_4 inst_5 _ _ X Z)

Tactic:
dsimp +instances [instEnrichedCategoryTransportEnrichment]

Premises used: CategoryTheory.instEnrichedCategoryTransportEnrichment