C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ F.ε.app ((F.obj n).obj X) =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X)) ≫ (F.map (ρ_ n).inv).app X ≫ (MonoidalFunctor.μIso F n (𝟙_ M)).inv.app X
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ F.ε.app ((F.obj n).obj X) = (F.map (ρ_ n).inv).app X ≫ (MonoidalFunctor.μIso F n (𝟙_ M)).inv.app X
refine' Eq.trans _ (Category.id_comp _)
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ F.ε.app ((F.obj n).obj X) ≫ inv ((MonoidalFunctor.μIso F n (𝟙_ M)).inv.app X) ≫ inv ((F.map (ρ_ n).inv).app X) =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X))
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ F.ε.app ((F.obj n).obj X) =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X)) ≫ (F.map (ρ_ n).inv).app X ≫ (MonoidalFunctor.μIso F n (𝟙_ M)).inv.app X
rw [← Category.assoc, ← IsIso.comp_inv_eq, ← IsIso.comp_inv_eq, Category.assoc]
case h.e'_2.h
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
e_1✝ :
  ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X) ⟶ (𝟙_ (C ⥤ C)).obj ((F.obj n).obj X)) =
    ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X) ⟶ (F.obj n).obj X)
⊢ F.ε.app ((F.obj n).obj X) ≫ inv ((MonoidalFunctor.μIso F n (𝟙_ M)).inv.app X) ≫ inv ((F.map (ρ_ n).inv).app X) =
    F.ε.app ((F.obj n).obj X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ F.ε.app ((F.obj n).obj X) ≫ inv ((MonoidalFunctor.μIso F n (𝟙_ M)).inv.app X) ≫ inv ((F.map (ρ_ n).inv).app X) =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X))
convert right_unitality_app F n X using 1
no goals
case h.e'_2.h
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
e_1✝ :
  ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X) ⟶ (𝟙_ (C ⥤ C)).obj ((F.obj n).obj X)) =
    ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X) ⟶ (F.obj n).obj X)
⊢ F.ε.app ((F.obj n).obj X) ≫ inv ((MonoidalFunctor.μIso F n (𝟙_ M)).inv.app X) ≫ inv ((F.map (ρ_ n).inv).app X) =
    F.ε.app ((F.obj n).obj X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X
simp