[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F G : LaxMonoidalFunctor C D
H K : LaxMonoidalFunctor D E
α : MonoidalNatTrans F G
β : MonoidalNatTrans H K
src✝ : F.toFunctor ⋙ H.toFunctor ⟶ G.toFunctor ⋙ K.toFunctor := α.toNatTrans ◫ β.toNatTrans
⊢ (F ⊗⋙ H).ε ≫ NatTrans.app (NatTrans.mk src✝.app) (𝟙_ C) = (G ⊗⋙ K).ε
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F G : LaxMonoidalFunctor C D
H K : LaxMonoidalFunctor D E
α : MonoidalNatTrans F G
β : MonoidalNatTrans H K
src✝ : F.toFunctor ⋙ H.toFunctor ⟶ G.toFunctor ⋙ K.toFunctor := α.toNatTrans ◫ β.toNatTrans
⊢ (H.ε ≫ H.map F.ε) ≫ NatTrans.app β.toNatTrans (F.obj (𝟙_ C)) ≫ K.map (NatTrans.app α.toNatTrans (𝟙_ C)) =
    K.ε ≫ K.map G.ε
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F G : LaxMonoidalFunctor C D
H K : LaxMonoidalFunctor D E
α : MonoidalNatTrans F G
β : MonoidalNatTrans H K
src✝ : F.toFunctor ⋙ H.toFunctor ⟶ G.toFunctor ⋙ K.toFunctor := α.toNatTrans ◫ β.toNatTrans
⊢ K.ε ≫ K.map F.ε ≫ K.map (NatTrans.app α.toNatTrans (𝟙_ C)) = K.ε ≫ K.map G.ε
[PROOFSTEP]
conv_lhs => rw [← K.toFunctor.map_comp, α.unit]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F G : LaxMonoidalFunctor C D
H K : LaxMonoidalFunctor D E
α : MonoidalNatTrans F G
β : MonoidalNatTrans H K
src✝ : F.toFunctor ⋙ H.toFunctor ⟶ G.toFunctor ⋙ K.toFunctor := α.toNatTrans ◫ β.toNatTrans
| K.ε ≫ K.map F.ε ≫ K.map (NatTrans.app α.toNatTrans (𝟙_ C))
[PROOFSTEP]
rw [← K.toFunctor.map_comp, α.unit]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F G : LaxMonoidalFunctor C D
H K : LaxMonoidalFunctor D E
α : MonoidalNatTrans F G
β : MonoidalNatTrans H K
src✝ : F.toFunctor ⋙ H.toFunctor ⟶ G.toFunctor ⋙ K.toFunctor := α.toNatTrans ◫ β.toNatTrans
| K.ε ≫ K.map F.ε ≫ K.map (NatTrans.app α.toNatTrans (𝟙_ C))
[PROOFSTEP]
rw [← K.toFunctor.map_comp, α.unit]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F G : LaxMonoidalFunctor C D
H K : LaxMonoidalFunctor D E
α : MonoidalNatTrans F G
β : MonoidalNatTrans H K
src✝ : F.toFunctor ⋙ H.toFunctor ⟶ G.toFunctor ⋙ K.toFunctor := α.toNatTrans ◫ β.toNatTrans
| K.ε ≫ K.map F.ε ≫ K.map (NatTrans.app α.toNatTrans (𝟙_ C))
[PROOFSTEP]
rw [← K.toFunctor.map_comp, α.unit]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F G : LaxMonoidalFunctor C D
H K : LaxMonoidalFunctor D E
α : MonoidalNatTrans F G
β : MonoidalNatTrans H K
src✝ : F.toFunctor ⋙ H.toFunctor ⟶ G.toFunctor ⋙ K.toFunctor := α.toNatTrans ◫ β.toNatTrans
X Y : C
⊢ LaxMonoidalFunctor.μ (F ⊗⋙ H) X Y ≫ NatTrans.app (NatTrans.mk src✝.app) (X ⊗ Y) =
    (NatTrans.app (NatTrans.mk src✝.app) X ⊗ NatTrans.app (NatTrans.mk src✝.app) Y) ≫ LaxMonoidalFunctor.μ (G ⊗⋙ K) X Y
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F G : LaxMonoidalFunctor C D
H K : LaxMonoidalFunctor D E
α : MonoidalNatTrans F G
β : MonoidalNatTrans H K
src✝ : F.toFunctor ⋙ H.toFunctor ⟶ G.toFunctor ⋙ K.toFunctor := α.toNatTrans ◫ β.toNatTrans
X Y : C
⊢ (LaxMonoidalFunctor.μ H (F.obj X) (F.obj Y) ≫ H.map (LaxMonoidalFunctor.μ F X Y)) ≫
      NatTrans.app β.toNatTrans (F.obj (X ⊗ Y)) ≫ K.map (NatTrans.app α.toNatTrans (X ⊗ Y)) =
    (NatTrans.app β.toNatTrans (F.obj X) ≫ K.map (NatTrans.app α.toNatTrans X) ⊗
        NatTrans.app β.toNatTrans (F.obj Y) ≫ K.map (NatTrans.app α.toNatTrans Y)) ≫
      LaxMonoidalFunctor.μ K (G.obj X) (G.obj Y) ≫ K.map (LaxMonoidalFunctor.μ G X Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F G : LaxMonoidalFunctor C D
H K : LaxMonoidalFunctor D E
α : MonoidalNatTrans F G
β : MonoidalNatTrans H K
src✝ : F.toFunctor ⋙ H.toFunctor ⟶ G.toFunctor ⋙ K.toFunctor := α.toNatTrans ◫ β.toNatTrans
X Y : C
⊢ (NatTrans.app β.toNatTrans (F.obj X) ⊗ NatTrans.app β.toNatTrans (F.obj Y)) ≫
      LaxMonoidalFunctor.μ K (F.obj X) (F.obj Y) ≫
        K.map (LaxMonoidalFunctor.μ F X Y) ≫ K.map (NatTrans.app α.toNatTrans (X ⊗ Y)) =
    (NatTrans.app β.toNatTrans (F.obj X) ⊗ NatTrans.app β.toNatTrans (F.obj Y)) ≫
      LaxMonoidalFunctor.μ K (F.obj X) (F.obj Y) ≫
        K.map (NatTrans.app α.toNatTrans X ⊗ NatTrans.app α.toNatTrans Y) ≫ K.map (LaxMonoidalFunctor.μ G X Y)
[PROOFSTEP]
conv_lhs => rw [← K.toFunctor.map_comp, α.tensor, K.toFunctor.map_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F G : LaxMonoidalFunctor C D
H K : LaxMonoidalFunctor D E
α : MonoidalNatTrans F G
β : MonoidalNatTrans H K
src✝ : F.toFunctor ⋙ H.toFunctor ⟶ G.toFunctor ⋙ K.toFunctor := α.toNatTrans ◫ β.toNatTrans
X Y : C
| (NatTrans.app β.toNatTrans (F.obj X) ⊗ NatTrans.app β.toNatTrans (F.obj Y)) ≫
    LaxMonoidalFunctor.μ K (F.obj X) (F.obj Y) ≫
      K.map (LaxMonoidalFunctor.μ F X Y) ≫ K.map (NatTrans.app α.toNatTrans (X ⊗ Y))
[PROOFSTEP]
rw [← K.toFunctor.map_comp, α.tensor, K.toFunctor.map_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F G : LaxMonoidalFunctor C D
H K : LaxMonoidalFunctor D E
α : MonoidalNatTrans F G
β : MonoidalNatTrans H K
src✝ : F.toFunctor ⋙ H.toFunctor ⟶ G.toFunctor ⋙ K.toFunctor := α.toNatTrans ◫ β.toNatTrans
X Y : C
| (NatTrans.app β.toNatTrans (F.obj X) ⊗ NatTrans.app β.toNatTrans (F.obj Y)) ≫
    LaxMonoidalFunctor.μ K (F.obj X) (F.obj Y) ≫
      K.map (LaxMonoidalFunctor.μ F X Y) ≫ K.map (NatTrans.app α.toNatTrans (X ⊗ Y))
[PROOFSTEP]
rw [← K.toFunctor.map_comp, α.tensor, K.toFunctor.map_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : MonoidalCategory E
F G : LaxMonoidalFunctor C D
H K : LaxMonoidalFunctor D E
α : MonoidalNatTrans F G
β : MonoidalNatTrans H K
src✝ : F.toFunctor ⋙ H.toFunctor ⟶ G.toFunctor ⋙ K.toFunctor := α.toNatTrans ◫ β.toNatTrans
X Y : C
| (NatTrans.app β.toNatTrans (F.obj X) ⊗ NatTrans.app β.toNatTrans (F.obj Y)) ≫
    LaxMonoidalFunctor.μ K (F.obj X) (F.obj Y) ≫
      K.map (LaxMonoidalFunctor.μ F X Y) ≫ K.map (NatTrans.app α.toNatTrans (X ⊗ Y))
[PROOFSTEP]
rw [← K.toFunctor.map_comp, α.tensor, K.toFunctor.map_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
src✝ : G.toFunctor ⟶ F.toFunctor := (NatIso.ofComponents app).inv
⊢ G.ε ≫ NatTrans.app (NatTrans.mk fun X => (app X).inv) (𝟙_ C) = F.ε
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
src✝ : G.toFunctor ⟶ F.toFunctor := (NatIso.ofComponents app).inv
⊢ G.ε ≫ (app (𝟙_ C)).inv = F.ε
[PROOFSTEP]
rw [← unit', assoc, Iso.hom_inv_id, comp_id]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
src✝ : G.toFunctor ⟶ F.toFunctor := (NatIso.ofComponents app).inv
X Y : C
⊢ LaxMonoidalFunctor.μ G X Y ≫ NatTrans.app (NatTrans.mk fun X => (app X).inv) (X ⊗ Y) =
    (NatTrans.app (NatTrans.mk fun X => (app X).inv) X ⊗ NatTrans.app (NatTrans.mk fun X => (app X).inv) Y) ≫
      LaxMonoidalFunctor.μ F X Y
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
src✝ : G.toFunctor ⟶ F.toFunctor := (NatIso.ofComponents app).inv
X Y : C
⊢ LaxMonoidalFunctor.μ G X Y ≫ (app (X ⊗ Y)).inv = ((app X).inv ⊗ (app Y).inv) ≫ LaxMonoidalFunctor.μ F X Y
[PROOFSTEP]
rw [Iso.comp_inv_eq, assoc, tensor', ← tensor_comp_assoc, Iso.inv_hom_id, Iso.inv_hom_id, tensor_id, id_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} 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
⊢ NatTrans.app (ofComponents app naturality unit tensor).inv.toNatTrans X = (app X).inv
[PROOFSTEP]
simp [ofComponents]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
⊢ LaxMonoidalFunctor.μ (LaxMonoidalFunctor.id C) X Y ≫ NatTrans.app (Equivalence.unit e) (X ⊗ Y) =
    (NatTrans.app (Equivalence.unit e) X ⊗ NatTrans.app (Equivalence.unit e) Y) ≫
      LaxMonoidalFunctor.μ (F.toLaxMonoidalFunctor ⊗⋙ (monoidalInverse F).toLaxMonoidalFunctor) X Y
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
⊢ 𝟙 (X ⊗ Y) ≫ NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    (NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
        NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y) ≫
      ↑(Adjunction.homEquiv (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1))
              ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj X) ⊗
                (Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj Y))
              (F.obj X ⊗ F.obj Y))
          (inv
              (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj X))
                ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj Y))) ≫
            (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit (F.obj X) ⊗
              NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit (F.obj Y))) ≫
        (Functor.inv F.toLaxMonoidalFunctor.1).map (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y)
[PROOFSTEP]
simp only [Adjunction.homEquiv_unit, Adjunction.homEquiv_naturality_right, id_comp, assoc]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
⊢ NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    (NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
        NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y) ≫
      NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit
          ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj X) ⊗
            (Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj Y)) ≫
        (Functor.inv F.toLaxMonoidalFunctor.1).map
            (inv
                (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj X))
                  ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj Y))) ≫
              (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit (F.obj X) ⊗
                NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit (F.obj Y))) ≫
          (Functor.inv F.toLaxMonoidalFunctor.1).map (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y)
