ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G H : CategoryTheory.Functor C C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.associator F G H).hom.app X = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj F G) H).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F G H : CategoryTheory.Functor C C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.associator F G H).inv.app X = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorObj F (CategoryTheory.MonoidalCategory.tensorObj G H)).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor F).hom.app X = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorObj (𝟙_ (CategoryTheory.Functor C C)) F).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor F).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor F).hom.app X = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorObj F (𝟙_ (CategoryTheory.Functor C C))).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor C C<VAR>X : C<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor F).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>∀ (X_1 : C), ((CategoryTheory.tensoringRightMonoidal C).μ X Y).app X_1 = (CategoryTheory.MonoidalCategory.associator X_1 X Y).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.tensoringRightMonoidal C).ε.app X = (CategoryTheory.MonoidalCategory.rightUnitor X).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>k j : C<GOAL>((CategoryTheory.tensoringRightMonoidal C).obj k).obj j = CategoryTheory.MonoidalCategory.tensorObj j k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>k : C<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.tensoringRightMonoidal C).obj k).map f = CategoryTheory.MonoidalCategory.whiskerRight f k
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>∀ {X Y : C} (f : X ⟶ Y) (j : C), ((CategoryTheory.tensoringRightMonoidal C).map f).app j = CategoryTheory.MonoidalCategory.whiskerLeft j f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>i j : M<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((F.μ i j).app X) ((F.μIso i j).inv.app X) = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategory.tensorObj (F.obj i) (F.obj j)).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>i j : M<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((F.μIso i j).inv.app X) ((F.μ i j).app X) = CategoryTheory.CategoryStruct.id ((F.obj (CategoryTheory.MonoidalCategory.tensorObj i j)).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (F.ε.app X) (F.εIso.inv.app X) = CategoryTheory.CategoryStruct.id ((𝟙_ (CategoryTheory.Functor C C)).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (F.εIso.inv.app X) (F.ε.app X) = CategoryTheory.CategoryStruct.id ((F.obj (𝟙_ M)).obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (F.ε.app X) ((F.obj (𝟙_ M)).map f) = CategoryTheory.CategoryStruct.comp f (F.ε.app Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (F.εIso.inv.app X) ((𝟙_ (CategoryTheory.Functor C C)).map f) = CategoryTheory.CategoryStruct.comp (F.εIso.inv.app X) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m n : M<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp ((F.obj n).map ((F.obj m).map f)) ((F.μ m n).app Y) = CategoryTheory.CategoryStruct.comp ((F.μ m n).app X) ((F.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m n : M<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp ((F.μIso m n).inv.app X) ((F.obj n).map ((F.obj m).map f)) = CategoryTheory.CategoryStruct.comp ((F.obj (CategoryTheory.MonoidalCategory.tensorObj m n)).map f) ((F.μIso m n).inv.app Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m n m' n' : M<VAR>f : m ⟶ m'<VAR>g : n ⟶ n'<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) (CategoryTheory.CategoryStruct.comp ((F.obj n').map ((F.map f).app X)) ((F.μ m' n').app X)) = CategoryTheory.CategoryStruct.comp ((F.μ m n).app X) ((F.map (CategoryTheory.MonoidalCategory.tensorHom f g)).app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m n m' : M<VAR>f : m ⟶ m'<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) ((F.μ m' n).app X) = CategoryTheory.CategoryStruct.comp ((F.μ m n).app X) ((F.map (CategoryTheory.MonoidalCategory.whiskerRight f n)).app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m n n' : M<VAR>g : n ⟶ n'<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) ((F.μ m n').app X) = CategoryTheory.CategoryStruct.comp ((F.μ m n).app X) ((F.map (CategoryTheory.MonoidalCategory.whiskerLeft m g)).app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m n m' : M<VAR>f : m ⟶ m'<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((F.μIso m n).inv.app X) ((F.obj n).map ((F.map f).app X)) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.whiskerRight f n)).app X) ((F.μIso m' n).inv.app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m n n' : M<VAR>g : n ⟶ n'<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((F.μIso m n).inv.app X) ((F.map g).app ((F.obj m).obj X)) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.whiskerLeft m g)).app X) ((F.μIso m n').inv.app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>n : M<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((F.obj n).map (F.ε.app X)) (CategoryTheory.CategoryStruct.comp ((F.μ (𝟙_ M) n).app X) ((F.map (CategoryTheory.MonoidalCategory.leftUnitor n).hom).app X)) = CategoryTheory.CategoryStruct.id ((F.obj n).obj ((𝟙_ (CategoryTheory.Functor C C)).obj X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>n : M<VAR>X : C<GOAL>(F.obj n).map (F.ε.app X) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.leftUnitor n).inv).app X) ((F.μIso (𝟙_ M) n).inv.app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>n : M<VAR>X : C<GOAL>(F.obj n).map (F.εIso.inv.app X) = CategoryTheory.CategoryStruct.comp ((F.μ (𝟙_ M) n).app X) ((F.map (CategoryTheory.MonoidalCategory.leftUnitor n).hom).app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>n : M<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (F.ε.app ((F.obj n).obj X)) (CategoryTheory.CategoryStruct.comp ((F.μ n (𝟙_ M)).app X) ((F.map (CategoryTheory.MonoidalCategory.rightUnitor n).hom).app X)) = CategoryTheory.CategoryStruct.id ((𝟙_ (CategoryTheory.Functor C C)).obj ((F.obj n).obj X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>n : M<VAR>X : C<GOAL>F.ε.app ((F.obj n).obj X) = CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.rightUnitor n).inv).app X) ((F.μIso n (𝟙_ M)).inv.app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>n : M<VAR>X : C<GOAL>F.εIso.inv.app ((F.obj n).obj X) = CategoryTheory.CategoryStruct.comp ((F.μ n (𝟙_ M)).app X) ((F.map (CategoryTheory.MonoidalCategory.rightUnitor n).hom).app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m₁ m₂ m₃ : M<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((F.obj m₃).map ((F.μ m₁ m₂).app X)) (CategoryTheory.CategoryStruct.comp ((F.μ (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂) m₃).app X) ((F.map (CategoryTheory.MonoidalCategory.associator m₁ m₂ m₃).hom).app X)) = CategoryTheory.CategoryStruct.comp ((F.μ m₂ m₃).app ((F.obj m₁).obj X)) ((F.μ m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m₁ m₂ m₃ : M<VAR>X : C<GOAL>(F.obj m₃).map ((F.μ m₁ m₂).app X) = CategoryTheory.CategoryStruct.comp ((F.μ m₂ m₃).app ((F.obj m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((F.μ m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).app X) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.associator m₁ m₂ m₃).inv).app X) ((F.μIso (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂) m₃).inv.app X)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m₁ m₂ m₃ : M<VAR>X : C<GOAL>(F.obj m₃).map ((F.μIso m₁ m₂).inv.app X) = CategoryTheory.CategoryStruct.comp ((F.μ (CategoryTheory.MonoidalCategory.tensorObj m₁ m₂) m₃).app X) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.associator m₁ m₂ m₃).hom).app X) (CategoryTheory.CategoryStruct.comp ((F.μIso m₁ (CategoryTheory.MonoidalCategory.tensorObj m₂ m₃)).inv.app X) ((F.μIso m₂ m₃).inv.app ((F.obj m₁).obj X))))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m : M<VAR>X Y : C<VAR>f : X ⟶ (F.obj m).obj Y<GOAL>CategoryTheory.CategoryStruct.comp ((F.obj (𝟙_ M)).map f) ((F.μ m (𝟙_ M)).app Y) = CategoryTheory.CategoryStruct.comp (F.εIso.inv.app X) (CategoryTheory.CategoryStruct.comp f ((F.map (CategoryTheory.MonoidalCategory.rightUnitor m).inv).app Y))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m₁ m₂ : M<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((F.μ (𝟙_ M) m₂).app ((F.obj m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((F.μ m₁ (CategoryTheory.MonoidalCategory.tensorObj (𝟙_ M) m₂)).app X) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.associator m₁ (𝟙_ M) m₂).inv).app X) ((F.μIso (CategoryTheory.MonoidalCategory.tensorObj m₁ (𝟙_ M)) m₂).inv.app X))) = CategoryTheory.CategoryStruct.comp ((F.μ (𝟙_ M) m₂).app ((F.obj m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategory.leftUnitor m₂).hom).app ((F.obj m₁).obj X)) ((F.obj m₂).map ((F.map (CategoryTheory.MonoidalCategory.rightUnitor m₁).inv).app X)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m n : M<VAR>h : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M<VAR>X : C<GOAL>(CategoryTheory.unitOfTensorIsoUnit F m n h).hom.app X = CategoryTheory.CategoryStruct.comp ((F.μ m n).app X) (CategoryTheory.CategoryStruct.comp ((F.map h.hom).app X) (F.εIso.inv.app X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m n : M<VAR>h : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M<VAR>X : C<GOAL>(CategoryTheory.unitOfTensorIsoUnit F m n h).inv.app X = CategoryTheory.CategoryStruct.comp (F.ε.app X) (CategoryTheory.CategoryStruct.comp ((F.map h.inv).app X) ((F.μIso m n).inv.app X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m n : M<VAR>h₁ : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M<VAR>h₂ : CategoryTheory.MonoidalCategory.tensorObj n m ≅ 𝟙_ M<VAR>H : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight h₁.hom m) (CategoryTheory.MonoidalCategory.leftUnitor m).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator m n m).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft m h₂.hom) (CategoryTheory.MonoidalCategory.rightUnitor m).hom)<GOAL>(CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).inverse = F.obj n
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m n : M<VAR>h₁ : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M<VAR>h₂ : CategoryTheory.MonoidalCategory.tensorObj n m ≅ 𝟙_ M<VAR>H : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight h₁.hom m) (CategoryTheory.MonoidalCategory.leftUnitor m).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator m n m).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft m h₂.hom) (CategoryTheory.MonoidalCategory.rightUnitor m).hom)<GOAL>(CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).functor = F.obj m
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m n : M<VAR>h₁ : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M<VAR>h₂ : CategoryTheory.MonoidalCategory.tensorObj n m ≅ 𝟙_ M<VAR>H : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight h₁.hom m) (CategoryTheory.MonoidalCategory.leftUnitor m).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator m n m).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft m h₂.hom) (CategoryTheory.MonoidalCategory.rightUnitor m).hom)<GOAL>(CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).counitIso = CategoryTheory.unitOfTensorIsoUnit F n m h₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>M : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} M<VAR>CategoryTheory.MonoidalCategory M<VAR>F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)<VAR>m n : M<VAR>h₁ : CategoryTheory.MonoidalCategory.tensorObj m n ≅ 𝟙_ M<VAR>h₂ : CategoryTheory.MonoidalCategory.tensorObj n m ≅ 𝟙_ M<VAR>H : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight h₁.hom m) (CategoryTheory.MonoidalCategory.leftUnitor m).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator m n m).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft m h₂.hom) (CategoryTheory.MonoidalCategory.rightUnitor m).hom)<GOAL>(CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).unitIso = (CategoryTheory.unitOfTensorIsoUnit F m n h₁).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Bimon_ C<VAR>f g : X ⟶ Y<VAR>w : f.hom.hom = g.hom.hom<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M : Bimon_ C<GOAL>(𝟙 M).hom = 𝟙 M.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M N K : Bimon_ C<VAR>f : M ⟶ N<VAR>g : N ⟶ K<GOAL>(f ≫ g).hom = f.hom ≫ g.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>Bimon_.toMon_ C ⋙ Mon_.forget C = Bimon_.forget C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>∀ {X Y : Comon_ (Mon_ C)} (f : X ⟶ Y), ((Bimon_.toComon_ C).map f).hom = f.hom.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A : Comon_ (Mon_ C)<GOAL>((Bimon_.toComon_ C).obj A).counit = A.counit.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A : Comon_ (Mon_ C)<GOAL>((Bimon_.toComon_ C).obj A).comul = A.comul.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A : Comon_ (Mon_ C)<GOAL>((Bimon_.toComon_ C).obj A).X = A.X.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>Bimon_.toComon_ C ⋙ Comon_.forget C = Bimon_.forget C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>∀ {X Y : Bimon_ C} (f : X ⟶ Y), ((Bimon_.toMon_Comon_ C).map f).hom = (Bimon_.toComon_ C).map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M : Bimon_ C<GOAL>(Bimon_.toMon_Comon_ C).obj M = Bimon_.toMon_Comon_obj C M
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M : Mon_ (Comon_ C)<GOAL>(Bimon_.ofMon_Comon_obj C M).comul.hom = M.X.comul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M : Mon_ (Comon_ C)<GOAL>(Bimon_.ofMon_Comon_obj C M).X = (Comon_.forgetMonoidal C).mapMon.obj M
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M : Mon_ (Comon_ C)<GOAL>(Bimon_.ofMon_Comon_obj C M).counit.hom = M.X.counit
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>∀ {X Y : Mon_ (Comon_ C)} (f : X ⟶ Y), ((Bimon_.ofMon_Comon_ C).map f).hom = (Comon_.forgetMonoidal C).mapMon.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>M : Mon_ (Comon_ C)<GOAL>(Bimon_.ofMon_Comon_ C).obj M = Bimon_.ofMon_Comon_obj C M
<VAR>M : Type u<VAR>Monoid M<VAR>x : CategoryTheory.SingleObj M<GOAL>𝟙 x = 1
<VAR>M : Type u<VAR>Monoid M<VAR>x y z : CategoryTheory.SingleObj M<VAR>f : x ⟶ y<VAR>g : y ⟶ z<GOAL>f ≫ g = g * f
<VAR>G : Type u<VAR>Group G<VAR>x y : CategoryTheory.SingleObj G<VAR>f : x ⟶ y<GOAL>CategoryTheory.inv f = f⁻¹
<VAR>M : Type u<VAR>Monoid M<VAR>x : M<GOAL>(CategoryTheory.SingleObj.toEnd M) x = x
<VAR>M : Type u<VAR>Monoid M<GOAL>(CategoryTheory.SingleObj.mapHom M M) (MonoidHom.id M) = 𝟭 (CategoryTheory.SingleObj M)
<VAR>M : Type u<VAR>Monoid M<VAR>N : Type v<VAR>Monoid N<VAR>f : M →* N<VAR>P : Type w<VAR>Monoid P<VAR>g : N →* P<GOAL>(CategoryTheory.SingleObj.mapHom M P) (g.comp f) = (CategoryTheory.SingleObj.mapHom M N) f ⋙ (CategoryTheory.SingleObj.mapHom N P) g
<VAR>G : Type u<VAR>Group G<VAR>C : Type v<VAR>CategoryTheory.Category.{w, v} C<VAR>f : C → G<GOAL>∀ (x : C), (CategoryTheory.SingleObj.differenceFunctor f).obj x = ()
<VAR>G : Type u<VAR>Group G<VAR>C : Type v<VAR>CategoryTheory.Category.{w, v} C<VAR>f : C → G<VAR>x y : C<GOAL>∀ (x_1 : x ⟶ y), (CategoryTheory.SingleObj.differenceFunctor f).map x_1 = f y * (f x)⁻¹
<VAR>M : Type u<VAR>Monoid M<VAR>C : Type v<VAR>CategoryTheory.Category.{w, v} C<VAR>X : C<VAR>f : M →* CategoryTheory.End X<GOAL>∀ (x : CategoryTheory.SingleObj M), (CategoryTheory.SingleObj.functor f).obj x = X
<VAR>M : Type u<VAR>Monoid M<VAR>C : Type v<VAR>CategoryTheory.Category.{w, v} C<VAR>X : C<VAR>f : M →* CategoryTheory.End X<GOAL>∀ {X_1 Y : CategoryTheory.SingleObj M} (a : X_1 ⟶ Y), (CategoryTheory.SingleObj.functor f).map a = f a
<VAR>M : Type u<VAR>Monoid M<VAR>C : Type v<VAR>CategoryTheory.Category.{w, v} C<VAR>F G : CategoryTheory.SingleObj M ⥤ C<VAR>u : F.obj (CategoryTheory.SingleObj.star M) ⟶ G.obj (CategoryTheory.SingleObj.star M)<VAR>h : ∀ (a : M), F.map a ≫ u = u ≫ G.map a<GOAL>∀ (x : CategoryTheory.SingleObj M), (CategoryTheory.SingleObj.natTrans u h).app x = u
<VAR>M : Type u<VAR>N : Type v<VAR>Monoid M<VAR>Monoid N<VAR>f : M →* N<VAR>P : Type w<VAR>Monoid P<VAR>g : N →* P<GOAL>(g.comp f).toFunctor = f.toFunctor ⋙ g.toFunctor