ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>e : C ≌ E<GOAL>CategoryTheory.regularTopology.EqualizerCondition P ↔ CategoryTheory.regularTopology.EqualizerCondition (e.op.inverse.comp P)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>X B : C<VAR>π : X ⟶ B<VAR>c : CategoryTheory.Limits.PullbackCone π π<VAR>hc : CategoryTheory.Limits.IsLimit c<GOAL>(CategoryTheory.Limits.parallelPair (CategoryTheory.Over.homMk c.fst ⋯).op (CategoryTheory.Over.homMk c.snd ⋯).op).Initial
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>P : CategoryTheory.Functor Cᵒᵖ D<VAR>X B : C<VAR>π : X ⟶ B<VAR>CategoryTheory.Limits.HasPullback π π<GOAL>CategoryTheory.regularTopology.SingleEqualizerCondition P π ↔ Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.ofArrows (fun x => X) fun x => π).arrows.cocone.op))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>F : CategoryTheory.Functor Cᵒᵖ D<VAR>CategoryTheory.Preregular C<VAR>∀ {Y X : C} (f : Y ⟶ X) [inst : CategoryTheory.EffectiveEpi f], CategoryTheory.Limits.HasPullback f f<GOAL>CategoryTheory.regularTopology.EqualizerCondition F ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>X : C<VAR>S : CategoryTheory.Presieve X<VAR>S.regular<VAR>CategoryTheory.Projective X<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type u_4)<GOAL>CategoryTheory.Presieve.IsSheafFor F S
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>F : CategoryTheory.Functor Cᵒᵖ D<VAR>CategoryTheory.Preregular C<VAR>∀ (X : C), CategoryTheory.Projective X<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preregular C<VAR>W : C<GOAL>CategoryTheory.Presieve.IsSheaf (CategoryTheory.regularTopology C) (CategoryTheory.yoneda.obj W)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Preregular C<GOAL>CategoryTheory.Sheaf.Subcanonical (CategoryTheory.regularTopology C)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>hp : CategoryTheory.Presieve.IsSheaf J P<VAR>R : CategoryTheory.Presieve X<VAR>hr : CategoryTheory.Sieve.generate R ∈ J.sieves X<GOAL>CategoryTheory.Presieve.IsSheafFor P R
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>J₁ J₂ : CategoryTheory.GrothendieckTopology C<GOAL>J₁ ≤ J₂ → CategoryTheory.Presieve.IsSheaf J₂ P → CategoryTheory.Presieve.IsSheaf J₁ P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>h : CategoryTheory.Presieve.IsSheaf J P<GOAL>CategoryTheory.Presieve.IsSeparated J P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P' : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>i : P ≅ P'<VAR>h : CategoryTheory.Presieve.IsSheaf J P<GOAL>CategoryTheory.Presieve.IsSheaf J P'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>h : ∀ {X : C}, ∀ S ∈ J.sieves X, CategoryTheory.Presieve.YonedaSheafCondition P S<GOAL>CategoryTheory.Presieve.IsSheaf J P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>K : CategoryTheory.Pretopology C<GOAL>CategoryTheory.Presieve.IsSheaf (CategoryTheory.Pretopology.toGrothendieck C K) P ↔ ∀ {X : C}, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor P R
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<GOAL>CategoryTheory.Presieve.IsSheaf ⊥ P
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>s : CategoryTheory.Limits.Cocone S.arrows.diagram<GOAL>(S.arrows.yonedaFamilyOfElements_fromCocone s).Compatible
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>(∀ (W : C), CategoryTheory.Presieve.IsSheafFor (CategoryTheory.yoneda.obj W) S.arrows) ↔ Nonempty (CategoryTheory.Limits.IsColimit S.arrows.cocone)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>self : CategoryTheory.SheafOfTypes J<GOAL>CategoryTheory.Presieve.IsSheaf J self.val
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<GOAL>∀ {X Y Z : CategoryTheory.SheafOfTypes J} (f : X ⟶ Y) (g : Y ⟶ Z), (CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<GOAL>∀ (x : CategoryTheory.SheafOfTypes J), (CategoryTheory.CategoryStruct.id x).val = CategoryTheory.CategoryStruct.id x.val
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X Y : CategoryTheory.SheafOfTypes J<VAR>f g : X ⟶ Y<VAR>w : f.val = g.val<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>self : CategoryTheory.SheafOfTypes J<GOAL>(CategoryTheory.sheafOfTypesToPresheaf J).obj self = self.val
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<GOAL>∀ {X Y : CategoryTheory.SheafOfTypes J} (f : X ⟶ Y), (CategoryTheory.sheafOfTypesToPresheaf J).map f = f.val
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.sheafOfTypesBotEquiv.functor = CategoryTheory.sheafOfTypesToPresheaf ⊥
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : X ⟶ Y), (CategoryTheory.sheafOfTypesBotEquiv.inverse.map f).val = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.sheafOfTypesBotEquiv.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.SheafOfTypes ⊥))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.sheafOfTypesBotEquiv.counitIso = CategoryTheory.Iso.refl ({ obj := fun P => { val := P, cond := ⋯ }, map := fun {X Y} f => { val := f }, map_id := ⋯, map_comp := ⋯ }.comp (CategoryTheory.sheafOfTypesToPresheaf ⊥))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<GOAL>(CategoryTheory.sheafOfTypesBotEquiv.inverse.obj P).val = P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>B : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} B<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : CategoryTheory.Functor A B<VAR>self : J.HasSheafCompose F<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>hP : CategoryTheory.Presheaf.IsSheaf J P<GOAL>CategoryTheory.Presheaf.IsSheaf J (P.comp F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>B : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} B<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : CategoryTheory.Functor A B<VAR>J.HasSheafCompose F<GOAL>∀ {X Y : CategoryTheory.Sheaf J A} (η : X ⟶ Y), ((CategoryTheory.sheafCompose J F).map η).val = CategoryTheory.whiskerRight η.val F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>B : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} B<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : CategoryTheory.Functor A B<VAR>J.HasSheafCompose F<VAR>G : CategoryTheory.Sheaf J A<GOAL>((CategoryTheory.sheafCompose J F).obj G).val = G.val.comp F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>B : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} B<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : CategoryTheory.Functor A B<VAR>J.HasSheafCompose F<GOAL>CategoryTheory.sheafCompose_map J (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id (CategoryTheory.sheafCompose J F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>B : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} B<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F G : CategoryTheory.Functor A B<VAR>H : CategoryTheory.Functor A B<VAR>η : F ⟶ G<VAR>γ : G ⟶ H<VAR>J.HasSheafCompose F<VAR>J.HasSheafCompose G<VAR>J.HasSheafCompose H<GOAL>CategoryTheory.sheafCompose_map J (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafCompose_map J η) (CategoryTheory.sheafCompose_map J γ)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>B : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} B<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : CategoryTheory.Functor A B<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>X : C<VAR>S : J.Cover X<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingMulticospan (S.index (P.comp F)).fstTo (S.index (P.comp F)).sndTo), (CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).hom.app X_1 = (match X_1 with | CategoryTheory.Limits.WalkingMulticospan.left a => CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op a.Y))) | CategoryTheory.Limits.WalkingMulticospan.right b => CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op b.r.Z)))).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>B : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} B<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : CategoryTheory.Functor A B<VAR>P : CategoryTheory.Functor Cᵒᵖ A<VAR>X : C<VAR>S : J.Cover X<GOAL>∀ (X_1 : CategoryTheory.Limits.WalkingMulticospan (S.index (P.comp F)).fstTo (S.index (P.comp F)).sndTo), (CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).inv.app X_1 = (match X_1 with | CategoryTheory.Limits.WalkingMulticospan.left a => CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op a.Y))) | CategoryTheory.Limits.WalkingMulticospan.right b => CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op b.r.Z)))).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>CategoryTheory.ConcreteCategory A<VAR>J.HasSheafCompose (CategoryTheory.forget A)<VAR>F : CategoryTheory.Sheaf J A<GOAL>CategoryTheory.Presheaf.IsSeparated J F.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : CategoryTheory.Functor Cᵒᵖ A<VAR>CategoryTheory.ConcreteCategory A<VAR>J.HasSheafCompose (CategoryTheory.forget A)<VAR>hF : CategoryTheory.Presheaf.IsSheaf J F<GOAL>CategoryTheory.Presheaf.IsSeparated J F
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} A<GOAL>J.W = CategoryTheory.Localization.LeftBousfield.W fun x => x ∈ Set.range (CategoryTheory.sheafToPresheaf J A).obj
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} A<VAR>F₁ F₂ : CategoryTheory.Sheaf J A<VAR>φ : F₁ ⟶ F₂<GOAL>J.W ((CategoryTheory.sheafToPresheaf J A).map φ) ↔ CategoryTheory.IsIso φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} A<VAR>G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)<VAR>adj : G ⊣ CategoryTheory.sheafToPresheaf J A<VAR>P : CategoryTheory.Functor Cᵒᵖ A<GOAL>J.W (adj.unit.app P)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} A<VAR>G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)<VAR>adj : G ⊣ CategoryTheory.sheafToPresheaf J A<VAR>P₁ P₂ : CategoryTheory.Functor Cᵒᵖ A<VAR>f : P₁ ⟶ P₂<GOAL>J.W f ↔ CategoryTheory.IsIso (G.map f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} A<VAR>G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)<VAR>adj : G ⊣ CategoryTheory.sheafToPresheaf J A<GOAL>J.W = (CategoryTheory.MorphismProperty.isomorphisms (CategoryTheory.Sheaf J A)).inverseImage G
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} A<VAR>CategoryTheory.HasWeakSheafify J A<VAR>P : CategoryTheory.Functor Cᵒᵖ A<GOAL>J.W (CategoryTheory.toSheafify J P)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} A<VAR>CategoryTheory.HasWeakSheafify J A<VAR>P₁ P₂ : CategoryTheory.Functor Cᵒᵖ A<VAR>f : P₁ ⟶ P₂<GOAL>J.W f ↔ CategoryTheory.IsIso ((CategoryTheory.presheafToSheaf J A).map f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} A<VAR>CategoryTheory.HasWeakSheafify J A<GOAL>J.W = (CategoryTheory.MorphismProperty.isomorphisms (CategoryTheory.Sheaf J A)).inverseImage (CategoryTheory.presheafToSheaf J A)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>hX : CategoryTheory.Limits.IsTerminal X<VAR>I : Type u_1<VAR>Y : I → C<GOAL>J.CoversTop Y ↔ CategoryTheory.Sieve.ofObjects Y X ∈ J.sieves X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>I : Type u_1<VAR>Y : I → C<VAR>hY : J.CoversTop Y<VAR>F : CategoryTheory.Sheaf J A<VAR>c : CategoryTheory.Limits.Cone F.val<VAR>hc : CategoryTheory.Limits.IsLimit c<VAR>X : A<VAR>f g : X ⟶ c.pt<VAR>h : ∀ (i : I), CategoryTheory.CategoryStruct.comp f (c.π.app (Opposite.op (Y i))) = CategoryTheory.CategoryStruct.comp g (c.π.app (Opposite.op (Y i)))<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>I : Type u_1<VAR>Y : I → C<VAR>hY : J.CoversTop Y<VAR>F : CategoryTheory.Sheaf J (Type u_2)<VAR>x y : ↑F.val.sections<VAR>h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))<GOAL>x = y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>I : Type u_1<VAR>Y : I → C<VAR>x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y<VAR>hx : x.IsCompatible<VAR>X Z : C<VAR>f : Z ⟶ X<VAR>i : I<VAR>φ : Z ⟶ Y i<GOAL>x.familyOfElements X f ⋯ = F.map φ.op (x i)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>I : Type u_1<VAR>Y : I → C<VAR>x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y<VAR>hx : x.IsCompatible<VAR>X : C<GOAL>(x.familyOfElements X).Compatible
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>I : Type u_1<VAR>Y : I → C<VAR>x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y<VAR>hx : x.IsCompatible<VAR>hY : J.CoversTop Y<VAR>hF : CategoryTheory.Presheaf.IsSheaf J F<GOAL>∃! s, ∀ (i : I), ↑s (Opposite.op (Y i)) = x i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type w)<VAR>I : Type u_1<VAR>Y : I → C<VAR>x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y<VAR>hx : x.IsCompatible<VAR>hY : J.CoversTop Y<VAR>hF : CategoryTheory.Presheaf.IsSheaf J F<VAR>i : I<GOAL>↑(hx.section_ hY hF) (Opposite.op (Y i)) = x i
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>x : E<GOAL>x ∈ IntermediateField.adjoin F S ↔ ∃ r s, x = (MvPolynomial.aeval Subtype.val) r / (MvPolynomial.aeval Subtype.val) s
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<VAR>x : E<GOAL>x ∈ F⟮α⟯ ↔ ∃ r s, x = (Polynomial.aeval α) r / (Polynomial.aeval α) s
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>T : IntermediateField F E<GOAL>IntermediateField.adjoin F S ≤ T ↔ S ≤ ↑T
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>GaloisConnection (IntermediateField.adjoin F) fun x => ↑x
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>↑⊥ = Set.range ⇑(algebraMap F E)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>x : E<GOAL>x ∈ ⊥ ↔ x ∈ Set.range ⇑(algebraMap F E)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>⊥.toSubalgebra = ⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>↑⊤ = Set.univ
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>x : E<GOAL>x ∈ ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>⊤.toSubalgebra = ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>⊤.toSubfield = ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S T : IntermediateField F E<GOAL>↑(S ⊓ T) = ↑S ∩ ↑T
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S T : IntermediateField F E<VAR>x : E<GOAL>x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S T : IntermediateField F E<GOAL>(S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S T : IntermediateField F E<GOAL>(S ⊓ T).toSubfield = S.toSubfield ⊓ T.toSubfield
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set (IntermediateField F E)<GOAL>↑(sInf S) = sInf ((fun x => ↑x) '' S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set (IntermediateField F E)<GOAL>(sInf S).toSubalgebra = sInf (IntermediateField.toSubalgebra '' S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set (IntermediateField F E)<GOAL>(sInf S).toSubfield = sInf (IntermediateField.toSubfield '' S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>ι : Sort u_3<VAR>S : ι → IntermediateField F E<GOAL>↑(iInf S) = ⋂ i, ↑(S i)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>ι : Sort u_3<VAR>S : ι → IntermediateField F E<GOAL>(iInf S).toSubalgebra = ⨅ i, (S i).toSubalgebra
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>ι : Sort u_3<VAR>S : ι → IntermediateField F E<GOAL>(iInf S).toSubfield = ⨅ i, (S i).toSubfield
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S T : IntermediateField F E<VAR>h : S = T<VAR>x : ↥S.toSubalgebra<GOAL>(IntermediateField.equivOfEq h) x = ⟨↑x, ⋯⟩
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S T : IntermediateField F E<VAR>h : S = T<GOAL>(IntermediateField.equivOfEq h).symm = IntermediateField.equivOfEq ⋯
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : IntermediateField F E<GOAL>IntermediateField.equivOfEq ⋯ = AlgEquiv.refl
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S T U : IntermediateField F E<VAR>hST : S = T<VAR>hTU : T = U<GOAL>(IntermediateField.equivOfEq hST).trans (IntermediateField.equivOfEq hTU) = IntermediateField.equivOfEq ⋯
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>x : F<GOAL>(IntermediateField.botEquiv F E) ((algebraMap F ↥⊥) x) = x
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>x : F<GOAL>(IntermediateField.botEquiv F E).symm x = (algebraMap F ↥⊥) x
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>⇑(algebraMap (↥⊥) F) = ⇑(IntermediateField.botEquiv F E)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>∀ (a : E), ↑(IntermediateField.topEquiv.symm a) = ↑((↑↑Subalgebra.topEquiv).symm a)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<GOAL>∀ (a : ↥⊤.toSubalgebra), IntermediateField.topEquiv a = ↑a
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : IntermediateField F E<GOAL>IntermediateField.restrictScalars F ⊥ = K
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra K E<VAR>Algebra K F<VAR>IsScalarTower K F E<GOAL>IntermediateField.restrictScalars K ⊤ = ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>f : E →ₐ[F] K<GOAL>IntermediateField.map f ⊥ = ⊥
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>s t : IntermediateField F E<VAR>f : E →ₐ[F] K<GOAL>IntermediateField.map f (s ⊔ t) = IntermediateField.map f s ⊔ IntermediateField.map f t
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>ι : Sort u_4<VAR>f : E →ₐ[F] K<VAR>s : ι → IntermediateField F E<GOAL>IntermediateField.map f (iSup s) = ⨆ i, IntermediateField.map f (s i)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>f : E →ₐ[F] K<GOAL>f.fieldRange = IntermediateField.map f ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>L : Type u_4<VAR>Field L<VAR>Algebra F L<VAR>f : E →ₐ[F] K<VAR>g : K →ₐ[F] L<GOAL>IntermediateField.map g f.fieldRange = (g.comp f).fieldRange
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>f : E →ₐ[F] K<GOAL>f.fieldRange = ⊤ ↔ Function.Surjective ⇑f
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>f : E ≃ₐ[F] K<GOAL>(↑f).fieldRange = ⊤
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>L : IntermediateField F E<VAR>f : E →ₐ[F] K<GOAL>(f.comp L.val).fieldRange = IntermediateField.map f L
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>K : Type u_3<VAR>Field K<VAR>Algebra F K<VAR>L : IntermediateField F E<VAR>f : E →ₐ[F] K<VAR>x : ↥L<GOAL>↑((L.equivMap f) x) = f ↑x
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<GOAL>↑(IntermediateField.adjoin F S) = Set.range ⇑(algebraMap (↥(IntermediateField.adjoin F S)) E)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>x : F<GOAL>(algebraMap F E) x ∈ IntermediateField.adjoin F S
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<GOAL>Set.range ⇑(algebraMap F E) ⊆ ↑(IntermediateField.adjoin F S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<GOAL>S ⊆ ↑(IntermediateField.adjoin F S)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>S T : Set E<VAR>h : S ⊆ T<GOAL>IntermediateField.adjoin F S ≤ IntermediateField.adjoin F T
<VAR>E : Type u_2<VAR>Field E<VAR>S : Set E<VAR>F : Subfield E<GOAL>↑F ⊆ ↑(IntermediateField.adjoin (↥F) S)
<VAR>E : Type u_2<VAR>Field E<VAR>S : Set E<VAR>F : Subfield E<VAR>T : Set E<VAR>HT : T ⊆ ↑F<GOAL>T ⊆ ↑(IntermediateField.adjoin (↥F) S)