[PROOFSTEP]
simp only [← Functor.map_comp, assoc]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
⊢ NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    (NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
        NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y) ≫
      NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit
          ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj X) ⊗
            (Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj Y)) ≫
        (Functor.inv F.toLaxMonoidalFunctor.1).map
          (inv
              (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj X))
                ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj Y))) ≫
            (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit (F.obj X) ⊗
                NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit (F.obj Y)) ≫
              LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y)
[PROOFSTEP]
erw [e.counit_app_functor, e.counit_app_functor, F.toLaxMonoidalFunctor.μ_natural, IsIso.inv_hom_id_assoc]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
⊢ NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    (NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
        NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y) ≫
      NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit
          ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj X) ⊗
            (Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj Y)) ≫
        (Functor.inv F.toLaxMonoidalFunctor.1).map
          (F.map (NatTrans.app (Equivalence.unitInv e) X ⊗ NatTrans.app (Equivalence.unitInv e) Y))
[PROOFSTEP]
simp only [CategoryTheory.IsEquivalence.inv_fun_map]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
⊢ NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    (NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
        NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y) ≫
      NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit
          ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj X) ⊗
            (Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj Y)) ≫
        NatTrans.app (Equivalence.unitInv (asEquivalence F.toLaxMonoidalFunctor.1))
            (((asEquivalence F.toFunctor).functor ⋙ (asEquivalence F.toFunctor).inverse).obj X ⊗
              ((asEquivalence F.toFunctor).functor ⋙ (asEquivalence F.toFunctor).inverse).obj Y) ≫
          (NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) X ⊗
              NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) Y) ≫
            NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) ((𝟭 C).obj X ⊗ (𝟭 C).obj Y)
