[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]


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X✝ : C
Y Y' : D
X : C
⊢ ↑(homEquiv adj X (F.obj X)) (𝟙 (F.obj X)) = NatTrans.app adj.unit X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X✝ : C
Y Y' X : D
⊢ ↑(homEquiv adj (G.obj X) X).symm (𝟙 (G.obj X)) = NatTrans.app adj.counit X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ ↑(homEquiv adj X' Y).symm (f ≫ g) = F.map f ≫ ↑(homEquiv adj X Y).symm g
[PROOFSTEP]
rw [homEquiv_counit, F.map_comp, assoc, adj.homEquiv_counit.symm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ ↑(homEquiv adj X' Y) (F.map f ≫ g) = f ≫ ↑(homEquiv adj X Y) g
[PROOFSTEP]
rw [← Equiv.eq_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = ↑(homEquiv adj X' Y).symm (f ≫ ↑(homEquiv adj X Y) g)
[PROOFSTEP]
simp only [Equiv.symm_apply_apply, eq_self_iff_true, homEquiv_naturality_left_symm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : F.obj X ⟶ Y
g : Y ⟶ Y'
⊢ ↑(homEquiv adj X Y') (f ≫ g) = ↑(homEquiv adj X Y) f ≫ G.map g
[PROOFSTEP]
rw [homEquiv_unit, G.map_comp, ← assoc, ← homEquiv_unit]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ ↑(homEquiv adj X Y').symm (f ≫ G.map g) = ↑(homEquiv adj X Y).symm f ≫ g
[PROOFSTEP]
rw [Equiv.symm_apply_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = ↑(homEquiv adj X Y') (↑(homEquiv adj X Y).symm f ≫ g)
[PROOFSTEP]
simp only [homEquiv_naturality_right, eq_self_iff_true, Equiv.apply_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
⊢ whiskerRight adj.unit F ≫ whiskerLeft F adj.counit = 𝟙 (𝟭 C ⋙ F)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
x✝ : C
⊢ NatTrans.app (whiskerRight adj.unit F ≫ whiskerLeft F adj.counit) x✝ = NatTrans.app (𝟙 (𝟭 C ⋙ F)) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
x✝ : C
⊢ F.map (NatTrans.app adj.unit x✝) ≫ NatTrans.app adj.counit (F.obj x✝) = 𝟙 (F.obj x✝)
[PROOFSTEP]
erw [← adj.homEquiv_counit, Equiv.symm_apply_eq, adj.homEquiv_unit]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
x✝ : C
⊢ NatTrans.app adj.unit x✝ = NatTrans.app adj.unit x✝ ≫ G.map (𝟙 (F.obj x✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
⊢ whiskerLeft G adj.unit ≫ whiskerRight adj.counit G = 𝟙 (G ⋙ 𝟭 C)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' x✝ : D
⊢ NatTrans.app (whiskerLeft G adj.unit ≫ whiskerRight adj.counit G) x✝ = NatTrans.app (𝟙 (G ⋙ 𝟭 C)) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' x✝ : D
⊢ NatTrans.app adj.unit (G.obj x✝) ≫ G.map (NatTrans.app adj.counit x✝) = 𝟙 (G.obj x✝)
[PROOFSTEP]
erw [← adj.homEquiv_unit, ← Equiv.eq_symm_apply, adj.homEquiv_counit]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' x✝ : D
⊢ NatTrans.app adj.counit x✝ = F.map (𝟙 (G.obj x✝)) ≫ NatTrans.app adj.counit x✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : ↑(homEquiv adj A B) f = g
⊢ f = ↑(homEquiv adj A B).symm g
[PROOFSTEP]
cases h
[GOAL]
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
⊢ f = ↑(homEquiv adj A B).symm (↑(homEquiv adj A B) f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : f = ↑(homEquiv adj A B).symm g
⊢ ↑(homEquiv adj A B) f = g
[PROOFSTEP]
cases h
[GOAL]
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
g : A ⟶ G.obj B
⊢ ↑(homEquiv adj A B) (↑(homEquiv adj A B).symm g) = g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : g = ↑(homEquiv adj A B) f
⊢ ↑(homEquiv adj A B).symm g = f
[PROOFSTEP]
cases h
[GOAL]
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
⊢ ↑(homEquiv adj A B).symm (↑(homEquiv adj A B) f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : ↑(homEquiv adj A B).symm g = f
⊢ g = ↑(homEquiv adj A B) f
[PROOFSTEP]
cases h
[GOAL]
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
g : A ⟶ G.obj B
⊢ g = ↑(homEquiv adj A B) (↑(homEquiv adj A B).symm g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ ↑(homEquiv adj X' (F.obj X)) (F.map f) ≫ G.map g = f ≫ ↑(homEquiv adj X Y) g
[PROOFSTEP]
rw [← homEquiv_naturality_right, ← Equiv.eq_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = ↑(homEquiv adj X' Y).symm (f ≫ ↑(homEquiv adj X Y) g)
[PROOFSTEP]
simp
  -- @[simp] -- Porting note: LHS simplifies, added aux lemma above
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ ↑(homEquiv adj X' Y) (F.map f ≫ g) = f ≫ ↑(homEquiv adj X Y) g
[PROOFSTEP]
rw [← Equiv.eq_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = ↑(homEquiv adj X' Y).symm (f ≫ ↑(homEquiv adj X Y) g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ F.map f ≫ ↑(homEquiv adj (G.obj Y) Y').symm (G.map g) = ↑(homEquiv adj X Y).symm f ≫ g
[PROOFSTEP]
rw [← homEquiv_naturality_left_symm, Equiv.symm_apply_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = ↑(homEquiv adj X Y') (↑(homEquiv adj X Y).symm f ≫ g)
[PROOFSTEP]
simp
  -- @[simp] -- Porting note: LHS simplifies, added aux lemma above
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ ↑(homEquiv adj X Y').symm (f ≫ G.map g) = ↑(homEquiv adj X Y).symm f ≫ g
[PROOFSTEP]
rw [Equiv.symm_apply_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = ↑(homEquiv adj X Y') (↑(homEquiv adj X Y).symm f ≫ g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
    (𝟭 C).map f ≫ (fun X => ↑(CoreHomEquiv.homEquiv adj X (F.obj X)) (𝟙 (F.obj X))) Y =
      (fun X => ↑(CoreHomEquiv.homEquiv adj X (F.obj X)) (𝟙 (F.obj X))) X ≫ (F ⋙ G).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (𝟭 C).map f✝ ≫ (fun X => ↑(CoreHomEquiv.homEquiv adj X (F.obj X)) (𝟙 (F.obj X))) Y✝ =
    (fun X => ↑(CoreHomEquiv.homEquiv adj X (F.obj X)) (𝟙 (F.obj X))) X✝ ≫ (F ⋙ G).map f✝
[PROOFSTEP]
erw [← adj.homEquiv_naturality_left, ← adj.homEquiv_naturality_right]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ↑(CoreHomEquiv.homEquiv adj ((𝟭 C).obj X✝) (F.obj Y✝)) (F.map ((𝟭 C).map f✝) ≫ 𝟙 (F.obj Y✝)) =
    ↑(CoreHomEquiv.homEquiv adj ((𝟭 C).obj X✝) (F.obj Y✝)) (𝟙 (F.obj X✝) ≫ F.map f✝)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ↑(CoreHomEquiv.homEquiv adj X✝ (F.obj Y✝)) (F.map f✝ ≫ 𝟙 (F.obj Y✝)) =
    ↑(CoreHomEquiv.homEquiv adj X✝ (F.obj Y✝)) (𝟙 (F.obj X✝) ≫ F.map f✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
⊢ ∀ ⦃X Y : D⦄ (f : X ⟶ Y),
    (G ⋙ F).map f ≫ (fun Y => Equiv.invFun (CoreHomEquiv.homEquiv adj (G.obj Y) ((𝟭 D).obj Y)) (𝟙 (G.obj Y))) Y =
      (fun Y => Equiv.invFun (CoreHomEquiv.homEquiv adj (G.obj Y) ((𝟭 D).obj Y)) (𝟙 (G.obj Y))) X ≫ (𝟭 D).map f
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
⊢ (G ⋙ F).map f✝ ≫ (fun Y => Equiv.invFun (CoreHomEquiv.homEquiv adj (G.obj Y) ((𝟭 D).obj Y)) (𝟙 (G.obj Y))) Y✝ =
    (fun Y => Equiv.invFun (CoreHomEquiv.homEquiv adj (G.obj Y) ((𝟭 D).obj Y)) (𝟙 (G.obj Y))) X✝ ≫ (𝟭 D).map f✝
[PROOFSTEP]
erw [← adj.homEquiv_naturality_left_symm, ← adj.homEquiv_naturality_right_symm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
⊢ ↑(CoreHomEquiv.homEquiv adj (G.obj X✝) ((𝟭 D).obj Y✝)).symm (G.map f✝ ≫ 𝟙 (G.obj Y✝)) =
    ↑(CoreHomEquiv.homEquiv adj (G.obj X✝) ((𝟭 D).obj Y✝)).symm (𝟙 (G.obj X✝) ≫ G.map ((𝟭 D).map f✝))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X✝ Y✝ : D
f✝ : X✝ ⟶ Y✝
⊢ ↑(CoreHomEquiv.homEquiv adj (G.obj X✝) Y✝).symm (G.map f✝ ≫ 𝟙 (G.obj Y✝)) =
    ↑(CoreHomEquiv.homEquiv adj (G.obj X✝) Y✝).symm (𝟙 (G.obj X✝) ≫ G.map f✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ↑(CoreHomEquiv.homEquiv adj X Y) f =
    NatTrans.app (NatTrans.mk fun X => ↑(CoreHomEquiv.homEquiv adj X (F.obj X)) (𝟙 (F.obj X))) X ≫ G.map f
[PROOFSTEP]
erw [← adj.homEquiv_naturality_right]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ↑(CoreHomEquiv.homEquiv adj X Y) f = ↑(CoreHomEquiv.homEquiv adj ((𝟭 C).obj X) Y) (𝟙 (F.obj X) ≫ f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y : D
f : X ⟶ G.obj Y
⊢ ↑(CoreHomEquiv.homEquiv adj X Y).symm f =
    F.map f ≫
      NatTrans.app (NatTrans.mk fun Y => Equiv.invFun (CoreHomEquiv.homEquiv adj (G.obj Y) ((𝟭 D).obj Y)) (𝟙 (G.obj Y)))
        Y
[PROOFSTEP]
erw [← adj.homEquiv_naturality_left_symm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y : D
f : X ⟶ G.obj Y
⊢ ↑(CoreHomEquiv.homEquiv adj X Y).symm f = ↑(CoreHomEquiv.homEquiv adj X ((𝟭 D).obj Y)).symm (f ≫ 𝟙 (G.obj Y))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (fun g => F.map g ≫ NatTrans.app adj.counit Y) ((fun f => NatTrans.app adj.unit X ≫ G.map f) f) = f
[PROOFSTEP]
change F.map (_ ≫ _) ≫ _ = _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ F.map (NatTrans.app adj.unit X ≫ G.map f) ≫ NatTrans.app adj.counit Y = f
[PROOFSTEP]
rw [F.map_comp, assoc, ← Functor.comp_map, adj.counit.naturality, ← assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (F.map (NatTrans.app adj.unit X) ≫ NatTrans.app adj.counit (F.obj X)) ≫ (𝟭 D).map f = f
[PROOFSTEP]
convert id_comp f
[GOAL]
case h.e'_2.h.e'_6.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
e_4✝ : (𝟭 D).obj (F.obj X) = F.obj X
⊢ F.map (NatTrans.app adj.unit X) ≫ NatTrans.app adj.counit (F.obj X) = 𝟙 (F.obj X)
[PROOFSTEP]
have t := congrArg (fun (s : NatTrans (𝟭 C ⋙ F) (F ⋙ 𝟭 D)) => s.app X) adj.left_triangle
[GOAL]
case h.e'_2.h.e'_6.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
e_4✝ : (𝟭 D).obj (F.obj X) = F.obj X
t :
  (fun s => NatTrans.app s X) (whiskerRight adj.unit F ≫ (Functor.associator F G F).hom ≫ whiskerLeft F adj.counit) =
    (fun s => NatTrans.app s X) (NatTrans.id (𝟭 C ⋙ F))
⊢ F.map (NatTrans.app adj.unit X) ≫ NatTrans.app adj.counit (F.obj X) = 𝟙 (F.obj X)
[PROOFSTEP]
dsimp at t
[GOAL]
case h.e'_2.h.e'_6.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
e_4✝ : (𝟭 D).obj (F.obj X) = F.obj X
t : F.map (NatTrans.app adj.unit X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ NatTrans.app adj.counit (F.obj X) = 𝟙 (F.obj X)
⊢ F.map (NatTrans.app adj.unit X) ≫ NatTrans.app adj.counit (F.obj X) = 𝟙 (F.obj X)
[PROOFSTEP]
simp only [id_comp] at t
[GOAL]
case h.e'_2.h.e'_6.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
f : F.obj X ⟶ Y
e_4✝ : (𝟭 D).obj (F.obj X) = F.obj X
t : F.map (NatTrans.app adj.unit X) ≫ NatTrans.app adj.counit (F.obj X) = 𝟙 (F.obj X)
⊢ F.map (NatTrans.app adj.unit X) ≫ NatTrans.app adj.counit (F.obj X) = 𝟙 (F.obj X)
[PROOFSTEP]
exact t
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
⊢ (fun f => NatTrans.app adj.unit X ≫ G.map f) ((fun g => F.map g ≫ NatTrans.app adj.counit Y) g) = g
[PROOFSTEP]
change _ ≫ G.map (_ ≫ _) = _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
⊢ NatTrans.app adj.unit X ≫ G.map (F.map g ≫ NatTrans.app adj.counit Y) = g
[PROOFSTEP]
rw [G.map_comp, ← assoc, ← Functor.comp_map, ← adj.unit.naturality, assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
⊢ (𝟭 C).map g ≫ NatTrans.app adj.unit (G.obj Y) ≫ G.map (NatTrans.app adj.counit Y) = g
[PROOFSTEP]
convert comp_id g
[GOAL]
case h.e'_2.h.e'_7.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
e_4✝ : (𝟭 C).obj (G.obj Y) = G.obj Y
⊢ NatTrans.app adj.unit (G.obj Y) ≫ G.map (NatTrans.app adj.counit Y) = 𝟙 (G.obj Y)
[PROOFSTEP]
have t := congrArg (fun t : NatTrans (G ⋙ 𝟭 C) (𝟭 D ⋙ G) => t.app Y) adj.right_triangle
[GOAL]
case h.e'_2.h.e'_7.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
e_4✝ : (𝟭 C).obj (G.obj Y) = G.obj Y
t :
  (fun t => NatTrans.app t Y) (whiskerLeft G adj.unit ≫ (Functor.associator G F G).inv ≫ whiskerRight adj.counit G) =
    (fun t => NatTrans.app t Y) (NatTrans.id (G ⋙ 𝟭 C))
⊢ NatTrans.app adj.unit (G.obj Y) ≫ G.map (NatTrans.app adj.counit Y) = 𝟙 (G.obj Y)
[PROOFSTEP]
dsimp at t
[GOAL]
case h.e'_2.h.e'_7.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
e_4✝ : (𝟭 C).obj (G.obj Y) = G.obj Y
t : NatTrans.app adj.unit (G.obj Y) ≫ 𝟙 (G.obj (F.obj (G.obj Y))) ≫ G.map (NatTrans.app adj.counit Y) = 𝟙 (G.obj Y)
⊢ NatTrans.app adj.unit (G.obj Y) ≫ G.map (NatTrans.app adj.counit Y) = 𝟙 (G.obj Y)
[PROOFSTEP]
simp only [id_comp] at t
[GOAL]
case h.e'_2.h.e'_7.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreUnitCounit F G
X : C
Y : D
g : X ⟶ G.obj Y
e_4✝ : (𝟭 C).obj (G.obj Y) = G.obj Y
t : NatTrans.app adj.unit (G.obj Y) ≫ G.map (NatTrans.app adj.counit Y) = 𝟙 (G.obj Y)
⊢ NatTrans.app adj.unit (G.obj Y) ≫ G.map (NatTrans.app adj.counit Y) = 𝟙 (G.obj Y)
[PROOFSTEP]
exact t
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ : C ⥤ D
G : D ⥤ C
F F' : C ⥤ D
iso : F ≅ F'
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (fun g => NatTrans.app iso.hom X ≫ g) ((fun f => NatTrans.app iso.inv X ≫ f) f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ : C ⥤ D
G : D ⥤ C
F F' : C ⥤ D
iso : F ≅ F'
X : C
Y : D
g : F'.obj X ⟶ Y
⊢ (fun f => NatTrans.app iso.inv X ≫ f) ((fun g => NatTrans.app iso.hom X ≫ g) g) = g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G✝ G G' : D ⥤ C
iso : G ≅ G'
X : C
Y : D
f : X ⟶ G.obj Y
⊢ (fun g => g ≫ NatTrans.app iso.inv Y) ((fun f => f ≫ NatTrans.app iso.hom Y) f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G✝ G G' : D ⥤ C
iso : G ≅ G'
X : C
Y : D
g : X ⟶ G'.obj Y
⊢ (fun f => f ≫ NatTrans.app iso.hom Y) ((fun g => g ≫ NatTrans.app iso.inv Y) g) = g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
[PROOFSTEP]
rw [Equiv.symm_apply_eq, he]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = ↑(e X Y) (↑(e X Y).symm f) ≫ G.map g
[PROOFSTEP]
simp
  -- #align category_theory.adjunction.he' category_theory.adjunction.he'
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
⊢ { obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map (f ≫ f') =
    { obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f ≫
      { obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f'
[PROOFSTEP]
rw [Equiv.symm_apply_eq, he, Equiv.apply_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
⊢ (f ≫ f') ≫ ↑(e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) =
    (f ≫ ↑(e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫
      G.map
        ({ obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f')
[PROOFSTEP]
conv =>
  rhs
  rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| (f ≫ f') ≫ ↑(e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) =
    (f ≫ ↑(e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫
      G.map
        ({ obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f')
[PROOFSTEP]
  rhs
  rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| (f ≫ f') ≫ ↑(e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) =
    (f ≫ ↑(e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫
      G.map
        ({ obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f')
[PROOFSTEP]
  rhs
  rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| (f ≫ f') ≫ ↑(e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) =
    (f ≫ ↑(e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫
      G.map
        ({ obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f')
[PROOFSTEP]
rhs
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
| (f ≫ ↑(e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫
    G.map
      ({ obj := F_obj, map := fun {X X'} f => ↑(e X (F_obj X')).symm (f ≫ ↑(e X' (F_obj X')) (𝟙 (F_obj X'))) }.map f')
[PROOFSTEP]
rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
⊢ (f ≫ f') ≫ ↑(e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)) = f ≫ f' ≫ ↑(e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ ↑(e X' Y).symm (f ≫ g) = (leftAdjointOfEquiv e he).map f ≫ ↑(e X Y).symm g
[PROOFSTEP]
have := @he' C _ D _ G F_obj e he
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'), ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
⊢ ↑(e X' Y).symm (f ≫ g) = (leftAdjointOfEquiv e he).map f ≫ ↑(e X Y).symm g
[PROOFSTEP]
erw [← this, ← Equiv.apply_eq_iff_eq (e X' Y)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'), ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
⊢ ↑(e X' Y) (↑(e X' Y).symm (f ≫ g)) =
    ↑(e X' Y)
      (↑(e X' Y).symm ((f ≫ ↑(e X ((fun X => F_obj X) X)) (𝟙 ((fun X => F_obj X) X))) ≫ G.map (↑(e X Y).symm g)))
[PROOFSTEP]
simp [(he X' (F_obj X) Y (e X Y |>.symm g) (leftAdjointOfEquiv e he |>.map f)).symm]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'), ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
⊢ f ≫ g = f ≫ ↑(e X (F_obj X)) (𝟙 (F_obj X)) ≫ G.map (↑(e X Y).symm g)
[PROOFSTEP]
congr
[GOAL]
case e_a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'), ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
⊢ g = ↑(e X (F_obj X)) (𝟙 (F_obj X)) ≫ G.map (↑(e X Y).symm g)
[PROOFSTEP]
rw [← he]
[GOAL]
case e_a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), ↑(e X Y') (h ≫ g) = ↑(e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'), ↑(e X Y').symm (f ≫ G.map g) = ↑(e X Y).symm f ≫ g
⊢ g = ↑(e X Y) (𝟙 (F_obj X) ≫ ↑(e X Y).symm g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ F.map f ≫ ↑(e X Y).symm g = ↑(e X' Y).symm (f ≫ g)
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ F.map f ≫ ↑(e X Y).symm g = ↑(e X' Y).symm (f ≫ g)
[PROOFSTEP]
rw [Equiv.eq_symm_apply, he]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ f ≫ ↑(e X Y) (↑(e X Y).symm g) = f ≫ g
[PROOFSTEP]
simp
  -- #align category_theory.adjunction.he' category_theory.adjunction.he'
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ { obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map (g ≫ g') =
    { obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g ≫
      { obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g'
[PROOFSTEP]
rw [← Equiv.eq_symm_apply, ← he'' e he, Equiv.symm_apply_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ ↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ({ obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g) ≫
      ↑(e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'
[PROOFSTEP]
conv =>
  rhs
  rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| ↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ({ obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g) ≫
      ↑(e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'
[PROOFSTEP]
  rhs
  rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| ↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ({ obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g) ≫
      ↑(e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'
[PROOFSTEP]
  rhs
  rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| ↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ({ obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g) ≫
      ↑(e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'
[PROOFSTEP]
rhs
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| F.map ({ obj := G_obj, map := fun {Y Y'} g => ↑(e (G_obj Y) Y') (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) }.map g) ≫
    ↑(e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'
[PROOFSTEP]
rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ ↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' = (↑(e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫ g'
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
⊢ ∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ (rightAdjointOfEquiv e he).obj Y),
    ↑(e X' Y).symm (f ≫ g) = F.map f ≫ ↑(e X Y).symm g
[PROOFSTEP]
intro X X' Y f g
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X X' : C
Y : D
f : X ⟶ X'
g : X' ⟶ (rightAdjointOfEquiv e he).obj Y
⊢ ↑(e X Y).symm (f ≫ g) = F.map f ≫ ↑(e X' Y).symm g
[PROOFSTEP]
rw [Equiv.symm_apply_eq]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X X' : C
Y : D
f : X ⟶ X'
g : X' ⟶ (rightAdjointOfEquiv e he).obj Y
⊢ f ≫ g = ↑(e X Y) (F.map f ≫ ↑(e X' Y).symm g)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X X' : C
Y : D
f : X ⟶ X'
g : X' ⟶ (rightAdjointOfEquiv e he).obj Y
⊢ f ≫ g = ↑(e X Y) (F.map f ≫ ↑(e X' Y).symm g)
[PROOFSTEP]
rw [he]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X X' : C
Y : D
f : X ⟶ X'
g : X' ⟶ (rightAdjointOfEquiv e he).obj Y
⊢ f ≫ g = f ≫ ↑(e X' Y) (↑(e X' Y).symm g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
⊢ ∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), ↑(e X Y') (f ≫ g) = ↑(e X Y) f ≫ (rightAdjointOfEquiv e he).map g
[PROOFSTEP]
intro X Y Y' g h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), ↑(e X' Y) (F.map f ≫ g) = f ≫ ↑(e X Y) g
X : C
Y Y' : D
g : F.obj X ⟶ Y
h : Y ⟶ Y'
⊢ ↑(e X Y') (g ≫ h) = ↑(e X Y) g ≫ (rightAdjointOfEquiv e he).map h
[PROOFSTEP]
erw [← he, Equiv.apply_eq_iff_eq, ← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
⊢ whiskerRight (unit e) e.functor ≫
      (Functor.associator e.functor e.inverse e.functor).hom ≫ whiskerLeft e.functor (counit e) =
    NatTrans.id (𝟭 C ⋙ e.functor)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
x✝ : C
⊢ NatTrans.app
      (whiskerRight (unit e) e.functor ≫
        (Functor.associator e.functor e.inverse e.functor).hom ≫ whiskerLeft e.functor (counit e))
      x✝ =
    NatTrans.app (NatTrans.id (𝟭 C ⋙ e.functor)) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
x✝ : C
⊢ e.functor.map (NatTrans.app (unit e) x✝) ≫
      𝟙 (e.functor.obj (e.inverse.obj (e.functor.obj x✝))) ≫ NatTrans.app (counit e) (e.functor.obj x✝) =
    𝟙 (e.functor.obj x✝)
[PROOFSTEP]
simp only [id_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
x✝ : C
⊢ e.functor.map (NatTrans.app (unit e) x✝) ≫ NatTrans.app (counit e) (e.functor.obj x✝) = 𝟙 (e.functor.obj x✝)
[PROOFSTEP]
exact e.functor_unit_comp _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
⊢ whiskerLeft e.inverse (unit e) ≫
      (Functor.associator e.inverse e.functor e.inverse).inv ≫ whiskerRight (counit e) e.inverse =
    NatTrans.id (e.inverse ⋙ 𝟭 C)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
x✝ : D
⊢ NatTrans.app
      (whiskerLeft e.inverse (unit e) ≫
        (Functor.associator e.inverse e.functor e.inverse).inv ≫ whiskerRight (counit e) e.inverse)
      x✝ =
    NatTrans.app (NatTrans.id (e.inverse ⋙ 𝟭 C)) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
x✝ : D
⊢ NatTrans.app (unit e) (e.inverse.obj x✝) ≫
      𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj x✝))) ≫ e.inverse.map (NatTrans.app (counit e) x✝) =
    𝟙 (e.inverse.obj x✝)
[PROOFSTEP]
simp only [id_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
x✝ : D
⊢ NatTrans.app (unit e) (e.inverse.obj x✝) ≫ e.inverse.map (NatTrans.app (counit e) x✝) = 𝟙 (e.inverse.obj x✝)
[PROOFSTEP]
exact e.unit_inverse_comp _