no goals
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category D
inst✝ : MonoidalCategory D
F : LaxMonoidalFunctor C D
X Y Z : C
⊢ (𝟙 (F.obj X) ⊗ μ F Y Z) ≫ μ F X (Y ⊗ Z) ≫ F.map (α_ X Y Z).inv =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).inv ≫ (μ F X Y ⊗ 𝟙 (F.obj Z)) ≫ μ F (X ⊗ Y) Z
rw [Iso.eq_inv_comp, ← F.associativity_assoc, ← F.toFunctor.map_comp, Iso.hom_inv_id,
  F.toFunctor.map_id, comp_id]