[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ C ⥤ C := tensoringRight C
X✝ Y✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
⊢ ((Functor.mk src✝.toPrefunctor).map f ⊗ (Functor.mk src✝.toPrefunctor).map g) ≫
      (fun X Y => NatTrans.mk fun Z => (α_ Z X Y).hom) Y✝ Y'✝ =
    (fun X Y => NatTrans.mk fun Z => (α_ Z X Y).hom) X✝ X'✝ ≫ (Functor.mk src✝.toPrefunctor).map (f ⊗ g)
[PROOFSTEP]
ext Z
[GOAL]
case w.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ C ⥤ C := tensoringRight C
X✝ Y✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
Z : C
⊢ NatTrans.app
      (((Functor.mk src✝.toPrefunctor).map f ⊗ (Functor.mk src✝.toPrefunctor).map g) ≫
        (fun X Y => NatTrans.mk fun Z => (α_ Z X Y).hom) Y✝ Y'✝)
      Z =
    NatTrans.app ((fun X Y => NatTrans.mk fun Z => (α_ Z X Y).hom) X✝ X'✝ ≫ (Functor.mk src✝.toPrefunctor).map (f ⊗ g))
      Z
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ C ⥤ C := tensoringRight C
X✝ Y✝ X'✝ Y'✝ : C
f : X✝ ⟶ Y✝
g : X'✝ ⟶ Y'✝
Z : C
⊢ ((𝟙 (Z ⊗ X✝) ⊗ g) ≫ ((𝟙 Z ⊗ f) ⊗ 𝟙 Y'✝)) ≫ (α_ Z Y✝ Y'✝).hom = (α_ Z X✝ X'✝).hom ≫ (𝟙 Z ⊗ f ⊗ g)
[PROOFSTEP]
simp only [← id_tensor_comp_tensor_id g f, id_tensor_comp, ← tensor_id, Category.assoc, associator_naturality,
  associator_naturality_assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ C ⥤ C := tensoringRight C
X Y Z : C
⊢ ((fun X Y => NatTrans.mk fun Z => (α_ Z X Y).hom) X Y ⊗ 𝟙 ((Functor.mk src✝.toPrefunctor).obj Z)) ≫
      (fun X Y => NatTrans.mk fun Z => (α_ Z X Y).hom) (X ⊗ Y) Z ≫ (Functor.mk src✝.toPrefunctor).map (α_ X Y Z).hom =
    (α_ ((Functor.mk src✝.toPrefunctor).obj X) ((Functor.mk src✝.toPrefunctor).obj Y)
          ((Functor.mk src✝.toPrefunctor).obj Z)).hom ≫
      (𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ (fun X Y => NatTrans.mk fun Z => (α_ Z X Y).hom) Y Z) ≫
        (fun X Y => NatTrans.mk fun Z => (α_ Z X Y).hom) X (Y ⊗ Z)
[PROOFSTEP]
ext W
[GOAL]
case w.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ C ⥤ C := tensoringRight C
X Y Z W : C
⊢ NatTrans.app
      (((fun X Y => NatTrans.mk fun Z => (α_ Z X Y).hom) X Y ⊗ 𝟙 ((Functor.mk src✝.toPrefunctor).obj Z)) ≫
        (fun X Y => NatTrans.mk fun Z => (α_ Z X Y).hom) (X ⊗ Y) Z ≫ (Functor.mk src✝.toPrefunctor).map (α_ X Y Z).hom)
      W =
    NatTrans.app
      ((α_ ((Functor.mk src✝.toPrefunctor).obj X) ((Functor.mk src✝.toPrefunctor).obj Y)
            ((Functor.mk src✝.toPrefunctor).obj Z)).hom ≫
        (𝟙 ((Functor.mk src✝.toPrefunctor).obj X) ⊗ (fun X Y => NatTrans.mk fun Z => (α_ Z X Y).hom) Y Z) ≫
          (fun X Y => NatTrans.mk fun Z => (α_ Z X Y).hom) X (Y ⊗ Z))
      W
[PROOFSTEP]
simp [pentagon]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ C ⥤ C := tensoringRight C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ ((LaxMonoidalFunctor.mk (Functor.mk src✝.toPrefunctor) (rightUnitorNatIso C).inv fun X Y =>
                  NatTrans.mk fun Z => (α_ Z X Y).hom).toFunctor.obj
            (X ⊗ Y)).map
        f ≫
      (fun Z => (α_ Z X Y).inv) Z' =
    (fun Z => (α_ Z X Y).inv) Z ≫
      ((LaxMonoidalFunctor.mk (Functor.mk src✝.toPrefunctor) (rightUnitorNatIso C).inv fun X Y =>
                    NatTrans.mk fun Z => (α_ Z X Y).hom).toFunctor.obj
              X ⊗
            (LaxMonoidalFunctor.mk (Functor.mk src✝.toPrefunctor) (rightUnitorNatIso C).inv fun X Y =>
                    NatTrans.mk fun Z => (α_ Z X Y).hom).toFunctor.obj
              Y).map
        f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ C ⥤ C := tensoringRight C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ (f ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ Z' X Y).inv = (α_ Z X Y).inv ≫ ((f ⊗ 𝟙 X) ⊗ 𝟙 Y)
[PROOFSTEP]
rw [← associator_inv_naturality]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ C ⥤ C := tensoringRight C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ (f ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ Z' X Y).inv = (f ⊗ 𝟙 X ⊗ 𝟙 Y) ≫ (α_ Z' X Y).inv
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
src✝ : C ⥤ C ⥤ C := tensoringRight C
X Y : C
⊢ (LaxMonoidalFunctor.μ
          (LaxMonoidalFunctor.mk (Functor.mk src✝.toPrefunctor) (rightUnitorNatIso C).inv fun X Y =>
            NatTrans.mk fun Z => (α_ Z X Y).hom)
          X Y ≫
        NatTrans.mk fun Z => (α_ Z X Y).inv) =
      𝟙
        ((LaxMonoidalFunctor.mk (Functor.mk src✝.toPrefunctor) (rightUnitorNatIso C).inv fun X Y =>
                  NatTrans.mk fun Z => (α_ Z X Y).hom).toFunctor.obj
            X ⊗
          (LaxMonoidalFunctor.mk (Functor.mk src✝.toPrefunctor) (rightUnitorNatIso C).inv fun X Y =>
                  NatTrans.mk fun Z => (α_ Z X Y).hom).toFunctor.obj
            Y) ∧
    (NatTrans.mk fun Z => (α_ Z X Y).inv) ≫
        LaxMonoidalFunctor.μ
          (LaxMonoidalFunctor.mk (Functor.mk src✝.toPrefunctor) (rightUnitorNatIso C).inv fun X Y =>
            NatTrans.mk fun Z => (α_ Z X Y).hom)
          X Y =
      𝟙
        ((LaxMonoidalFunctor.mk (Functor.mk src✝.toPrefunctor) (rightUnitorNatIso C).inv fun X Y =>
                NatTrans.mk fun Z => (α_ Z X Y).hom).toFunctor.obj
          (X ⊗ Y))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
X Y : C
f : X ⟶ Y
⊢ NatTrans.app (MonoidalFunctor.εIso F).inv X ≫ (𝟙_ (C ⥤ C)).map f = NatTrans.app (MonoidalFunctor.εIso F).inv X ≫ f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
⊢ NatTrans.app (F.map g) ((F.obj m).obj X) ≫
      (F.obj n').map (NatTrans.app (F.map f) X) ≫ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n') X =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n) X ≫ NatTrans.app (F.map (f ⊗ g)) X
[PROOFSTEP]
have := congr_app (F.toLaxMonoidalFunctor.μ_natural f g) X
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
this :
  NatTrans.app ((F.map f ⊗ F.map g) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n') X =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n ≫ F.map (f ⊗ g)) X
⊢ NatTrans.app (F.map g) ((F.obj m).obj X) ≫
      (F.obj n').map (NatTrans.app (F.map f) X) ≫ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n') X =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n) X ≫ NatTrans.app (F.map (f ⊗ g)) X
[PROOFSTEP]
dsimp at this 
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
this :
  (NatTrans.app (F.map g) ((F.obj m).obj X) ≫ (F.obj n').map (NatTrans.app (F.map f) X)) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n') X =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n) X ≫ NatTrans.app (F.map (f ⊗ g)) X
⊢ NatTrans.app (F.map g) ((F.obj m).obj X) ≫
      (F.obj n').map (NatTrans.app (F.map f) X) ≫ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n') X =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n) X ≫ NatTrans.app (F.map (f ⊗ g)) X
[PROOFSTEP]
simpa using this
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n m' : M
f : m ⟶ m'
X : C
⊢ (F.obj n).map (NatTrans.app (F.map f) X) ≫ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n) X =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n) X ≫ NatTrans.app (F.map (f ⊗ 𝟙 n)) X
[PROOFSTEP]
rw [← μ_naturality₂ F f (𝟙 n) X]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n m' : M
f : m ⟶ m'
X : C
⊢ (F.obj n).map (NatTrans.app (F.map f) X) ≫ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n) X =
    NatTrans.app (F.map (𝟙 n)) ((F.obj m).obj X) ≫
      (F.obj n).map (NatTrans.app (F.map f) X) ≫ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n) X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n n' : M
g : n ⟶ n'
X : C
⊢ NatTrans.app (F.map g) ((F.obj m).obj X) ≫ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n') X =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n) X ≫ NatTrans.app (F.map (𝟙 m ⊗ g)) X
[PROOFSTEP]
rw [← μ_naturality₂ F (𝟙 m) g X]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n n' : M
g : n ⟶ n'
X : C
⊢ NatTrans.app (F.map g) ((F.obj m).obj X) ≫ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n') X =
    NatTrans.app (F.map g) ((F.obj m).obj X) ≫
      (F.obj n').map (NatTrans.app (F.map (𝟙 m)) X) ≫ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n') X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n m' : M
f : m ⟶ m'
X : C
⊢ NatTrans.app (MonoidalFunctor.μIso F m n).inv X ≫ (F.obj n).map (NatTrans.app (F.map f) X) =
    NatTrans.app (F.map (f ⊗ 𝟙 n)) X ≫ NatTrans.app (MonoidalFunctor.μIso F m' n).inv X
[PROOFSTEP]
rw [← IsIso.comp_inv_eq, Category.assoc, ← IsIso.eq_inv_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n m' : M
f : m ⟶ m'
X : C
⊢ (F.obj n).map (NatTrans.app (F.map f) X) ≫ inv (NatTrans.app (MonoidalFunctor.μIso F m' n).inv X) =
    inv (NatTrans.app (MonoidalFunctor.μIso F m n).inv X) ≫ NatTrans.app (F.map (f ⊗ 𝟙 n)) X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n n' : M
g : n ⟶ n'
X : C
⊢ NatTrans.app (MonoidalFunctor.μIso F m n).inv X ≫ NatTrans.app (F.map g) ((F.obj m).obj X) =
    NatTrans.app (F.map (𝟙 m ⊗ g)) X ≫ NatTrans.app (MonoidalFunctor.μIso F m n').inv X
[PROOFSTEP]
rw [← IsIso.comp_inv_eq, Category.assoc, ← IsIso.eq_inv_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n n' : M
g : n ⟶ n'
X : C
⊢ NatTrans.app (F.map g) ((F.obj m).obj X) ≫ inv (NatTrans.app (MonoidalFunctor.μIso F m n').inv X) =
    inv (NatTrans.app (MonoidalFunctor.μIso F m n).inv X) ≫ NatTrans.app (F.map (𝟙 m ⊗ g)) X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ (F.obj n).map (NatTrans.app F.ε X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) n) X ≫ NatTrans.app (F.map (λ_ n).hom) X =
    𝟙 ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X))
[PROOFSTEP]
have := congr_app (F.toLaxMonoidalFunctor.left_unitality n) X
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
this :
  NatTrans.app (λ_ (F.obj n)).hom X =
    NatTrans.app ((F.ε ⊗ 𝟙 (F.obj n)) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) n ≫ F.map (λ_ n).hom) X
⊢ (F.obj n).map (NatTrans.app F.ε X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) n) X ≫ NatTrans.app (F.map (λ_ n).hom) X =
    𝟙 ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X))
[PROOFSTEP]
dsimp at this 
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
this :
  𝟙 ((F.obj n).obj X) =
    (𝟙 ((F.obj n).obj X) ≫ (F.obj n).map (NatTrans.app F.ε X)) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) n) X ≫ NatTrans.app (F.map (λ_ n).hom) X
