C : Type u
inst✝² : Category C
M : Type u_2
inst✝¹ : Category M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n n' : M
g : n ⟶ n'
X : C
⊢ (F.map g).app ((F.obj m).obj X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n').app X =
    (F.map g).app ((F.obj m).obj X) ≫
      (F.obj n').map ((F.map (𝟙 m)).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 n' : M
g : n ⟶ n'
X : C
⊢ (F.map g).app ((F.obj m).obj X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n').app X =
    (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app X ≫ (F.map (𝟙 m ⊗ g)).app X
rw [← μ_naturality₂ F (𝟙 m) g 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 n' : M
g : n ⟶ n'
X : C
⊢ (F.map g).app ((F.obj m).obj X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n').app X =
    (F.map g).app ((F.obj m).obj X) ≫
      (F.obj n').map ((F.map (𝟙 m)).app X) ≫ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n').app X
simp