ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>F G : Cᵒᵖ ⥤ Type w<VAR>f : F ⟶ G<VAR>CategoryTheory.Limits.PreservesFiniteProducts F<VAR>CategoryTheory.Limits.PreservesFiniteProducts G<VAR>h : CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.coherentTopology C) f<GOAL>CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.ConcreteCategory D<VAR>F G : Cᵒᵖ ⥤ D<VAR>f : F ⟶ G<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryPreExtensive C<VAR>CategoryTheory.Limits.PreservesFiniteProducts F<VAR>CategoryTheory.Limits.PreservesFiniteProducts G<VAR>CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)<GOAL>CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.coherentTopology C) f ↔ CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>CategoryTheory.ConcreteCategory D<VAR>CategoryTheory.Preregular C<VAR>CategoryTheory.FinitaryExtensive C<VAR>F G : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) D<VAR>f : F ⟶ G<VAR>CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)<GOAL>CategoryTheory.Sheaf.IsLocallySurjective f ↔ CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f.val
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w w' : CategoryTheory.TwoSquare T L R B<VAR>h : ∀ (X : C₁), w.app X = w'.app X<GOAL>w = w'
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₃ : C₃<GOAL>∀ {X Y : CategoryTheory.CostructuredArrow L X₃} (f : X ⟶ Y), (w.costructuredArrowRightwards X₃).map f = (CategoryTheory.CostructuredArrow.pre T R (B.obj X₃)).map ((CategoryTheory.Comma.mapLeft (CategoryTheory.Functor.fromPUnit (B.obj X₃)) w).map (CategoryTheory.CostructuredArrow.homMk f.left ⋯))
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₃ : C₃<VAR>X : CategoryTheory.CostructuredArrow L X₃<GOAL>(w.costructuredArrowRightwards X₃).obj X = (CategoryTheory.CostructuredArrow.pre T R (B.obj X₃)).obj ((CategoryTheory.Comma.mapLeft (CategoryTheory.Functor.fromPUnit (B.obj X₃)) w).obj (CategoryTheory.CostructuredArrow.mk (B.map X.hom)))
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ : C₂<VAR>X : CategoryTheory.StructuredArrow X₂ T<GOAL>(w.structuredArrowDownwards X₂).obj X = (CategoryTheory.StructuredArrow.pre (R.obj X₂) L B).obj ((CategoryTheory.Comma.mapRight (CategoryTheory.Functor.fromPUnit (R.obj X₂)) w).obj (CategoryTheory.StructuredArrow.mk (R.map X.hom)))
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ : C₂<GOAL>∀ {X Y : CategoryTheory.StructuredArrow X₂ T} (f : X ⟶ Y), (w.structuredArrowDownwards X₂).map f = (CategoryTheory.StructuredArrow.pre (R.obj X₂) L B).map ((CategoryTheory.Comma.mapRight (CategoryTheory.Functor.fromPUnit (R.obj X₂)) w).map (CategoryTheory.StructuredArrow.homMk f.right ⋯))
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f : w.StructuredArrowRightwards g<GOAL>∃ X₁ a b, ∃ (comm : CategoryTheory.CategoryStruct.comp (R.map a) (CategoryTheory.CategoryStruct.comp (w.app X₁) (B.map b)) = g), f = CategoryTheory.TwoSquare.StructuredArrowRightwards.mk w g X₁ a b comm
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f : w.CostructuredArrowDownwards g<GOAL>∃ X₁ a b, ∃ (comm : CategoryTheory.CategoryStruct.comp (R.map a) (CategoryTheory.CategoryStruct.comp (w.app X₁) (B.map b)) = g), f = CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk w g X₁ a b comm
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f₁ f₂ : w.StructuredArrowRightwards g<VAR>φ : f₁ ⟶ f₂<GOAL>(CategoryTheory.TwoSquare.EquivalenceJ.functor w g).map φ = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.StructuredArrow.homMk φ.right.left ⋯) ⋯
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f : w.StructuredArrowRightwards g<GOAL>(CategoryTheory.TwoSquare.EquivalenceJ.functor w g).obj f = CategoryTheory.CostructuredArrow.mk (CategoryTheory.StructuredArrow.homMk f.right.hom ⋯)
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f : w.CostructuredArrowDownwards g<GOAL>(CategoryTheory.TwoSquare.EquivalenceJ.inverse w g).obj f = CategoryTheory.StructuredArrow.mk (CategoryTheory.CostructuredArrow.homMk f.left.hom ⋯)
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>f₁ f₂ : w.CostructuredArrowDownwards g<VAR>φ : f₁ ⟶ f₂<GOAL>(CategoryTheory.TwoSquare.EquivalenceJ.inverse w g).map φ = CategoryTheory.StructuredArrow.homMk (CategoryTheory.CostructuredArrow.homMk φ.left.right ⋯) ⋯
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<GOAL>(w.equivalenceJ g).functor = CategoryTheory.TwoSquare.EquivalenceJ.functor w g
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<GOAL>(w.equivalenceJ g).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (w.StructuredArrowRightwards g))
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<GOAL>(w.equivalenceJ g).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.TwoSquare.EquivalenceJ.inverse w g).comp (CategoryTheory.TwoSquare.EquivalenceJ.functor w g))
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<GOAL>(w.equivalenceJ g).inverse = CategoryTheory.TwoSquare.EquivalenceJ.inverse w g
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<GOAL>CategoryTheory.IsConnected (w.StructuredArrowRightwards g) ↔ CategoryTheory.IsConnected (w.CostructuredArrowDownwards g)
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ X₂' : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>g' : R.obj X₂' ⟶ B.obj X₃<VAR>γ : X₂' ⟶ X₂<VAR>hγ : CategoryTheory.CategoryStruct.comp (R.map γ) g = g'<VAR>A : w.CostructuredArrowDownwards g<GOAL>(w.costructuredArrowDownwardsPrecomp g g' γ hγ).obj A = CategoryTheory.TwoSquare.CostructuredArrowDownwards.mk w g' A.left.right (CategoryTheory.CategoryStruct.comp γ A.left.hom) A.hom.right ⋯
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>X₂ X₂' : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<VAR>g' : R.obj X₂' ⟶ B.obj X₃<VAR>γ : X₂' ⟶ X₂<VAR>hγ : CategoryTheory.CategoryStruct.comp (R.map γ) g = g'<VAR>A A' : w.CostructuredArrowDownwards g<VAR>φ : A ⟶ A'<GOAL>(w.costructuredArrowDownwardsPrecomp g g' γ hγ).map φ = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.StructuredArrow.homMk φ.left.right ⋯) ⋯
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<VAR>self : w.GuitartExact<VAR>X₂ : C₂<VAR>X₃ : C₃<VAR>g : R.obj X₂ ⟶ B.obj X₃<GOAL>CategoryTheory.IsConnected (w.StructuredArrowRightwards g)
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<GOAL>w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), CategoryTheory.IsConnected (w.StructuredArrowRightwards g)
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<GOAL>w.GuitartExact ↔ ∀ {X₂ : C₂} {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃), CategoryTheory.IsConnected (w.CostructuredArrowDownwards g)
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<GOAL>w.GuitartExact ↔ ∀ (X₃ : C₃), (w.costructuredArrowRightwards X₃).Final
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>C₄ : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} C₁<VAR>CategoryTheory.Category.{v₂, u₂} C₂<VAR>CategoryTheory.Category.{v₃, u₃} C₃<VAR>CategoryTheory.Category.{v₄, u₄} C₄<VAR>T : CategoryTheory.Functor C₁ C₂<VAR>L : CategoryTheory.Functor C₁ C₃<VAR>R : CategoryTheory.Functor C₂ C₄<VAR>B : CategoryTheory.Functor C₃ C₄<VAR>w : CategoryTheory.TwoSquare T L R B<GOAL>w.GuitartExact ↔ ∀ (X₂ : C₂), (w.structuredArrowDownwards X₂).Initial
<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>Field.finSepDegree F E = Field.finSepDegree F K
<VAR>F : Type u<VAR>Field F<GOAL>Field.finSepDegree F F = 1
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<GOAL>Field.finSepDegree F ↥⊥ = 1
<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<GOAL>Field.finSepDegree F ↥⊥ = Field.finSepDegree 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<GOAL>Field.finSepDegree F ↥⊤ = Field.finSepDegree 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>S : Set E<VAR>hS : IntermediateField.adjoin F S = ⊤<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)<GOAL>Field.finSepDegree F E = Nat.card (E →ₐ[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.IsAlgebraic F E<VAR>IsAlgClosed K<GOAL>Field.finSepDegree F E = Nat.card (E →ₐ[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 E K<GOAL>Field.finSepDegree F E * Field.finSepDegree E K = Field.finSepDegree F K
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<GOAL>f.natSepDegree ≤ f.natDegree
<VAR>F : Type u<VAR>Field F<VAR>x : F<GOAL>(Polynomial.X - Polynomial.C x).natSepDegree = 1
<VAR>F : Type u<VAR>Field F<GOAL>Polynomial.X.natSepDegree = 1
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>h : f.natDegree = 0<GOAL>f.natSepDegree = 0
<VAR>F : Type u<VAR>Field F<VAR>x : F<GOAL>(Polynomial.C x).natSepDegree = 0
<VAR>F : Type u<VAR>Field F<GOAL>Polynomial.natSepDegree 0 = 0
<VAR>F : Type u<VAR>Field F<GOAL>Polynomial.natSepDegree 1 = 0
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>h : f.natDegree ≠ 0<GOAL>f.natSepDegree ≠ 0
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<GOAL>f.natSepDegree = 0 ↔ f.natDegree = 0
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<GOAL>f.natSepDegree ≠ 0 ↔ f.natDegree ≠ 0
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>hf : f ≠ 0<GOAL>f.natSepDegree = f.natDegree ↔ f.Separable
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>h : f.Separable<GOAL>f.natSepDegree = f.natDegree
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>f : F[X]<VAR>h : Polynomial.Splits (algebraMap F E) f<GOAL>f.natSepDegree = (f.aroots E).toFinset.card
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>f : F[X]<VAR>IsAlgClosed E<GOAL>f.natSepDegree = (f.aroots E).toFinset.card
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>f : F[X]<GOAL>(Polynomial.map (algebraMap F E) f).natSepDegree = f.natSepDegree
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>x : F<VAR>hx : x ≠ 0<GOAL>(Polynomial.C x * f).natSepDegree = f.natSepDegree
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>x : F<VAR>hx : x ≠ 0<GOAL>(x • f).natSepDegree = f.natSepDegree
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>n : ℕ<GOAL>(f ^ n).natSepDegree = if n = 0 then 0 else f.natSepDegree
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(f ^ n).natSepDegree = f.natSepDegree
<VAR>F : Type u<VAR>Field F<VAR>n : ℕ<GOAL>(Polynomial.X ^ n).natSepDegree = if n = 0 then 0 else 1
<VAR>F : Type u<VAR>Field F<VAR>x : F<VAR>n : ℕ<GOAL>((Polynomial.X - Polynomial.C x) ^ n).natSepDegree = if n = 0 then 0 else 1
<VAR>F : Type u<VAR>Field F<VAR>x y : F<VAR>n : ℕ<VAR>hx : x ≠ 0<GOAL>(Polynomial.C x * (Polynomial.X - Polynomial.C y) ^ n).natSepDegree = if n = 0 then 0 else 1
<VAR>F : Type u<VAR>Field F<VAR>f g : F[X]<GOAL>(f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
<VAR>F : Type u<VAR>Field F<VAR>f g : F[X]<GOAL>(f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
<VAR>F : Type u<VAR>Field F<VAR>f g : F[X]<VAR>hc : IsCoprime f g<GOAL>(f * g).natSepDegree = f.natSepDegree + g.natSepDegree
<VAR>F : Type u<VAR>Field F<VAR>f g : F[X]<VAR>h1 : f ∣ g<VAR>h2 : g ≠ 0<GOAL>f.natSepDegree ≤ g.natSepDegree
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>q : ℕ<VAR>hF : ExpChar F q<VAR>n : ℕ<GOAL>((Polynomial.expand F (q ^ n)) f).natSepDegree = f.natSepDegree
<VAR>F : Type u<VAR>Field F<VAR>q : ℕ<VAR>ExpChar F q<VAR>n : ℕ<VAR>y : F<GOAL>(Polynomial.X ^ q ^ n - Polynomial.C y).natSepDegree = 1
<VAR>F : Type u<VAR>Field F<VAR>f g : F[X]<VAR>q : ℕ<VAR>ExpChar F q<VAR>h : Polynomial.IsSeparableContraction q f g<GOAL>f.natSepDegree = g.natDegree
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>q : ℕ<VAR>ExpChar F q<VAR>hf : Polynomial.HasSeparableContraction q f<GOAL>f.natSepDegree = hf.degree
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>h : Irreducible f<GOAL>f.natSepDegree ∣ f.natDegree
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>q : ℕ<VAR>ExpChar F q<VAR>hm : f.Monic<VAR>hi : Irreducible f<GOAL>f.natSepDegree = 1 ↔ ∃ n y, f = (Polynomial.expand F (q ^ n)) (Polynomial.X - Polynomial.C y)
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>q : ℕ<VAR>ExpChar F q<VAR>hm : f.Monic<VAR>hi : Irreducible f<GOAL>f.natSepDegree = 1 ↔ ∃ n y, f = Polynomial.X ^ q ^ n - Polynomial.C y
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>hm : f.Monic<VAR>hs : Polynomial.Splits (RingHom.id F) f<VAR>h : f.natSepDegree = 1<GOAL>∃ m y, m ≠ 0 ∧ f = (Polynomial.X - Polynomial.C y) ^ m
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>q : ℕ<VAR>ExpChar F q<VAR>hm : f.Monic<VAR>hi : Irreducible f<VAR>h : f.natSepDegree = 1<GOAL>∃ n y, (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = Polynomial.X ^ q ^ n - Polynomial.C y
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>q : ℕ<VAR>ExpChar F q<VAR>hm : f.Monic<VAR>h : f.natSepDegree = 1<GOAL>∃ m n y, m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (Polynomial.X ^ q ^ n - Polynomial.C y) ^ m
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>q : ℕ<VAR>ExpChar F q<VAR>hm : f.Monic<GOAL>f.natSepDegree = 1 ↔ ∃ m n y, m ≠ 0 ∧ f = (Polynomial.X ^ q ^ n - Polynomial.C y) ^ m
<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>(minpoly F x).natSepDegree = 1 ↔ ∃ n y, minpoly F x = (Polynomial.expand F (q ^ n)) (Polynomial.X - 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<VAR>x : E<GOAL>(minpoly F x).natSepDegree = 1 ↔ ∃ 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<VAR>x : E<GOAL>(minpoly F x).natSepDegree = 1 ↔ ∃ 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>x : E<GOAL>(minpoly F x).natSepDegree = 1 ↔ ∃ 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>α : E<VAR>halg : IsAlgebraic F α<GOAL>Field.finSepDegree F ↥F⟮α⟯ = (minpoly F α).natSepDegree
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>α : E<GOAL>Field.finSepDegree F ↥F⟮α⟯ ∣ FiniteDimensional.finrank F ↥F⟮α⟯
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>α : E<VAR>halg : IsAlgebraic F α<GOAL>Field.finSepDegree F ↥F⟮α⟯ ≤ FiniteDimensional.finrank F ↥F⟮α⟯
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>α : E<VAR>halg : IsAlgebraic F α<GOAL>Field.finSepDegree F ↥F⟮α⟯ = FiniteDimensional.finrank F ↥F⟮α⟯ ↔ IsSeparable F α
<VAR>F : Type u<VAR>E : Type v<VAR>Field F<VAR>Field E<VAR>Algebra 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