no goals
C : Type u₁
inst✝³ : Category C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category D
inst✝ : MonoidalCategory D
F G : LaxMonoidalFunctor C D
app : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f
unit : F.ε ≫ (app (𝟙_ C)).hom = G.ε
tensor :
  ∀ (X Y : C), LaxMonoidalFunctor.μ F X Y ≫ (app (X ⊗ Y)).hom = ((app X).hom ⊗ (app Y).hom) ≫ LaxMonoidalFunctor.μ G X Y
X : C
⊢ (ofComponents app naturality unit tensor).inv.app X = (app X).inv
simp [ofComponents]