ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsSeparable F E<GOAL>Field.finSepDegree F E = FiniteDimensional.finrank F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>FiniteDimensional F E<GOAL>Field.finSepDegree F E = FiniteDimensional.finrank F E ↔ Algebra.IsSeparable F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>L : IntermediateField F E<VAR>Algebra.IsSeparable F ↥L<VAR>x : E<VAR>h : x ∈ L<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>x : E<GOAL>Algebra.IsSeparable F ↥F⟮x⟯ ↔ IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>K : Type w<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<VAR>Algebra.IsSeparable F E<VAR>x : K<VAR>hsep : IsSeparable E x<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>K : Type w<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<VAR>Algebra.IsSeparable F E<VAR>Algebra.IsSeparable E K<GOAL>Algebra.IsSeparable F K
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>x y : E<VAR>hx : IsSeparable F x<VAR>hy : IsSeparable F y<GOAL>Algebra.IsSeparable F ↥F⟮x, y⟯
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>x : F<GOAL>IsSeparable F ((algebraMap F E) x)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>x y : E<VAR>hx : IsSeparable F x<VAR>hy : IsSeparable F y<GOAL>IsSeparable F (x * y)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>x y : E<VAR>hx : IsSeparable F x<VAR>hy : IsSeparable F y<GOAL>IsSeparable F (x + y)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>x : E<VAR>hx : IsSeparable F x<GOAL>IsSeparable F x⁻¹
<VAR>F : Type u_1<VAR>Field F<GOAL>PerfectField F ↔ ∀ (f : F[X]), f.natSepDegree = 1 → Polynomial.Splits (RingHom.id F) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>self : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>U V : Cᵒᵖ<VAR>i : U ⟶ V<GOAL>self.obj U ⊆ F.map i ⁻¹' self.obj V
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>U : Cᵒᵖ<GOAL>G.toPresheaf.obj U = ↑(G.obj U)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>U V : Cᵒᵖ<VAR>i : U ⟶ V<VAR>x : ↑(G.obj U)<GOAL>↑(G.toPresheaf.map i x) = F.map i ↑x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>U : Cᵒᵖ<VAR>x : G.toPresheaf.obj U<GOAL>G.ι.app U x = ↑x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G G' : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>h : G ≤ G'<VAR>U : Cᵒᵖ<VAR>x : G.toPresheaf.obj U<GOAL>↑((CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe h).app U x) = ↑x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G G' : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>h : G ≤ G'<GOAL>CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe h ≫ G'.ι = G.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<GOAL>G = ⊤ ↔ CategoryTheory.IsIso G.ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F' : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>f : F' ⟶ F<VAR>hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ G.obj U<VAR>U : Cᵒᵖ<VAR>x : F'.obj U<GOAL>↑((G.lift f hf).app U x) = f.app U x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F' : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>f : F' ⟶ F<VAR>hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ G.obj U<GOAL>G.lift f hf ≫ G.ι = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>U : Cᵒᵖ<VAR>s : F.obj U<VAR>V : C<VAR>f : V ⟶ Opposite.unop U<GOAL>(G.sieveOfSection s).arrows f = (F.map f.op s ∈ G.obj (Opposite.op V))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>U : Cᵒᵖ<VAR>s : F.obj U<GOAL>(G.familyOfElementsOfSection s).Compatible
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F' : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>f : F' ⟶ G.toPresheaf<VAR>U V : Cᵒᵖ<VAR>i : U ⟶ V<VAR>x : F'.obj U<GOAL>↑(f.app V (F'.map i x)) = F.map i ↑(f.app U x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<GOAL>G ≤ CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>h : CategoryTheory.Presieve.IsSheaf J F<VAR>hG : CategoryTheory.Presieve.IsSheaf J G.toPresheaf<GOAL>G = CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>hF : CategoryTheory.Presieve.IsSheaf J F<GOAL>CategoryTheory.Presieve.IsSheaf J (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G).toPresheaf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>h : CategoryTheory.Presieve.IsSheaf J F<GOAL>G = CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G ↔ CategoryTheory.Presieve.IsSheaf J G.toPresheaf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>h : CategoryTheory.Presieve.IsSheaf J F<GOAL>CategoryTheory.Presieve.IsSheaf J G.toPresheaf ↔ ∀ (U : Cᵒᵖ) (s : F.obj U), G.sieveOfSection s ∈ J.sieves (Opposite.unop U) → s ∈ G.obj U
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>h : CategoryTheory.Presieve.IsSheaf J F<GOAL>CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G) = CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F F' : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>f : G.toPresheaf ⟶ F'<VAR>h : CategoryTheory.Presieve.IsSheaf J F'<GOAL>CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe ⋯ ≫ G.sheafifyLift f h = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F F' : Cᵒᵖ ⥤ Type w<VAR>G : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>h : CategoryTheory.Presieve.IsSheaf J F'<VAR>l₁ l₂ : (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G).toPresheaf ⟶ F'<VAR>e : CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe ⋯ ≫ l₁ = CategoryTheory.GrothendieckTopology.Subpresheaf.homOfLe ⋯ ≫ l₂<GOAL>l₁ = l₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>G G' : CategoryTheory.GrothendieckTopology.Subpresheaf F<VAR>h : G ≤ G'<VAR>hF : CategoryTheory.Presieve.IsSheaf J F<VAR>hG' : CategoryTheory.Presieve.IsSheaf J G'.toPresheaf<GOAL>CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J G ≤ G'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F' : Cᵒᵖ ⥤ Type w<VAR>f : F' ⟶ F<VAR>U : Cᵒᵖ<GOAL>(CategoryTheory.GrothendieckTopology.imagePresheaf f).obj U = Set.range (f.app U)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>U : Cᵒᵖ<GOAL>⊤.obj U = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : Cᵒᵖ ⥤ Type w<GOAL>CategoryTheory.GrothendieckTopology.imagePresheaf (𝟙 F) = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F' : Cᵒᵖ ⥤ Type w<VAR>f : F' ⟶ F<VAR>U : Cᵒᵖ<VAR>x : F'.obj U<GOAL>↑((CategoryTheory.GrothendieckTopology.toImagePresheaf f).app U x) = f.app U x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F F' : Cᵒᵖ ⥤ Type w<VAR>f : F' ⟶ F<VAR>X : Cᵒᵖ<GOAL>∀ (a : F'.obj X), ↑((J.toImagePresheafSheafify f).app X a) = f.app X a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F' : Cᵒᵖ ⥤ Type w<VAR>f : F' ⟶ F<GOAL>CategoryTheory.GrothendieckTopology.toImagePresheaf f ≫ (CategoryTheory.GrothendieckTopology.imagePresheaf f).ι = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F F' F'' : Cᵒᵖ ⥤ Type w<VAR>f₁ : F ⟶ F'<VAR>f₂ : F' ⟶ F''<GOAL>CategoryTheory.GrothendieckTopology.imagePresheaf (f₁ ≫ f₂) ≤ CategoryTheory.GrothendieckTopology.imagePresheaf f₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F F' : CategoryTheory.Sheaf J (Type w)<VAR>f : F ⟶ F'<GOAL>(CategoryTheory.GrothendieckTopology.imageSheaf f).val = (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.imagePresheaf f.val)).toPresheaf
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F F' : CategoryTheory.Sheaf J (Type w)<VAR>f : F ⟶ F'<GOAL>(CategoryTheory.GrothendieckTopology.toImageSheaf f).val = J.toImagePresheafSheafify f.val
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F F' : CategoryTheory.Sheaf J (Type w)<VAR>f : F ⟶ F'<GOAL>(CategoryTheory.GrothendieckTopology.imageSheafι f).val = (CategoryTheory.GrothendieckTopology.Subpresheaf.sheafify J (CategoryTheory.GrothendieckTopology.imagePresheaf f.val)).ι
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F F' : CategoryTheory.Sheaf J (Type w)<VAR>f : F ⟶ F'<GOAL>CategoryTheory.GrothendieckTopology.toImageSheaf f ≫ CategoryTheory.GrothendieckTopology.imageSheafι f = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>i : I<GOAL>1 i = 1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>γ : CategoryTheory.PresheafOfGroups.ZeroCochain G U<VAR>i : I<GOAL>γ⁻¹ i = (γ i)⁻¹
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>γ₁ γ₂ : CategoryTheory.PresheafOfGroups.ZeroCochain G U<VAR>i : I<GOAL>(γ₁ * γ₂) i = γ₁ i * γ₂ i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>self : CategoryTheory.PresheafOfGroups.OneCochain G U<VAR>i j : I<VAR>T T' : C<VAR>φ : T ⟶ T'<VAR>a : T' ⟶ U i<VAR>b : T' ⟶ U j<GOAL>(G.map φ.op) (self.ev i j a b) = self.ev i j (CategoryTheory.CategoryStruct.comp φ a) (CategoryTheory.CategoryStruct.comp φ b)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>i j : I<VAR>T : C<VAR>a : T ⟶ U i<VAR>b : T ⟶ U j<GOAL>CategoryTheory.PresheafOfGroups.OneCochain.ev 1 i j a b = 1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>γ₁ γ₂ : CategoryTheory.PresheafOfGroups.OneCochain G U<VAR>i j : I<VAR>T : C<VAR>a : T ⟶ U i<VAR>b : T ⟶ U j<GOAL>(γ₁ * γ₂).ev i j a b = γ₁.ev i j a b * γ₂.ev i j a b
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>γ : CategoryTheory.PresheafOfGroups.OneCochain G U<VAR>i j : I<VAR>T : C<VAR>a : T ⟶ U i<VAR>b : T ⟶ U j<GOAL>γ⁻¹.ev i j a b = (γ.ev i j a b)⁻¹
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>self : CategoryTheory.PresheafOfGroups.OneCocycle G U<VAR>i j k : I<VAR>T : C<VAR>a : T ⟶ U i<VAR>b : T ⟶ U j<VAR>c : T ⟶ U k<GOAL>self.ev i j a b * self.ev j k b c = self.ev i k a c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<GOAL>CategoryTheory.PresheafOfGroups.OneCocycle.toOneCochain 1 = 1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>γ : CategoryTheory.PresheafOfGroups.OneCocycle G U<VAR>i : I<VAR>T : C<VAR>a : T ⟶ U i<GOAL>γ.ev i i a a = 1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>γ : CategoryTheory.PresheafOfGroups.OneCocycle G U<VAR>i j : I<VAR>T : C<VAR>a : T ⟶ U i<VAR>b : T ⟶ U j<GOAL>γ.ev i j a b = (γ.ev j i b a)⁻¹
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>γ : CategoryTheory.PresheafOfGroups.OneCochain G U<GOAL>CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ γ 1
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>γ₁ γ₂ : CategoryTheory.PresheafOfGroups.OneCochain G U<VAR>α : CategoryTheory.PresheafOfGroups.ZeroCochain G U<VAR>h : CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ₁ γ₂ α<GOAL>CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ₂ γ₁ α⁻¹
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>γ₁ γ₂ γ₃ : CategoryTheory.PresheafOfGroups.OneCochain G U<VAR>α β : CategoryTheory.PresheafOfGroups.ZeroCochain G U<VAR>h₁₂ : CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ₁ γ₂ α<VAR>h₂₃ : CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ₂ γ₃ β<GOAL>CategoryTheory.PresheafOfGroups.OneCohomologyRelation γ₁ γ₃ (β * α)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<GOAL>Equivalence CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>γ₁ γ₂ : CategoryTheory.PresheafOfGroups.OneCocycle G U<GOAL>γ₁.class = γ₂.class ↔ γ₁.IsCohomologous γ₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>G : CategoryTheory.Functor Cᵒᵖ Grp<VAR>I : Type w'<VAR>U : I → C<VAR>γ₁ γ₂ : CategoryTheory.PresheafOfGroups.OneCocycle G U<VAR>h : γ₁.IsCohomologous γ₂<GOAL>γ₁.class = γ₂.class
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>self : CategoryTheory.HasPullbacksOfInclusions C<VAR>X Y Z : C<VAR>f : Z ⟶ X ⨿ Y<GOAL>CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inl f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.FinitaryPreExtensive C<VAR>X Y : C<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<GOAL>CategoryTheory.Limits.IsColimit c → CategoryTheory.IsUniversalColimit c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.FinitaryPreExtensive C<GOAL>CategoryTheory.HasPullbacksOfInclusions C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.FinitaryPreExtensive C<GOAL>CategoryTheory.Limits.HasFiniteCoproducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.FinitaryExtensive C<GOAL>CategoryTheory.HasPullbacksOfInclusions C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.FinitaryExtensive C<VAR>X Y : C<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<GOAL>CategoryTheory.Limits.IsColimit c → CategoryTheory.IsVanKampenColimit c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.FinitaryExtensive C<GOAL>CategoryTheory.Limits.HasFiniteCoproducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.FinitaryExtensive C<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.IsVanKampenColimit c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.FinitaryExtensive C<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.Mono c.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.FinitaryExtensive C<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.Mono c.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.FinitaryExtensive C<VAR>c : CategoryTheory.Limits.BinaryCofan X Y<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (CategoryTheory.Limits.initial.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) c.inl c.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>CategoryTheory.HasPullbacksOfInclusions C<VAR>T : C<VAR>HT : CategoryTheory.Limits.IsTerminal T<VAR>c₀ : CategoryTheory.Limits.BinaryCofan T T<VAR>hc₀ : CategoryTheory.Limits.IsColimit c₀<GOAL>CategoryTheory.FinitaryExtensive C ↔ CategoryTheory.IsVanKampenColimit c₀
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u''<VAR>CategoryTheory.Category.{v'', u''} D<VAR>CategoryTheory.Limits.HasFiniteCoproducts D<VAR>CategoryTheory.HasPullbacksOfInclusions D<VAR>CategoryTheory.FinitaryExtensive C<VAR>Gl : CategoryTheory.Functor C D<VAR>Gr : CategoryTheory.Functor D C<VAR>adj : Gl ⊣ Gr<VAR>Gr.Full<VAR>Gr.Faithful<VAR>∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), CategoryTheory.Limits.HasPullback (Gr.map f) (adj.unit.app Y)<VAR>(X : D) → (Y : C) → (f : X ⟶ Gl.obj Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (Gr.map f) (adj.unit.app Y)) Gl<VAR>CategoryTheory.PreservesPullbacksOfInclusions Gl<GOAL>CategoryTheory.FinitaryExtensive D
<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>CategoryTheory.FinitaryExtensive D<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>CategoryTheory.HasPullbacksOfInclusions C<VAR>CategoryTheory.PreservesPullbacksOfInclusions F<VAR>CategoryTheory.Limits.ReflectsLimitsOfShape CategoryTheory.Limits.WalkingCospan F<VAR>CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>CategoryTheory.Limits.ReflectsColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<GOAL>CategoryTheory.FinitaryExtensive C
<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>CategoryTheory.FinitaryExtensive D<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F<VAR>CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>F.ReflectsIsomorphisms<GOAL>CategoryTheory.FinitaryExtensive C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>n : ℕ<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete (Fin n)) C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.IsUniversalColimit c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>ι : Type u_1<VAR>Finite ι<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.IsUniversalColimit c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.FinitaryExtensive C<VAR>n : ℕ<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete (Fin n)) C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.IsVanKampenColimit c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.FinitaryExtensive C<VAR>ι : Type u_1<VAR>Finite ι<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>CategoryTheory.IsVanKampenColimit c
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>ι : Type u_1<VAR>Finite ι<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>i : CategoryTheory.Discrete ι<VAR>X : C<VAR>g : X ⟶ ((CategoryTheory.Functor.const (CategoryTheory.Discrete ι)).obj c.pt).obj i<GOAL>CategoryTheory.Limits.HasPullback g (c.ι.app i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.FinitaryExtensive C<VAR>ι : Type u_1<VAR>Finite ι<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>i : CategoryTheory.Discrete ι<GOAL>CategoryTheory.Mono (c.ι.app i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.FinitaryExtensive C<VAR>ι : Type u_1<VAR>Finite ι<VAR>F : CategoryTheory.Functor (CategoryTheory.Discrete ι) C<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>i j : CategoryTheory.Discrete ι<VAR>e : i ≠ j<GOAL>CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (F.obj i)) (CategoryTheory.Limits.initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.FinitaryExtensive C<VAR>ι : Type u_1<VAR>Finite ι<VAR>X : ι → C<VAR>i j : ι<VAR>e : i ≠ j<GOAL>CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (CategoryTheory.Limits.Sigma.ι X i) (CategoryTheory.Limits.Sigma.ι X j)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>α : Type<VAR>Finite α<VAR>X : C<VAR>Z : α → C<VAR>π : (a : α) → Z a ⟶ X<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hπ : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc π)<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc fun x => CategoryTheory.Limits.pullback.fst f (π x))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>I : C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>hF : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : CategoryTheory.Limits.IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : CategoryTheory.Limits.Cofan X<VAR>(CategoryTheory.Presieve.ofArrows X c.inj).hasPullbacks<VAR>CategoryTheory.Limits.HasInitial C<VAR>∀ (i : α), CategoryTheory.Mono (c.inj i)<VAR>hd : Pairwise fun i j => CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i)) (CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)<GOAL>CategoryTheory.Equalizer.Presieve.Arrows.firstMap F X c.inj = CategoryTheory.Equalizer.Presieve.Arrows.secondMap F X c.inj
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>α : Type<VAR>X : α → C<VAR>c : CategoryTheory.Limits.Cofan X<VAR>hc : CategoryTheory.Limits.IsColimit c<GOAL>let_fun this := ⋯;
(CategoryTheory.Limits.piComparison F fun x => Opposite.op (X x)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.opCoproductIsoProduct' hc (CategoryTheory.Limits.productIsProduct fun x => Opposite.op (X x))).inv) (CategoryTheory.Equalizer.Presieve.Arrows.forkMap F X c.inj)