[PROOFSTEP]
slice_rhs 2 3 => erw [Iso.hom_inv_id_app]
[GOAL]
case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit
      ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj X) ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj Y)) ≫
    NatTrans.app (Equivalence.unitInv (asEquivalence F.toLaxMonoidalFunctor.1))
      (((asEquivalence F.toFunctor).functor ⋙ (asEquivalence F.toFunctor).inverse).obj X ⊗
        ((asEquivalence F.toFunctor).functor ⋙ (asEquivalence F.toFunctor).inverse).obj Y)
case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) X ⊗
    NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) Y
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) ((𝟭 C).obj X ⊗ (𝟭 C).obj Y)
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
    NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y
[PROOFSTEP]
erw [Iso.hom_inv_id_app]
[GOAL]
case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit
      ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj X) ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj Y)) ≫
    NatTrans.app (Equivalence.unitInv (asEquivalence F.toLaxMonoidalFunctor.1))
      (((asEquivalence F.toFunctor).functor ⋙ (asEquivalence F.toFunctor).inverse).obj X ⊗
        ((asEquivalence F.toFunctor).functor ⋙ (asEquivalence F.toFunctor).inverse).obj Y)
case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) X ⊗
    NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) Y
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) ((𝟭 C).obj X ⊗ (𝟭 C).obj Y)
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
    NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y
