[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ Quiver.Hom.unmop (Quiver.Hom.mop f.hom ≫ Quiver.Hom.mop f.inv) = Quiver.Hom.unmop (𝟙 (MonoidalOpposite.mop X))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ≅ Y
⊢ Quiver.Hom.unmop (Quiver.Hom.mop f.inv ≫ Quiver.Hom.mop f.hom) = Quiver.Hom.unmop (𝟙 (MonoidalOpposite.mop Y))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : Cᵒᵖ
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
h : X₃✝ ⟶ Y₃✝
⊢ ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) f g) h ≫
        ((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) Y₁✝ Y₂✝ Y₃✝).hom).unop =
    (((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) X₁✝ X₂✝ X₃✝).hom ≫
        (fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) f ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) g h)).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) (𝟙 (op (𝟙_ C))) f ≫
        ((fun X => Iso.op (λ_ X.unop).symm) Y✝).hom).unop =
    (((fun X => Iso.op (λ_ X.unop).symm) X✝).hom ≫ f).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) f (𝟙 (op (𝟙_ C))) ≫
        ((fun X => Iso.op (ρ_ X.unop).symm) Y✝).hom).unop =
    (((fun X => Iso.op (ρ_ X.unop).symm) X✝).hom ≫ f).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᵒᵖ
⊢ ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) ((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) W X Y).hom
          (𝟙 Z) ≫
        ((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) W ((fun X Y => op (X.unop ⊗ Y.unop)) X Y) Z).hom ≫
          (fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) (𝟙 W)
            ((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) X Y Z).hom).unop =
    (((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) ((fun X Y => op (X.unop ⊗ Y.unop)) W X) Y Z).hom ≫
        ((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) W X ((fun X Y => op (X.unop ⊗ Y.unop)) Y Z)).hom).unop
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᵒᵖ
⊢ ((𝟙 W.unop ⊗ (α_ X.unop Y.unop Z.unop).inv) ≫ (α_ W.unop (X.unop ⊗ Y.unop) Z.unop).inv) ≫
      ((α_ W.unop X.unop Y.unop).inv ⊗ 𝟙 Z.unop) =
    (α_ W.unop X.unop (Y.unop ⊗ Z.unop)).inv ≫ (α_ (W.unop ⊗ X.unop) Y.unop Z.unop).inv
[PROOFSTEP]
coherence
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᵒᵖ
⊢ (((fun X Y Z => Iso.op (α_ X.unop Y.unop Z.unop).symm) X (op (𝟙_ C)) Y).hom ≫
        (fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) (𝟙 X) ((fun X => Iso.op (λ_ X.unop).symm) Y).hom).unop =
    ((fun {X₁ Y₁ X₂ Y₂} f g => (f.unop ⊗ g.unop).op) ((fun X => Iso.op (ρ_ X.unop).symm) X).hom (𝟙 Y)).unop
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᵒᵖ
⊢ (𝟙 X.unop ⊗ (λ_ Y.unop).inv) ≫ (α_ X.unop (𝟙_ C) Y.unop).inv = (ρ_ X.unop).inv ⊗ 𝟙 Y.unop
[PROOFSTEP]
coherence
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : Cᴹᵒᵖ
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
h : X₃✝ ⟶ Y₃✝
⊢ Quiver.Hom.unmop
      ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f))
          ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) f g) h ≫
        ((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) Y₁✝ Y₂✝ Y₃✝).hom) =
    Quiver.Hom.unmop
      (((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) X₁✝ X₂✝ X₃✝).hom ≫
        (fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) f
          ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) g h))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X✝ Y✝ : Cᴹᵒᵖ
f : X✝ ⟶ Y✝
⊢ Quiver.Hom.unmop
      ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) (𝟙 (mop (𝟙_ C))) f ≫
        ((fun X => Iso.mop (ρ_ (unmop X))) Y✝).hom) =
    Quiver.Hom.unmop (((fun X => Iso.mop (ρ_ (unmop X))) X✝).hom ≫ f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X✝ Y✝ : Cᴹᵒᵖ
f : X✝ ⟶ Y✝
⊢ Quiver.Hom.unmop
      ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) f (𝟙 (mop (𝟙_ C))) ≫
        ((fun X => Iso.mop (λ_ (unmop X))) Y✝).hom) =
    Quiver.Hom.unmop (((fun X => Iso.mop (λ_ (unmop X))) X✝).hom ≫ f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᴹᵒᵖ
⊢ Quiver.Hom.unmop
      ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f))
          ((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) W X Y).hom (𝟙 Z) ≫
        ((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) W ((fun X Y => mop (unmop Y ⊗ unmop X)) X Y)
              Z).hom ≫
          (fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) (𝟙 W)
            ((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) X Y Z).hom) =
    Quiver.Hom.unmop
      (((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) ((fun X Y => mop (unmop Y ⊗ unmop X)) W X) Y
            Z).hom ≫
        ((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) W X
            ((fun X Y => mop (unmop Y ⊗ unmop X)) Y Z)).hom)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
W X Y Z : Cᴹᵒᵖ
⊢ (𝟙 (unmop Z) ⊗ (α_ (unmop Y) (unmop X) (unmop W)).inv) ≫
      (α_ (unmop Z) (unmop Y ⊗ unmop X) (unmop W)).inv ≫ ((α_ (unmop Z) (unmop Y) (unmop X)).inv ⊗ 𝟙 (unmop W)) =
    (α_ (unmop Z) (unmop Y) (unmop X ⊗ unmop W)).inv ≫ (α_ (unmop Z ⊗ unmop Y) (unmop X) (unmop W)).inv
[PROOFSTEP]
coherence
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Cᴹᵒᵖ
⊢ Quiver.Hom.unmop
      (((fun X Y Z => Iso.mop (α_ (unmop Z) (unmop Y) (unmop X)).symm) X (mop (𝟙_ C)) Y).hom ≫
        (fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f)) (𝟙 X)
          ((fun X => Iso.mop (ρ_ (unmop X))) Y).hom) =
    Quiver.Hom.unmop
      ((fun {X₁ Y₁ X₂ Y₂} f g => Quiver.Hom.mop (Quiver.Hom.unmop g ⊗ Quiver.Hom.unmop f))
        ((fun X => Iso.mop (λ_ (unmop X))) X).hom (𝟙 Y))
[PROOFSTEP]
simp