⊢ (F.obj n).map (NatTrans.app F.ε X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) n) X ≫ NatTrans.app (F.map (λ_ n).hom) X =
    𝟙 ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X))
[PROOFSTEP]
simpa using this.symm
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ (F.obj n).map (NatTrans.app F.ε X) =
    NatTrans.app (F.map (λ_ n).inv) X ≫ NatTrans.app (MonoidalFunctor.μIso F (𝟙_ M) n).inv X
[PROOFSTEP]
refine' Eq.trans _ (Category.id_comp _)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ (F.obj n).map (NatTrans.app F.ε X) =
    𝟙 ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X)) ≫
      NatTrans.app (F.map (λ_ n).inv) X ≫ NatTrans.app (MonoidalFunctor.μIso F (𝟙_ M) n).inv X
[PROOFSTEP]
rw [← Category.assoc, ← IsIso.comp_inv_eq, ← IsIso.comp_inv_eq, Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ (F.obj n).map (NatTrans.app F.ε X) ≫
      inv (NatTrans.app (MonoidalFunctor.μIso F (𝟙_ M) n).inv X) ≫ inv (NatTrans.app (F.map (λ_ n).inv) X) =
    𝟙 ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X))
[PROOFSTEP]
convert left_unitality_app F n X
[GOAL]
case h.e'_2.h.h.e'_7.h.h.e'_6
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
e_1✝ :
  ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X) ⟶ (F.obj n).obj ((𝟙_ (C ⥤ C)).obj X)) =
    ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X) ⟶ (F.obj n).obj X)
