[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
P : C → Prop
inst✝² : MonoidalPredicate P
P' : C → Prop
inst✝¹ : MonoidalPredicate P'
inst✝ : BraidedCategory C
X Y : FullSubcategory P
⊢ LaxMonoidalFunctor.μ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor X Y ≫
      (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.map
        ((fun X Y => Iso.mk (β_ X.obj Y.obj).hom (β_ X.obj Y.obj).inv) X Y).hom =
    (β_ ((fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.obj X)
          ((fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.obj Y)).hom ≫
      LaxMonoidalFunctor.μ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor Y X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
P : C → Prop
inst✝² : MonoidalPredicate P
P' : C → Prop
inst✝¹ : MonoidalPredicate P'
inst✝ : BraidedCategory C
X Y : FullSubcategory P
⊢ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.map (β_ X Y).hom =
    inv (LaxMonoidalFunctor.μ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor X Y) ≫
      (β_ ((fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.obj X)
            ((fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.obj Y)).hom ≫
        LaxMonoidalFunctor.μ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor Y X
[PROOFSTEP]
rw [IsIso.eq_inv_comp]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
P : C → Prop
inst✝² : MonoidalPredicate P
P' : C → Prop
inst✝¹ : MonoidalPredicate P'
inst✝ : BraidedCategory C
X Y : FullSubcategory P
⊢ LaxMonoidalFunctor.μ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor X Y ≫
      (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.map (β_ X Y).hom =
    (β_ ((fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.obj X)
          ((fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor.obj Y)).hom ≫
      LaxMonoidalFunctor.μ (fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor Y X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
P : C → Prop
inst✝² : MonoidalPredicate P
P' : C → Prop
inst✝¹ : MonoidalPredicate P'
inst✝ : BraidedCategory C
h : ∀ ⦃X : C⦄, P X → P' X
X Y : FullSubcategory P
⊢ (fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor.map (β_ X Y).hom =
    inv (LaxMonoidalFunctor.μ (fullMonoidalSubcategory.map h).toLaxMonoidalFunctor X Y) ≫
      (β_ ((fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor.obj X)
            ((fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor.obj Y)).hom ≫
        LaxMonoidalFunctor.μ (fullMonoidalSubcategory.map h).toLaxMonoidalFunctor Y X
[PROOFSTEP]
rw [IsIso.eq_inv_comp]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
P : C → Prop
inst✝² : MonoidalPredicate P
P' : C → Prop
inst✝¹ : MonoidalPredicate P'
inst✝ : BraidedCategory C
h : ∀ ⦃X : C⦄, P X → P' X
X Y : FullSubcategory P
⊢ LaxMonoidalFunctor.μ (fullMonoidalSubcategory.map h).toLaxMonoidalFunctor X Y ≫
      (fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor.map (β_ X Y).hom =
    (β_ ((fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor.obj X)
          ((fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor.obj Y)).hom ≫
      LaxMonoidalFunctor.μ (fullMonoidalSubcategory.map h).toLaxMonoidalFunctor Y X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
P : C → Prop
inst✝³ : MonoidalPredicate P
P' : C → Prop
inst✝² : MonoidalPredicate P'
inst✝¹ : MonoidalClosed C
inst✝ : ClosedPredicate P
X : FullSubcategory P
⊢ CategoryTheory.whiskerRight (NatTrans.mk fun Y => NatTrans.app (ihom.coev X.obj) Y.obj) (tensorLeft X) ≫
      (Functor.associator (tensorLeft X)
            (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
              (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))
            (tensorLeft X)).hom ≫
        CategoryTheory.whiskerLeft (tensorLeft X) (NatTrans.mk fun Y => NatTrans.app (ihom.ev X.obj) Y.obj) =
    NatTrans.id (𝟭 (FullSubcategory P) ⋙ tensorLeft X)
[PROOFSTEP]
ext Y
[GOAL]
case w.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
P : C → Prop
inst✝³ : MonoidalPredicate P
P' : C → Prop
inst✝² : MonoidalPredicate P'
inst✝¹ : MonoidalClosed C
inst✝ : ClosedPredicate P
X Y : FullSubcategory P
⊢ NatTrans.app
      (CategoryTheory.whiskerRight (NatTrans.mk fun Y => NatTrans.app (ihom.coev X.obj) Y.obj) (tensorLeft X) ≫
        (Functor.associator (tensorLeft X)
              (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
                (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))
              (tensorLeft X)).hom ≫
          CategoryTheory.whiskerLeft (tensorLeft X) (NatTrans.mk fun Y => NatTrans.app (ihom.ev X.obj) Y.obj))
      Y =
    NatTrans.app (NatTrans.id (𝟭 (FullSubcategory P) ⋙ tensorLeft X)) Y
[PROOFSTEP]
simp
[GOAL]
case w.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
P : C → Prop
inst✝³ : MonoidalPredicate P
P' : C → Prop
inst✝² : MonoidalPredicate P'
inst✝¹ : MonoidalClosed C
inst✝ : ClosedPredicate P
X Y : FullSubcategory P
⊢ (𝟙 X ⊗ NatTrans.app (ihom.coev X.obj) Y.obj) ≫ NatTrans.app (ihom.ev X.obj) (X ⊗ Y).obj = 𝟙 (X ⊗ Y)
[PROOFSTEP]
exact ihom.ev_coev X.1 Y.1
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
P : C → Prop
inst✝³ : MonoidalPredicate P
P' : C → Prop
inst✝² : MonoidalPredicate P'
inst✝¹ : MonoidalClosed C
inst✝ : ClosedPredicate P
X : FullSubcategory P
⊢ CategoryTheory.whiskerLeft
        (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
          (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))
        (NatTrans.mk fun Y => NatTrans.app (ihom.coev X.obj) Y.obj) ≫
      (Functor.associator
            (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
              (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))
            (tensorLeft X)
            (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
              (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))).inv ≫
        CategoryTheory.whiskerRight (NatTrans.mk fun Y => NatTrans.app (ihom.ev X.obj) Y.obj)
          (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
            (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y)))) =
    NatTrans.id
      (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
          (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))) ⋙
        𝟭 (FullSubcategory P))
[PROOFSTEP]
ext Y
[GOAL]
case w.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
P : C → Prop
inst✝³ : MonoidalPredicate P
P' : C → Prop
inst✝² : MonoidalPredicate P'
inst✝¹ : MonoidalClosed C
inst✝ : ClosedPredicate P
X Y : FullSubcategory P
⊢ NatTrans.app
      (CategoryTheory.whiskerLeft
          (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
            (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))
          (NatTrans.mk fun Y => NatTrans.app (ihom.coev X.obj) Y.obj) ≫
        (Functor.associator
              (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
                (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))
              (tensorLeft X)
              (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
                (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))))).inv ≫
          CategoryTheory.whiskerRight (NatTrans.mk fun Y => NatTrans.app (ihom.ev X.obj) Y.obj)
            (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
              (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y)))))
      Y =
    NatTrans.app
      (NatTrans.id
        (FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
            (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj ((fullSubcategoryInclusion P).obj Y))) ⋙
          𝟭 (FullSubcategory P)))
      Y
[PROOFSTEP]
simp
[GOAL]
case w.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
P : C → Prop
inst✝³ : MonoidalPredicate P
P' : C → Prop
inst✝² : MonoidalPredicate P'
inst✝¹ : MonoidalClosed C
inst✝ : ClosedPredicate P
X Y : FullSubcategory P
⊢ NatTrans.app (ihom.coev X.obj) ((ihom X.obj).obj Y.obj) ≫ (ihom X.obj).map (NatTrans.app (ihom.ev X.obj) Y.obj) =
    𝟙
      ((FullSubcategory.lift P (fullSubcategoryInclusion P ⋙ ihom X.obj)
            (_ : ∀ (Y : FullSubcategory P), P ((ihom X.obj).obj Y.obj))).obj
        Y)
[PROOFSTEP]
exact ihom.coev_ev X.1 Y.1