[PROOFSTEP]
erw [Iso.hom_inv_id_app]
[GOAL]
case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit
      ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj X) ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj Y)) ≫
    NatTrans.app (Equivalence.unitInv (asEquivalence F.toLaxMonoidalFunctor.1))
      (((asEquivalence F.toFunctor).functor ⋙ (asEquivalence F.toFunctor).inverse).obj X ⊗
        ((asEquivalence F.toFunctor).functor ⋙ (asEquivalence F.toFunctor).inverse).obj Y)
case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) X ⊗
    NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) Y
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) ((𝟭 C).obj X ⊗ (𝟭 C).obj Y)
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
    NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y
[PROOFSTEP]
erw [Iso.hom_inv_id_app]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
⊢ NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    (NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
        NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y) ≫
      (𝟙
            ((𝟭 C).obj
              ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj X) ⊗
                (Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj Y))) ≫
          (NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) X ⊗
            NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) Y)) ≫
        NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) ((𝟭 C).obj X ⊗ (𝟭 C).obj Y)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
⊢ NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    (NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
        NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y) ≫
      (𝟙 ((Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj X) ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj (F.obj Y)) ≫
          (NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) X ⊗
            NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) Y)) ≫
        NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) (X ⊗ Y)
[PROOFSTEP]
simp only [CategoryTheory.Category.id_comp]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
⊢ NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    (NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
        NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y) ≫
      (NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) X ⊗
          NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) Y) ≫
        NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) (X ⊗ Y)
