Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (λ_ (𝟙_ W)).inv ≫
      (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g) ≫
        Functor.LaxMonoidal.μ F (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)
            (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝) ≫
          F.map (eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)) =
    Functor.LaxMonoidal.ε F ≫
      F.map (λ_ (𝟙_ V)).inv ≫
        F.map
            ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f) ⊗ₘ
              (e (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (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]

Goal state after:
V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : ForgetEnrichment W (TransportEnrichment F D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (λ_ (𝟙_ W)).inv ≫
      (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g) ≫
        Functor.LaxMonoidal.μ F (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)
            (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝) ≫
          F.map (eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝)) =
    ((λ_ (𝟙_ W)).inv ≫
        (Functor.LaxMonoidal.ε F ≫
              F.map ((e (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)).symm (ForgetEnrichment.homTo W f)) ⊗ₘ
            Functor.LaxMonoidal.ε F ≫
              F.map ((e (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)).symm (ForgetEnrichment.homTo W g))) ≫
          Functor.LaxMonoidal.μ F (ForgetEnrichment.to W X✝ ⟶[V] ForgetEnrichment.to W Y✝)
            (ForgetEnrichment.to W Y✝ ⟶[V] ForgetEnrichment.to W Z✝)) ≫
      F.map (eComp V (ForgetEnrichment.to W X✝) (ForgetEnrichment.to W Y✝) (ForgetEnrichment.to W Z✝))