C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n m' : M
f : m ⟶ m'
X : C
⊢ (F.obj n).map ((F.map f).app X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n).app X =
    (F.map (𝟙 n)).app ((F.obj m).obj X) ≫
      (F.obj n).map ((F.map f).app X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n).app X
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n m' : M
f : m ⟶ m'
X : C
⊢ (F.obj n).map ((F.map f).app X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n).app X =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app X ≫ (F.map (f ⊗ 𝟙 n)).app X
rw [← μ_naturality₂ F f (𝟙 n) X]
no goals
C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n m' : M
f : m ⟶ m'
X : C
⊢ (F.obj n).map ((F.map f).app X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n).app X =
    (F.map (𝟙 n)).app ((F.obj m).obj X) ≫
      (F.obj n).map ((F.map f).app X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n).app X
simp