[PROOFSTEP]
slice_rhs 1 2 =>
  rw [← tensor_comp, Iso.hom_inv_id_app, Iso.hom_inv_id_app]
  dsimp
  rw [tensor_id]
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| (NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y) ≫
    (NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) Y)
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) (X ⊗ Y)
[PROOFSTEP]
  rw [← tensor_comp, Iso.hom_inv_id_app, Iso.hom_inv_id_app]
  dsimp
  rw [tensor_id]
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| (NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y) ≫
    (NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) Y)
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) (X ⊗ Y)
[PROOFSTEP]
  rw [← tensor_comp, Iso.hom_inv_id_app, Iso.hom_inv_id_app]
  dsimp
  rw [tensor_id]
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| (NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) Y) ≫
    (NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor)) Y)
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) (X ⊗ Y)
[PROOFSTEP]
rw [← tensor_comp, Iso.hom_inv_id_app, Iso.hom_inv_id_app]
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| 𝟙 ((𝟭 C).obj X) ⊗ 𝟙 ((𝟭 C).obj Y)
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) (X ⊗ Y)
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| 𝟙 X ⊗ 𝟙 Y
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
| NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) (X ⊗ Y)
[PROOFSTEP]
rw [tensor_id]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : C
⊢ NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    𝟙 (X ⊗ Y) ≫ NatTrans.app (Equivalence.unit (asEquivalence F.toLaxMonoidalFunctor.1)) (X ⊗ Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
⊢ ∀ (X : C), IsIso (NatTrans.app (monoidalUnit F).toNatTrans X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
⊢ ∀ (X : C), IsIso (NatTrans.app (Equivalence.unit (asEquivalence F.toFunctor)) X)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
⊢ ((monoidalInverse F).toLaxMonoidalFunctor ⊗⋙ F.toLaxMonoidalFunctor).ε ≫ NatTrans.app (Equivalence.counit e) (𝟙_ D) =
    (LaxMonoidalFunctor.id D).ε
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
⊢ (F.ε ≫
        F.map
          (↑(Adjunction.homEquiv (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)) (𝟙_ C) (𝟙_ D))
            (inv F.ε))) ≫
      NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) (𝟙_ D) =
    𝟙 (𝟙_ D)
[PROOFSTEP]
simp only [comp_id, assoc, Functor.map_inv, Functor.map_comp, NatIso.inv_inv_app, IsIso.inv_comp,
  IsEquivalence.fun_inv_map, Adjunction.homEquiv_unit]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
⊢ F.ε ≫
      F.map (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit (𝟙_ C)) ≫
        NatTrans.app (asEquivalence F.toFunctor).counitIso.hom (F.obj (𝟙_ C)) ≫
          inv F.ε ≫
            inv (NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) (𝟙_ D)) ≫
              NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) (𝟙_ D) =
    𝟙 (𝟙_ D)
