ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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.OplaxNatTrans 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)) 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) 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) (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.OplaxNatTrans 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))) (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))
<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.OplaxNatTrans F G<VAR>a : B<VAR>a' : C<VAR>f : G.obj a ⟶ a'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.id a)) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.id a)) f).hom (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.mapId a) f))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (η.app a)) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv f) (CategoryTheory.Bicategory.associator (η.app a) (CategoryTheory.CategoryStruct.id (G.obj a)) f).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>η : CategoryTheory.OplaxNatTrans F G<VAR>θ : CategoryTheory.OplaxNatTrans G H<VAR>a : B<GOAL>(η.vcomp θ).app a = CategoryTheory.CategoryStruct.comp (η.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>η : CategoryTheory.OplaxNatTrans F G<VAR>θ : CategoryTheory.OplaxNatTrans G H<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(η.vcomp θ).naturality f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.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) (G.map f) (θ.app b)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f)) (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (H.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>CategoryTheory.CategoryStruct.id F = CategoryTheory.OplaxNatTrans.id F
<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), CategoryTheory.CategoryStruct.comp η θ = η.vcomp θ
<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>self : CategoryTheory.OplaxNatTrans.Modification η θ<VAR>a b : B<VAR>f : a ⟶ b<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b)) (θ.naturality f) = CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map 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>η : F ⟶ G<VAR>a : B<GOAL>(CategoryTheory.OplaxNatTrans.Modification.id η).app a = CategoryTheory.CategoryStruct.id (η.app a)
<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>Γ : CategoryTheory.OplaxNatTrans.Modification η θ<VAR>b c : B<VAR>a' : C<VAR>f : a' ⟶ F.obj b<VAR>g : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (F.map g) (Γ.app c))) (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (η.naturality g)) (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (Γ.app b) (G.map g)))
<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>Γ : CategoryTheory.OplaxNatTrans.Modification η θ<VAR>a b : B<VAR>a' : C<VAR>f : a ⟶ b<VAR>g : G.obj b ⟶ a'<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (CategoryTheory.Bicategory.whiskerRight (Γ.app b) g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (θ.app b) g).inv (CategoryTheory.Bicategory.whiskerRight (θ.naturality f) g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (η.app b) g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) g) (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (Γ.app a) (G.map f)) g))
<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>Γ : CategoryTheory.OplaxNatTrans.Modification η θ<VAR>Δ : CategoryTheory.OplaxNatTrans.Modification θ ι<VAR>a : B<GOAL>(Γ.vcomp Δ).app a = CategoryTheory.CategoryStruct.comp (Γ.app a) (Δ.app a)
<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<GOAL>CategoryTheory.CategoryStruct.id η = CategoryTheory.OplaxNatTrans.Modification.id η
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F G : CategoryTheory.OplaxFunctor B C<GOAL>∀ {X Y Z : F ⟶ G} (Γ : CategoryTheory.OplaxNatTrans.Modification X Y) (Δ : CategoryTheory.OplaxNatTrans.Modification Y Z), CategoryTheory.CategoryStruct.comp Γ Δ = Γ.vcomp Δ
<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>m n : α ⟶ β<VAR>w : ∀ (b : B), m.app b = n.app b<GOAL>m = n
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>X : B<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>α : F ⟶ G<GOAL>(CategoryTheory.CategoryStruct.id α).app X = CategoryTheory.CategoryStruct.id (α.app X)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>X : B<VAR>F G : CategoryTheory.OplaxFunctor B C<VAR>α β γ : F ⟶ G<VAR>m : α ⟶ β<VAR>n : β ⟶ γ<GOAL>(CategoryTheory.CategoryStruct.comp m n).app X = CategoryTheory.CategoryStruct.comp (m.app X) (n.app X)
<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>app : (a : B) → η.app a ≅ θ.app a<VAR>naturality : ∀ {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom) (θ.naturality f) = CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))<VAR>a : B<GOAL>(CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents app naturality).inv.app a = (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>app : (a : B) → η.app a ≅ θ.app a<VAR>naturality : ∀ {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (app b).hom) (θ.naturality f) = CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerRight (app a).hom (G.map f))<VAR>a : B<GOAL>(CategoryTheory.OplaxNatTrans.ModificationIso.ofComponents app naturality).hom.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>η : CategoryTheory.OplaxNatTrans F G<VAR>self : η.StrongCore<VAR>a b : B<VAR>f : a ⟶ b<GOAL>(self.naturality f).hom = η.naturality f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>α β : F ⟶ G<VAR>w : α.app = β.app<GOAL>α = β
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G H : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>β : G ⟶ H<GOAL>CategoryTheory.NatTrans.vcomp α β = CategoryTheory.CategoryStruct.comp α β
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G H : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>β : G ⟶ H<VAR>X : C<GOAL>(CategoryTheory.CategoryStruct.comp α β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>α β : F ⟶ G<VAR>h : α = β<VAR>X : C<GOAL>α.app X = β.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>(CategoryTheory.CategoryStruct.id F).app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F G : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>T : F ⟶ G<VAR>X : C<VAR>Y Z : D<VAR>f : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp ((F.obj X).map f) ((T.app X).app Z) = CategoryTheory.CategoryStruct.comp ((T.app X).app Y) ((G.obj X).map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F G : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>T : F ⟶ G<VAR>Z : D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp ((F.map f).app Z) ((T.app Y).app Z) = CategoryTheory.CategoryStruct.comp ((T.app X).app Z) ((G.map f).app Z)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>∀ (X : C), CategoryTheory.Mono (α.app X)<GOAL>CategoryTheory.Mono α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>∀ (X : C), CategoryTheory.Epi (α.app X)<GOAL>CategoryTheory.Epi α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>α β : CategoryTheory.Functor.id C ⟶ CategoryTheory.Functor.id C<GOAL>CategoryTheory.CategoryStruct.comp α β = CategoryTheory.CategoryStruct.comp β α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F G : CategoryTheory.Functor C D<VAR>H I : CategoryTheory.Functor D E<VAR>α : F ⟶ G<VAR>β : H ⟶ I<VAR>X : C<GOAL>(α ◫ β).app X = CategoryTheory.CategoryStruct.comp (β.app (F.obj X)) (I.map (α.app X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F G : CategoryTheory.Functor C D<VAR>H : CategoryTheory.Functor D E<VAR>α : F ⟶ G<VAR>X : C<GOAL>(α ◫ CategoryTheory.CategoryStruct.id H).app X = H.map (α.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F G : CategoryTheory.Functor C D<VAR>H : CategoryTheory.Functor E C<VAR>α : F ⟶ G<VAR>X : E<GOAL>(CategoryTheory.CategoryStruct.id H ◫ α).app X = α.app (H.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F G H : CategoryTheory.Functor C D<VAR>I J K : CategoryTheory.Functor D E<VAR>α : F ⟶ G<VAR>β : G ⟶ H<VAR>γ : I ⟶ J<VAR>δ : J ⟶ K<GOAL>CategoryTheory.CategoryStruct.comp α β ◫ CategoryTheory.CategoryStruct.comp γ δ = CategoryTheory.CategoryStruct.comp (α ◫ γ) (β ◫ δ)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>k : D<VAR>j : C<GOAL>(F.flip.obj k).obj j = (F.obj j).obj k
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<GOAL>∀ {X Y : D} (f : X ⟶ Y) (j : C), (F.flip.map f).app j = (F.obj j).map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>k : D<GOAL>∀ {X Y : C} (f : X ⟶ Y), (F.flip.obj k).map f = (F.map f).app k
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>X Y : C<VAR>e : X ≅ Y<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>Z : D<GOAL>CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z) ((F.map e.inv).app Z) = CategoryTheory.CategoryStruct.id ((F.obj X).obj Z)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>X Y : C<VAR>e : X ≅ Y<VAR>F : CategoryTheory.Functor C (CategoryTheory.Functor D E)<VAR>Z : D<GOAL>CategoryTheory.CategoryStruct.comp ((F.map e.inv).app Z) ((F.map e.hom).app Z) = CategoryTheory.CategoryStruct.id ((F.obj Y).obj Z)
<VAR>B : Type u<VAR>Quiver B<VAR>a : B<GOAL>(CategoryTheory.FreeBicategory.preinclusion B).obj { as := a } = a
<VAR>B : Type u<VAR>Quiver B<VAR>a b : B<VAR>f g : CategoryTheory.Discrete (Quiver.Path a b)<VAR>η : f ⟶ g<GOAL>(CategoryTheory.FreeBicategory.preinclusion B).map₂ η = CategoryTheory.eqToHom ⋯
<VAR>B : Type u<VAR>Quiver B<VAR>a b c : B<VAR>p : Quiver.Path a b<VAR>f g : CategoryTheory.FreeBicategory.Hom b c<VAR>η : f ⟶ g<GOAL>CategoryTheory.FreeBicategory.normalizeAux p f = CategoryTheory.FreeBicategory.normalizeAux p g
<VAR>B : Type u<VAR>Quiver B<VAR>a b c : B<VAR>p : Quiver.Path a b<VAR>f g : CategoryTheory.FreeBicategory.Hom b c<VAR>η : f ⟶ g<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p }) η) (CategoryTheory.FreeBicategory.normalizeIso p g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.normalizeIso p f).hom ((CategoryTheory.FreeBicategory.preinclusion B).map₂ (CategoryTheory.eqToHom ⋯))
<VAR>B : Type u<VAR>Quiver B<VAR>a b c : B<VAR>f : CategoryTheory.FreeBicategory.Hom a b<VAR>g : CategoryTheory.FreeBicategory.Hom b c<GOAL>CategoryTheory.FreeBicategory.normalizeAux Quiver.Path.nil (f.comp g) = (CategoryTheory.FreeBicategory.normalizeAux Quiver.Path.nil f).comp (CategoryTheory.FreeBicategory.normalizeAux Quiver.Path.nil g)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : Mon_ C<GOAL>self.X ◁ self.one ≫ self.mul = (ρ_ self.X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : Mon_ C<GOAL>self.one ▷ self.X ≫ self.mul = (λ_ self.X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : Mon_ C<GOAL>self.mul ▷ self.X ≫ self.mul = (α_ self.X self.X self.X).hom ≫ self.X ◁ self.mul ≫ self.mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Mon_.trivial C).X = 𝟙_ C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Mon_.trivial C).mul = (λ_ (𝟙_ C)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(Mon_.trivial C).one = 𝟙 (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M : Mon_ C<VAR>Z : C<VAR>f : Z ⟶ M.X<GOAL>(M.one ⊗ f) ≫ M.mul = (λ_ Z).hom ≫ f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M : Mon_ C<VAR>Z : C<VAR>f : Z ⟶ M.X<GOAL>(f ⊗ M.one) ≫ M.mul = (ρ_ Z).hom ≫ f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M : Mon_ C<GOAL>M.X ◁ M.mul ≫ M.mul = (α_ M.X M.X M.X).inv ≫ M.mul ▷ M.X ≫ M.mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M N : Mon_ C<VAR>self : M.Hom N<GOAL>M.mul ≫ self.hom = (self.hom ⊗ self.hom) ≫ N.mul
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M N : Mon_ C<VAR>self : M.Hom N<GOAL>M.one ≫ self.hom = N.one
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M : Mon_ 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 : Mon_ C<VAR>f : M.Hom N<VAR>g : N.Hom O<GOAL>(Mon_.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 : Mon_ 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 : Mon_ C<GOAL>(𝟙 M).hom = 𝟙 M.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M N K : Mon_ 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 : Mon_ C<GOAL>(Mon_.forget C).obj A = A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>∀ {X Y : Mon_ C} (f : X ⟶ Y), (Mon_.forget C).map f = f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M N : Mon_ C<VAR>f : M.X ≅ N.X<VAR>one_f : M.one ≫ f.hom = N.one := by aesop_cat<VAR>mul_f : M.mul ≫ f.hom = (f.hom ⊗ f.hom) ≫ N.mul := by aesop_cat<GOAL>(Mon_.mkIso f one_f mul_f).inv.hom = f.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M N : Mon_ C<VAR>f : M.X ≅ N.X<VAR>one_f : M.one ≫ f.hom = N.one := by aesop_cat<VAR>mul_f : M.mul ≫ f.hom = (f.hom ⊗ f.hom) ≫ N.mul := by aesop_cat<GOAL>(Mon_.mkIso f one_f mul_f).hom.hom = 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.LaxMonoidalFunctor C D<VAR>A : Mon_ C<GOAL>(F.mapMon.obj A).mul = F.μ A.X A.X ≫ F.map A.mul
<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.LaxMonoidalFunctor C D<VAR>A : Mon_ C<GOAL>(F.mapMon.obj A).one = F.ε ≫ F.map A.one
<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.LaxMonoidalFunctor C D<GOAL>∀ {X Y : Mon_ C} (f : X ⟶ Y), (F.mapMon.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.LaxMonoidalFunctor C D<VAR>A : Mon_ C<GOAL>(F.mapMon.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.LaxMonoidalFunctor C D<GOAL>(CategoryTheory.LaxMonoidalFunctor.mapMonFunctor C D).obj F = F.mapMon
<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<GOAL>∀ {X Y : CategoryTheory.LaxMonoidalFunctor C D} (α : X ⟶ Y) (A : Mon_ C), (((CategoryTheory.LaxMonoidalFunctor.mapMonFunctor C D).map α).app A).hom = α.app A.X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>∀ {X Y : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C} (α : X ⟶ Y), (Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).map α = ((CategoryTheory.LaxMonoidalFunctor.mapMonFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C).map α).app (Mon_.trivial (CategoryTheory.Discrete PUnit.{u + 1}))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C<GOAL>(Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).obj F = F.mapMon.obj (Mon_.trivial (CategoryTheory.Discrete PUnit.{u + 1}))