C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
⊢ F.map (λ_ X).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X) ≫
      (inv F.ε ⊗ 𝟙 (F.obj X)) ≫
        (F.ε ⊗ 𝟙 (F.obj X)) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X ≫ F.map (λ_ X).hom
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
⊢ F.map (λ_ X).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X) ≫ (inv F.ε ⊗ 𝟙 (F.obj X)) ≫ (λ_ (F.obj X)).hom
simp only [LaxMonoidalFunctor.left_unitality]
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
⊢ F.map (λ_ X).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X) ≫
      (𝟙 (F.obj (𝟙_ C) ⊗ F.obj X) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X) ≫ F.map (λ_ X).hom
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
⊢ F.map (λ_ X).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X) ≫
      (inv F.ε ⊗ 𝟙 (F.obj X)) ≫
        (F.ε ⊗ 𝟙 (F.obj X)) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X ≫ F.map (λ_ X).hom
slice_rhs 2 3 =>
  rw [← comp_tensor_id]
  simp
no goals
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category D
inst✝ : MonoidalCategory D
F : MonoidalFunctor C D
X : C
⊢ F.map (λ_ X).hom =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X) ≫
      (𝟙 (F.obj (𝟙_ C) ⊗ F.obj X) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ C) X) ≫ F.map (λ_ X).hom
simp