[PROOFSTEP]
erw [e.counit_app_functor, ← e.functor.map_comp_assoc, Iso.hom_inv_id_app]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
⊢ F.ε ≫
      e.functor.map (𝟙 ((𝟭 C).obj (𝟙_ C))) ≫
        inv F.ε ≫
          inv (NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) (𝟙_ D)) ≫
            NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) (𝟙_ D) =
    𝟙 (𝟙_ D)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
⊢ F.ε ≫
      F.map (𝟙 (𝟙_ C)) ≫
        inv F.ε ≫
          inv (NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) (𝟙_ D)) ≫
            NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) (𝟙_ D) =
    𝟙 (𝟙_ D)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : D
⊢ LaxMonoidalFunctor.μ ((monoidalInverse F).toLaxMonoidalFunctor ⊗⋙ F.toLaxMonoidalFunctor) X Y ≫
      NatTrans.app (Equivalence.counit e) (X ⊗ Y) =
    (NatTrans.app (Equivalence.counit e) X ⊗ NatTrans.app (Equivalence.counit e) Y) ≫
      LaxMonoidalFunctor.μ (LaxMonoidalFunctor.id D) X Y
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : D
⊢ (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
          ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y) ≫
        F.map
          (↑(Adjunction.homEquiv (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1))
                ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y) (X ⊗ Y))
            (inv
                (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
                  ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
              (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit X ⊗
                NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit Y)))) ≫
      NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    (NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) X ⊗
        NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) Y) ≫
      𝟙 (X ⊗ Y)
[PROOFSTEP]
simp only [Adjunction.homEquiv_unit, Adjunction.homEquiv_naturality_right, assoc, comp_id, Functor.map_comp]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : D
⊢ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
        ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y) ≫
      F.map
          (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit
            ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
        F.map
            ((Functor.inv F.toLaxMonoidalFunctor.1).map
              (inv
                (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
                  ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)))) ≫
          F.map
              ((Functor.inv F.toLaxMonoidalFunctor.1).map
                (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit X ⊗
                  NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit Y)) ≫
            NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) Y
[PROOFSTEP]
simp only [IsEquivalence.fun_inv_map]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : D
⊢ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
        ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y) ≫
      F.map
          (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit
            ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
        (NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor))
              (F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
            inv
                (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
                  ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
              NatTrans.app (Equivalence.counitInv (asEquivalence F.toFunctor))
                (F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj X) ⊗
                  F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y))) ≫
          (NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor))
                (F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj X) ⊗
                  F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
              (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit X ⊗
                  NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit Y) ≫
                NatTrans.app (Equivalence.counitInv (asEquivalence F.toFunctor)) (X ⊗ Y)) ≫
            NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) Y
[PROOFSTEP]
erw [e.counit_app_functor]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : D
⊢ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
        ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y) ≫
      F.map
          (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit
            ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
        (e.functor.map
              (NatTrans.app (Equivalence.unitInv e)
                ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
            inv
                (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
                  ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
              NatTrans.app (Equivalence.counitInv (asEquivalence F.toFunctor))
                (F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj X) ⊗
                  F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y))) ≫
          (NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor))
                (F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj X) ⊗
                  F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
              (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit X ⊗
                  NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit Y) ≫
                NatTrans.app (Equivalence.counitInv (asEquivalence F.toFunctor)) (X ⊗ Y)) ≫
            NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) Y
[PROOFSTEP]
simp only [assoc]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : D
⊢ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
        ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y) ≫
      F.map
          (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit
            ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
        (asEquivalence F.toFunctor).functor.map
            (NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor))
              ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
          inv
              (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
                ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
            NatTrans.app (Equivalence.counitInv (asEquivalence F.toFunctor))
                (F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj X) ⊗
                  F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
              NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor))
                  (F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj X) ⊗
                    F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
                (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit X ⊗
                    NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit Y) ≫
                  NatTrans.app (Equivalence.counitInv (asEquivalence F.toFunctor)) (X ⊗ Y) ≫
                    NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) Y