e_5✝ : (F.obj n).obj ((𝟙_ (C ⥤ C)).obj X) = (F.obj n).obj X
⊢ inv (NatTrans.app (MonoidalFunctor.μIso F (𝟙_ M) n).inv X) =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) n) X
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h.h.e'_7.h.h.e'_7.h
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
e_1✝ :
  ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X) ⟶ (F.obj n).obj ((𝟙_ (C ⥤ C)).obj X)) =
    ((F.obj n).obj ((𝟙_ (C ⥤ C)).obj X) ⟶ (F.obj n).obj X)
e_5✝ : (F.obj n).obj ((𝟙_ (C ⥤ C)).obj X) = (F.obj n).obj X
⊢ inv (NatTrans.app (F.map (λ_ n).inv) X) = NatTrans.app (F.map (λ_ n).hom) X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ (F.obj n).map (NatTrans.app (MonoidalFunctor.εIso F).inv X) =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) n) X ≫ NatTrans.app (F.map (λ_ n).hom) X
[PROOFSTEP]
rw [← cancel_mono ((F.obj n).map (F.ε.app X)), ← Functor.map_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ (F.obj n).map (NatTrans.app (MonoidalFunctor.εIso F).inv X ≫ NatTrans.app F.ε X) =
    (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) n) X ≫ NatTrans.app (F.map (λ_ n).hom) X) ≫
      (F.obj n).map (NatTrans.app F.ε X)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ NatTrans.app F.ε ((F.obj n).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)) X ≫ NatTrans.app (F.map (ρ_ n).hom) X =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X))
