ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>Opposite.op (CategoryTheory.MonoidalCategory.tensorObj X Y) = CategoryTheory.MonoidalCategory.tensorObj (Opposite.op X) (Opposite.op Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : Cᵒᵖ<GOAL>Opposite.unop (CategoryTheory.MonoidalCategory.tensorObj X Y) = CategoryTheory.MonoidalCategory.tensorObj (Opposite.unop X) (Opposite.unop Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>Opposite.op (𝟙_ C) = 𝟙_ Cᵒᵖ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>Opposite.unop (𝟙_ Cᵒᵖ) = 𝟙_ C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ Y₁ X₂ Y₂ : C<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>(CategoryTheory.MonoidalCategory.tensorHom f g).op = CategoryTheory.MonoidalCategory.tensorHom f.op g.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ Y₁ X₂ Y₂ : Cᵒᵖ<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>(CategoryTheory.MonoidalCategory.tensorHom f g).unop = CategoryTheory.MonoidalCategory.tensorHom f.unop g.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ⟶ Z<GOAL>(CategoryTheory.MonoidalCategory.whiskerLeft X f).op = CategoryTheory.MonoidalCategory.whiskerLeft (Opposite.op X) f.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᵒᵖ<VAR>Y Z : Cᵒᵖ<VAR>f : Y ⟶ Z<GOAL>(CategoryTheory.MonoidalCategory.whiskerLeft X f).unop = CategoryTheory.MonoidalCategory.whiskerLeft (Opposite.unop X) f.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>(CategoryTheory.MonoidalCategory.whiskerRight f Z).op = CategoryTheory.MonoidalCategory.whiskerRight f.op (Opposite.op Z)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>Z : Cᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.whiskerRight f Z).unop = CategoryTheory.MonoidalCategory.whiskerRight f.unop (Opposite.unop Z)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).op = (CategoryTheory.MonoidalCategory.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : Cᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).unop = (CategoryTheory.MonoidalCategory.associator (Opposite.unop X) (Opposite.unop Y) (Opposite.unop Z)).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).hom.op = (CategoryTheory.MonoidalCategory.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : Cᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).hom.unop = (CategoryTheory.MonoidalCategory.associator (Opposite.unop X) (Opposite.unop Y) (Opposite.unop Z)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).inv.op = (CategoryTheory.MonoidalCategory.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : Cᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).inv.unop = (CategoryTheory.MonoidalCategory.associator (Opposite.unop X) (Opposite.unop Y) (Opposite.unop Z)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).op = (CategoryTheory.MonoidalCategory.leftUnitor (Opposite.op X)).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).unop = (CategoryTheory.MonoidalCategory.leftUnitor (Opposite.unop X)).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).hom.op = (CategoryTheory.MonoidalCategory.leftUnitor (Opposite.op X)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).hom.unop = (CategoryTheory.MonoidalCategory.leftUnitor (Opposite.unop X)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).inv.op = (CategoryTheory.MonoidalCategory.leftUnitor (Opposite.op X)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).inv.unop = (CategoryTheory.MonoidalCategory.leftUnitor (Opposite.unop X)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).op = (CategoryTheory.MonoidalCategory.rightUnitor (Opposite.op X)).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).unop = (CategoryTheory.MonoidalCategory.rightUnitor (Opposite.unop X)).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).hom.op = (CategoryTheory.MonoidalCategory.rightUnitor (Opposite.op X)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).hom.unop = (CategoryTheory.MonoidalCategory.rightUnitor (Opposite.unop X)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).inv.op = (CategoryTheory.MonoidalCategory.rightUnitor (Opposite.op X)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).inv.unop = (CategoryTheory.MonoidalCategory.rightUnitor (Opposite.unop X)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.MonoidalCategory.tensorHom f.op g.op = (CategoryTheory.MonoidalCategory.tensorHom f g).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : Cᵒᵖ<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.MonoidalCategory.tensorHom f.unop g.unop = (CategoryTheory.MonoidalCategory.tensorHom f g).unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>{ unmop := CategoryTheory.MonoidalCategory.tensorObj X Y } = CategoryTheory.MonoidalCategory.tensorObj { unmop := Y } { unmop := X }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.tensorObj X Y).unmop = CategoryTheory.MonoidalCategory.tensorObj Y.unmop X.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>{ unmop := 𝟙_ C } = 𝟙_ Cᴹᵒᵖ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(𝟙_ Cᴹᵒᵖ).unmop = 𝟙_ C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ Y₁ X₂ Y₂ : C<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>(CategoryTheory.MonoidalCategory.tensorHom f g).mop = CategoryTheory.MonoidalCategory.tensorHom g.mop f.mop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X₁ Y₁ X₂ Y₂ : Cᴹᵒᵖ<VAR>f : X₁ ⟶ Y₁<VAR>g : X₂ ⟶ Y₂<GOAL>(CategoryTheory.MonoidalCategory.tensorHom f g).unmop = CategoryTheory.MonoidalCategory.tensorHom g.unmop f.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ⟶ Z<GOAL>(CategoryTheory.MonoidalCategory.whiskerLeft X f).mop = CategoryTheory.MonoidalCategory.whiskerRight f.mop { unmop := X }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<VAR>Y Z : Cᴹᵒᵖ<VAR>f : Y ⟶ Z<GOAL>(CategoryTheory.MonoidalCategory.whiskerLeft X f).unmop = CategoryTheory.MonoidalCategory.whiskerRight f.unmop X.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>(CategoryTheory.MonoidalCategory.whiskerRight f Z).mop = CategoryTheory.MonoidalCategory.whiskerLeft { unmop := Z } f.mop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : Cᴹᵒᵖ<VAR>f : X ⟶ Y<VAR>Z : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.whiskerRight f Z).unmop = CategoryTheory.MonoidalCategory.whiskerLeft Z.unmop f.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).mop = (CategoryTheory.MonoidalCategory.associator { unmop := Z } { unmop := Y } { unmop := X }).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).unmop = (CategoryTheory.MonoidalCategory.associator Z.unmop Y.unmop X.unmop).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).hom.mop = (CategoryTheory.MonoidalCategory.associator { unmop := Z } { unmop := Y } { unmop := X }).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).hom.unmop = (CategoryTheory.MonoidalCategory.associator Z.unmop Y.unmop X.unmop).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).inv.mop = (CategoryTheory.MonoidalCategory.associator { unmop := Z } { unmop := Y } { unmop := X }).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).inv.unmop = (CategoryTheory.MonoidalCategory.associator Z.unmop Y.unmop X.unmop).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).mop = CategoryTheory.MonoidalCategory.rightUnitor { unmop := X }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).unmop = CategoryTheory.MonoidalCategory.rightUnitor X.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).hom.mop = (CategoryTheory.MonoidalCategory.rightUnitor { unmop := X }).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).hom.unmop = (CategoryTheory.MonoidalCategory.rightUnitor X.unmop).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).inv.mop = (CategoryTheory.MonoidalCategory.rightUnitor { unmop := X }).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).inv.unmop = (CategoryTheory.MonoidalCategory.rightUnitor X.unmop).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).mop = CategoryTheory.MonoidalCategory.leftUnitor { unmop := X }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).unmop = CategoryTheory.MonoidalCategory.leftUnitor X.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).hom.mop = (CategoryTheory.MonoidalCategory.leftUnitor { unmop := X }).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).hom.unmop = (CategoryTheory.MonoidalCategory.leftUnitor X.unmop).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).inv.mop = (CategoryTheory.MonoidalCategory.leftUnitor { unmop := X }).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).inv.unmop = (CategoryTheory.MonoidalCategory.leftUnitor X.unmop).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>(CategoryTheory.MonoidalOpposite.mopEquiv C).inverse = CategoryTheory.unmopFunctor C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>(CategoryTheory.MonoidalOpposite.mopEquiv C).counitIso = CategoryTheory.Iso.refl (CategoryTheory.unmopFunctor C ⋙ CategoryTheory.mopFunctor C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>(CategoryTheory.MonoidalOpposite.mopEquiv C).functor = CategoryTheory.mopFunctor C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>(CategoryTheory.MonoidalOpposite.mopEquiv C).unitIso = CategoryTheory.Iso.refl (𝟭 C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Cᴹᵒᵖ<GOAL>((CategoryTheory.MonoidalOpposite.unmopEquiv C).unitIso.inv.app X).unmop = 𝟙 X.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>unmop : C<GOAL>((CategoryTheory.MonoidalOpposite.unmopEquiv C).inverse.obj unmop).unmop = unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.MonoidalOpposite.unmopEquiv C).inverse.map f).unmop = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : Cᴹᵒᵖ} (f : X ⟶ Y), (CategoryTheory.MonoidalOpposite.unmopEquiv C).functor.map f = f.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.MonoidalOpposite.unmopEquiv C).counitIso.inv.app X = 𝟙 X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Cᴹᵒᵖ<GOAL>((CategoryTheory.MonoidalOpposite.unmopEquiv C).unitIso.hom.app X).unmop = 𝟙 X.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>self : Cᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalOpposite.unmopEquiv C).functor.obj self = self.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.MonoidalOpposite.unmopEquiv C).counitIso.hom.app X = 𝟙 X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : Cᴹᵒᵖᴹᵒᵖ} (f : X ⟶ Y), (CategoryTheory.MonoidalOpposite.mopMopEquivalence C).functor.map f = f.unmop.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Cᴹᵒᵖᴹᵒᵖ<GOAL>((CategoryTheory.MonoidalOpposite.mopMopEquivalence C).unitIso.hom.app X).unmop.unmop = (𝟙 X.unmop).unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.MonoidalOpposite.mopMopEquivalence C).counitIso.hom.app X = 𝟙 X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>((CategoryTheory.MonoidalOpposite.mopMopEquivalence C).inverse.obj X).unmop.unmop = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.MonoidalOpposite.mopMopEquivalence C).inverse.map f).unmop.unmop = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.MonoidalOpposite.mopMopEquivalence C).counitIso.inv.app X = 𝟙 X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Cᴹᵒᵖᴹᵒᵖ<GOAL>((CategoryTheory.MonoidalOpposite.mopMopEquivalence C).unitIso.inv.app X).unmop.unmop = (𝟙 X.unmop).unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Cᴹᵒᵖᴹᵒᵖ<GOAL>(CategoryTheory.MonoidalOpposite.mopMopEquivalence C).functor.obj X = X.unmop.unmop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ × Cᴹᵒᵖ<GOAL>((CategoryTheory.MonoidalOpposite.tensorIso C).hom.app X).unmop = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X.2.unmop X.1.unmop)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ × Cᴹᵒᵖ<GOAL>((CategoryTheory.MonoidalOpposite.tensorIso C).inv.app X).unmop = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X.2.unmop X.1.unmop)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>∀ (X_1 : Cᴹᵒᵖ), (X.tensorLeftIso.hom.app X_1).unmop = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X_1.unmop X.unmop)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>∀ (X_1 : Cᴹᵒᵖ), (X.tensorLeftIso.inv.app X_1).unmop = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X_1.unmop X.unmop)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>∀ (X_1 : Cᴹᵒᵖ), ((CategoryTheory.MonoidalOpposite.tensorLeftMopIso X).hom.app X_1).unmop = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X_1.unmop X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>∀ (X_1 : Cᴹᵒᵖ), ((CategoryTheory.MonoidalOpposite.tensorLeftMopIso X).inv.app X_1).unmop = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X_1.unmop X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>∀ (X_1 : C), X.tensorLeftUnmopIso.hom.app X_1 = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X.unmop X_1)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>∀ (X_1 : C), X.tensorLeftUnmopIso.inv.app X_1 = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X.unmop X_1)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>∀ (X_1 : Cᴹᵒᵖ), (X.tensorRightIso.inv.app X_1).unmop = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X.unmop X_1.unmop)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>∀ (X_1 : Cᴹᵒᵖ), (X.tensorRightIso.hom.app X_1).unmop = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X.unmop X_1.unmop)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>∀ (X_1 : Cᴹᵒᵖ), ((CategoryTheory.MonoidalOpposite.tensorRightMopIso X).inv.app X_1).unmop = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X X_1.unmop)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>∀ (X_1 : Cᴹᵒᵖ), ((CategoryTheory.MonoidalOpposite.tensorRightMopIso X).hom.app X_1).unmop = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X X_1.unmop)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>∀ (X_1 : C), X.tensorRightUnmopIso.inv.app X_1 = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X_1 X.unmop)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : Cᴹᵒᵖ<GOAL>∀ (X_1 : C), X.tensorRightUnmopIso.hom.app X_1 = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X_1 X.unmop)
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y W Z : Cᵒᵖ<GOAL>(CategoryTheory.tensor_μ Cᵒᵖ (X, W) (Y, Z)).unop = CategoryTheory.tensor_μ C (Opposite.unop X, Opposite.unop Y) (Opposite.unop W, Opposite.unop Z)
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y W Z : C<GOAL>(CategoryTheory.tensor_μ C (X, W) (Y, Z)).op = CategoryTheory.tensor_μ Cᵒᵖ (Opposite.op X, Opposite.op Y) (Opposite.op W, Opposite.op Z)
<VAR>R : Type u_1<VAR>Semiring R<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>self : CategoryTheory.MonoidalLinear R C<VAR>r : R<VAR>Y Z : C<VAR>f : Y ⟶ Z<VAR>X : C<GOAL>CategoryTheory.MonoidalCategory.whiskerRight (r • f) X = r • CategoryTheory.MonoidalCategory.whiskerRight f X
<VAR>R : Type u_1<VAR>Semiring R<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>self : CategoryTheory.MonoidalLinear R C<VAR>X : C<VAR>Y Z : C<VAR>r : R<VAR>f : Y ⟶ Z<GOAL>CategoryTheory.MonoidalCategory.whiskerLeft X (r • f) = r • CategoryTheory.MonoidalCategory.whiskerLeft X f
<VAR>R : Type u_1<VAR>Semiring R<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalPreadditive C<VAR>CategoryTheory.MonoidalLinear R C<VAR>D : Type u_3<VAR>CategoryTheory.Category.{u_4, u_3} D<VAR>CategoryTheory.Preadditive D<VAR>CategoryTheory.Linear R D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.MonoidalPreadditive D<VAR>F : CategoryTheory.MonoidalFunctor D C<VAR>F.Faithful<VAR>F.Additive<VAR>CategoryTheory.Functor.Linear R F.toFunctor<GOAL>CategoryTheory.MonoidalLinear R D
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>self : CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>X Y : C<GOAL>P X → P Y → P (CategoryTheory.MonoidalCategory.tensorObj X Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>self : CategoryTheory.MonoidalCategory.MonoidalPredicate P<GOAL>P (𝟙_ C)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>X : CategoryTheory.FullSubcategory P<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).inv = (CategoryTheory.MonoidalCategory.rightUnitor X.obj).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>X Y Z : CategoryTheory.FullSubcategory P<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).inv = (CategoryTheory.MonoidalCategory.associator X.obj Y.obj Z.obj).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<GOAL>∀ {X₁ Y₁ X₂ Y₂ : CategoryTheory.FullSubcategory P} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), CategoryTheory.MonoidalCategory.tensorHom f g = CategoryTheory.MonoidalCategory.tensorHom f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>P : C → Prop<VAR>CategoryTheory.MonoidalCategory.MonoidalPredicate P<VAR>X₁ X₂ : CategoryTheory.FullSubcategory P<VAR>f : X₁.obj ⟶ X₂.obj<VAR>Y : CategoryTheory.FullSubcategory P<GOAL>CategoryTheory.MonoidalCategory.whiskerRight f Y = CategoryTheory.MonoidalCategory.whiskerRight f Y.obj