[PROOFSTEP]
erw [← e.functor.map_comp_assoc]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : D
⊢ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
        ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y) ≫
      e.functor.map
          (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit
              ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y) ≫
            NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor))
              ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
        inv
            (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
              ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
          NatTrans.app (Equivalence.counitInv (asEquivalence F.toFunctor))
              (F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj X) ⊗
                F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
            NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor))
                (F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj X) ⊗
                  F.obj ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
              (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit X ⊗
                  NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit Y) ≫
                NatTrans.app (Equivalence.counitInv (asEquivalence F.toFunctor)) (X ⊗ Y) ≫
                  NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) (X ⊗ Y) =
    NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) Y
[PROOFSTEP]
simp only [CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.inv_hom_id_app_assoc]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : D
⊢ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
        ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y) ≫
      (asEquivalence F.toFunctor).functor.map
          (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).unit
              ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y) ≫
            NatTrans.app (Equivalence.unitInv (asEquivalence F.toFunctor))
              ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
        inv
            (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
              ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
          (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit X ⊗
              NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit Y) ≫
            𝟙 ((𝟭 D).obj (X ⊗ Y)) =
    NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) Y
[PROOFSTEP]
erw [Iso.hom_inv_id_app, CategoryTheory.Functor.map_id]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : D
⊢ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
        ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y) ≫
      𝟙
          ((asEquivalence F.toFunctor).functor.obj
            ((Functor.inv F.toLaxMonoidalFunctor.1).obj X ⊗ (Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
        inv
            (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor ((Functor.inv F.toLaxMonoidalFunctor.1).obj X)
              ((Functor.inv F.toLaxMonoidalFunctor.1).obj Y)) ≫
          (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit X ⊗
              NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit Y) ≫
            𝟙 ((𝟭 D).obj (X ⊗ Y)) =
    NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) Y
[PROOFSTEP]
simp only [id_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.IsIso.hom_inv_id_assoc]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : D
⊢ (NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit X ⊗
        NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit Y) ≫
      𝟙 ((𝟭 D).obj (X ⊗ Y)) =
    NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) Y
[PROOFSTEP]
erw [comp_id]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
e : C ≌ D := asEquivalence F.toFunctor
X Y : D
⊢ NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit X ⊗
      NatTrans.app (Equivalence.toAdjunction (asEquivalence F.toLaxMonoidalFunctor.1)).counit Y =
    NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) X ⊗
      NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) Y
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
⊢ ∀ (X : D), IsIso (NatTrans.app (monoidalCounit F).toNatTrans X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝ : IsEquivalence F.toFunctor
⊢ ∀ (X : D), IsIso (NatTrans.app (Equivalence.counit (asEquivalence F.toFunctor)) X)
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.129, u_1} C
inst✝⁴ : Category.{?u.133, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : Faithful F.toFunctor
X Y : C
eval : Y ⊗ X ⟶ 𝟙_ C
coeval : 𝟙_ C ⟶ X ⊗ Y
inst✝ : ExactPairing (F.obj X) (F.obj Y)
map_eval : F.map eval = inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X) ≫ ε_ (F.obj X) (F.obj Y) ≫ F.ε
map_coeval : F.map coeval = inv F.ε ≫ η_ (F.obj X) (F.obj Y) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y
⊢ F.map ((𝟙 Y ⊗ coeval) ≫ (α_ Y X Y).inv ≫ (eval ⊗ 𝟙 Y)) = F.map ((ρ_ Y).hom ≫ (λ_ Y).inv)
[PROOFSTEP]
simp [map_eval, map_coeval, MonoidalFunctor.map_tensor]
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.129, u_1} C
inst✝⁴ : Category.{?u.133, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : Faithful F.toFunctor
X Y : C
eval : Y ⊗ X ⟶ 𝟙_ C
coeval : 𝟙_ C ⟶ X ⊗ Y
inst✝ : ExactPairing (F.obj X) (F.obj Y)
map_eval : F.map eval = inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X) ≫ ε_ (F.obj X) (F.obj Y) ≫ F.ε
map_coeval : F.map coeval = inv F.ε ≫ η_ (F.obj X) (F.obj Y) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y
⊢ F.map ((coeval ⊗ 𝟙 X) ≫ (α_ X Y X).hom ≫ (𝟙 X ⊗ eval)) = F.map ((λ_ X).hom ≫ (ρ_ X).inv)
[PROOFSTEP]
simp [map_eval, map_coeval, MonoidalFunctor.map_tensor]
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{?u.23115, u_1} C
inst✝⁵ : Category.{?u.23119, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝² : Full F.toFunctor
inst✝¹ : Faithful F.toFunctor
X Y : C
inst✝ : ExactPairing (F.obj X) (F.obj Y)
⊢ F.map (F.preimage (inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X) ≫ ε_ (F.obj X) (F.obj Y) ≫ F.ε)) =
    inv (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X) ≫ ε_ (F.obj X) (F.obj Y) ≫ F.ε
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{?u.23115, u_1} C
inst✝⁵ : Category.{?u.23119, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : MonoidalFunctor C D
inst✝² : Full F.toFunctor
inst✝¹ : Faithful F.toFunctor
X Y : C
inst✝ : ExactPairing (F.obj X) (F.obj Y)
⊢ F.map (F.preimage (inv F.ε ≫ η_ (F.obj X) (F.obj Y) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y)) =
    inv F.ε ≫ η_ (F.obj X) (F.obj Y) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.27280, u_1} C
