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 : C
⊢ (λ_ (F.obj X)).inv ≫ (F.ε ⊗ 𝟙 (F.obj X)) ≫ μ F (𝟙_ C) X = F.map (λ_ X).inv
rw [Iso.inv_comp_eq, F.left_unitality, Category.assoc, Category.assoc, ← F.toFunctor.map_comp,
  Iso.hom_inv_id, F.toFunctor.map_id, comp_id]