ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>l : f.left ≅ g.left<VAR>r : f.right ≅ g.right<VAR>h : CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom := by aesop_cat<GOAL>(CategoryTheory.Arrow.isoMk l r h).hom.left = l.hom
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>l : f.left ≅ g.left<VAR>r : f.right ≅ g.right<VAR>h : CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom := by aesop_cat<GOAL>(CategoryTheory.Arrow.isoMk l r h).hom.right = r.hom
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>l : f.left ≅ g.left<VAR>r : f.right ≅ g.right<VAR>h : CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom := by aesop_cat<GOAL>(CategoryTheory.Arrow.isoMk l r h).inv.right = r.inv
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>φ₁ φ₂ : f ⟶ g<VAR>h : φ₁ = φ₂<GOAL>φ₁.left = φ₂.left
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>φ₁ φ₂ : f ⟶ g<VAR>h : φ₁ = φ₂<GOAL>φ₁.right = φ₂.right
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>e : f ≅ g<GOAL>g.hom = CategoryTheory.CategoryStruct.comp e.inv.left (CategoryTheory.CategoryStruct.comp f.hom e.hom.right)
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>W X Y Z : T<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<VAR>e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g<GOAL>g = CategoryTheory.CategoryStruct.comp e.inv.left (CategoryTheory.CategoryStruct.comp f e.hom.right)
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>sq : f ⟶ g<VAR>CategoryTheory.IsIso sq<GOAL>(CategoryTheory.inv sq).left = CategoryTheory.inv sq.left
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>sq : f ⟶ g<VAR>CategoryTheory.IsIso sq<GOAL>(CategoryTheory.inv sq).right = CategoryTheory.inv sq.right
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>sq : f ⟶ g<VAR>CategoryTheory.IsIso sq<GOAL>CategoryTheory.CategoryStruct.comp sq.left (CategoryTheory.CategoryStruct.comp g.hom (CategoryTheory.inv sq.right)) = f.hom
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>sq : f ⟶ g<VAR>CategoryTheory.IsIso sq<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.inv sq.left) (CategoryTheory.CategoryStruct.comp f.hom sq.right) = g.hom
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>e : f ≅ g<GOAL>CategoryTheory.CategoryStruct.comp e.hom.left e.inv.left = CategoryTheory.CategoryStruct.id f.left
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>e : f ≅ g<GOAL>CategoryTheory.CategoryStruct.comp e.inv.left e.hom.left = CategoryTheory.CategoryStruct.id g.left
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>e : f ≅ g<GOAL>CategoryTheory.CategoryStruct.comp e.hom.right e.inv.right = CategoryTheory.CategoryStruct.id f.right
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>f g : CategoryTheory.Arrow T<VAR>e : f ≅ g<GOAL>CategoryTheory.CategoryStruct.comp e.inv.right e.hom.right = CategoryTheory.CategoryStruct.id g.right
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>i : CategoryTheory.Arrow T<VAR>X Y : T<VAR>p : X ≅ Y<VAR>sq : i ⟶ CategoryTheory.Arrow.mk p.hom<GOAL>CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.CategoryStruct.comp sq.right p.inv) = sq.left
<VAR>T : Type u<VAR>CategoryTheory.Category.{v, u} T<VAR>X Y : T<VAR>i : X ≅ Y<VAR>p : CategoryTheory.Arrow T<VAR>sq : CategoryTheory.Arrow.mk i.hom ⟶ p<GOAL>CategoryTheory.CategoryStruct.comp i.inv (CategoryTheory.CategoryStruct.comp sq.left p.hom) = sq.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>i : CategoryTheory.Arrow C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>sq : i ⟶ CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp f g)<GOAL>(CategoryTheory.Arrow.squareToSnd sq).right = sq.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>i : CategoryTheory.Arrow C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>sq : i ⟶ CategoryTheory.Arrow.mk (CategoryTheory.CategoryStruct.comp f g)<GOAL>(CategoryTheory.Arrow.squareToSnd sq).left = CategoryTheory.CategoryStruct.comp sq.left f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)} (f : X ⟶ Y), CategoryTheory.Arrow.leftFunc.map f = f.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)<GOAL>CategoryTheory.Arrow.leftFunc.obj X = X.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)} (f : X ⟶ Y), CategoryTheory.Arrow.rightFunc.map f = f.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)<GOAL>CategoryTheory.Arrow.rightFunc.obj X = X.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow C<GOAL>CategoryTheory.Arrow.leftToRight.app f = f.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<GOAL>∀ {X Y : CategoryTheory.Arrow C} (f : X ⟶ Y), (F.mapArrow.map f).right = F.map f.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<GOAL>∀ {X Y : CategoryTheory.Arrow C} (f : X ⟶ Y), (F.mapArrow.map f).left = F.map f.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>a : CategoryTheory.Arrow C<GOAL>(F.mapArrow.obj a).left = F.obj a.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>a : CategoryTheory.Arrow C<GOAL>(F.mapArrow.obj a).hom = F.map a.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>a : CategoryTheory.Arrow C<GOAL>(F.mapArrow.obj a).right = F.obj a.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>∀ {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y) (f : CategoryTheory.Arrow C), (((CategoryTheory.Functor.mapArrowFunctor C D).map τ).app f).left = τ.app f.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>∀ {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y) (f : CategoryTheory.Arrow C), (((CategoryTheory.Functor.mapArrowFunctor C D).map τ).app f).right = τ.app f.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<GOAL>(CategoryTheory.Functor.mapArrowFunctor C D).obj F = F.mapArrow
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>X : (C × D) × E<GOAL>(CategoryTheory.prod.associator C D E).obj X = (X.1.1, X.1.2, X.2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<GOAL>∀ (x x_1 : (C × D) × E) (f : x ⟶ x_1), (CategoryTheory.prod.associator C D E).map f = (f.1.1, f.1.2, f.2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>X : C × D × E<GOAL>(CategoryTheory.prod.inverseAssociator C D E).obj X = ((X.1, X.2.1), X.2.2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<GOAL>∀ (x x_1 : C × D × E) (f : x ⟶ x_1), (CategoryTheory.prod.inverseAssociator C D E).map f = ((f.1, f.2.1), f.2.2)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : C<GOAL>(α.app X).inv = α.inv.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : C<GOAL>(α.app X).hom = α.hom.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : C<GOAL>α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : C<GOAL>α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G H : C ⥤ D<VAR>α : F ≅ G<VAR>β : G ≅ H<VAR>X : C<GOAL>(α ≪≫ β).app X = α.app X ≪≫ β.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : C<VAR>Z : D<VAR>g g' : G.obj X ⟶ Z<GOAL>α.hom.app X ≫ g = α.hom.app X ≫ g' ↔ g = g'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : C<VAR>Z : D<VAR>g g' : F.obj X ⟶ Z<GOAL>α.inv.app X ≫ g = α.inv.app X ≫ g' ↔ g = g'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : D<VAR>Y : C<VAR>f f' : X ⟶ F.obj Y<GOAL>f ≫ α.hom.app Y = f' ≫ α.hom.app Y ↔ f = f'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : D<VAR>Y : C<VAR>f f' : X ⟶ G.obj Y<GOAL>f ≫ α.inv.app Y = f' ≫ α.inv.app Y ↔ f = f'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>W X X' : D<VAR>Y : C<VAR>f : W ⟶ X<VAR>g : X ⟶ F.obj Y<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ F.obj Y<GOAL>f ≫ g ≫ α.hom.app Y = f' ≫ g' ≫ α.hom.app Y ↔ f ≫ g = f' ≫ g'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>W X X' : D<VAR>Y : C<VAR>f : W ⟶ X<VAR>g : X ⟶ G.obj Y<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ G.obj Y<GOAL>f ≫ g ≫ α.inv.app Y = f' ≫ g' ≫ α.inv.app Y ↔ f ≫ g = f' ≫ g'
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>e : F ≅ G<VAR>X : C<GOAL>CategoryTheory.inv (e.inv.app X) = e.hom.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>X Y : C<VAR>α : F ≅ G<VAR>f : X ⟶ Y<GOAL>α.inv.app X ≫ F.map f ≫ α.hom.app Y = G.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>X Y : C<VAR>α : F ≅ G<VAR>f : X ⟶ Y<GOAL>α.hom.app X ≫ G.map f ≫ α.inv.app Y = F.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>X Y : C<VAR>α : F ⟶ G<VAR>f : X ⟶ Y<GOAL>∀ {x : CategoryTheory.IsIso (α.app X)}, CategoryTheory.inv (α.app X) ≫ F.map f ≫ α.app Y = G.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>X Y : C<VAR>α : F ⟶ G<VAR>f : X ⟶ Y<GOAL>∀ {x : CategoryTheory.IsIso (α.app Y)}, α.app X ≫ G.map f ≫ CategoryTheory.inv (α.app Y) = F.map f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<GOAL>∀ {x : CategoryTheory.IsIso α} (X : C), (CategoryTheory.inv α).app X = CategoryTheory.inv (α.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : C ⥤ D ⥤ E<VAR>X Y : C<VAR>e : X ≅ Y<VAR>Z : D<GOAL>CategoryTheory.inv ((F.map e.inv).app Z) = (F.map e.hom).app Z
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>app : (X : C) → F.obj X ≅ G.obj X<VAR>naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f := by aesop_cat<VAR>X : C<GOAL>(CategoryTheory.NatIso.ofComponents app naturality).hom.app X = (app X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>app : (X : C) → F.obj X ≅ G.obj X<VAR>naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f := by aesop_cat<VAR>X : C<GOAL>(CategoryTheory.NatIso.ofComponents app naturality).inv.app X = (app X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>app' : (X : C) → F.obj X ≅ G.obj X<VAR>naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app' Y).hom = (app' X).hom ≫ G.map f<VAR>X : C<GOAL>(CategoryTheory.NatIso.ofComponents app' naturality).app X = app' X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>α : F ⟶ G<VAR>∀ (X : C), CategoryTheory.IsIso (α.app X)<GOAL>CategoryTheory.IsIso α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>H I : D ⥤ E<VAR>α : F ≅ G<VAR>β : H ≅ I<GOAL>(CategoryTheory.NatIso.hcomp α β).hom = α.hom ◫ β.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>H I : D ⥤ E<VAR>α : F ≅ G<VAR>β : H ≅ I<GOAL>(CategoryTheory.NatIso.hcomp α β).inv = α.inv ◫ β.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F₁ F₂ : C ⥤ D<VAR>e : F₁ ≅ F₂<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso (F₁.map f) ↔ CategoryTheory.IsIso (F₂.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : C ⥤ D<VAR>τ : F ⟶ G<GOAL>CategoryTheory.IsIso τ ↔ ∀ (X : C), CategoryTheory.IsIso (τ.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>obj : C → D<VAR>e : (X : C) → F.obj X ≅ obj X<GOAL>∀ (a : C), (F.copyObj obj e).obj a = obj a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>obj : C → D<VAR>e : (X : C) → F.obj X ≅ obj X<VAR>X : C<GOAL>(F.isoCopyObj obj e).hom.app X = (e X).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>obj : C → D<VAR>e : (X : C) → F.obj X ≅ obj X<VAR>X : C<GOAL>(F.isoCopyObj obj e).inv.app X = (e X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>self : CategoryTheory.PreGaloisCategory C<VAR>G : Type u₂<VAR>Group G<VAR>Finite G<GOAL>CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.SingleObj G) C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>self : CategoryTheory.PreGaloisCategory C<GOAL>CategoryTheory.Limits.HasFiniteCoproducts C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>self : CategoryTheory.PreGaloisCategory C<GOAL>CategoryTheory.Limits.HasTerminal C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>self : CategoryTheory.PreGaloisCategory C<VAR>X Y : C<VAR>i : X ⟶ Y<VAR>CategoryTheory.Mono i<GOAL>∃ Z u, Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk i u))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>self : CategoryTheory.PreGaloisCategory C<GOAL>CategoryTheory.Limits.HasPullbacks C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>self : CategoryTheory.PreGaloisCategory.FiberFunctor F<GOAL>F.PreservesEpimorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>self : CategoryTheory.PreGaloisCategory.FiberFunctor F<GOAL>F.ReflectsIsomorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>X : C<VAR>self : CategoryTheory.PreGaloisCategory.IsConnected X<VAR>Y : C<VAR>i : Y ⟶ X<VAR>CategoryTheory.Mono i<GOAL>(CategoryTheory.Limits.IsInitial Y → False) → CategoryTheory.IsIso i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>X : C<VAR>self : CategoryTheory.PreGaloisCategory.IsConnected X<GOAL>CategoryTheory.Limits.IsInitial X → False
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>D : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} D<VAR>F : CategoryTheory.Functor C D<VAR>self : CategoryTheory.PreGaloisCategory.PreservesIsConnected F<VAR>X : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected X<GOAL>CategoryTheory.PreGaloisCategory.IsConnected (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>X : C<VAR>σ : CategoryTheory.Aut F<VAR>x : ↑(F.obj X)<GOAL>σ • x = σ.hom.app X x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X : C<GOAL>Nonempty (CategoryTheory.Limits.IsInitial X) ↔ IsEmpty ↑(F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X : C<GOAL>CategoryTheory.Limits.IsInitial X → False ↔ Nonempty ↑(F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X : C<VAR>x : ↑(F.obj X)<VAR>h : CategoryTheory.Limits.IsInitial X<GOAL>False
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>X : C<VAR>hc : ¬CategoryTheory.PreGaloisCategory.IsConnected X<VAR>hi : CategoryTheory.Limits.IsInitial X → False<GOAL>∃ Y v, (CategoryTheory.Limits.IsInitial Y → False) ∧ CategoryTheory.Mono v ∧ ¬CategoryTheory.IsIso v
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>x : ↑(F.obj X)<VAR>h : F.map f x = F.map g x<GOAL>F.map (CategoryTheory.Limits.equalizer.ι f g) ((CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv F f g).symm ⟨x, h⟩) = x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X A B : C<VAR>f : A ⟶ X<VAR>g : B ⟶ X<VAR>a : ↑(F.obj A)<VAR>b : ↑(F.obj B)<VAR>h : F.map f a = F.map g b<GOAL>F.map (CategoryTheory.Limits.pullback.fst f g) ((CategoryTheory.PreGaloisCategory.fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X A B : C<VAR>f : A ⟶ X<VAR>g : B ⟶ X<VAR>a : ↑(F.obj A)<VAR>b : ↑(F.obj B)<VAR>h : F.map f a = F.map g b<GOAL>F.map (CategoryTheory.Limits.pullback.snd f g) ((CategoryTheory.PreGaloisCategory.fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) = b
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X Y : C<VAR>x : ↑(F.obj X)<VAR>y : ↑(F.obj Y)<GOAL>F.map CategoryTheory.Limits.prod.fst ((CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv F X Y).symm (x, y)) = x
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X Y : C<VAR>x : ↑(F.obj X)<VAR>y : ↑(F.obj Y)<GOAL>F.map CategoryTheory.Limits.prod.snd ((CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv F X Y).symm (x, y)) = y
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>A X : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<VAR>a : ↑(F.obj A)<GOAL>Function.Injective fun f => F.map f a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>A : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<VAR>a : ↑(F.obj A)<GOAL>Function.Injective fun f => F.map f.hom a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X A : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<VAR>h : Nonempty ↑(F.obj X)<VAR>f : X ⟶ A<GOAL>CategoryTheory.Epi f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Epi f<GOAL>Function.Surjective (F.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X A : C<VAR>Nonempty ↑(F.obj X)<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<VAR>f : X ⟶ A<GOAL>Function.Surjective (F.map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>h : Nat.card ↑(F.obj X) = Nat.card ↑(F.obj Y)<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<VAR>h : ¬CategoryTheory.IsIso f<GOAL>Nat.card ↑(F.obj X) < Nat.card ↑(F.obj Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X : C<VAR>h : CategoryTheory.Limits.IsInitial X → False<GOAL>Nat.card ↑(F.obj X) ≠ 0
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>X Y : C<GOAL>Nat.card ↑(F.obj (X ⨿ Y)) = Nat.card ↑(F.obj X) + Nat.card ↑(F.obj Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>X Y : C<VAR>i : X ≅ Y<GOAL>Nat.card ↑(F.obj X) = Nat.card ↑(F.obj Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>CategoryTheory.PreGaloisCategory C<VAR>F : CategoryTheory.Functor C FintypeCat<VAR>CategoryTheory.PreGaloisCategory.FiberFunctor F<VAR>A X : C<VAR>CategoryTheory.PreGaloisCategory.IsConnected A<GOAL>Nat.card (A ⟶ X) ≤ Nat.card ↑(F.obj X)