ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.cokernelBiprodInlIso.hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.inl 0) (CategoryTheory.Limits.biprod.inlCokernelCofork X Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.cokernelBiprodInlIso.inv = (CategoryTheory.Limits.biprod.isCokernelInlCokernelFork X Y).desc (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.inl 0))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.cokernelBiprodInrIso.inv = (CategoryTheory.Limits.biprod.isCokernelInrCokernelFork X Y).desc (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.inr 0))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<GOAL>CategoryTheory.Limits.cokernelBiprodInrIso.hom = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.inr 0) (CategoryTheory.Limits.biprod.inrCokernelCofork X Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>hY : CategoryTheory.Limits.IsZero Y<GOAL>(CategoryTheory.Limits.isoBiprodZero hY).hom = CategoryTheory.Limits.biprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>hY : CategoryTheory.Limits.IsZero Y<GOAL>(CategoryTheory.Limits.isoBiprodZero hY).inv = CategoryTheory.Limits.biprod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>hY : CategoryTheory.Limits.IsZero X<GOAL>(CategoryTheory.Limits.isoZeroBiprod hY).inv = CategoryTheory.Limits.biprod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct X Y<VAR>hY : CategoryTheory.Limits.IsZero X<GOAL>(CategoryTheory.Limits.isoZeroBiprod hY).hom = CategoryTheory.Limits.biprod.inr
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>A B : C<VAR>CategoryTheory.Limits.HasBinaryBiproduct A B<GOAL>CategoryTheory.Limits.IsZero (A ⊞ B) ↔ CategoryTheory.Limits.IsZero A ∧ CategoryTheory.Limits.IsZero B
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>P Q : C<GOAL>(CategoryTheory.Limits.biprod.braiding P Q).inv = CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>P Q : C<GOAL>(CategoryTheory.Limits.biprod.braiding P Q).hom = CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>P Q : C<GOAL>(CategoryTheory.Limits.biprod.braiding' P Q).hom = CategoryTheory.Limits.biprod.desc CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>P Q : C<GOAL>(CategoryTheory.Limits.biprod.braiding' P Q).inv = CategoryTheory.Limits.biprod.desc CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.inl
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>P Q : C<GOAL>CategoryTheory.Limits.biprod.braiding' P Q = CategoryTheory.Limits.biprod.braiding P Q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Z ⟶ W<GOAL>CategoryTheory.Limits.biprod.map f g ≫ (CategoryTheory.Limits.biprod.braiding Y W).hom = (CategoryTheory.Limits.biprod.braiding X Z).hom ≫ CategoryTheory.Limits.biprod.map g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<GOAL>(CategoryTheory.Limits.biprod.braiding X W).hom ≫ CategoryTheory.Limits.biprod.map f g ≫ (CategoryTheory.Limits.biprod.braiding Y Z).hom = CategoryTheory.Limits.biprod.map g f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>P Q : C<GOAL>CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst ≫ CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst = 𝟙 (P ⊞ Q)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>P Q : C<GOAL>(CategoryTheory.Limits.biprod.braiding P Q).hom ≫ (CategoryTheory.Limits.biprod.braiding Q P).hom = 𝟙 (P ⊞ Q)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>P Q R : C<GOAL>(CategoryTheory.Limits.biprod.associator P Q R).hom = CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.biprod.fst ≫ CategoryTheory.Limits.biprod.fst) (CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.biprod.fst ≫ CategoryTheory.Limits.biprod.snd) CategoryTheory.Limits.biprod.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>P Q R : C<GOAL>(CategoryTheory.Limits.biprod.associator P Q R).inv = CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.fst (CategoryTheory.Limits.biprod.snd ≫ CategoryTheory.Limits.biprod.fst)) (CategoryTheory.Limits.biprod.snd ≫ CategoryTheory.Limits.biprod.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>U V W X Y Z : C<VAR>f : U ⟶ X<VAR>g : V ⟶ Y<VAR>h : W ⟶ Z<GOAL>CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h ≫ (CategoryTheory.Limits.biprod.associator X Y Z).hom = (CategoryTheory.Limits.biprod.associator U V W).hom ≫ CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>U V W X Y Z : C<VAR>f : U ⟶ X<VAR>g : V ⟶ Y<VAR>h : W ⟶ Z<GOAL>CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h) ≫ (CategoryTheory.Limits.biprod.associator X Y Z).inv = (CategoryTheory.Limits.biprod.associator U V W).inv ≫ CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso (CategoryTheory.Limits.biprod.map f g)<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasBinaryBiproducts C<VAR>W X Y Z : C<VAR>f : W ⟶ Y<VAR>g : X ⟶ Z<VAR>CategoryTheory.IsIso (CategoryTheory.Limits.biprod.map f g)<GOAL>CategoryTheory.IsIso g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>self : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<GOAL>CategoryTheory.PreGaloisCategory.IsGalois self.obj
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<VAR>self : A.Hom B<GOAL>F.map self.val A.pt = B.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<VAR>f g : A ⟶ B<VAR>h : f.val = g.val<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<GOAL>(CategoryTheory.CategoryStruct.id A).val = CategoryTheory.CategoryStruct.id A.obj
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<GOAL>∀ {C_1 : CategoryTheory.PreGaloisCategory.PointedGaloisObject F} (f : A ⟶ B) (g : B ⟶ C_1), (CategoryTheory.CategoryStruct.comp f g).val = CategoryTheory.CategoryStruct.comp f.val g.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<GOAL>(CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).obj A = A.obj
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<VAR>f : A ⟶ B<GOAL>(CategoryTheory.PreGaloisCategory.PointedGaloisObject.incl F).map f = f.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<VAR>B : C<VAR>f : A.obj ⟶ B<GOAL>((CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone F).ι.app (Opposite.op A)).app B f = F.map f A.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<GOAL>(CategoryTheory.PreGaloisCategory.autGaloisSystem F).obj A = Grp.of (CategoryTheory.Aut A.obj)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<VAR>f : A ⟶ B<GOAL>(CategoryTheory.PreGaloisCategory.autGaloisSystem F).map f = CategoryTheory.PreGaloisCategory.autMapHom f.val
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<VAR>x : CategoryTheory.PreGaloisCategory.AutGalois F<GOAL>(CategoryTheory.PreGaloisCategory.AutGalois.π F A) x = ↑x A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>A B : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<VAR>f : A ⟶ B<GOAL>Function.Surjective ⇑((CategoryTheory.PreGaloisCategory.autGaloisSystem F).map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<GOAL>Function.Surjective ⇑(CategoryTheory.PreGaloisCategory.AutGalois.π F A)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>f g : CategoryTheory.PreGaloisCategory.AutGalois F<VAR>h : ∀ (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F), (CategoryTheory.PreGaloisCategory.AutGalois.π F A) f = (CategoryTheory.PreGaloisCategory.AutGalois.π F A) g<GOAL>f = g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>f : CategoryTheory.End F<VAR>A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<GOAL>↑((CategoryTheory.PreGaloisCategory.endEquivSectionsFibers F) f) A = f.app A.obj A.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<VAR>b : ↑(F.obj A.obj)<GOAL>(CategoryTheory.PreGaloisCategory.autIsoFibers F).inv.app A b = (CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A.obj A.pt).symm b
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>f : CategoryTheory.End F<VAR>A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<GOAL>F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F A) ((CategoryTheory.PreGaloisCategory.endEquivAutGalois F) f)).hom A.pt = f.app A.obj A.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>f g : CategoryTheory.End F<GOAL>(CategoryTheory.PreGaloisCategory.endEquivAutGalois F) (CategoryTheory.CategoryStruct.comp g f) = (CategoryTheory.PreGaloisCategory.endEquivAutGalois F) g * (CategoryTheory.PreGaloisCategory.endEquivAutGalois F) f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>f : CategoryTheory.End F<VAR>A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F<GOAL>F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F A) (MulOpposite.unop ((CategoryTheory.PreGaloisCategory.endMulEquivAutGalois F) f))).hom A.pt = f.app A.obj A.pt
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>f : CategoryTheory.End F<GOAL>IsUnit f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>f : CategoryTheory.Aut F<VAR>A : C<VAR>CategoryTheory.PreGaloisCategory.IsGalois A<VAR>a : ↑(F.obj A)<GOAL>F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) (MulOpposite.unop ((CategoryTheory.PreGaloisCategory.autMulEquivAutGalois F) f))).hom a = f.hom.app A a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>x : CategoryTheory.PreGaloisCategory.AutGalois F<VAR>A : C<VAR>CategoryTheory.PreGaloisCategory.IsGalois A<VAR>a : ↑(F.obj A)<GOAL>((CategoryTheory.PreGaloisCategory.autMulEquivAutGalois F).symm { unop' := x }).hom.app A a = F.map ((CategoryTheory.PreGaloisCategory.AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) x).hom a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X : C<VAR>CategoryTheory.PreGaloisCategory.IsGalois X<GOAL>MulAction.IsPretransitive (CategoryTheory.Aut F) ↑(F.obj X)
<VAR>m : Type u_1 → Type u_2<VAR>Monad m<VAR>α : CategoryTheory.KleisliCat m<GOAL>CategoryTheory.CategoryStruct.id α = pure
<VAR>m : Type u_1 → Type u_2<VAR>Monad m<VAR>α β γ : CategoryTheory.KleisliCat m<VAR>xs : α ⟶ β<VAR>ys : β ⟶ γ<VAR>a : α<GOAL>CategoryTheory.CategoryStruct.comp xs ys a = xs a >>= ys
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>X : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected X<GOAL>∃ ι f g x, (∀ (i : ι), CategoryTheory.PreGaloisCategory.IsConnected (f i)) ∧ Finite ι
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>X : C<VAR>h : CategoryTheory.Limits.IsInitial X<GOAL>∃ ι f g x, (∀ (i : ι), CategoryTheory.PreGaloisCategory.IsConnected (f i)) ∧ Finite ι
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>n : ℕ<VAR>X : C<GOAL>n = Nat.card ↑(F.obj X) → ∃ ι f g x, (∀ (i : ι), CategoryTheory.PreGaloisCategory.IsConnected (f i)) ∧ Finite ι
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>X : C<GOAL>∃ ι f g x, (∀ (i : ι), CategoryTheory.PreGaloisCategory.IsConnected (f i)) ∧ Finite ι
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>X : C<GOAL>∃ ι, ∃ (x : Finite ι), ∃ f x, ∀ (i : ι), CategoryTheory.PreGaloisCategory.IsConnected (f i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X : C<VAR>x : ↑(F.obj X)<GOAL>∃ Y i y, F.map i y = x ∧ CategoryTheory.PreGaloisCategory.IsConnected Y ∧ CategoryTheory.Mono i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X A B : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<VAR>CategoryTheory.PreGaloisCategory.IsConnected B<VAR>a : ↑(F.obj A)<VAR>b : ↑(F.obj B)<VAR>i : A ⟶ X<VAR>j : B ⟶ X<VAR>h : F.map i a = F.map j b<VAR>CategoryTheory.Mono i<VAR>CategoryTheory.Mono j<GOAL>∃ f, F.map f.hom a = b
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X : C<VAR>t : ↑(F.obj X)<GOAL>F.map (CategoryTheory.Limits.Pi.π (fun x => X) t) (CategoryTheory.PreGaloisCategory.mkSelfProdFib F X) = t
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X A : C<VAR>u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X<VAR>a : ↑(F.obj A)<VAR>h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X<VAR>x : ↑(F.obj X)<GOAL>F.map (CategoryTheory.PreGaloisCategory.selfProdProj u x) a = x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X A : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<VAR>u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X<VAR>a : ↑(F.obj A)<VAR>h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X<VAR>b : ↑(F.obj A)<GOAL>F.map u b = F.map (CategoryTheory.PreGaloisCategory.selfProdPermIncl h b) a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X A : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<VAR>u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X<VAR>CategoryTheory.Mono u<VAR>a : ↑(F.obj A)<VAR>h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X<VAR>b : ↑(F.obj A)<GOAL>∃ f, F.map f.hom b = a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X : C<GOAL>∃ A a, CategoryTheory.PreGaloisCategory.IsGalois A ∧ Function.Bijective fun f => F.map f a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X : C<VAR>x : ↑(F.obj X)<GOAL>∃ A f a, CategoryTheory.PreGaloisCategory.IsGalois A ∧ F.map f a = x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X : C<VAR>h : Nonempty ↑(F.obj X)<GOAL>∃ A x, CategoryTheory.PreGaloisCategory.IsGalois A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.GaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected X<GOAL>∃ A x, CategoryTheory.PreGaloisCategory.IsGalois A
<VAR>X : Type u_3<VAR>toTwoPointing : TwoPointing X<GOAL>(TwoP.of toTwoPointing).X = X
<VAR>X : TwoP<GOAL>X.toBipointed.X = X.X
<VAR>X : TwoP<GOAL>(TwoP.swap.obj X).X = X.X
<VAR>X : TwoP<GOAL>(TwoP.swap.obj X).toTwoPointing = X.toTwoPointing.swap
<GOAL>∀ {X Y : TwoP} (f : X ⟶ Y) (a : X.toBipointed.X), (TwoP.swap.map f).toFun a = f.toFun a
<VAR>X : TwoP<GOAL>(TwoP.swapEquiv.inverse.obj X).X = X.X
<VAR>X : TwoP<GOAL>(TwoP.swapEquiv.functor.obj X).toTwoPointing.toProd = (X.toTwoPointing.toProd.2, X.toTwoPointing.toProd.1)
<VAR>X : TwoP<VAR>a : ((TwoP.swap ⋙ TwoP.swap).obj X).toBipointed.X<GOAL>(TwoP.swapEquiv.counitIso.hom.app X).toFun a = a
<VAR>X : TwoP<GOAL>(TwoP.swapEquiv.functor.obj X).X = X.X
<VAR>X : TwoP<VAR>a : ((𝟭 TwoP).obj X).toBipointed.X<GOAL>(TwoP.swapEquiv.counitIso.inv.app X).toFun a = a
<GOAL>∀ {X Y : TwoP} (f : X ⟶ Y) (a : X.toBipointed.X), (TwoP.swapEquiv.inverse.map f).toFun a = f.toFun a
<GOAL>∀ {X Y : TwoP} (f : X ⟶ Y) (a : X.toBipointed.X), (TwoP.swapEquiv.functor.map f).toFun a = f.toFun a
<VAR>X : TwoP<GOAL>∀ (a : ((𝟭 TwoP).obj X).toBipointed.X), (TwoP.swapEquiv.unitIso.hom.app X).toFun a = (𝟙 (TwoP.swap.obj (TwoP.swap.obj X))).toFun (({ toFun := id, map_fst := ⋯, map_snd := ⋯ } ≫ TwoP.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ } ≫ TwoP.swap.map (TwoP.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ })).toFun a)
<VAR>X : TwoP<GOAL>∀ (a : ((TwoP.swap ⋙ TwoP.swap).obj X).toBipointed.X), (TwoP.swapEquiv.unitIso.inv.app X).toFun a = (TwoP.swap.map (TwoP.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ }) ≫ TwoP.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ } ≫ { toFun := id, map_fst := ⋯, map_snd := ⋯ }).toFun ((𝟙 (TwoP.swap.obj (TwoP.swap.obj X))).toFun a)
<VAR>X : TwoP<GOAL>(TwoP.swapEquiv.inverse.obj X).toTwoPointing.toProd = (X.toTwoPointing.toProd.2, X.toTwoPointing.toProd.1)
<GOAL>TwoP.swapEquiv.symm = TwoP.swapEquiv
<GOAL>TwoP.swap ⋙ CategoryTheory.forget₂ TwoP Bipointed = CategoryTheory.forget₂ TwoP Bipointed ⋙ Bipointed.swap
<GOAL>∀ {X Y : Pointed} (f : X ⟶ Y) (a : Option X.X), (pointedToTwoPFst.map f).toFun a = Option.map f.toFun a
<VAR>X : Pointed<GOAL>(pointedToTwoPFst.obj X).toTwoPointing.toProd = (some X.point, none)
<VAR>X : Pointed<GOAL>(pointedToTwoPFst.obj X).X = Option X.X
<GOAL>∀ {X Y : Pointed} (f : X ⟶ Y) (a : Option X.X), (pointedToTwoPSnd.map f).toFun a = Option.map f.toFun a
<VAR>X : Pointed<GOAL>(pointedToTwoPSnd.obj X).X = Option X.X
<VAR>X : Pointed<GOAL>(pointedToTwoPSnd.obj X).toTwoPointing.toProd = (none, some X.point)
<GOAL>pointedToTwoPFst ⋙ TwoP.swap = pointedToTwoPSnd
<GOAL>pointedToTwoPSnd ⋙ TwoP.swap = pointedToTwoPFst
<GOAL>pointedToTwoPFst ⋙ CategoryTheory.forget₂ TwoP Bipointed = pointedToBipointedFst
<GOAL>pointedToTwoPSnd ⋙ CategoryTheory.forget₂ TwoP Bipointed = pointedToBipointedSnd
<VAR>X : Type u_3<VAR>point : X<GOAL>(Pointed.of point).X = X
<VAR>X Y : Pointed<VAR>self : X.Hom Y<GOAL>self.toFun X.point = Y.point
<VAR>X : Pointed<VAR>a : X.X<GOAL>(Pointed.Hom.id X).toFun a = id a