ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasInitial C<VAR>h : ∀ (A : C) (f : A ⟶ ⊥_ C), CategoryTheory.IsIso f<GOAL>CategoryTheory.Limits.HasStrictInitialObjects C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Limits.HasStrictTerminalObjects C<VAR>I A : C<VAR>f : I ⟶ A<GOAL>CategoryTheory.Limits.IsTerminal I → CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictTerminalObjects C<VAR>I : C<VAR>hI : CategoryTheory.Limits.IsTerminal I<VAR>A : C<VAR>f : I ⟶ A<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictTerminalObjects C<VAR>I : C<VAR>hI : CategoryTheory.Limits.IsTerminal I<VAR>A : C<VAR>f g : I ⟶ A<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictTerminalObjects C<VAR>I : C<VAR>hI : CategoryTheory.Limits.IsTerminal I<VAR>A : C<GOAL>Subsingleton (I ⟶ A)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictTerminalObjects C<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>F : CategoryTheory.Functor J C<VAR>CategoryTheory.Limits.HasLimit F<VAR>i : J<VAR>H : (j : J) → j ≠ i → CategoryTheory.Limits.IsTerminal (F.obj j)<VAR>Subsingleton (i ⟶ i)<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictTerminalObjects C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>A : C<VAR>f g : ⊤_ C ⟶ A<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasStrictTerminalObjects C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>A : C<GOAL>Subsingleton (⊤_ C ⟶ A)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : C<VAR>h : ∀ (A : C) (f : I ⟶ A), CategoryTheory.IsIso f<GOAL>CategoryTheory.Limits.HasStrictTerminalObjects C
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>c : CategoryTheory.Limits.Cone F<GOAL>Nonempty (CategoryTheory.Limits.IsLimit c) ↔ ∀ s ∈ F.sections, ∃! x, ∀ (j : J), c.π.app j x = s j
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>c : CategoryTheory.Limits.Cone F<GOAL>Nonempty (CategoryTheory.Limits.IsLimit c) ↔ Function.Bijective (CategoryTheory.Limits.Types.sectionOfCone c)
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>c : CategoryTheory.Limits.Cone F<VAR>t : CategoryTheory.Limits.IsLimit c<VAR>j : J<VAR>x : c.pt<GOAL>↑((CategoryTheory.Limits.Types.isLimitEquivSections t) x) j = c.π.app j x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>c : CategoryTheory.Limits.Cone F<VAR>t : CategoryTheory.Limits.IsLimit c<VAR>x : ↑F.sections<VAR>j : J<GOAL>c.π.app j ((CategoryTheory.Limits.Types.isLimitEquivSections t).symm x) = ↑x j
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>Small.{u, max u v} ↑F.sections<GOAL>(CategoryTheory.Limits.Types.Small.limitCone F).pt = Shrink.{u, max u v} ↑F.sections
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>Small.{u, max u v} ↑F.sections<VAR>j : J<VAR>u : ((CategoryTheory.Functor.const J).obj (Shrink.{u, max u v} ↑F.sections)).obj j<GOAL>(CategoryTheory.Limits.Types.Small.limitCone F).π.app j u = ↑((equivShrink ↑F.sections).symm u) j
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>Small.{u, max u v} ↑F.sections<VAR>x y : (CategoryTheory.Limits.Types.Small.limitCone F).pt<VAR>w : (equivShrink ↑F.sections).symm x = (equivShrink ↑F.sections).symm y<GOAL>x = y
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>Small.{u, max u v} ↑F.sections<VAR>s : CategoryTheory.Limits.Cone F<VAR>v : s.pt<GOAL>(CategoryTheory.Limits.Types.Small.limitConeIsLimit F).lift s v = (equivShrink ↑F.sections) ⟨fun j => s.π.app j v, ⋯⟩
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<GOAL>CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑F.sections
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ TypeMax<VAR>j : J<VAR>u : ((CategoryTheory.Functor.const J).obj ↑F.sections).obj j<GOAL>(CategoryTheory.Limits.Types.limitCone F).π.app j u = ↑u j
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ TypeMax<GOAL>(CategoryTheory.Limits.Types.limitCone F).pt = ↑F.sections
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ TypeMax<VAR>s : CategoryTheory.Limits.Cone F<VAR>v : s.pt<VAR>j : J<GOAL>↑((CategoryTheory.Limits.Types.limitConeIsLimit F).lift s v) j = s.π.app j v
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasLimit F<VAR>x : CategoryTheory.Limits.limit F<VAR>j : J<GOAL>↑((CategoryTheory.Limits.Types.limitEquivSections F) x) j = CategoryTheory.Limits.limit.π F j x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasLimit F<VAR>x : ↑F.sections<VAR>j : J<GOAL>CategoryTheory.Limits.limit.π F j ((CategoryTheory.Limits.Types.limitEquivSections F).symm x) = ↑x j
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasLimit F<VAR>x : (j : J) → F.obj j<VAR>h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j'<VAR>j : J<GOAL>CategoryTheory.Limits.limit.π F j (CategoryTheory.Limits.Types.Limit.mk F x h) = x j
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasLimit F<VAR>x y : CategoryTheory.Limits.limit F<VAR>w : ∀ (j : J), CategoryTheory.Limits.limit.π F j x = CategoryTheory.Limits.limit.π F j y<GOAL>x = y
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type v<VAR>x y : CategoryTheory.Limits.limit F<VAR>w : ∀ (j : J), CategoryTheory.Limits.limit.π F j x = CategoryTheory.Limits.limit.π F j y<GOAL>x = y
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasLimit F<VAR>x y : CategoryTheory.Limits.limit F<GOAL>x = y ↔ ∀ (j : J), CategoryTheory.Limits.limit.π F j x = CategoryTheory.Limits.limit.π F j y
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type v<VAR>x y : CategoryTheory.Limits.limit F<GOAL>x = y ↔ ∀ (j : J), CategoryTheory.Limits.limit.π F j x = CategoryTheory.Limits.limit.π F j y
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasLimit F<VAR>j j' : J<VAR>x : CategoryTheory.Limits.limit F<VAR>f : j ⟶ j'<GOAL>F.map f (CategoryTheory.Limits.limit.π F j x) = CategoryTheory.Limits.limit.π F j' x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasLimit F<VAR>s : CategoryTheory.Limits.Cone F<VAR>j : J<VAR>x : s.pt<GOAL>CategoryTheory.Limits.limit.π F j (CategoryTheory.Limits.limit.lift F s x) = s.π.app j x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F G : J ⥤ Type u<VAR>CategoryTheory.Limits.HasLimit F<VAR>CategoryTheory.Limits.HasLimit G<VAR>α : F ⟶ G<VAR>j : J<VAR>x : CategoryTheory.Limits.limit F<GOAL>CategoryTheory.Limits.limit.π G j (CategoryTheory.Limits.limMap α x) = α.app j (CategoryTheory.Limits.limit.π F j x)
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type v<VAR>j j' : J<VAR>x : CategoryTheory.Limits.limit F<VAR>f : j ⟶ j'<GOAL>F.map f (CategoryTheory.Limits.limit.π F j x) = CategoryTheory.Limits.limit.π F j' x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type v<VAR>s : CategoryTheory.Limits.Cone F<VAR>j : J<VAR>x : s.pt<GOAL>CategoryTheory.Limits.limit.π F j (CategoryTheory.Limits.limit.lift F s x) = s.π.app j x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F G : J ⥤ Type v<VAR>α : F ⟶ G<VAR>j : J<VAR>x : CategoryTheory.Limits.limit F<GOAL>CategoryTheory.Limits.limit.π G j (CategoryTheory.Limits.limMap α x) = α.app j (CategoryTheory.Limits.limit.π F j x)
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>x : CategoryTheory.Limits.Types.Quot F<GOAL>∃ j y, x = CategoryTheory.Limits.Types.Quot.ι F j y
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>c : CategoryTheory.Limits.Cocone F<VAR>j : J<VAR>x : F.obj j<GOAL>CategoryTheory.Limits.Types.Quot.desc c (CategoryTheory.Limits.Types.Quot.ι F j x) = c.ι.app j x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>x : F.obj j<GOAL>CategoryTheory.Limits.Types.Quot.ι F j' (F.map f x) = CategoryTheory.Limits.Types.Quot.ι F j x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>α : Type u<VAR>f : CategoryTheory.Limits.Types.Quot F → α<GOAL>(CategoryTheory.Limits.Types.toCocone f).pt = α
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>α : Type u<VAR>f : CategoryTheory.Limits.Types.Quot F → α<VAR>j : J<GOAL>∀ (a : F.obj j), (CategoryTheory.Limits.Types.toCocone f).ι.app j a = (f ∘ CategoryTheory.Limits.Types.Quot.ι F j) a
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>c : CategoryTheory.Limits.Cocone F<VAR>α : Type u<VAR>f : CategoryTheory.Limits.Types.Quot F → α<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>x : CategoryTheory.Limits.Types.Quot F<GOAL>hc.desc (CategoryTheory.Limits.Types.toCocone f) (CategoryTheory.Limits.Types.Quot.desc c x) = f x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>c : CategoryTheory.Limits.Cocone F<GOAL>Nonempty (CategoryTheory.Limits.IsColimit c) ↔ Function.Bijective (CategoryTheory.Limits.Types.Quot.desc c)
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>Small.{u, max u v} (CategoryTheory.Limits.Types.Quot F)<GOAL>(CategoryTheory.Limits.Types.colimitCocone F).pt = Shrink.{u, max u v} (CategoryTheory.Limits.Types.Quot F)
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>Small.{u, max u v} (CategoryTheory.Limits.Types.Quot F)<VAR>j : J<VAR>x : F.obj j<GOAL>(CategoryTheory.Limits.Types.colimitCocone F).ι.app j x = (equivShrink (CategoryTheory.Limits.Types.Quot F)) (Quot.mk (CategoryTheory.Limits.Types.Quot.Rel F) ⟨j, x⟩)
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>Small.{u, max u v} (CategoryTheory.Limits.Types.Quot F)<GOAL>CategoryTheory.Limits.Types.Quot.desc (CategoryTheory.Limits.Types.colimitCocone F) = ⇑(equivShrink (CategoryTheory.Limits.Types.Quot F))
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<GOAL>CategoryTheory.Limits.HasColimit F ↔ Small.{u, max u v} (CategoryTheory.Limits.Types.Quot F)
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasColimit F<GOAL>Small.{u, max u v} (CategoryTheory.Limits.Types.Quot F)
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ TypeMax<GOAL>(CategoryTheory.Limits.Types.TypeMax.colimitCocone F).pt = CategoryTheory.Limits.Types.Quot F
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ TypeMax<VAR>j : J<VAR>x : F.obj j<GOAL>(CategoryTheory.Limits.Types.TypeMax.colimitCocone F).ι.app j x = Quot.mk (CategoryTheory.Limits.Types.Quot.Rel F) ⟨j, x⟩
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasColimit F<VAR>j : J<VAR>x : F.obj j<GOAL>(CategoryTheory.Limits.Types.colimitEquivQuot F).symm (Quot.mk (CategoryTheory.Limits.Types.Quot.Rel F) ⟨j, x⟩) = CategoryTheory.Limits.colimit.ι F j x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasColimit F<VAR>j : J<VAR>x : F.obj j<GOAL>(CategoryTheory.Limits.Types.colimitEquivQuot F) (CategoryTheory.Limits.colimit.ι F j x) = Quot.mk (CategoryTheory.Limits.Types.Quot.Rel F) ⟨j, x⟩
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasColimit F<VAR>j j' : J<VAR>x : F.obj j<VAR>f : j ⟶ j'<GOAL>CategoryTheory.Limits.colimit.ι F j' (F.map f x) = CategoryTheory.Limits.colimit.ι F j x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasColimit F<VAR>s : CategoryTheory.Limits.Cocone F<VAR>j : J<VAR>x : F.obj j<GOAL>CategoryTheory.Limits.colimit.desc F s (CategoryTheory.Limits.colimit.ι F j x) = s.ι.app j x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F G : J ⥤ Type u<VAR>CategoryTheory.Limits.HasColimitsOfShape J (Type u)<VAR>α : F ⟶ G<VAR>j : J<VAR>x : F.obj j<GOAL>CategoryTheory.Limits.colim.map α (CategoryTheory.Limits.colimit.ι F j x) = CategoryTheory.Limits.colimit.ι G j (α.app j x)
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type v<VAR>j j' : J<VAR>x : F.obj j<VAR>f : j ⟶ j'<GOAL>CategoryTheory.Limits.colimit.ι F j' (F.map f x) = CategoryTheory.Limits.colimit.ι F j x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type v<VAR>s : CategoryTheory.Limits.Cocone F<VAR>j : J<VAR>x : F.obj j<GOAL>CategoryTheory.Limits.colimit.desc F s (CategoryTheory.Limits.colimit.ι F j x) = s.ι.app j x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F G : J ⥤ Type v<VAR>α : F ⟶ G<VAR>j : J<VAR>x : F.obj j<GOAL>CategoryTheory.Limits.colim.map α (CategoryTheory.Limits.colimit.ι F j x) = CategoryTheory.Limits.colimit.ι G j (α.app j x)
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasColimit F<VAR>j j' : J<VAR>x : F.obj j<VAR>x' : F.obj j'<VAR>f : j ⟶ j'<VAR>w : F.map f x = x'<GOAL>CategoryTheory.Limits.colimit.ι F j x = CategoryTheory.Limits.colimit.ι F j' x'
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasColimit F<VAR>j j' : J<VAR>x : F.obj j<VAR>x' : F.obj j'<VAR>j'' : J<VAR>f : j ⟶ j''<VAR>f' : j' ⟶ j''<VAR>w : F.map f x = F.map f' x'<GOAL>CategoryTheory.Limits.colimit.ι F j x = CategoryTheory.Limits.colimit.ι F j' x'
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasColimit F<VAR>j j' : J<VAR>x : F.obj j<VAR>x' : F.obj j'<VAR>w : CategoryTheory.Limits.colimit.ι F j x = CategoryTheory.Limits.colimit.ι F j' x'<GOAL>EqvGen (CategoryTheory.Limits.Types.Quot.Rel F) ⟨j, x⟩ ⟨j', x'⟩
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>t : CategoryTheory.Limits.Cocone F<VAR>h : CategoryTheory.Limits.IsColimit t<VAR>x : t.pt<GOAL>∃ j y, t.ι.app j y = x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasColimit F<VAR>x : CategoryTheory.Limits.colimit F<GOAL>∃ j y, CategoryTheory.Limits.colimit.ι F j y = x
<VAR>J : Type v<VAR>CategoryTheory.Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>CategoryTheory.Limits.HasColimit F<GOAL>Nonempty (CategoryTheory.Limits.colimit F) → Nonempty J
<VAR>α β : Type u<VAR>f : α ⟶ β<VAR>F' : CategoryTheory.Limits.MonoFactorisation f<GOAL>CategoryTheory.Limits.Types.Image.lift F' ≫ F'.m = CategoryTheory.Limits.Types.Image.ι f
<VAR>F : ℕᵒᵖ ⥤ Type u<VAR>hF : ∀ (n : ℕ), Function.Surjective (F.map (CategoryTheory.homOfLE ⋯).op)<GOAL>Function.Surjective ((CategoryTheory.Limits.Types.limitCone F).π.app (Opposite.op 0))
<VAR>F : ℕᵒᵖ ⥤ Type u<VAR>c : CategoryTheory.Limits.Cone F<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>hF : ∀ (n : ℕ), Function.Surjective (F.map (CategoryTheory.homOfLE ⋯).op)<GOAL>Function.Surjective (c.π.app (Opposite.op 0))
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>F : J ⥤ C<VAR>X : C<VAR>s : ↑(F ⋙ CategoryTheory.coyoneda.obj (Opposite.op X)).sections<VAR>j : J<GOAL>((CategoryTheory.Limits.compCoyonedaSectionsEquiv F X) s).app j = ↑s j
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>F : J ⥤ C<VAR>X : C<VAR>τ : (CategoryTheory.Functor.const J).obj X ⟶ F<GOAL>∀ (X_1 : J), ↑((CategoryTheory.Limits.compCoyonedaSectionsEquiv F X).symm τ) X_1 = τ.app X_1
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>F : J ⥤ C<VAR>X : C<VAR>τ : F ⟶ (CategoryTheory.Functor.const J).obj X<VAR>j : Jᵒᵖ<GOAL>↑((CategoryTheory.Limits.opCompYonedaSectionsEquiv F X).symm τ) j = τ.app (Opposite.unop j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>F : J ⥤ C<VAR>X : C<VAR>s : ↑(F.op ⋙ CategoryTheory.yoneda.obj X).sections<VAR>j : J<GOAL>((CategoryTheory.Limits.opCompYonedaSectionsEquiv F X) s).app j = ↑s (Opposite.op j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>F : J ⥤ Cᵒᵖ<VAR>X : C<VAR>s : ↑(F ⋙ CategoryTheory.yoneda.obj X).sections<VAR>j : J<GOAL>((CategoryTheory.Limits.compYonedaSectionsEquiv F X) s).app j = Quiver.Hom.op (↑s j)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} J<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>F : J ⥤ Cᵒᵖ<VAR>X : C<VAR>τ : (CategoryTheory.Functor.const J).obj (Opposite.op X) ⟶ F<VAR>j : J<GOAL>↑((CategoryTheory.Limits.compYonedaSectionsEquiv F X).symm τ) j = (τ.app j).unop
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>X : C<GOAL>∀ (a : CategoryTheory.Limits.limit (F ⋙ CategoryTheory.coyoneda.obj (Opposite.op X))) (j : J), ((CategoryTheory.Limits.limitCompCoyonedaIsoCone F X).hom a).app j = CategoryTheory.Limits.limit.π (F ⋙ CategoryTheory.coyoneda.obj (Opposite.op X)) j a
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>X : C<GOAL>∀ (a : (CategoryTheory.Functor.const J).obj X ⟶ F), (CategoryTheory.Limits.limitCompCoyonedaIsoCone F X).inv a = (CategoryTheory.Limits.Types.limitEquivSections (F ⋙ CategoryTheory.coyoneda.obj (Opposite.op X))).symm ((CategoryTheory.Limits.compCoyonedaSectionsEquiv F X).symm a)
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>X : Cᵒᵖ<GOAL>∀ (a : F.cones.obj X), (CategoryTheory.Limits.coyonedaCompLimIsoCones F).inv.app X a = (CategoryTheory.Limits.Types.limitEquivSections (F ⋙ CategoryTheory.coyoneda.obj X)).symm ((CategoryTheory.Limits.compCoyonedaSectionsEquiv F (Opposite.unop X)).symm a)
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>X : Cᵒᵖ<GOAL>∀ (a : (CategoryTheory.coyoneda ⋙ (CategoryTheory.whiskeringLeft J C (Type v)).obj F ⋙ CategoryTheory.Limits.lim).obj X) (j : J), ((CategoryTheory.Limits.coyonedaCompLimIsoCones F).hom.app X a).app j = CategoryTheory.Limits.limit.π (F ⋙ CategoryTheory.coyoneda.obj X) j a
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : J ⥤ C<GOAL>∀ (X_1 : Cᵒᵖ) (a : X.cones.obj X_1), ((CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C).inv.app X).app X_1 a = (CategoryTheory.Limits.Types.limitEquivSections (X ⋙ CategoryTheory.coyoneda.obj X_1)).symm ((CategoryTheory.Limits.compCoyonedaSectionsEquiv X (Opposite.unop X_1)).symm a)
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : J ⥤ C<GOAL>∀ (X_1 : Cᵒᵖ) (a : (CategoryTheory.coyoneda ⋙ (CategoryTheory.whiskeringLeft J C (Type v)).obj X ⋙ CategoryTheory.Limits.lim).obj X_1) (j : J), (((CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C).hom.app X).app X_1 a).app j = CategoryTheory.Limits.limit.π (X ⋙ CategoryTheory.coyoneda.obj X_1) j a
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>X : C<GOAL>∀ (a : F ⟶ (CategoryTheory.Functor.const J).obj X), (CategoryTheory.Limits.limitCompYonedaIsoCocone F X).inv a = (CategoryTheory.Limits.Types.limitEquivSections (F.op ⋙ CategoryTheory.yoneda.obj X)).symm ((CategoryTheory.Limits.opCompYonedaSectionsEquiv F X).symm a)
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>X : C<GOAL>∀ (a : CategoryTheory.Limits.limit (F.op ⋙ CategoryTheory.yoneda.obj X)) (j : J), ((CategoryTheory.Limits.limitCompYonedaIsoCocone F X).hom a).app j = CategoryTheory.Limits.limit.π (F.op ⋙ CategoryTheory.yoneda.obj X) (Opposite.op j) a
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>X : C<GOAL>∀ (a : F.cocones.obj X), (CategoryTheory.Limits.yonedaCompLimIsoCocones F).inv.app X a = (CategoryTheory.Limits.Types.limitEquivSections (F.op ⋙ CategoryTheory.yoneda.obj X)).symm ((CategoryTheory.Limits.opCompYonedaSectionsEquiv F X).symm a)
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : J ⥤ C<VAR>X : C<GOAL>∀ (a : (CategoryTheory.yoneda ⋙ (CategoryTheory.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj F.op ⋙ CategoryTheory.Limits.lim).obj X) (j : J), ((CategoryTheory.Limits.yonedaCompLimIsoCocones F).hom.app X a).app j = CategoryTheory.Limits.limit.π (F.op ⋙ CategoryTheory.yoneda.obj X) (Opposite.op j) a
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : (J ⥤ C)ᵒᵖ<GOAL>∀ (X_1 : C) (a : (CategoryTheory.yoneda ⋙ (CategoryTheory.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj (Opposite.unop X).op ⋙ CategoryTheory.Limits.lim).obj X_1) (j : J), (((CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones J C).hom.app X).app X_1 a).app j = CategoryTheory.Limits.limit.π ((Opposite.unop X).op ⋙ CategoryTheory.yoneda.obj X_1) (Opposite.op j) a
<VAR>J : Type v<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : (J ⥤ C)ᵒᵖ<GOAL>∀ (X_1 : C) (a : (Opposite.unop X).cocones.obj X_1), ((CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones J C).inv.app X).app X_1 a = (CategoryTheory.Limits.Types.limitEquivSections ((Opposite.unop X).op ⋙ CategoryTheory.yoneda.obj X_1)).symm ((CategoryTheory.Limits.opCompYonedaSectionsEquiv (Opposite.unop X) X_1).symm a)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j : CategoryTheory.Bicone J<GOAL>CategoryTheory.CategoryStruct.id j = CategoryTheory.Bicone.casesOn j CategoryTheory.BiconeHom.left_id CategoryTheory.BiconeHom.right_id fun k => CategoryTheory.BiconeHom.diagram (CategoryTheory.CategoryStruct.id k)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<GOAL>∀ (a a_1 : CategoryTheory.Bicone J), (a ⟶ a_1) = CategoryTheory.BiconeHom J a a_1
<VAR>J : Type v₁<VAR>CategoryTheory.SmallCategory J<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>F : CategoryTheory.Functor J C<VAR>c₁ c₂ : CategoryTheory.Limits.Cone F<VAR>X : CategoryTheory.Bicone J<GOAL>(CategoryTheory.biconeMk J c₁ c₂).obj X = CategoryTheory.Bicone.casesOn X c₁.pt c₂.pt fun j => F.obj j
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>F : J → C<VAR>CategoryTheory.Limits.HasProduct F<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)<VAR>x : (CategoryTheory.forget C).obj (∏ᶜ F)<VAR>j : J<GOAL>(CategoryTheory.Limits.Concrete.productEquiv F) x j = (CategoryTheory.Limits.Pi.π F j) x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.ConcreteCategory C<VAR>J : Type w<VAR>F : J → C<VAR>CategoryTheory.Limits.HasProduct F<VAR>CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor F) (CategoryTheory.forget C)<VAR>x : (j : J) → (CategoryTheory.forget C).obj (F j)<VAR>j : J<GOAL>(CategoryTheory.Limits.Pi.π F j) ((CategoryTheory.Limits.Concrete.productEquiv F).symm x) = x j