ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>CategoryTheory.Category.{u_15, u_1} C₁<VAR>CategoryTheory.Category.{u_16, u_2} C₂<VAR>CategoryTheory.Category.{u_14, u_3} C₃<VAR>CategoryTheory.Category.{u_11, u_4} C₄<VAR>CategoryTheory.Category.{u_13, u_5} C₁₂<VAR>F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)<VAR>G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q<VAR>H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃<VAR>j : J<VAR>A : C₄<VAR>f g : CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ A<VAR>h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) g<GOAL>f = g
<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>self : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r<VAR>i : I₁ × I₂ × I₃<GOAL>self.q (i.1, self.p i.2) = r i
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₂₃ : Type u_6<VAR>CategoryTheory.Category.{u_14, u_1} C₁<VAR>CategoryTheory.Category.{u_16, u_2} C₂<VAR>CategoryTheory.Category.{u_15, u_3} C₃<VAR>CategoryTheory.Category.{u_12, u_4} C₄<VAR>CategoryTheory.Category.{u_13, u_6} C₂₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)<VAR>G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<VAR>i₂₃ : ρ₂₃.I₂₃<VAR>h₂₃ : ρ₂₃.p (i₂, i₃) = i₂₃<GOAL>CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h = CategoryTheory.CategoryStruct.comp ((F.obj (X₁ i₁)).map (CategoryTheory.GradedObject.ιMapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃ i₂ i₃ i₂₃ h₂₃)) (CategoryTheory.GradedObject.ιMapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) i₁ i₂₃ j ⋯)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₂₃ : Type u_6<VAR>CategoryTheory.Category.{u_14, u_1} C₁<VAR>CategoryTheory.Category.{u_13, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_11, u_4} C₄<VAR>CategoryTheory.Category.{u_15, u_6} C₂₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)<VAR>G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<GOAL>((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₂₃ : Type u_6<VAR>CategoryTheory.Category.{u_14, u_1} C₁<VAR>CategoryTheory.Category.{u_13, u_2} C₂<VAR>CategoryTheory.Category.{u_12, u_3} C₃<VAR>CategoryTheory.Category.{u_11, u_4} C₄<VAR>CategoryTheory.Category.{u_15, u_6} C₂₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)<VAR>G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j) = CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₂₃ : Type u_6<VAR>CategoryTheory.Category.{u_13, u_1} C₁<VAR>CategoryTheory.Category.{u_15, u_2} C₂<VAR>CategoryTheory.Category.{u_14, u_3} C₃<VAR>CategoryTheory.Category.{u_11, u_4} C₄<VAR>CategoryTheory.Category.{u_12, u_6} C₂₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)<VAR>G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>((((CategoryTheory.GradedObject.mapTrifunctor (CategoryTheory.bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₃ : I₃<VAR>j : J<VAR>h : r (i₁, i₂, i₃) = j<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ((CategoryTheory.GradedObject.mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).inv j) = CategoryTheory.GradedObject.ιMapTrifunctorMapObj (CategoryTheory.bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₂₃ : Type u_6<VAR>CategoryTheory.Category.{u_13, u_1} C₁<VAR>CategoryTheory.Category.{u_15, u_2} C₂<VAR>CategoryTheory.Category.{u_16, u_3} C₃<VAR>CategoryTheory.Category.{u_11, u_4} C₄<VAR>CategoryTheory.Category.{u_14, u_6} C₂₃<VAR>F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)<VAR>G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)<VAR>I₁ : Type u_7<VAR>I₂ : Type u_8<VAR>I₃ : Type u_9<VAR>J : Type u_10<VAR>r : I₁ × I₂ × I₃ → J<VAR>ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r<VAR>X₁ : CategoryTheory.GradedObject I₁ C₁<VAR>X₂ : CategoryTheory.GradedObject I₂ C₂<VAR>X₃ : CategoryTheory.GradedObject I₃ C₃<VAR>(((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p<VAR>(((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q<VAR>H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃<VAR>j : J<VAR>A : C₄<VAR>f g : CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁ (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶ A<VAR>h : ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) g<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>A : Mon_ (C ⥤ D)<VAR>X : C<GOAL>((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj A).obj X).X = A.X.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>A : Mon_ (C ⥤ D)<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj A).map f).hom = A.X.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>A : Mon_ (C ⥤ D)<VAR>X : C<GOAL>((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj A).obj X).mul = A.mul.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>A : Mon_ (C ⥤ D)<VAR>X : C<GOAL>((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj A).obj X).one = A.one.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<GOAL>∀ {X Y : Mon_ (C ⥤ D)} (f : X ⟶ Y) (X_1 : C), ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor.map f).app X_1).hom = f.hom.app X_1
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>A : Mon_ (C ⥤ D)<GOAL>CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor.obj A = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C ⥤ Mon_ D<VAR>X : C<GOAL>(CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F).one.app X = (F.obj X).one
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C ⥤ Mon_ D<GOAL>(CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F).X = F ⋙ Mon_.forget D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C ⥤ Mon_ D<VAR>X : C<GOAL>(CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F).mul.app X = (F.obj X).mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C ⥤ Mon_ D<GOAL>CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse.obj F = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<GOAL>∀ {X Y : C ⥤ Mon_ D} (α : X ⟶ Y) (X_1 : C), (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse.map α).hom.app X_1 = (α.app X_1).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>X : Mon_ (C ⥤ D)<GOAL>∀ (x : C), (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso.inv.app X).hom.app x = 𝟙 (X.X.obj x)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>X : Mon_ (C ⥤ D)<GOAL>∀ (x : C), (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso.hom.app X).hom.app x = 𝟙 (X.X.obj x)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>X : C ⥤ Mon_ D<GOAL>∀ (X_1 : C), ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso.hom.app X).app X_1).hom = 𝟙 (X.obj X_1).X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>X : C ⥤ Mon_ D<GOAL>∀ (X_1 : C), ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso.inv.app X).app X_1).hom = 𝟙 (X.obj X_1).X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<GOAL>(CategoryTheory.Monoidal.monFunctorCategoryEquivalence C D).counitIso = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<GOAL>(CategoryTheory.Monoidal.monFunctorCategoryEquivalence C D).unitIso = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<GOAL>(CategoryTheory.Monoidal.monFunctorCategoryEquivalence C D).functor = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<GOAL>(CategoryTheory.Monoidal.monFunctorCategoryEquivalence C D).inverse = CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>A : Comon_ (C ⥤ D)<VAR>X : C<GOAL>((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj A).obj X).counit = A.counit.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>A : Comon_ (C ⥤ D)<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj A).map f).hom = A.X.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>A : Comon_ (C ⥤ D)<VAR>X : C<GOAL>((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj A).obj X).comul = A.comul.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>A : Comon_ (C ⥤ D)<VAR>X : C<GOAL>((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj A).obj X).X = A.X.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<GOAL>∀ {X Y : Comon_ (C ⥤ D)} (f : X ⟶ Y) (X_1 : C), ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor.map f).app X_1).hom = f.hom.app X_1
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>A : Comon_ (C ⥤ D)<GOAL>CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor.obj A = CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C ⥤ Comon_ D<VAR>X : C<GOAL>(CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj F).comul.app X = (F.obj X).comul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C ⥤ Comon_ D<GOAL>(CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj F).X = F ⋙ Comon_.forget D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C ⥤ Comon_ D<VAR>X : C<GOAL>(CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj F).counit.app X = (F.obj X).counit
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : C ⥤ Comon_ D<GOAL>CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse.obj F = CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<GOAL>∀ {X Y : C ⥤ Comon_ D} (α : X ⟶ Y) (X_1 : C), (CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse.map α).hom.app X_1 = (α.app X_1).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>X : Comon_ (C ⥤ D)<GOAL>∀ (x : C), (CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.unitIso.inv.app X).hom.app x = 𝟙 (X.X.obj x)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>X : Comon_ (C ⥤ D)<GOAL>∀ (x : C), (CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.unitIso.hom.app X).hom.app x = 𝟙 (X.X.obj x)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>X : C ⥤ Comon_ D<GOAL>∀ (X_1 : C), ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso.hom.app X).app X_1).hom = 𝟙 (X.obj X_1).X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>X : C ⥤ Comon_ D<GOAL>∀ (X_1 : C), ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso.inv.app X).app X_1).hom = 𝟙 (X.obj X_1).X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<GOAL>(CategoryTheory.Monoidal.comonFunctorCategoryEquivalence C D).inverse = CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<GOAL>(CategoryTheory.Monoidal.comonFunctorCategoryEquivalence C D).functor = CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<GOAL>(CategoryTheory.Monoidal.comonFunctorCategoryEquivalence C D).counitIso = CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<GOAL>(CategoryTheory.Monoidal.comonFunctorCategoryEquivalence C D).unitIso = CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.unitIso
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<GOAL>∀ {X Y : CommMon_ (C ⥤ D)} (f : X ⟶ Y) (X_1 : C), ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.map f).app X_1).hom = f.hom.app X_1
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>A : CommMon_ (C ⥤ D)<GOAL>∀ {X Y : C} (a : X ⟶ Y), ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).map a).hom = A.X.map a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>A : CommMon_ (C ⥤ D)<VAR>X : C<GOAL>((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).obj X).mul = A.mul.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>A : CommMon_ (C ⥤ D)<VAR>X : C<GOAL>((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).obj X).one = A.one.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>A : CommMon_ (C ⥤ D)<VAR>X : C<GOAL>((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj A).obj X).X = A.X.obj X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<GOAL>∀ {X Y : C ⥤ CommMon_ D} (α : X ⟶ Y) (X_1 : C), (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.map α).hom.app X_1 = (α.app X_1).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F : C ⥤ CommMon_ D<VAR>X : C<GOAL>(CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).mul.app X = (F.obj X).mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F : C ⥤ CommMon_ D<VAR>X : C<GOAL>(CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).X.obj X = ((CommMon_.forget₂Mon_ D).obj (F.obj X)).X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F : C ⥤ CommMon_ D<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).X.map f = (F.map f).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>F : C ⥤ CommMon_ D<VAR>X : C<GOAL>(CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse.obj F).one.app X = (F.obj X).one
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>X : CommMon_ (C ⥤ D)<GOAL>∀ (x : C), (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso.inv.app X).hom.app x = 𝟙 ((CommMon_.forget₂Mon_ D).obj ((CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor.obj X).obj x)).X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>CategoryTheory.BraidedCategory D<VAR>X : CommMon_ (C ⥤ D)<GOAL>∀ (x : C), (CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso.hom.app X).hom.app x = 𝟙 (X.X.obj x)