[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.41, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }.map (f ≫ g) =
    { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }.map f ≫
      { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }.map g
[PROOFSTEP]
simp [comp_rightAdjointMate]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.41, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (𝟙_ (C ⥤ D)).map f ≫
      (fun X => η_ (F.obj X) ((Functor.mk { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }).obj X))
        Y =
    (fun X => η_ (F.obj X) ((Functor.mk { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }).obj X))
        X ≫
      (F ⊗ Functor.mk { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.41, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ 𝟙 (𝟙_ D) ≫ η_ (F.obj Y) (F.obj Y)ᘁ = η_ (F.obj X) (F.obj X)ᘁ ≫ (F.map f ⊗ F.map (inv f)ᘁ)
[PROOFSTEP]
rw [Functor.map_inv, Category.id_comp, ← id_tensor_comp_tensor_id, ← Category.assoc, coevaluation_comp_rightAdjointMate,
  Category.assoc, ← comp_tensor_id, IsIso.inv_hom_id, tensor_id, Category.comp_id]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.41, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (Functor.mk { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ } ⊗ F).map f ≫
      (fun X => ε_ (F.obj X) ((Functor.mk { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }).obj X))
        Y =
    (fun X => ε_ (F.obj X) ((Functor.mk { obj := fun X => (F.obj X)ᘁ, map := fun {X Y} f => F.map (inv f)ᘁ }).obj X))
        X ≫
      (𝟙_ (C ⥤ D)).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.41, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F.map (inv f)ᘁ ⊗ F.map f) ≫ ε_ (F.obj Y) (F.obj Y)ᘁ = ε_ (F.obj X) (F.obj X)ᘁ ≫ 𝟙 (𝟙_ D)
[PROOFSTEP]
rw [Category.comp_id, Functor.map_inv, ← id_tensor_comp_tensor_id, Category.assoc, rightAdjointMate_comp_evaluation, ←
  Category.assoc, ← id_tensor_comp, IsIso.hom_inv_id, tensor_id, Category.id_comp]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.37015, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }.map (f ≫ g) =
    { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }.map f ≫
      { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }.map g
[PROOFSTEP]
simp [comp_leftAdjointMate]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.37015, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (𝟙_ (C ⥤ D)).map f ≫
      (fun X => η_ ((Functor.mk { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }).obj X) (F.obj X))
        Y =
    (fun X => η_ ((Functor.mk { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }).obj X) (F.obj X))
        X ≫
      (Functor.mk { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) } ⊗ F).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.37015, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ 𝟙 (𝟙_ D) ≫ η_ (ᘁ(F.obj Y)) (F.obj Y) = η_ (ᘁ(F.obj X)) (F.obj X) ≫ ((ᘁF.map (inv f)) ⊗ F.map f)
[PROOFSTEP]
rw [Functor.map_inv, Category.id_comp, ← tensor_id_comp_id_tensor, ← Category.assoc, coevaluation_comp_leftAdjointMate,
  Category.assoc, ← id_tensor_comp, IsIso.inv_hom_id, tensor_id, Category.comp_id]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.37015, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F ⊗ Functor.mk { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }).map f ≫
      (fun X => ε_ ((Functor.mk { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }).obj X) (F.obj X))
        Y =
    (fun X => ε_ ((Functor.mk { obj := fun X => ᘁ(F.obj X), map := fun {X Y} f => ᘁF.map (inv f) }).obj X) (F.obj X))
        X ≫
      (𝟙_ (C ⥤ D)).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{?u.37015, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F.map f ⊗ ᘁF.map (inv f)) ≫ ε_ (ᘁ(F.obj Y)) (F.obj Y) = ε_ (ᘁ(F.obj X)) (F.obj X) ≫ 𝟙 (𝟙_ D)
[PROOFSTEP]
rw [Category.comp_id, Functor.map_inv, ← tensor_id_comp_id_tensor, Category.assoc, leftAdjointMate_comp_evaluation, ←
  Category.assoc, ← comp_tensor_id, IsIso.hom_inv_id, tensor_id, Category.id_comp]