[PROOFSTEP]
have := congr_app (F.toLaxMonoidalFunctor.right_unitality n) X
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
this :
  NatTrans.app (ρ_ (F.obj n)).hom X =
    NatTrans.app ((𝟙 (F.obj n) ⊗ F.ε) ≫ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M) ≫ F.map (ρ_ n).hom) X
⊢ NatTrans.app F.ε ((F.obj n).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)) X ≫ NatTrans.app (F.map (ρ_ n).hom) X =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X))
[PROOFSTEP]
dsimp at this 
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
this :
  𝟙 ((F.obj n).obj X) =
    (NatTrans.app F.ε ((F.obj n).obj X) ≫ (F.obj (𝟙_ M)).map (𝟙 ((F.obj n).obj X))) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)) X ≫ NatTrans.app (F.map (ρ_ n).hom) X
⊢ NatTrans.app F.ε ((F.obj n).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)) X ≫ NatTrans.app (F.map (ρ_ n).hom) X =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X))
[PROOFSTEP]
simpa using this.symm
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ NatTrans.app F.ε ((F.obj n).obj X) =
    NatTrans.app (F.map (ρ_ n).inv) X ≫ NatTrans.app (MonoidalFunctor.μIso F n (𝟙_ M)).inv X
[PROOFSTEP]
refine' Eq.trans _ (Category.id_comp _)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ NatTrans.app F.ε ((F.obj n).obj X) =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X)) ≫
      NatTrans.app (F.map (ρ_ n).inv) X ≫ NatTrans.app (MonoidalFunctor.μIso F n (𝟙_ M)).inv X
