ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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.MonoidalFunctor C D<VAR>X Y : C<GOAL>F.μ X Y ≫ (F.μIso X Y).inv = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y))
<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.MonoidalFunctor C D<GOAL>F.εIso.hom = F.ε
<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.MonoidalFunctor C D<GOAL>F.εIso.inv ≫ F.ε = 𝟙 (F.obj (𝟙_ C))
<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.MonoidalFunctor C D<GOAL>F.ε ≫ F.εIso.inv = 𝟙 (𝟙_ D)
<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.MonoidalFunctor C D<VAR>X : C<GOAL>∀ (X_1 : C), (F.commTensorLeft X).inv.app X_1 = (F.μIso X X_1).inv
<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.MonoidalFunctor C D<VAR>X : C<GOAL>∀ (X_1 : C), (F.commTensorLeft X).hom.app X_1 = F.μ X X_1
<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.MonoidalFunctor C D<VAR>X : C<GOAL>∀ (X_1 : C), (F.commTensorRight X).inv.app X_1 = (F.μIso X_1 X).inv
<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.MonoidalFunctor C D<VAR>X : C<GOAL>∀ (X_1 : C), (F.commTensorRight X).hom.app X_1 = F.μ X_1 X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>(CategoryTheory.MonoidalFunctor.id C).μ X Y = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj ((𝟭 C).obj X) ((𝟭 C).obj Y))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.MonoidalFunctor.id C).ε = 𝟙 (𝟙_ C)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.MonoidalFunctor.id C).toFunctor = 𝟭 C
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>F : CategoryTheory.LaxMonoidalFunctor C D<VAR>G : CategoryTheory.LaxMonoidalFunctor D E<GOAL>(F ⊗⋙ G).toFunctor = F.toFunctor ⋙ G.toFunctor
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>F : CategoryTheory.LaxMonoidalFunctor C D<VAR>G : CategoryTheory.LaxMonoidalFunctor D E<VAR>X Y : C<GOAL>(F ⊗⋙ G).μ X Y = G.μ (F.obj X) (F.obj Y) ≫ G.map (F.μ X Y)
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>F : CategoryTheory.LaxMonoidalFunctor C D<VAR>G : CategoryTheory.LaxMonoidalFunctor D E<GOAL>(F ⊗⋙ G).ε = G.ε ≫ G.map F.ε
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>F : CategoryTheory.OplaxMonoidalFunctor C D<VAR>G : CategoryTheory.OplaxMonoidalFunctor D E<VAR>X Y : C<GOAL>(F ⊗⋙ G).δ X Y = G.map (F.δ X Y) ≫ G.δ (F.obj X) (F.obj Y)
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>F : CategoryTheory.OplaxMonoidalFunctor C D<VAR>G : CategoryTheory.OplaxMonoidalFunctor D E<GOAL>(F ⊗⋙ G).η = G.map F.η ≫ G.η
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>F : CategoryTheory.OplaxMonoidalFunctor C D<VAR>G : CategoryTheory.OplaxMonoidalFunctor D E<GOAL>(F ⊗⋙ G).toFunctor = F.toFunctor ⋙ G.toFunctor
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>B : Type u₀<VAR>CategoryTheory.Category.{v₀, u₀} B<VAR>CategoryTheory.MonoidalCategory B<VAR>F : CategoryTheory.LaxMonoidalFunctor B C<VAR>G : CategoryTheory.LaxMonoidalFunctor D E<GOAL>(F.prod G).ε = (F.ε, G.ε)
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>B : Type u₀<VAR>CategoryTheory.Category.{v₀, u₀} B<VAR>CategoryTheory.MonoidalCategory B<VAR>F : CategoryTheory.LaxMonoidalFunctor B C<VAR>G : CategoryTheory.LaxMonoidalFunctor D E<GOAL>(F.prod G).toFunctor = F.prod G.toFunctor
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>B : Type u₀<VAR>CategoryTheory.Category.{v₀, u₀} B<VAR>CategoryTheory.MonoidalCategory B<VAR>F : CategoryTheory.LaxMonoidalFunctor B C<VAR>G : CategoryTheory.LaxMonoidalFunctor D E<VAR>X Y : B × D<GOAL>(F.prod G).μ X Y = (F.μ X.1 Y.1, G.μ X.2 Y.2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.MonoidalFunctor.diag C).toFunctor = CategoryTheory.Functor.diag C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<GOAL>(CategoryTheory.MonoidalFunctor.diag C).ε = 𝟙 (𝟙_ (C × C))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<GOAL>(CategoryTheory.MonoidalFunctor.diag C).μ X Y = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.diag C).obj X) ((CategoryTheory.Functor.diag C).obj Y))
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>F : CategoryTheory.LaxMonoidalFunctor C D<VAR>G : CategoryTheory.LaxMonoidalFunctor C E<GOAL>(F.prod' G).toFunctor = F.prod' G.toFunctor
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>F : CategoryTheory.LaxMonoidalFunctor C D<VAR>G : CategoryTheory.LaxMonoidalFunctor C E<GOAL>(F.prod' G).ε = (F.ε, G.ε)
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>F : CategoryTheory.LaxMonoidalFunctor C D<VAR>G : CategoryTheory.LaxMonoidalFunctor C E<VAR>X Y : C<GOAL>(F.prod' G).μ X Y = (F.μ X Y, G.μ X Y)
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>F : CategoryTheory.MonoidalFunctor C D<VAR>G : CategoryTheory.MonoidalFunctor D E<GOAL>(F ⊗⋙ G).toLaxMonoidalFunctor = F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>B : Type u₀<VAR>CategoryTheory.Category.{v₀, u₀} B<VAR>CategoryTheory.MonoidalCategory B<VAR>F : CategoryTheory.MonoidalFunctor B C<VAR>G : CategoryTheory.MonoidalFunctor D E<GOAL>(F.prod G).toLaxMonoidalFunctor = F.prod G.toLaxMonoidalFunctor
<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>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>CategoryTheory.MonoidalCategory E<VAR>F : CategoryTheory.MonoidalFunctor C D<VAR>G : CategoryTheory.MonoidalFunctor C E<GOAL>(F.prod' G).toLaxMonoidalFunctor = F.prod' G.toLaxMonoidalFunctor
<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.MonoidalFunctor C D<VAR>G : D ⥤ C<VAR>h : F.toFunctor ⊣ G<VAR>F.IsEquivalence<GOAL>(CategoryTheory.monoidalInverse F h).toLaxMonoidalFunctor = CategoryTheory.monoidalAdjoint F h
<VAR>J : Type u<VAR>CategoryTheory.SmallCategory J<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>F : J ⥤ Type u<VAR>hf : ∀ (j : J), Finite (F.obj j)<VAR>hne : ∀ (j : J), Nonempty (F.obj j)<GOAL>F.sections.Nonempty
<VAR>J : Type u<VAR>CategoryTheory.Category.{w, u} J<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>F : J ⥤ Type v<VAR>∀ (j : J), Finite (F.obj j)<VAR>∀ (j : J), Nonempty (F.obj j)<GOAL>F.sections.Nonempty
<VAR>J : Type u<VAR>Preorder J<VAR>IsDirected J fun x x_1 => x ≤ x_1<VAR>F : Jᵒᵖ ⥤ Type v<VAR>∀ (j : Jᵒᵖ), Finite (F.obj j)<VAR>∀ (j : Jᵒᵖ), Nonempty (F.obj j)<GOAL>F.sections.Nonempty
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>j : J<VAR>x : F.obj j<GOAL>x ∈ F.eventualRange j ↔ ∀ ⦃i : J⦄ (f : i ⟶ j), x ∈ Set.range (F.map f)
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<GOAL>F.IsMittagLeffler ↔ ∀ (j : J), ∃ i f, F.eventualRange j = Set.range (F.map f)
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j : J<VAR>h : F.IsMittagLeffler<VAR>f : j ⟶ i<GOAL>F.eventualRange i ⊆ F.map f '' F.eventualRange j
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>f : i ⟶ j<VAR>g : j ⟶ k<VAR>h : F.eventualRange k = Set.range (F.map g)<GOAL>F.eventualRange k = Set.range (F.map (f ≫ g))
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>h : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<GOAL>F.IsMittagLeffler
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i : J<VAR>s : Set (F.obj i)<VAR>j : J<GOAL>(F.toPreimages s).obj j = ↑(⋂ f, F.map f ⁻¹' s)
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i : J<VAR>s : Set (F.obj i)<GOAL>∀ {X Y : J} (g : X ⟶ Y) (a : ↑(⋂ f, F.map f ⁻¹' s)), (F.toPreimages s).map g a = Set.MapsTo.restrict (F.map g) (⋂ f, F.map f ⁻¹' s) (⋂ f, F.map f ⁻¹' s) ⋯ a
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j : J<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>f : j ⟶ i<GOAL>Set.MapsTo (F.map f) (F.eventualRange j) (F.eventualRange i)
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j : J<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>h : F.IsMittagLeffler<VAR>f : j ⟶ i<GOAL>F.eventualRange i = F.map f '' F.eventualRange j
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j : J<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>f : i ⟶ j<GOAL>F.eventualRange j = Set.range (F.map f) ↔ ∀ ⦃k : J⦄ (g : k ⟶ i), Set.range (F.map f) ⊆ Set.range (F.map (g ≫ f))
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>CategoryTheory.IsCofilteredOrEmpty J<GOAL>F.IsMittagLeffler ↔ ∀ (j : J), ∃ i f, ∀ ⦃k : J⦄ (g : k ⟶ i), Set.range (F.map f) ⊆ Set.range (F.map (g ≫ f))
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i : J<VAR>s : Set (F.obj i)<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>h : F.IsMittagLeffler<GOAL>(F.toPreimages s).IsMittagLeffler
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>h : ∀ (j : J), ∃ i f, (Set.range (F.map f)).Finite<GOAL>F.IsMittagLeffler
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>j : J<GOAL>F.toEventualRanges.obj j = ↑(F.eventualRange j)
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>CategoryTheory.IsCofilteredOrEmpty J<GOAL>∀ {X Y : J} (f : X ⟶ Y) (a : ↑(F.eventualRange X)), F.toEventualRanges.map f a = Set.MapsTo.restrict (F.map f) (F.eventualRange X) (F.eventualRange Y) ⋯ a
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>h : F.IsMittagLeffler<VAR>i j : J<VAR>f : i ⟶ j<GOAL>Function.Surjective (F.toEventualRanges.map f)
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>h : F.IsMittagLeffler<VAR>∀ (j : J), Nonempty (F.obj j)<VAR>j : J<GOAL>Nonempty (F.toEventualRanges.obj j)
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>i j : J<VAR>f g : i ⟶ j<GOAL>F.map f = F.map g
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i : J<VAR>s : Set (F.obj i)<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>hFn : ∀ (j : J), Nonempty (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>hs : s.Nonempty<VAR>j : J<GOAL>Nonempty ((F.toPreimages s).obj j)
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>j : J<VAR>Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)<VAR>i : J<VAR>f : i ⟶ j<GOAL>Function.Injective fun s => ↑s j
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>∀ (j : J), Nonempty (F.obj j)<VAR>∀ (j : J), Finite (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>i : J<GOAL>Function.Surjective fun s => ↑s i
<VAR>J : Type u<VAR>CategoryTheory.Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>CategoryTheory.IsCofilteredOrEmpty J<VAR>∀ (j : J), Nonempty (F.obj j)<VAR>∀ (j : J), Finite (F.obj j)<VAR>Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective (F.map f)<VAR>Nonempty J<VAR>Finite ↑F.sections<GOAL>∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective (F.map f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.ConcreteCategory C<GOAL>CategoryTheory.ConcreteCategory.forget.Faithful
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>w : ∀ (x : (CategoryTheory.forget C).obj X), f x = g x<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.forget C).map f = ⇑f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>h : f = g<VAR>x : (CategoryTheory.forget C).obj X<GOAL>f x = g x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X : C<GOAL>⇑(CategoryTheory.CategoryStruct.id X) = id
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>⇑(CategoryTheory.CategoryStruct.comp f g) = ⇑g ∘ ⇑f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X : C<VAR>x : (CategoryTheory.forget C).obj X<GOAL>(CategoryTheory.CategoryStruct.id X) x = x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : (CategoryTheory.forget C).obj X<GOAL>(CategoryTheory.CategoryStruct.comp f g) x = g (f x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : (CategoryTheory.forget C).obj X<GOAL>(CategoryTheory.forget C).map (CategoryTheory.CategoryStruct.comp f g) x = (CategoryTheory.forget C).map g ((CategoryTheory.forget C).map f x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>x x' : (CategoryTheory.forget C).obj X<VAR>h : x = x'<GOAL>f x = f x'
<VAR>X Y : Type u<VAR>f : X ⟶ Y<GOAL>CoeFun.coe f = f
<VAR>C : Type u<VAR>D : Type u'<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>self : CategoryTheory.HasForget₂ C D<GOAL>CategoryTheory.HasForget₂.forget₂.comp (CategoryTheory.forget D) = CategoryTheory.forget C
<VAR>C : Type u<VAR>D : Type u'<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.HasForget₂ C D<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>x : (CategoryTheory.forget D).obj ((CategoryTheory.forget₂ C D).obj X)<GOAL>((CategoryTheory.forget₂ C D).map (CategoryTheory.CategoryStruct.comp f g)) x = ((CategoryTheory.forget₂ C D).map g) (((CategoryTheory.forget₂ C D).map f) x)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.ConcreteCategory D<VAR>F G : CategoryTheory.Functor C D<VAR>φ : F ⟶ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>x : (CategoryTheory.forget D).obj (F.obj X)<GOAL>(φ.app Y) ((F.map f) x) = (G.map f) ((φ.app X) x)
<VAR>B : Type u<VAR>self : CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h h' : c ⟶ d<VAR>η : h ⟶ h'<GOAL>CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η)) (CategoryTheory.Bicategory.associator f g h').inv)
<VAR>B : Type u<VAR>self : CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g h i : b ⟶ c<VAR>η : g ⟶ h<VAR>θ : h ⟶ i<GOAL>CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η) (CategoryTheory.Bicategory.whiskerLeft f θ)
<VAR>B : Type u<VAR>self : CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<GOAL>CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.leftUnitor g).inv)
<VAR>B : Type u<VAR>self : CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f : a ⟶ b<VAR>g g' : b ⟶ c<VAR>η : g ⟶ g'<VAR>h : c ⟶ d<GOAL>CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h)) (CategoryTheory.Bicategory.associator f g' h).inv)
<VAR>B : Type u<VAR>self : CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.id f) g = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
<VAR>B : Type u<VAR>self : CategoryTheory.Bicategory B<VAR>a b c d : B<VAR>f f' : a ⟶ b<VAR>η : f ⟶ f'<VAR>g : b ⟶ c<VAR>h : c ⟶ d<GOAL>CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h) (CategoryTheory.Bicategory.associator f' g h).hom)
<VAR>B : Type u<VAR>self : CategoryTheory.Bicategory B<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<GOAL>CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.rightUnitor g).inv)
<VAR>B : Type u<VAR>self : CategoryTheory.Bicategory B<VAR>a b c d e : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<VAR>h : c ⟶ d<VAR>i : d ⟶ e<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom
<VAR>B : Type u<VAR>self : CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f g : a ⟶ b<VAR>h i : b ⟶ c<VAR>η : f ⟶ g<VAR>θ : h ⟶ i<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f θ) (CategoryTheory.Bicategory.whiskerRight η i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η h) (CategoryTheory.Bicategory.whiskerLeft g θ)
<VAR>B : Type u<VAR>self : CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom) = CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g
<VAR>B : Type u<VAR>self : CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.CategoryStruct.id g) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
<VAR>B : Type u<VAR>self : CategoryTheory.Bicategory B<VAR>a b c : B<VAR>f g h : a ⟶ b<VAR>η : f ⟶ g<VAR>θ : g ⟶ h<VAR>i : b ⟶ c<GOAL>CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.comp η θ) i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η i) (CategoryTheory.Bicategory.whiskerRight θ i)