C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m : M
X Y : C
f : X ⟶ (F.obj m).obj Y
⊢ (inv ((MonoidalFunctor.εIso F).inv.app X) ≫
        (F.obj (𝟙_ M)).map f ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m (𝟙_ M)).app Y) ≫
      inv ((F.map (ρ_ m).inv).app Y) =
    f
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m : M
X Y : C
f : X ⟶ (F.obj m).obj Y
⊢ (F.obj (𝟙_ M)).map f ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m (𝟙_ M)).app Y =
    (MonoidalFunctor.εIso F).inv.app X ≫ f ≫ (F.map (ρ_ m).inv).app Y
rw [← IsIso.inv_comp_eq, ← IsIso.comp_inv_eq]
no goals
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m : M
X Y : C
f : X ⟶ (F.obj m).obj Y
⊢ (inv ((MonoidalFunctor.εIso F).inv.app X) ≫
        (F.obj (𝟙_ M)).map f ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m (𝟙_ M)).app Y) ≫
      inv ((F.map (ρ_ m).inv).app Y) =
    f
simp