ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>self : CategoryTheory.EnrichedCategory V C<VAR>W X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.EnrichedCategory.Hom W X) (CategoryTheory.EnrichedCategory.Hom X Y) (CategoryTheory.EnrichedCategory.Hom Y Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.EnrichedCategory.comp W X Y) (CategoryTheory.EnrichedCategory.Hom Y Z)) (CategoryTheory.EnrichedCategory.comp W Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom W X) (CategoryTheory.EnrichedCategory.comp X Y Z)) (CategoryTheory.EnrichedCategory.comp W X Z)
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>self : CategoryTheory.EnrichedCategory V C<VAR>X Y : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.EnrichedCategory.Hom X Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.EnrichedCategory.id X) (CategoryTheory.EnrichedCategory.Hom X Y)) (CategoryTheory.EnrichedCategory.comp X X Y)) = CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom X Y)
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>CategoryTheory.EnrichedCategory V C<VAR>X Y : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.EnrichedCategory.Hom X Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.eId V X) (CategoryTheory.EnrichedCategory.Hom X Y)) (CategoryTheory.eComp V X X Y)) = CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom X Y)
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>CategoryTheory.EnrichedCategory V C<VAR>X Y : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.EnrichedCategory.Hom X Y)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom X Y) (CategoryTheory.eId V Y)) (CategoryTheory.eComp V X Y Y)) = CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom X Y)
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>CategoryTheory.EnrichedCategory V C<VAR>W X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.EnrichedCategory.Hom W X) (CategoryTheory.EnrichedCategory.Hom X Y) (CategoryTheory.EnrichedCategory.Hom Y Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.eComp V W X Y) (CategoryTheory.EnrichedCategory.Hom Y Z)) (CategoryTheory.eComp V W Y Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom W X) (CategoryTheory.eComp V X Y Z)) (CategoryTheory.eComp V W X Z)
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>CategoryTheory.EnrichedCategory V C<VAR>W X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.EnrichedCategory.Hom W X) (CategoryTheory.EnrichedCategory.Hom X Y) (CategoryTheory.EnrichedCategory.Hom Y Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom W X) (CategoryTheory.eComp V X Y Z)) (CategoryTheory.eComp V W X Z)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.eComp V W X Y) (CategoryTheory.EnrichedCategory.Hom Y Z)) (CategoryTheory.eComp V W Y Z)
<VAR>C : Type u₁<VAR>W : Type (v + 1)<VAR>CategoryTheory.Category.{v, v + 1} W<VAR>CategoryTheory.MonoidalCategory W<VAR>CategoryTheory.EnrichedCategory W C<VAR>X : C<GOAL>CategoryTheory.ForgetEnrichment.to W (CategoryTheory.ForgetEnrichment.of W X) = X
<VAR>C : Type u₁<VAR>W : Type (v + 1)<VAR>CategoryTheory.Category.{v, v + 1} W<VAR>CategoryTheory.MonoidalCategory W<VAR>CategoryTheory.EnrichedCategory W C<VAR>X : CategoryTheory.ForgetEnrichment W C<GOAL>CategoryTheory.ForgetEnrichment.of W (CategoryTheory.ForgetEnrichment.to W X) = X
<VAR>C : Type u₁<VAR>W : Type (v + 1)<VAR>CategoryTheory.Category.{v, v + 1} W<VAR>CategoryTheory.MonoidalCategory W<VAR>CategoryTheory.EnrichedCategory W C<VAR>X Y : C<VAR>f : 𝟙_ W ⟶ CategoryTheory.EnrichedCategory.Hom X Y<GOAL>CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.ForgetEnrichment.homOf W f) = f
<VAR>C : Type u₁<VAR>W : Type (v + 1)<VAR>CategoryTheory.Category.{v, v + 1} W<VAR>CategoryTheory.MonoidalCategory W<VAR>CategoryTheory.EnrichedCategory W C<VAR>X Y : CategoryTheory.ForgetEnrichment W C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.ForgetEnrichment.homOf W (CategoryTheory.ForgetEnrichment.homTo W f) = f
<VAR>C : Type u₁<VAR>W : Type (v + 1)<VAR>CategoryTheory.Category.{v, v + 1} W<VAR>CategoryTheory.MonoidalCategory W<VAR>CategoryTheory.EnrichedCategory W C<VAR>X : CategoryTheory.ForgetEnrichment W C<GOAL>CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.CategoryStruct.id X) = CategoryTheory.eId W (CategoryTheory.ForgetEnrichment.to W X)
<VAR>C : Type u₁<VAR>W : Type (v + 1)<VAR>CategoryTheory.Category.{v, v + 1} W<VAR>CategoryTheory.MonoidalCategory W<VAR>CategoryTheory.EnrichedCategory W C<VAR>X : C<GOAL>CategoryTheory.ForgetEnrichment.homOf W (CategoryTheory.eId W X) = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of W X)
<VAR>C : Type u₁<VAR>W : Type (v + 1)<VAR>CategoryTheory.Category.{v, v + 1} W<VAR>CategoryTheory.MonoidalCategory W<VAR>CategoryTheory.EnrichedCategory W C<VAR>X Y Z : CategoryTheory.ForgetEnrichment W C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ W)).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.ForgetEnrichment.homTo W f) (CategoryTheory.ForgetEnrichment.homTo W g))) (CategoryTheory.eComp W (CategoryTheory.ForgetEnrichment.to W X) (CategoryTheory.ForgetEnrichment.to W Y) (CategoryTheory.ForgetEnrichment.to W Z))
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>CategoryTheory.EnrichedCategory V C<VAR>D : Type u₂<VAR>CategoryTheory.EnrichedCategory V D<VAR>self : CategoryTheory.EnrichedFunctor V C D<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (self.map X X) = CategoryTheory.eId V (self.obj X)
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>CategoryTheory.EnrichedCategory V C<VAR>D : Type u₂<VAR>CategoryTheory.EnrichedCategory V D<VAR>self : CategoryTheory.EnrichedFunctor V C D<VAR>X Y Z : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.eComp V X Y Z) (self.map X Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.map X Y) (self.map Y Z)) (CategoryTheory.eComp V (self.obj X) (self.obj Y) (self.obj Z))
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>CategoryTheory.EnrichedCategory V C<VAR>X Y : C<GOAL>(CategoryTheory.EnrichedFunctor.id V C).map X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.EnrichedCategory.Hom X Y)
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>CategoryTheory.EnrichedCategory V C<VAR>X : C<GOAL>(CategoryTheory.EnrichedFunctor.id V C).obj X = X
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>CategoryTheory.EnrichedCategory V C<VAR>CategoryTheory.EnrichedCategory V D<VAR>CategoryTheory.EnrichedCategory V E<VAR>F : CategoryTheory.EnrichedFunctor V C D<VAR>G : CategoryTheory.EnrichedFunctor V D E<VAR>X : C<GOAL>(CategoryTheory.EnrichedFunctor.comp V F G).obj X = G.obj (F.obj X)
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>CategoryTheory.EnrichedCategory V C<VAR>CategoryTheory.EnrichedCategory V D<VAR>CategoryTheory.EnrichedCategory V E<VAR>F : CategoryTheory.EnrichedFunctor V C D<VAR>G : CategoryTheory.EnrichedFunctor V D E<VAR>X Y : C<GOAL>(CategoryTheory.EnrichedFunctor.comp V F G).map X Y = CategoryTheory.CategoryStruct.comp (F.map X Y) (G.map (F.obj X) (F.obj Y))
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>CategoryTheory.EnrichedCategory V C<VAR>D : Type u₂<VAR>CategoryTheory.EnrichedCategory V D<VAR>A : CategoryTheory.Center V<VAR>F G : CategoryTheory.EnrichedFunctor V C D<VAR>self : CategoryTheory.GradedNatTrans A F G<VAR>X Y : C<GOAL>CategoryTheory.CategoryStruct.comp (A.snd.β (CategoryTheory.EnrichedCategory.Hom X Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (F.map X Y) (self.app Y)) (CategoryTheory.eComp V (F.obj X) (F.obj Y) (G.obj Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (self.app X) (G.map X Y)) (CategoryTheory.eComp V (F.obj X) (G.obj X) (G.obj Y))
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>CategoryTheory.EnrichedCategory V C<VAR>D : Type u₂<VAR>CategoryTheory.EnrichedCategory V D<VAR>CategoryTheory.BraidedCategory V<VAR>F G : CategoryTheory.EnrichedFunctor V C D<VAR>A : Vᵒᵖ<GOAL>(CategoryTheory.enrichedNatTransYoneda F G).obj A = CategoryTheory.GradedNatTrans ((CategoryTheory.Center.ofBraided V).obj (Opposite.unop A)) F G
<VAR>V : Type v<VAR>CategoryTheory.Category.{w, v} V<VAR>CategoryTheory.MonoidalCategory V<VAR>C : Type u₁<VAR>CategoryTheory.EnrichedCategory V C<VAR>D : Type u₂<VAR>CategoryTheory.EnrichedCategory V D<VAR>CategoryTheory.BraidedCategory V<VAR>F G : CategoryTheory.EnrichedFunctor V C D<GOAL>∀ {X Y : Vᵒᵖ} (f : X ⟶ Y) (σ : CategoryTheory.GradedNatTrans ((CategoryTheory.Center.ofBraided V).obj (Opposite.unop X)) F G) (X_1 : C), ((CategoryTheory.enrichedNatTransYoneda F G).map f σ).app X_1 = CategoryTheory.CategoryStruct.comp f.unop (σ.app X_1)
<VAR>C : Type u₁<VAR>𝒞 : CategoryTheory.EnrichedCategory (Type v) C<VAR>D : Type u₂<VAR>𝒟 : CategoryTheory.EnrichedCategory (Type v) D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>(CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F).obj X = F.obj X
<VAR>C : Type u₁<VAR>𝒞 : CategoryTheory.EnrichedCategory (Type v) C<VAR>D : Type u₂<VAR>𝒟 : CategoryTheory.EnrichedCategory (Type v) D<VAR>F : CategoryTheory.EnrichedFunctor (Type v) C D<VAR>X : C<GOAL>(CategoryTheory.enrichedFunctorTypeEquivFunctor F).obj X = F.obj X
<VAR>C : Type u₁<VAR>𝒞 : CategoryTheory.EnrichedCategory (Type v) C<VAR>D : Type u₂<VAR>𝒟 : CategoryTheory.EnrichedCategory (Type v) D<VAR>F : CategoryTheory.EnrichedFunctor (Type v) C D<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.enrichedFunctorTypeEquivFunctor F).map f = F.map X Y f
<VAR>C : Type u₁<VAR>𝒞 : CategoryTheory.EnrichedCategory (Type v) C<VAR>D : Type u₂<VAR>𝒟 : CategoryTheory.EnrichedCategory (Type v) D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : C<VAR>f : CategoryTheory.EnrichedCategory.Hom X Y<GOAL>(CategoryTheory.enrichedFunctorTypeEquivFunctor.symm F).map X Y f = F.map f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)<GOAL>(CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ({ obj := fun X => X, map := fun {X Y} f => f, map_id := ⋯, map_comp := ⋯ }.obj X) ({ obj := fun X => X, map := fun {X Y} f => f, map_id := ⋯, map_comp := ⋯ }.obj Y))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).ε = CategoryTheory.CategoryStruct.id (𝟙_ C)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)<GOAL>(CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).obj X = X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>∀ {X Y : CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)} (f : X ⟶ Y), (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).map f = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence C).counitIso = CategoryTheory.Iso.refl ({ obj := fun X => X, map := fun {X Y} f => f, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).toFunctor)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<GOAL>(CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence C).inverse.obj X = X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.EndMonoidal (CategoryTheory.MonoidalSingleObj.star C)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence C).functor = (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor C).toFunctor
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence C).inverse.map f = f
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>self : CategoryTheory.StrongOplaxNatTrans F G<VAR>a : B<GOAL>CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)).hom (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).hom (CategoryTheory.Bicategory.rightUnitor (self.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>self : CategoryTheory.StrongOplaxNatTrans F G<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b)) (self.naturality g).hom = CategoryTheory.CategoryStruct.comp (self.naturality f).hom (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>self : CategoryTheory.StrongOplaxNatTrans F G<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)).hom (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f).hom (G.map g)) (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).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>η : CategoryTheory.StrongOplaxNatTrans F G<GOAL>∀ {a b : B} (f : a ⟶ b), η.toOplax.naturality f = (η.naturality f).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>η : CategoryTheory.StrongOplaxNatTrans F G<VAR>a : B<GOAL>η.toOplax.app a = η.app a
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<GOAL>∀ {a b : B} (f : a ⟶ b), ((CategoryTheory.StrongOplaxNatTrans.id F).naturality f).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom (CategoryTheory.Bicategory.rightUnitor (F.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<GOAL>∀ {a b : B} (f : a ⟶ b), ((CategoryTheory.StrongOplaxNatTrans.id F).naturality f).hom = 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 : CategoryTheory.OplaxFunctor B C<VAR>a : B<GOAL>(CategoryTheory.StrongOplaxNatTrans.id F).app a = CategoryTheory.CategoryStruct.id (F.obj a)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.OplaxFunctor B C<GOAL>(CategoryTheory.StrongOplaxNatTrans.id F).toOplax = CategoryTheory.OplaxNatTrans.id F
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>G H : CategoryTheory.OplaxFunctor B C<VAR>θ : CategoryTheory.StrongOplaxNatTrans G H<VAR>a b : B<VAR>a' : C<VAR>f : a' ⟶ G.obj a<VAR>g h : a ⟶ b<VAR>β : g ⟶ h<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) (θ.app b))) (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality h).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g).hom) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.map₂ β)))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>η : CategoryTheory.StrongOplaxNatTrans F G<VAR>a b : B<VAR>a' : C<VAR>f g : a ⟶ b<VAR>β : f ⟶ g<VAR>h : G.obj b ⟶ a'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.map₂ β) (η.app b)) h) (CategoryTheory.Bicategory.whiskerRight (η.naturality g).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) h)) (CategoryTheory.Bicategory.associator (η.app a) (G.map g) h).inv))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>G H : CategoryTheory.OplaxFunctor B C<VAR>θ : CategoryTheory.StrongOplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f : a' ⟶ G.obj a<VAR>g : a ⟶ b<VAR>h : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.comp g h)).hom) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapComp g h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapComp g h) (θ.app c))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (G.map g) (θ.naturality h).hom)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (θ.naturality g).hom (H.map h))) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator (θ.app a) (H.map g) (H.map h)).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>η : CategoryTheory.StrongOplaxNatTrans F G<VAR>a b c : B<VAR>a' : C<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : G.obj c ⟶ a'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.comp f g)).hom h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.comp f g)) h).hom (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapComp f g) h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (η.app c)) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (η.app c)).hom h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) (η.app c)) h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (CategoryTheory.Bicategory.whiskerRight (η.naturality g).hom h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (η.app b) (G.map g)) h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (G.map g)).inv h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom (G.map g)) h) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (G.map g)).hom h) (CategoryTheory.Bicategory.associator (η.app a) (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) h).hom)))))))
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>G H : CategoryTheory.OplaxFunctor B C<VAR>θ : CategoryTheory.StrongOplaxNatTrans G H<VAR>a : B<VAR>a' : C<VAR>f : a' ⟶ G.obj a<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.id a)).hom) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapId a))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapId a) (θ.app a))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor (θ.app a)).hom) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor (θ.app a)).inv))