[PROOFSTEP]
rw [← Category.assoc, ← IsIso.comp_inv_eq, ← IsIso.comp_inv_eq, Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ NatTrans.app F.ε ((F.obj n).obj X) ≫
      inv (NatTrans.app (MonoidalFunctor.μIso F n (𝟙_ M)).inv X) ≫ inv (NatTrans.app (F.map (ρ_ n).inv) X) =
    𝟙 ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X))
[PROOFSTEP]
convert right_unitality_app F n X using 1
[GOAL]
case h.e'_2.h
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
e_1✝ :
  ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X) ⟶ (𝟙_ (C ⥤ C)).obj ((F.obj n).obj X)) =
    ((𝟙_ (C ⥤ C)).obj ((F.obj n).obj X) ⟶ (F.obj n).obj X)
⊢ NatTrans.app F.ε ((F.obj n).obj X) ≫
      inv (NatTrans.app (MonoidalFunctor.μIso F n (𝟙_ M)).inv X) ≫ inv (NatTrans.app (F.map (ρ_ n).inv) X) =
    NatTrans.app F.ε ((F.obj n).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)) X ≫ NatTrans.app (F.map (ρ_ n).hom) X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ NatTrans.app (MonoidalFunctor.εIso F).inv ((F.obj n).obj X) =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)) X ≫ NatTrans.app (F.map (ρ_ n).hom) X
[PROOFSTEP]
rw [← cancel_mono (F.ε.app ((F.obj n).obj X)), ε_inv_hom_app]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
n : M
X : C
⊢ 𝟙 ((F.obj (𝟙_ M)).obj ((F.obj n).obj X)) =
    (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n (𝟙_ M)) X ≫ NatTrans.app (F.map (ρ_ n).hom) X) ≫
      NatTrans.app F.ε ((F.obj n).obj X)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.obj m₃).map (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂) X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃) X ≫
        NatTrans.app (F.map (α_ m₁ m₂ m₃).hom) X =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃) ((F.obj m₁).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)) X
[PROOFSTEP]
have := congr_app (F.toLaxMonoidalFunctor.associativity m₁ m₂ m₃) X
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
this :
  NatTrans.app
      ((LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂ ⊗ 𝟙 (F.obj m₃)) ≫
        LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃ ≫ F.map (α_ m₁ m₂ m₃).hom)
      X =
    NatTrans.app
      ((α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)).hom ≫
        (𝟙 (F.obj m₁) ⊗ LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃) ≫
          LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃))
      X
⊢ (F.obj m₃).map (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂) X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃) X ≫
        NatTrans.app (F.map (α_ m₁ m₂ m₃).hom) X =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃) ((F.obj m₁).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)) X
[PROOFSTEP]
dsimp at this 
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
this :
  (𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
        (F.obj m₃).map (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂) X)) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃) X ≫
        NatTrans.app (F.map (α_ m₁ m₂ m₃).hom) X =
    𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
      (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃) ((F.obj m₁).obj X) ≫
          (F.obj (m₂ ⊗ m₃)).map (𝟙 ((F.obj m₁).obj X))) ≫
        NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)) X
⊢ (F.obj m₃).map (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂) X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃) X ≫
        NatTrans.app (F.map (α_ m₁ m₂ m₃).hom) X =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃) ((F.obj m₁).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)) X
[PROOFSTEP]
simpa using this
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.obj m₃).map (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂) X) =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃) ((F.obj m₁).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)) X ≫
        NatTrans.app (F.map (α_ m₁ m₂ m₃).inv) X ≫ NatTrans.app (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv X
[PROOFSTEP]
rw [← associativity_app_assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.obj m₃).map (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂) X) =
    (F.obj m₃).map (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂) X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃) X ≫
        NatTrans.app (F.map (α_ m₁ m₂ m₃).hom) X ≫
          NatTrans.app (F.map (α_ m₁ m₂ m₃).inv) X ≫ NatTrans.app (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.obj m₃).map (NatTrans.app (MonoidalFunctor.μIso F m₁ m₂).inv X) =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃) X ≫
      NatTrans.app (F.map (α_ m₁ m₂ m₃).hom) X ≫
        NatTrans.app (MonoidalFunctor.μIso F m₁ (m₂ ⊗ m₃)).inv X ≫
          NatTrans.app (MonoidalFunctor.μIso F m₂ m₃).inv ((F.obj m₁).obj X)
[PROOFSTEP]
rw [← IsIso.inv_eq_inv]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv ((F.obj m₃).map (NatTrans.app (MonoidalFunctor.μIso F m₁ m₂).inv X)) =
    inv
      (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃) X ≫
        NatTrans.app (F.map (α_ m₁ m₂ m₃).hom) X ≫
          NatTrans.app (MonoidalFunctor.μIso F m₁ (m₂ ⊗ m₃)).inv X ≫
            NatTrans.app (MonoidalFunctor.μIso F m₂ m₃).inv ((F.obj m₁).obj X))
[PROOFSTEP]
convert obj_μ_app F m₁ m₂ m₃ X using 1
[GOAL]
case h.e'_2
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv ((F.obj m₃).map (NatTrans.app (MonoidalFunctor.μIso F m₁ m₂).inv X)) =
    (F.obj m₃).map (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂) X)
[PROOFSTEP]
refine' IsIso.inv_eq_of_hom_inv_id _
[GOAL]
case h.e'_2
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.obj m₃).map (NatTrans.app (MonoidalFunctor.μIso F m₁ m₂).inv X) ≫
      (F.obj m₃).map (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂) X) =
    𝟙 ((F.obj m₃).obj ((F.obj (m₁ ⊗ m₂)).obj X))
