ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type (u + 1)<VAR>CategoryTheory.Category.{u_1, u + 1} C<VAR>CategoryTheory.ConcreteCategory C<VAR>D : Type (u + 1)<VAR>CategoryTheory.Category.{u_2, u + 1} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.HasForget₂ C D<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<GOAL>(CategoryTheory.forget₂ C D).ReflectsIsomorphisms
<VAR>B : Type u₁<VAR>Quiver B<VAR>(a b : B) → Quiver (a ⟶ b)<VAR>C : Type u₂<VAR>Quiver C<VAR>(a b : C) → Quiver (a ⟶ b)<VAR>F : B → C<VAR>F' : (a b : B) → (a ⟶ b) ⥤q (F a ⟶ F b)<VAR>a b : B<GOAL>∀ (a_1 : a ⟶ b), (CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F').map a_1 = (F' a b).obj a_1
<VAR>B : Type u₁<VAR>Quiver B<VAR>(a b : B) → Quiver (a ⟶ b)<VAR>C : Type u₂<VAR>Quiver C<VAR>(a b : C) → Quiver (a ⟶ b)<VAR>F : B → C<VAR>F' : (a b : B) → (a ⟶ b) ⥤q (F a ⟶ F b)<VAR>a b : B<GOAL>∀ {f g : a ⟶ b} (a_1 : f ⟶ g), (CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F').map₂ a_1 = (F' a b).map a_1
<VAR>B : Type u₁<VAR>Quiver B<VAR>(a b : B) → Quiver (a ⟶ b)<VAR>C : Type u₂<VAR>Quiver C<VAR>(a b : C) → Quiver (a ⟶ b)<VAR>F : B → C<VAR>F' : (a b : B) → (a ⟶ b) ⥤q (F a ⟶ F b)<GOAL>∀ (a : B), (CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F').obj a = F a
<VAR>B : Type u₁<VAR>Quiver B<VAR>(a b : B) → Quiver (a ⟶ b)<GOAL>(CategoryTheory.PrelaxFunctorStruct.id B).toPrefunctor = 𝟭q B
<VAR>B : Type u₁<VAR>Quiver B<VAR>(a b : B) → Quiver (a ⟶ b)<GOAL>∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), (CategoryTheory.PrelaxFunctorStruct.id B).map₂ η = η
<VAR>B : Type u₁<VAR>Quiver B<VAR>(a b : B) → Quiver (a ⟶ b)<VAR>C : Type u₂<VAR>Quiver C<VAR>(a b : C) → Quiver (a ⟶ b)<VAR>D : Type u₃<VAR>Quiver D<VAR>(a b : D) → Quiver (a ⟶ b)<VAR>F : CategoryTheory.PrelaxFunctorStruct B C<VAR>G : CategoryTheory.PrelaxFunctorStruct C D<GOAL>∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), (F.comp G).map₂ η = G.map₂ (F.map₂ η)
<VAR>B : Type u₁<VAR>Quiver B<VAR>(a b : B) → Quiver (a ⟶ b)<VAR>C : Type u₂<VAR>Quiver C<VAR>(a b : C) → Quiver (a ⟶ b)<VAR>D : Type u₃<VAR>Quiver D<VAR>(a b : D) → Quiver (a ⟶ b)<VAR>F : CategoryTheory.PrelaxFunctorStruct B C<VAR>G : CategoryTheory.PrelaxFunctorStruct C D<GOAL>(F.comp G).toPrefunctor = F.toPrefunctor ⋙q G.toPrefunctor
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.PrelaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>self.map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id (self.map f)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>self : CategoryTheory.PrelaxFunctor B C<VAR>a b : B<VAR>f g h : a ⟶ b<VAR>η : f ⟶ g<VAR>θ : g ⟶ h<GOAL>self.map₂ (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (self.map₂ η) (self.map₂ θ)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : B → C<VAR>F' : (a b : B) → CategoryTheory.Functor (a ⟶ b) (F a ⟶ F b)<GOAL>(CategoryTheory.PrelaxFunctor.mkOfHomFunctors F F').toPrelaxFunctorStruct = CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F fun a b => (F' a b).toPrefunctor
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<GOAL>(CategoryTheory.PrelaxFunctor.id B).toPrelaxFunctorStruct = CategoryTheory.PrelaxFunctorStruct.id B
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>D : Type u₃<VAR>CategoryTheory.Bicategory D<VAR>F : CategoryTheory.PrelaxFunctor B C<VAR>G : CategoryTheory.PrelaxFunctor C D<GOAL>(F.comp G).toPrelaxFunctorStruct = F.comp G.toPrelaxFunctorStruct
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.PrelaxFunctor B C<VAR>a b : B<GOAL>∀ {X Y : a ⟶ b} (η : X ⟶ Y), (F.mapFunctor a b).map η = F.map₂ η
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.PrelaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(F.mapFunctor a b).obj f = F.map f
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : B → C<VAR>F' : (a b : B) → CategoryTheory.Functor (a ⟶ b) (F a ⟶ F b)<VAR>a b : B<GOAL>(CategoryTheory.PrelaxFunctor.mkOfHomFunctors F F').mapFunctor a b = F' a b
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.PrelaxFunctor B C<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ≅ g<GOAL>(F.map₂Iso η).inv = F.map₂ η.inv
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.PrelaxFunctor B C<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ≅ g<GOAL>(F.map₂Iso η).hom = F.map₂ η.hom
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.PrelaxFunctor B C<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<VAR>CategoryTheory.IsIso η<GOAL>F.map₂ (CategoryTheory.inv η) = CategoryTheory.inv (F.map₂ η)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.PrelaxFunctor B C<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ≅ g<GOAL>CategoryTheory.CategoryStruct.comp (F.map₂ η.hom) (F.map₂ η.inv) = CategoryTheory.CategoryStruct.id (F.map f)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.PrelaxFunctor B C<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<VAR>CategoryTheory.IsIso η<GOAL>CategoryTheory.CategoryStruct.comp (F.map₂ η) (F.map₂ (CategoryTheory.inv η)) = CategoryTheory.CategoryStruct.id (F.map f)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.PrelaxFunctor B C<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ≅ g<GOAL>CategoryTheory.CategoryStruct.comp (F.map₂ η.inv) (F.map₂ η.hom) = CategoryTheory.CategoryStruct.id (F.map g)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.PrelaxFunctor B C<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<VAR>CategoryTheory.IsIso η<GOAL>CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.inv η)) (F.map₂ η) = CategoryTheory.CategoryStruct.id (F.map g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : Function.Injective ⇑f<GOAL>CategoryTheory.Mono f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<GOAL>CategoryTheory.MorphismProperty.surjective C ≤ CategoryTheory.MorphismProperty.epimorphisms C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<GOAL>CategoryTheory.MorphismProperty.injective C ≤ CategoryTheory.MorphismProperty.monomorphisms C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<GOAL>CategoryTheory.MorphismProperty.surjective C = CategoryTheory.MorphismProperty.epimorphisms C ↔ (CategoryTheory.forget C).PreservesEpimorphisms
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<GOAL>CategoryTheory.MorphismProperty.injective C = CategoryTheory.MorphismProperty.monomorphisms C ↔ (CategoryTheory.forget C).PreservesMonomorphisms
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>(CategoryTheory.forget C).PreservesMonomorphisms<GOAL>CategoryTheory.MorphismProperty.injective C = CategoryTheory.MorphismProperty.monomorphisms C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>(CategoryTheory.forget C).PreservesEpimorphisms<GOAL>CategoryTheory.MorphismProperty.surjective C = CategoryTheory.MorphismProperty.epimorphisms C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget C)<GOAL>Function.Injective ⇑f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget C)<GOAL>CategoryTheory.Mono f ↔ Function.Injective ⇑f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>s : Function.Surjective ⇑f<GOAL>CategoryTheory.Epi f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<VAR>CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan (CategoryTheory.forget C)<GOAL>Function.Surjective ⇑f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan (CategoryTheory.forget C)<GOAL>CategoryTheory.Epi f ↔ Function.Surjective ⇑f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>Function.Bijective ((CategoryTheory.forget C).map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>(CategoryTheory.forget C).ReflectsIsomorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso f ↔ Function.Bijective ((CategoryTheory.forget C).map f)
<VAR>c : Type u → Type v<VAR>α : Type u<VAR>str : c α<GOAL>↑{ α := α, str := str } = α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : Comon_ C<GOAL>self.comul ≫ self.X ◁ self.comul = self.comul ≫ self.comul ▷ self.X ≫ (α_ self.X self.X self.X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : Comon_ C<GOAL>self.comul ≫ self.X ◁ self.counit = (ρ_ self.X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : Comon_ C<GOAL>self.comul ≫ self.counit ▷ self.X = (λ_ self.X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Comon_.trivial C).counit = 𝟙 (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Comon_.trivial C).comul = (λ_ (𝟙_ C)).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Comon_.trivial C).X = 𝟙_ C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M : Comon_ C<VAR>Z : C<VAR>f : M.X ⟶ Z<GOAL>M.comul ≫ (M.counit ⊗ f) = f ≫ (λ_ Z).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M : Comon_ C<VAR>Z : C<VAR>f : M.X ⟶ Z<GOAL>M.comul ≫ (f ⊗ M.counit) = f ≫ (ρ_ Z).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M : Comon_ C<GOAL>M.comul ≫ M.comul ▷ M.X = M.comul ≫ M.X ◁ M.comul ≫ (α_ M.X M.X M.X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M N : Comon_ C<VAR>self : M.Hom N<GOAL>self.hom ≫ N.counit = M.counit
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M N : Comon_ C<VAR>self : M.Hom N<GOAL>self.hom ≫ N.comul = M.comul ≫ (self.hom ⊗ self.hom)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M : Comon_ C<GOAL>M.id.hom = 𝟙 M.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M N O : Comon_ C<VAR>f : M.Hom N<VAR>g : N.Hom O<GOAL>(Comon_.comp f g).hom = f.hom ≫ g.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : Comon_ C<VAR>f g : X ⟶ Y<VAR>w : f.hom = g.hom<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M : Comon_ C<GOAL>(𝟙 M).hom = 𝟙 M.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M N K : Comon_ 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>A : Comon_ C<GOAL>(Comon_.forget C).obj A = A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>∀ {X Y : Comon_ C} (f : X ⟶ Y), (Comon_.forget C).map f = f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M N : Comon_ C<VAR>f : M.X ≅ N.X<VAR>f_counit : f.hom ≫ N.counit = M.counit := by aesop_cat<VAR>f_comul : f.hom ≫ N.comul = M.comul ≫ (f.hom ⊗ f.hom) := by aesop_cat<GOAL>(Comon_.mkIso f f_counit f_comul).inv.hom = f.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M N : Comon_ C<VAR>f : M.X ≅ N.X<VAR>f_counit : f.hom ≫ N.counit = M.counit := by aesop_cat<VAR>f_comul : f.hom ≫ N.comul = M.comul ≫ (f.hom ⊗ f.hom) := by aesop_cat<GOAL>(Comon_.mkIso f f_counit f_comul).hom.hom = f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Comon_ C<GOAL>(Comon_.Comon_ToMon_OpOp_obj' C A).one = A.counit.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Comon_ C<GOAL>(Comon_.Comon_ToMon_OpOp_obj' C A).mul = A.comul.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Comon_ C<GOAL>(Comon_.Comon_ToMon_OpOp_obj' C A).X = Opposite.op A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>∀ {X Y : Comon_ C} (f : X ⟶ Y), (Comon_.Comon_ToMon_OpOp C).map f = Opposite.op { hom := f.hom.op, one_hom := ⋯, mul_hom := ⋯ }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Comon_ C<GOAL>(Comon_.Comon_ToMon_OpOp C).obj A = Opposite.op (Comon_.Comon_ToMon_OpOp_obj' C A)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ Cᵒᵖ<GOAL>(Comon_.Mon_OpOpToComon_obj' C A).counit = A.one.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ Cᵒᵖ<GOAL>(Comon_.Mon_OpOpToComon_obj' C A).comul = A.mul.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : Mon_ Cᵒᵖ<GOAL>(Comon_.Mon_OpOpToComon_obj' C A).X = Opposite.unop A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>∀ {X Y : (Mon_ Cᵒᵖ)ᵒᵖ} (f : X ⟶ Y), ((Comon_.Mon_OpOpToComon_ C).map f).hom = f.unop.hom.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : (Mon_ Cᵒᵖ)ᵒᵖ<GOAL>(Comon_.Mon_OpOpToComon_ C).obj A = Comon_.Mon_OpOpToComon_obj' C (Opposite.unop A)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Comon_.Comon_EquivMon_OpOp C).unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((𝟭 (Comon_ C)).obj x)) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Comon_.Comon_EquivMon_OpOp C).inverse = Comon_.Mon_OpOpToComon_ C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Comon_.Comon_EquivMon_OpOp C).functor = Comon_.Comon_ToMon_OpOp C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Comon_.Comon_EquivMon_OpOp C).counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((Comon_.Mon_OpOpToComon_ C ⋙ Comon_.Comon_ToMon_OpOp C).obj x)) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A B : Comon_ C<GOAL>(A ⊗ B).X = A.X ⊗ B.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A B : Comon_ C<GOAL>(A ⊗ B).counit = (A.counit ⊗ B.counit) ≫ (λ_ (𝟙_ C)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A B : Comon_ C<GOAL>(A ⊗ B).comul = (A.comul ⊗ B.comul) ≫ (CategoryTheory.tensor_μ Cᵒᵖ (Opposite.op A.X, Opposite.op B.X) (Opposite.op A.X, Opposite.op B.X)).unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>A B : Comon_ C<GOAL>(A ⊗ B).comul = (A.comul ⊗ B.comul) ≫ CategoryTheory.tensor_μ C (A.X, A.X) (B.X, B.X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(Comon_.forgetMonoidal C).toFunctor = Comon_.forget C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<GOAL>(Comon_.forgetMonoidal C).ε = 𝟙 (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.BraidedCategory C<VAR>X Y : Comon_ C<GOAL>(Comon_.forgetMonoidal C).μ X Y = 𝟙 (X.X ⊗ Y.X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : CategoryTheory.OplaxMonoidalFunctor C D<VAR>A : Comon_ C<GOAL>(F.mapComon.obj A).comul = F.map A.comul ≫ F.δ A.X A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : CategoryTheory.OplaxMonoidalFunctor C D<GOAL>∀ {X Y : Comon_ C} (f : X ⟶ Y), (F.mapComon.map f).hom = F.map f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : CategoryTheory.OplaxMonoidalFunctor C D<VAR>A : Comon_ C<GOAL>(F.mapComon.obj A).X = F.obj A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>CategoryTheory.MonoidalCategory D<VAR>F : CategoryTheory.OplaxMonoidalFunctor C D<VAR>A : Comon_ C<GOAL>(F.mapComon.obj A).counit = F.map A.counit ≫ F.η
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G H : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<VAR>θ ι : G ⟶ H<VAR>Γ : θ ⟶ ι<VAR>a : B<GOAL>(CategoryTheory.OplaxNatTrans.whiskerLeft η Γ).app a = CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.app a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G H : CategoryTheory.OplaxFunctor B C<VAR>η θ : F ⟶ G<VAR>Γ : η ⟶ θ<VAR>ι : G ⟶ H<VAR>a : B<GOAL>(CategoryTheory.OplaxNatTrans.whiskerRight Γ ι).app a = CategoryTheory.Bicategory.whiskerRight (Γ.app a) (ι.app a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G H I : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<VAR>θ : G ⟶ H<VAR>ι : H ⟶ I<VAR>a : B<GOAL>(CategoryTheory.OplaxNatTrans.associator η θ ι).inv.app a = (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G H I : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<VAR>θ : G ⟶ H<VAR>ι : H ⟶ I<VAR>a : B<GOAL>(CategoryTheory.OplaxNatTrans.associator η θ ι).hom.app a = (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<VAR>a : B<GOAL>(CategoryTheory.OplaxNatTrans.leftUnitor η).hom.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<VAR>a : B<GOAL>(CategoryTheory.OplaxNatTrans.leftUnitor η).inv.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).inv
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<VAR>a : B<GOAL>(CategoryTheory.OplaxNatTrans.rightUnitor η).hom.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<VAR>a : B<GOAL>(CategoryTheory.OplaxNatTrans.rightUnitor η).inv.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<VAR>a : B<GOAL>(CategoryTheory.Bicategory.rightUnitor η).hom.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).hom
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>a b : CategoryTheory.OplaxFunctor B C<VAR>η : a ⟶ b<GOAL>∀ (a_1 : B), (CategoryTheory.CategoryStruct.id η).app a_1 = CategoryTheory.CategoryStruct.id (η.app a_1)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<GOAL>∀ {X Y Z : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.OplaxNatTrans X Y) (θ : CategoryTheory.OplaxNatTrans Y Z) {a b : B} (f : a ⟶ b), (CategoryTheory.CategoryStruct.comp η θ).naturality f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (X.map f) (η.app b) (θ.app b)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) (θ.app b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (Y.map f) (θ.app b)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f)) (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (Z.map f)).inv)))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(CategoryTheory.CategoryStruct.id F).naturality f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G H : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<GOAL>∀ (x x_1 : G ⟶ H) (Γ : x ⟶ x_1) (a : B), (CategoryTheory.Bicategory.whiskerLeft η Γ).app a = CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.app a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G H : CategoryTheory.OplaxFunctor B C<VAR>I : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<VAR>θ : G ⟶ H<VAR>ι : H ⟶ I<VAR>a : B<GOAL>(CategoryTheory.Bicategory.associator η θ ι).hom.app a = (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G H : CategoryTheory.OplaxFunctor B C<VAR>I : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<VAR>θ : G ⟶ H<VAR>ι : H ⟶ I<VAR>a : B<GOAL>(CategoryTheory.Bicategory.associator η θ ι).inv.app a = (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>a b : CategoryTheory.OplaxFunctor B C<GOAL>∀ {X Y Z : a ⟶ b} (Γ : CategoryTheory.OplaxNatTrans.Modification X Y) (Δ : CategoryTheory.OplaxNatTrans.Modification Y Z) (a_1 : B), (CategoryTheory.CategoryStruct.comp Γ Δ).app a_1 = CategoryTheory.CategoryStruct.comp (Γ.app a_1) (Δ.app a_1)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>η : F ⟶ G<VAR>a : B<GOAL>(CategoryTheory.Bicategory.rightUnitor η).inv.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv