-- 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 : TransportEnrichment F (ForgetEnrichment.{v', u', u} V D)
f : X ⟶ Y
g : Y ⟶ Z
rw :
  Eq (α :=
    Quiver.Hom (V := ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) (ForgetEnrichment.of W X)
      (ForgetEnrichment.of W Z))
    (ForgetEnrichment.homOf W
      (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))))
        ((Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f) ⊗ₘ
            Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g)) ≫
          eComp W (ForgetEnrichment.to V X) (ForgetEnrichment.to V Y) (ForgetEnrichment.to V Z))))
    (ForgetEnrichment.homOf W
      (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))))
        ((Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f) ⊗ₘ
            Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g)) ≫
          eComp W X Y Z)))
⊢ Eq.{v'' + 1} (α :=
    Quiver.Hom (V := ForgetEnrichment.{v'', u'', u} W (TransportEnrichment F D)) (ForgetEnrichment.of W X)
      (ForgetEnrichment.of W Z))
    (ForgetEnrichment.homOf W
      ((e (@Hom.{v', u', u} _ inst inst_1 _ _ X Z) : (a : 𝟙_ V ⟶ X ⟶[V] Z) → 𝟙_ W ⟶ F.obj (X ⟶[V] Z))
        (ForgetEnrichment.homTo V (f ≫ g))))
    (CategoryStruct.comp (Y := ForgetEnrichment.of W Y)
      (ForgetEnrichment.homOf W
        ((e (@Hom.{v', u', u} _ inst inst_1 _ _ X Y) : (a : 𝟙_ V ⟶ X ⟶[V] Y) → 𝟙_ W ⟶ F.obj (X ⟶[V] Y))
          (ForgetEnrichment.homTo V f)))
      (ForgetEnrichment.homOf W
        ((e (@Hom.{v', u', u} _ inst inst_1 _ _ Y Z) : (a : 𝟙_ V ⟶ Y ⟶[V] Z) → 𝟙_ W ⟶ F.obj (Y ⟶[V] Z))
          (ForgetEnrichment.homTo V g))))

Tactic:
rw [h, h, h, ForgetEnrichment.homTo_comp, F.map_comp, F.map_comp, ← Category.assoc,
      ← Functor.LaxMonoidal.left_unitality_inv, Category.assoc, Category.assoc, Category.assoc,
      Category.assoc, ← Functor.LaxMonoidal.μ_natural_assoc, ← TransportEnrichment.eComp_eq,
      ← ForgetEnrichment.homOf_comp, leftUnitor_inv_naturality_assoc, ← tensorHom_def'_assoc,
      tensorHom_comp_tensorHom_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc, CategoryTheory.ForgetEnrichment.homOf_comp, CategoryTheory.ForgetEnrichment.homTo_comp, CategoryTheory.MonoidalCategory.tensorHom_def'_assoc, CategoryTheory.TransportEnrichment.eComp_eq, CategoryTheory.Functor.map_comp, CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality_assoc, CategoryTheory.Functor.LaxMonoidal.μ_natural_assoc, CategoryTheory.Functor.LaxMonoidal.left_unitality_inv