[PROOFSTEP]
rw [← Functor.map_comp]
[GOAL]
case h.e'_2
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ (F.obj m₃).map
      (NatTrans.app (MonoidalFunctor.μIso F m₁ m₂).inv X ≫
        NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ m₂) X) =
    𝟙 ((F.obj m₃).obj ((F.obj (m₁ ⊗ m₂)).obj X))
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv
      (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃) X ≫
        NatTrans.app (F.map (α_ m₁ m₂ m₃).hom) X ≫
          NatTrans.app (MonoidalFunctor.μIso F m₁ (m₂ ⊗ m₃)).inv X ≫
            NatTrans.app (MonoidalFunctor.μIso F m₂ m₃).inv ((F.obj m₁).obj X)) =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃) ((F.obj m₁).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)) X ≫
        NatTrans.app (F.map (α_ m₁ m₂ m₃).inv) X ≫ NatTrans.app (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv X
[PROOFSTEP]
simp only [MonoidalFunctor.μIso_hom, Category.assoc, NatIso.inv_inv_app, IsIso.inv_comp]
[GOAL]
case h.e'_3
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃) ((F.obj m₁).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)) X ≫
        inv (NatTrans.app (F.map (α_ m₁ m₂ m₃).hom) X) ≫
          inv (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃) X) =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₂ m₃) ((F.obj m₁).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (m₂ ⊗ m₃)) X ≫
        NatTrans.app (F.map (α_ m₁ m₂ m₃).inv) X ≫ NatTrans.app (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv X
[PROOFSTEP]
congr
[GOAL]
case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv (NatTrans.app (F.map (α_ m₁ m₂ m₃).hom) X) = NatTrans.app (F.map (α_ m₁ m₂ m₃).inv) X
[PROOFSTEP]
refine' IsIso.inv_eq_of_hom_inv_id _
[GOAL]
case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ NatTrans.app (F.map (α_ m₁ m₂ m₃).hom) X ≫ NatTrans.app (F.map (α_ m₁ m₂ m₃).inv) X =
    𝟙 ((F.obj ((m₁ ⊗ m₂) ⊗ m₃)).obj X)
[PROOFSTEP]
simp
[GOAL]
case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ inv (NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃) X) =
    NatTrans.app (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv X
[PROOFSTEP]
refine' IsIso.inv_eq_of_hom_inv_id _
[GOAL]
case h.e'_3.e_a.e_a.e_a
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ m₃ : M
X : C
⊢ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (m₁ ⊗ m₂) m₃) X ≫
      NatTrans.app (MonoidalFunctor.μIso F (m₁ ⊗ m₂) m₃).inv X =
    𝟙 ((F.obj m₃).obj ((F.obj (m₁ ⊗ m₂)).obj X))
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m : M
X Y : C
f : X ⟶ (F.obj m).obj Y
⊢ (F.obj (𝟙_ M)).map f ≫ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m (𝟙_ M)) Y =
    NatTrans.app (MonoidalFunctor.εIso F).inv X ≫ f ≫ NatTrans.app (F.map (ρ_ m).inv) Y
[PROOFSTEP]
rw [← IsIso.inv_comp_eq, ← IsIso.comp_inv_eq]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m : M
X Y : C
f : X ⟶ (F.obj m).obj Y
⊢ (inv (NatTrans.app (MonoidalFunctor.εIso F).inv X) ≫
        (F.obj (𝟙_ M)).map f ≫ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m (𝟙_ M)) Y) ≫
      inv (NatTrans.app (F.map (ρ_ m).inv) Y) =
    f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ : M
X : C
⊢ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) m₂) ((F.obj m₁).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (𝟙_ M ⊗ m₂)) X ≫
        NatTrans.app (F.map (α_ m₁ (𝟙_ M) m₂).inv) X ≫ NatTrans.app (MonoidalFunctor.μIso F (m₁ ⊗ 𝟙_ M) m₂).inv X =
    NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) m₂) ((F.obj m₁).obj X) ≫
      NatTrans.app (F.map (λ_ m₂).hom) ((F.obj m₁).obj X) ≫ (F.obj m₂).map (NatTrans.app (F.map (ρ_ m₁).inv) X)
[PROOFSTEP]
rw [← obj_ε_inv_app_assoc, ← Functor.map_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ : M
X : C
⊢ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) m₂) ((F.obj m₁).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (𝟙_ M ⊗ m₂)) X ≫
        NatTrans.app (F.map (α_ m₁ (𝟙_ M) m₂).inv) X ≫ NatTrans.app (MonoidalFunctor.μIso F (m₁ ⊗ 𝟙_ M) m₂).inv X =
    (F.obj m₂).map (NatTrans.app (MonoidalFunctor.εIso F).inv ((F.obj m₁).obj X) ≫ NatTrans.app (F.map (ρ_ m₁).inv) X)