inst✝⁴ : Category.{?u.27284, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasLeftDual (F.obj X)
⊢ ExactPairing ((Functor.inv F.toFunctor).obj ᘁ(F.obj X)) X
[PROOFSTEP]
refine @exactPairingOfFullyFaithful _ _ _ _ _ _ F _ _ _ _ ?_
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.27280, u_1} C
inst✝⁴ : Category.{?u.27284, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasLeftDual (F.obj X)
⊢ ExactPairing (F.obj ((Functor.inv F.toFunctor).obj ᘁ(F.obj X))) (F.obj X)
[PROOFSTEP]
refine @exactPairingCongrLeft _ _ _ _ _ _ ?_ (F.toFunctor.asEquivalence.counitIso.app _)
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.27280, u_1} C
inst✝⁴ : Category.{?u.27284, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasLeftDual (F.obj X)
⊢ ExactPairing ((𝟭 D).obj ᘁ(F.obj X)) (F.obj X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.27280, u_1} C
inst✝⁴ : Category.{?u.27284, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasLeftDual (F.obj X)
⊢ ExactPairing (ᘁ(F.obj X)) (F.obj X)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.30444, u_1} C
inst✝⁴ : Category.{?u.30448, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasRightDual (F.obj X)
⊢ ExactPairing X ((Functor.inv F.toFunctor).obj (F.obj X)ᘁ)
[PROOFSTEP]
refine @exactPairingOfFullyFaithful _ _ _ _ _ _ F _ _ _ _ ?_
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.30444, u_1} C
inst✝⁴ : Category.{?u.30448, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasRightDual (F.obj X)
⊢ ExactPairing (F.obj X) (F.obj ((Functor.inv F.toFunctor).obj (F.obj X)ᘁ))
[PROOFSTEP]
refine @exactPairingCongrRight _ _ _ _ _ _ ?_ (F.toFunctor.asEquivalence.counitIso.app _)
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.30444, u_1} C
inst✝⁴ : Category.{?u.30448, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasRightDual (F.obj X)
⊢ ExactPairing (F.obj X) ((𝟭 D).obj (F.obj X)ᘁ)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{?u.30444, u_1} C
inst✝⁴ : Category.{?u.30448, u_2} D
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory D
F : MonoidalFunctor C D
inst✝¹ : IsEquivalence F.toFunctor
X : C
inst✝ : HasRightDual (F.obj X)
⊢ ExactPairing (F.obj X) (F.obj X)ᘁ
[PROOFSTEP]
infer_instance