ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>I : Type u_1<VAR>B : C<VAR>s : Finset I<VAR>P : I → CategoryTheory.Subobject B<VAR>i : I<VAR>m : i ∈ s<GOAL>(P i).Factors (s.inf P).arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>A : C<VAR>f₁ : CategoryTheory.MonoOver A<VAR>f₂ : CategoryTheory.Subobject A<GOAL>(CategoryTheory.Subobject.inf.obj (Quotient.mk'' f₁)).obj f₂ = (CategoryTheory.Subobject.map f₁.arrow).obj ((CategoryTheory.Subobject.pullback f₁.arrow).obj f₂)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>A : C<VAR>f₁ : CategoryTheory.MonoOver A<VAR>f₂ : CategoryTheory.Subobject A<GOAL>Quotient.mk'' f₁ ⊓ f₂ = (CategoryTheory.Subobject.map f₁.arrow).obj ((CategoryTheory.Subobject.pullback f₁.arrow).obj f₂)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>A : C<VAR>f₁ f₂ : CategoryTheory.Subobject A<VAR>CategoryTheory.Limits.HasBinaryProduct f₁ f₂<GOAL>(f₁ ⨯ f₂) = f₁ ⊓ f₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>B : C<VAR>m m' : CategoryTheory.Subobject B<GOAL>m ⊓ m' = (CategoryTheory.Subobject.inf.obj m).obj m'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : C<VAR>g : X ⟶ Y<VAR>f₁ f₂ : CategoryTheory.Subobject Y<GOAL>(CategoryTheory.Subobject.pullback g).obj (f₁ ⊓ f₂) = (CategoryTheory.Subobject.pullback g).obj f₁ ⊓ (CategoryTheory.Subobject.pullback g).obj f₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : C<VAR>g : Y ⟶ X<VAR>CategoryTheory.Mono g<VAR>f₁ f₂ : CategoryTheory.Subobject Y<GOAL>(CategoryTheory.Subobject.map g).obj (f₁ ⊓ f₂) = (CategoryTheory.Subobject.map g).obj f₁ ⊓ (CategoryTheory.Subobject.map g).obj f₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasImages C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>A B : C<VAR>X Y : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>P : X.Factors f<GOAL>(X ⊔ Y).Factors f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasImages C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>A B : C<VAR>X Y : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>P : Y.Factors f<GOAL>(X ⊔ Y).Factors f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasImages C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasInitial C<VAR>CategoryTheory.Limits.InitialMonoClass C<VAR>I : Type u_1<VAR>A B : C<VAR>s : Finset I<VAR>P : I → CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>h : ∃ i ∈ s, (P i).Factors f<GOAL>(s.sup P).Factors f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.WellPowered C<VAR>A : C<VAR>s : Set (CategoryTheory.Subobject A)<VAR>j : ↑(⇑(equivShrink (CategoryTheory.Subobject A)) '' s)<GOAL>(CategoryTheory.Subobject.wideCospan s).map (CategoryTheory.Limits.WidePullbackShape.Hom.term j) = ((equivShrink (CategoryTheory.Subobject A)).symm ↑j).arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.WellPowered C<VAR>A : C<VAR>s : Set (CategoryTheory.Subobject A)<VAR>f : CategoryTheory.Subobject A<VAR>k : ∀ g ∈ s, f ≤ g<GOAL>(CategoryTheory.Subobject.leInfCone s f k).π.app none = f.arrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.WellPowered C<VAR>CategoryTheory.Limits.HasWidePullbacks C<VAR>A : C<VAR>s : Set (CategoryTheory.Subobject A)<VAR>f : CategoryTheory.Subobject A<VAR>hf : f ∈ s<GOAL>CategoryTheory.Subobject.sInf s ≤ f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.WellPowered C<VAR>CategoryTheory.Limits.HasWidePullbacks C<VAR>A : C<VAR>s : Set (CategoryTheory.Subobject A)<VAR>f : CategoryTheory.Subobject A<VAR>k : ∀ g ∈ s, f ≤ g<GOAL>f ≤ CategoryTheory.Subobject.sInf s
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.WellPowered C<VAR>CategoryTheory.Limits.HasCoproducts C<VAR>CategoryTheory.Limits.HasImages C<VAR>A : C<VAR>s : Set (CategoryTheory.Subobject A)<VAR>f : CategoryTheory.Subobject A<VAR>hf : f ∈ s<GOAL>f ≤ CategoryTheory.Subobject.sSup s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>x : β<GOAL>e.symm x ∈ s ↔ x ∈ ⇑e '' s
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.WellPowered C<VAR>CategoryTheory.Limits.HasCoproducts C<VAR>CategoryTheory.Limits.HasImages C<VAR>A : C<VAR>s : Set (CategoryTheory.Subobject A)<VAR>f : CategoryTheory.Subobject A<VAR>k : ∀ g ∈ s, g ≤ f<GOAL>CategoryTheory.Subobject.sSup s ≤ f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>X : C<VAR>h : ¬CategoryTheory.Limits.IsZero X<GOAL>Nontrivial (CategoryTheory.Subobject X)
<VAR>C : Type v₁<VAR>CategoryTheory.SmallCategory C<VAR>D : Type v₁<VAR>CategoryTheory.SmallCategory D<VAR>G : CategoryTheory.Functor C D<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>CategoryTheory.ConcreteCategory A<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)<VAR>CategoryTheory.Limits.HasColimits A<VAR>CategoryTheory.Limits.HasLimits A<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)<VAR>(CategoryTheory.forget A).ReflectsIsomorphisms<VAR>X : CategoryTheory.Sheaf J A<GOAL>(G.sheafPullback A J K).obj X = (CategoryTheory.presheafToSheaf K A).obj (G.op.lan.obj X.val)
<VAR>C : Type v₁<VAR>CategoryTheory.SmallCategory C<VAR>D : Type v₁<VAR>CategoryTheory.SmallCategory D<VAR>G : CategoryTheory.Functor C D<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>K : CategoryTheory.GrothendieckTopology D<VAR>CategoryTheory.ConcreteCategory A<VAR>CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)<VAR>CategoryTheory.Limits.HasColimits A<VAR>CategoryTheory.Limits.HasLimits A<VAR>CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)<VAR>(CategoryTheory.forget A).ReflectsIsomorphisms<GOAL>∀ {X Y : CategoryTheory.Sheaf J A} (f : X ⟶ Y), (G.sheafPullback A J K).map f = (CategoryTheory.presheafToSheaf K A).map (G.op.lan.map f.val)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.HasWeakSheafify J D<VAR>T : C<VAR>hT : CategoryTheory.Limits.IsTerminal T<VAR>F : CategoryTheory.Sheaf J D<GOAL>(CategoryTheory.constantSheafAdj J D hT).counit.app F = CategoryTheory.CategoryStruct.comp ((CategoryTheory.presheafToSheaf J D).map ((CategoryTheory.constantPresheafAdj D hT).counit.app F.val)) ((CategoryTheory.sheafificationAdjunction J D).counit.app F)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>self : IsPurelyInseparable F E<GOAL>Algebra.IsIntegral F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>self : IsPurelyInseparable F E<VAR>x : E<GOAL>IsSeparable F x → x ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsPurelyInseparable F E<VAR>x : E<GOAL>IsIntegral F x
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsPurelyInseparable F E<GOAL>Algebra.IsAlgebraic F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsPurelyInseparable F E<VAR>x : E<GOAL>IsSeparable F x → x ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>IsPurelyInseparable F E ↔ ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
<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>e : K ≃ₐ[F] E<VAR>IsPurelyInseparable F K<GOAL>IsPurelyInseparable F E
<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>e : K ≃ₐ[F] E<GOAL>IsPurelyInseparable F K ↔ IsPurelyInseparable F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsAlgebraic F E<VAR>IsSepClosed F<GOAL>IsPurelyInseparable F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsPurelyInseparable F E<VAR>Algebra.IsSeparable F E<GOAL>Function.Surjective ⇑(algebraMap F E)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsPurelyInseparable F E<VAR>Algebra.IsSeparable F E<GOAL>Function.Bijective ⇑(algebraMap 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>IsPurelyInseparable F ↥L<VAR>Algebra.IsSeparable F ↥L<GOAL>L = ⊥
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsPurelyInseparable F E<GOAL>separableClosure F E = ⊥
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsAlgebraic F E<GOAL>separableClosure F E = ⊥ ↔ IsPurelyInseparable F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>q : ℕ<VAR>ExpChar F q<GOAL>IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>q : ℕ<VAR>ExpChar F q<VAR>IsPurelyInseparable F E<VAR>x : E<GOAL>∃ n, x ^ q ^ n ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>x : E<GOAL>x ∈ perfectClosure F E ↔ ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>q : ℕ<VAR>ExpChar F q<VAR>x : E<GOAL>x ∈ perfectClosure F E ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>x : E<GOAL>x ∈ perfectClosure F E ↔ (minpoly F x).natSepDegree = 1
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>IsPurelyInseparable F E ↔ perfectClosure F E = ⊤
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsSeparable F E<GOAL>perfectClosure 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>h : IsPurelyInseparable F ↥L<GOAL>L ≤ perfectClosure 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<GOAL>L ≤ perfectClosure F E ↔ IsPurelyInseparable F ↥L
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>separableClosure F E ⊓ perfectClosure F E = ⊥
<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>i : E →ₐ[F] K<VAR>x : E<GOAL>i x ∈ perfectClosure F K ↔ x ∈ perfectClosure F E
<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>i : E →ₐ[F] K<GOAL>IntermediateField.comap i (perfectClosure F K) = perfectClosure F E
<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>i : E →ₐ[F] K<GOAL>IntermediateField.map i (perfectClosure F E) ≤ perfectClosure F K
<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>i : E ≃ₐ[F] K<GOAL>IntermediateField.map (↑i) (perfectClosure F E) = perfectClosure F K
<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>IsPurelyInseparable F K<GOAL>IsPurelyInseparable F E
<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>h : IsPurelyInseparable F K<GOAL>IsPurelyInseparable E K
<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>h1 : IsPurelyInseparable F E<VAR>h2 : IsPurelyInseparable E K<GOAL>IsPurelyInseparable F K
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>IsPurelyInseparable F E ↔ ∀ (x : E), (minpoly F x).natSepDegree = 1
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsPurelyInseparable F E<VAR>x : E<GOAL>(minpoly F x).natSepDegree = 1
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>q : ℕ<VAR>hF : ExpChar F q<GOAL>IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n y, minpoly F x = Polynomial.X ^ q ^ n - Polynomial.C y
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>q : ℕ<VAR>ExpChar F q<VAR>IsPurelyInseparable F E<VAR>x : E<GOAL>∃ n y, minpoly F x = Polynomial.X ^ q ^ n - Polynomial.C y
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>q : ℕ<VAR>hF : ExpChar F q<GOAL>IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (Polynomial.X - Polynomial.C x) ^ q ^ n
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>q : ℕ<VAR>ExpChar F q<VAR>IsPurelyInseparable F E<VAR>x : E<GOAL>∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (Polynomial.X - Polynomial.C x) ^ q ^ n
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsAlgebraic F E<VAR>hdeg : Field.finSepDegree F E = 1<GOAL>IsPurelyInseparable F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsPurelyInseparable F E<VAR>L : Type w<VAR>CommRing L<VAR>IsReduced L<GOAL>Function.Injective fun f => f.comp (algebraMap F E)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsPurelyInseparable F E<GOAL>Field.finSepDegree F E = 1
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsPurelyInseparable F E<GOAL>Field.sepDegree F E = 1
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsPurelyInseparable F E<GOAL>Field.insepDegree F E = Module.rank F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsPurelyInseparable F E<GOAL>Field.finInsepDegree 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>Algebra.IsAlgebraic F E<GOAL>IsPurelyInseparable F E ↔ Field.finSepDegree F E = 1
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsAlgebraic F E<GOAL>IsPurelyInseparable F E ↔ ∀ (L : IntermediateField F E), FiniteDimensional F ↥L → IsPurelyInseparable F ↥L
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsAlgebraic F E<GOAL>IsPurelyInseparable (↥(separableClosure F E)) 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>h : IsPurelyInseparable (↥L) E<GOAL>separableClosure F E ≤ L
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsAlgebraic F E<VAR>L : IntermediateField F E<GOAL>separableClosure F E ≤ L ↔ IsPurelyInseparable (↥L) 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>IsPurelyInseparable (↥L) E<GOAL>L = separableClosure F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsAlgebraic F E<VAR>L : IntermediateField F E<GOAL>L = separableClosure F E ↔ Algebra.IsSeparable F ↥L ∧ IsPurelyInseparable (↥L) E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>x : E<GOAL>IsPurelyInseparable F ↥F⟮x⟯ ↔ (minpoly F x).natSepDegree = 1
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<GOAL>IsPurelyInseparable F ↥F⟮x⟯ ↔ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>q : ℕ<VAR>hF : ExpChar F q<VAR>S : Set E<GOAL>IsPurelyInseparable F ↥(IntermediateField.adjoin F S) ↔ ∀ x ∈ S, ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>Algebra.IsSeparable F ↥(IntermediateField.adjoin F S)<VAR>q : ℕ<VAR>ExpChar F q<VAR>n : ℕ<GOAL>IntermediateField.adjoin F S = IntermediateField.adjoin F ((fun x => x ^ q ^ n) '' S)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsSeparable F E<VAR>S : Set E<VAR>q : ℕ<VAR>ExpChar F q<VAR>n : ℕ<GOAL>IntermediateField.adjoin F S = IntermediateField.adjoin F ((fun x => x ^ q ^ n) '' S)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>S : Set E<VAR>Algebra.IsSeparable F ↥(IntermediateField.adjoin F S)<VAR>q : ℕ<VAR>ExpChar F q<GOAL>IntermediateField.adjoin F S = IntermediateField.adjoin F ((fun x => x ^ q) '' S)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsSeparable F E<VAR>S : Set E<VAR>q : ℕ<VAR>ExpChar F q<GOAL>IntermediateField.adjoin F S = IntermediateField.adjoin F ((fun x => x ^ q) '' S)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>Algebra.IsSeparable F E<VAR>h : Submodule.span F (Set.range v) = ⊤<GOAL>Submodule.span F (Set.range fun x => v x ^ q ^ n) = ⊤
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>FiniteDimensional F E<VAR>Algebra.IsSeparable F E<VAR>h : LinearIndependent F v<GOAL>LinearIndependent F fun x => v x ^ q ^ n
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>Algebra.IsSeparable F E<VAR>h : LinearIndependent F v<GOAL>LinearIndependent F fun x => v x ^ q ^ n
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>q n : ℕ<VAR>hF : ExpChar F q<VAR>ι : Type u_1<VAR>v : ι → E<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<GOAL>LinearIndependent F fun x => v x ^ q ^ n
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsAlgClosure F E<GOAL>IsSepClosed F ↔ IsPurelyInseparable F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsAlgebraic F E<VAR>IsSepClosed F<GOAL>IsSepClosed E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>h : PerfectField E<VAR>eq : perfectClosure F E = ⊥<GOAL>PerfectField F
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsSeparable F E<VAR>PerfectField E<GOAL>PerfectField F
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>IsAlgClosure F E<GOAL>PerfectField F ↔ Algebra.IsSeparable F E
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Algebra.IsAlgebraic F E<GOAL>Field.finSepDegree F E = Cardinal.toNat (Field.sepDegree F E)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>Field.finSepDegree F E * Field.finInsepDegree 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>K : Type w<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<VAR>Algebra.IsAlgebraic F E<VAR>Algebra.IsSeparable E K<GOAL>IntermediateField.adjoin E ↑(separableClosure F K) = ⊤
<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.IsAlgebraic F E<GOAL>IntermediateField.adjoin E ↑(separableClosure F K) = separableClosure E K
<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>IsPurelyInseparable F E<VAR>ι : Type u_1<VAR>v : ι → K<VAR>hsep : ∀ (i : ι), IsSeparable F (v i)<VAR>h : LinearIndependent F v<GOAL>LinearIndependent E v
<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>IsPurelyInseparable F E<VAR>Algebra.IsSeparable E K<GOAL>Field.sepDegree F K = Module.rank E K
<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<GOAL>Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (Field.sepDegree E K) = Cardinal.lift.{v, w} (Field.sepDegree F K)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>K : Type v<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<VAR>Algebra.IsSeparable F E<GOAL>Module.rank F E * Field.sepDegree E K = Field.sepDegree F K
<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>IsPurelyInseparable F E<GOAL>Field.sepDegree F K = Field.sepDegree E K
<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.IsAlgebraic F E<GOAL>Cardinal.lift.{w, v} (Field.sepDegree F E) * Cardinal.lift.{v, w} (Field.sepDegree E K) = Cardinal.lift.{v, w} (Field.sepDegree F K)
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>K : Type v<VAR>Field K<VAR>Algebra F K<VAR>Algebra E K<VAR>IsScalarTower F E K<VAR>Algebra.IsAlgebraic F E<GOAL>Field.sepDegree F E * Field.sepDegree E K = Field.sepDegree F K
<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>S : Set K<VAR>Algebra.IsAlgebraic F ↥(IntermediateField.adjoin F S)<VAR>IsPurelyInseparable F E<GOAL>Field.sepDegree E ↥(IntermediateField.adjoin E S) = Field.sepDegree F ↥(IntermediateField.adjoin F S)
<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>S : IntermediateField F K<VAR>Algebra.IsAlgebraic F ↥S<VAR>IsPurelyInseparable F E<GOAL>Field.sepDegree E ↥(IntermediateField.adjoin E ↑S) = Field.sepDegree F ↥S
<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>x : K<VAR>hsep : IsSeparable F x<VAR>IsPurelyInseparable F E<GOAL>Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>f : F[X]<VAR>hsep : f.Separable<VAR>hirr : Irreducible f<VAR>IsPurelyInseparable F E<GOAL>Irreducible (Polynomial.map (algebraMap F E) f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>D : Type w<VAR>CategoryTheory.Category.{w', w} D<VAR>K : Type z<VAR>CategoryTheory.Category.{z', z} K<VAR>CategoryTheory.Limits.HasLimitsOfShape K D<VAR>F : CategoryTheory.Functor K (CategoryTheory.Sheaf J D)<VAR>E : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.sheafToPresheaf J D))<VAR>hE : CategoryTheory.Limits.IsLimit E<GOAL>CategoryTheory.Presheaf.IsSheaf J E.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>F : CategoryTheory.Functor Cᵒᵖ D<VAR>X : Cᵒᵖ<VAR>x y : (CategoryTheory.forget D).obj (F.obj X)<GOAL>∀ (x_1 : C) (f : x_1 ⟶ Opposite.unop X), (CategoryTheory.Presheaf.equalizerSieve x y).arrows f = ((F.map f.op) x = (F.map f.op) y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>F : CategoryTheory.Functor Cᵒᵖ D<VAR>X : Cᵒᵖ<VAR>x : (CategoryTheory.forget D).obj (F.obj X)<GOAL>CategoryTheory.Presheaf.equalizerSieve x x = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>CategoryTheory.ConcreteCategory D<VAR>F : CategoryTheory.Functor Cᵒᵖ D<VAR>X : Cᵒᵖ<VAR>x y : (CategoryTheory.forget D).obj (F.obj X)<GOAL>CategoryTheory.Presheaf.equalizerSieve x y = ⊤ ↔ x = y