[PROOFSTEP]
congr
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{u_2, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m₁ m₂ : M
X : C
⊢ NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor (𝟙_ M) m₂) ((F.obj m₁).obj X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m₁ (𝟙_ M ⊗ m₂)) X ≫
        NatTrans.app (F.map (α_ m₁ (𝟙_ M) m₂).inv) X ≫ NatTrans.app (MonoidalFunctor.μIso F (m₁ ⊗ 𝟙_ M) m₂).inv X =
    (F.obj m₂).map (NatTrans.app (MonoidalFunctor.εIso F).inv ((F.obj m₁).obj X) ≫ NatTrans.app (F.map (ρ_ m₁).inv) X)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{?u.152575, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n : M
h₁ : m ⊗ n ≅ 𝟙_ M
h₂ : n ⊗ m ≅ 𝟙_ M
H : (h₁.hom ⊗ 𝟙 m) ≫ (λ_ m).hom = (α_ m n m).hom ≫ (𝟙 m ⊗ h₂.hom) ≫ (ρ_ m).hom
⊢ ∀ (X : C),
    (F.obj m).map (NatTrans.app (unitOfTensorIsoUnit F m n h₁).symm.hom X) ≫
        NatTrans.app (unitOfTensorIsoUnit F n m h₂).hom ((F.obj m).obj X) =
      𝟙 ((F.obj m).obj X)
[PROOFSTEP]
intro X
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{?u.152575, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n : M
h₁ : m ⊗ n ≅ 𝟙_ M
h₂ : n ⊗ m ≅ 𝟙_ M
H : (h₁.hom ⊗ 𝟙 m) ≫ (λ_ m).hom = (α_ m n m).hom ≫ (𝟙 m ⊗ h₂.hom) ≫ (ρ_ m).hom
X : C
⊢ (F.obj m).map (NatTrans.app (unitOfTensorIsoUnit F m n h₁).symm.hom X) ≫
      NatTrans.app (unitOfTensorIsoUnit F n m h₂).hom ((F.obj m).obj X) =
    𝟙 ((F.obj m).obj X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{?u.152575, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n : M
h₁ : m ⊗ n ≅ 𝟙_ M
h₂ : n ⊗ m ≅ 𝟙_ M
H : (h₁.hom ⊗ 𝟙 m) ≫ (λ_ m).hom = (α_ m n m).hom ≫ (𝟙 m ⊗ h₂.hom) ≫ (ρ_ m).hom
X : C
⊢ (F.obj m).map (NatTrans.app (unitOfTensorIsoUnit F m n h₁).inv X) ≫
      NatTrans.app (LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor n m) ((F.obj m).obj X) ≫
        NatTrans.app (F.map h₂.hom) ((F.obj m).obj X) ≫ NatTrans.app (MonoidalFunctor.εIso F).inv ((F.obj m).obj X) =
    𝟙 ((F.obj m).obj X)
[PROOFSTEP]
simp only [μ_naturalityᵣ_assoc, μ_naturalityₗ_assoc, ε_inv_app_obj, Category.assoc, obj_μ_inv_app, Functor.map_comp,
  μ_inv_hom_app_assoc, obj_ε_app, unitOfTensorIsoUnit_inv_app]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
M : Type u_1
inst✝¹ : Category.{?u.152575, u_1} M
inst✝ : MonoidalCategory M
F : MonoidalFunctor M (C ⥤ C)
m n : M
h₁ : m ⊗ n ≅ 𝟙_ M
h₂ : n ⊗ m ≅ 𝟙_ M
H : (h₁.hom ⊗ 𝟙 m) ≫ (λ_ m).hom = (α_ m n m).hom ≫ (𝟙 m ⊗ h₂.hom) ≫ (ρ_ m).hom
X : C
⊢ NatTrans.app (F.map (λ_ m).inv) X ≫
      NatTrans.app (F.map (h₁.inv ⊗ 𝟙 m)) X ≫
        NatTrans.app (F.map (α_ m n m).hom) X ≫
          NatTrans.app (F.map (𝟙 m ⊗ h₂.hom)) X ≫ NatTrans.app (F.map (ρ_ m).hom) X =
    𝟙 ((F.obj m).obj X)
[PROOFSTEP]
simp [← NatTrans.comp_app, ← F.toFunctor.map_comp, ← H, -Functor.map_comp]
