ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>G : CategoryTheory.Functor D C<VAR>adj : CategoryTheory.Adjunction.CoreUnitCounit F G<GOAL>(CategoryTheory.Adjunction.mkOfUnitCounit adj).unit = adj.unit
<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>G : CategoryTheory.Functor D C<VAR>adj : CategoryTheory.Adjunction.CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>f : F.obj X ⟶ Y<GOAL>((CategoryTheory.Adjunction.mkOfUnitCounit adj).homEquiv X Y) f = CategoryTheory.CategoryStruct.comp (adj.unit.app X) (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 : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D C<VAR>adj : CategoryTheory.Adjunction.CoreUnitCounit F G<VAR>X : C<VAR>Y : D<VAR>g : X ⟶ G.obj Y<GOAL>((CategoryTheory.Adjunction.mkOfUnitCounit adj).homEquiv X Y).symm g = CategoryTheory.CategoryStruct.comp (F.map g) (adj.counit.app Y)
<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>G : CategoryTheory.Functor D C<VAR>adj : CategoryTheory.Adjunction.CoreUnitCounit F G<GOAL>(CategoryTheory.Adjunction.mkOfUnitCounit adj).counit = adj.counit
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F F' : CategoryTheory.Functor C D<VAR>iso : F ≅ F'<VAR>X : C<VAR>Y : D<VAR>f : F.obj X ⟶ Y<GOAL>(CategoryTheory.Adjunction.equivHomsetLeftOfNatIso iso) f = CategoryTheory.CategoryStruct.comp (iso.inv.app X) f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F F' : CategoryTheory.Functor C D<VAR>iso : F ≅ F'<VAR>X : C<VAR>Y : D<VAR>g : F'.obj X ⟶ Y<GOAL>(CategoryTheory.Adjunction.equivHomsetLeftOfNatIso iso).symm g = CategoryTheory.CategoryStruct.comp (iso.hom.app X) g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G G' : CategoryTheory.Functor D C<VAR>iso : G ≅ G'<VAR>X : C<VAR>Y : D<VAR>f : X ⟶ G.obj Y<GOAL>(CategoryTheory.Adjunction.equivHomsetRightOfNatIso iso) f = CategoryTheory.CategoryStruct.comp f (iso.hom.app Y)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G G' : CategoryTheory.Functor D C<VAR>iso : G ≅ G'<VAR>X : C<VAR>Y : D<VAR>g : X ⟶ G'.obj Y<GOAL>(CategoryTheory.Adjunction.equivHomsetRightOfNatIso iso).symm g = CategoryTheory.CategoryStruct.comp g (iso.inv.app Y)
<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>G : CategoryTheory.Functor D C<VAR>E : Type u₃<VAR>ℰ : CategoryTheory.Category.{v₃, u₃} E<VAR>H : CategoryTheory.Functor D E<VAR>I : CategoryTheory.Functor E D<VAR>adj₁ : F ⊣ G<VAR>adj₂ : H ⊣ I<VAR>X : C<GOAL>(adj₁.comp adj₂).unit.app X = CategoryTheory.CategoryStruct.comp (adj₁.unit.app X) (G.map (adj₂.unit.app (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 : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D C<VAR>E : Type u₃<VAR>ℰ : CategoryTheory.Category.{v₃, u₃} E<VAR>H : CategoryTheory.Functor D E<VAR>I : CategoryTheory.Functor E D<VAR>adj₁ : F ⊣ G<VAR>adj₂ : H ⊣ I<VAR>X : E<GOAL>(adj₁.comp adj₂).counit.app X = CategoryTheory.CategoryStruct.comp (H.map (adj₁.counit.app (I.obj X))) (adj₂.counit.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F_obj : C → D<VAR>e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)<VAR>he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)<VAR>X X' : C<VAR>f : X ⟶ X'<GOAL>(CategoryTheory.Adjunction.leftAdjointOfEquiv e he).map f = (e X (F_obj X')).symm (CategoryTheory.CategoryStruct.comp f ((e X' (F_obj X')) (CategoryTheory.CategoryStruct.id (F_obj X'))))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F_obj : C → D<VAR>e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)<VAR>he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)<GOAL>∀ (a : C), (CategoryTheory.Adjunction.leftAdjointOfEquiv e he).obj a = F_obj a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F_obj : C → D<VAR>e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)<VAR>he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)<VAR>Y : D<GOAL>(CategoryTheory.Adjunction.adjunctionOfEquivLeft e he).counit.app Y = (e (G.obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G.obj Y))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F_obj : C → D<VAR>e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)<VAR>he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)<VAR>X : C<GOAL>(CategoryTheory.Adjunction.adjunctionOfEquivLeft e he).unit.app X = (e X (F_obj X)) (CategoryTheory.CategoryStruct.id (F_obj X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor D C<VAR>F_obj : C → D<VAR>e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)<VAR>he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)<VAR>X : C<VAR>Y : D<GOAL>(CategoryTheory.Adjunction.adjunctionOfEquivLeft e he).homEquiv X Y = e X Y
<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>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)<VAR>X' X : C<VAR>Y : D<VAR>f : X' ⟶ X<VAR>g : X ⟶ G_obj Y<GOAL>CategoryTheory.CategoryStruct.comp (F.map f) ((e X Y).symm g) = (e X' Y).symm (CategoryTheory.CategoryStruct.comp f g)
<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>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)<VAR>Y Y' : D<VAR>g : Y ⟶ Y'<GOAL>(CategoryTheory.Adjunction.rightAdjointOfEquiv e he).map g = (e (G_obj Y) Y') (CategoryTheory.CategoryStruct.comp ((e (G_obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G_obj Y))) g)
<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>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)<GOAL>∀ (a : D), (CategoryTheory.Adjunction.rightAdjointOfEquiv e he).obj a = G_obj a
<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>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)<VAR>X : C<GOAL>(CategoryTheory.Adjunction.adjunctionOfEquivRight e he).unit.app X = (e X (F.obj X)) (CategoryTheory.CategoryStruct.id (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 : CategoryTheory.Functor C D<VAR>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)<VAR>Y : D<GOAL>(CategoryTheory.Adjunction.adjunctionOfEquivRight e he).counit.app Y = (e (G_obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G_obj Y))
<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>G_obj : D → C<VAR>e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)<VAR>he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g)<VAR>X : C<VAR>Y : D<GOAL>(CategoryTheory.Adjunction.adjunctionOfEquivRight e he).homEquiv X Y = e X Y
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)<VAR>∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)<GOAL>adj.toEquivalence.functor = F
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)<VAR>∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)<VAR>X : C<GOAL>adj.toEquivalence.unitIso.inv.app X = CategoryTheory.inv (adj.unit.app X)
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)<VAR>∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)<VAR>X : D<GOAL>adj.toEquivalence.counitIso.inv.app X = CategoryTheory.inv (adj.counit.app X)
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)<VAR>∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)<GOAL>adj.toEquivalence.inverse = G
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)<VAR>∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)<VAR>X : C<GOAL>adj.toEquivalence.unitIso.hom.app X = adj.unit.app X
<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>G : CategoryTheory.Functor D C<VAR>adj : F ⊣ G<VAR>∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)<VAR>∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)<VAR>X : D<GOAL>adj.toEquivalence.counitIso.hom.app X = adj.counit.app X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>G : CategoryTheory.Functor C D<VAR>G.IsRightAdjoint<VAR>∀ (X : D), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofIsRightAdjoint G).unit.app X)<VAR>∀ (Y : C), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofIsRightAdjoint G).counit.app Y)<GOAL>G.IsEquivalence
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.toAdjunction.counit = e.counit
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.toAdjunction.unit = e.unit
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.functor.IsLeftAdjoint
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.inverse.IsRightAdjoint
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.inverse.IsLeftAdjoint
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.functor.IsRightAdjoint
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>h : F ≅ G<VAR>F.IsRightAdjoint<GOAL>G.IsRightAdjoint
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>h : F ≅ G<VAR>F.IsLeftAdjoint<GOAL>G.IsLeftAdjoint
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>CategoryTheory.Limits.HasCoproduct X<VAR>∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), CategoryTheory.Limits.HasPullback g (CategoryTheory.Limits.Sigma.ι X a)<VAR>∀ {Z : C} (g : Z ⟶ ∐ X), CategoryTheory.Limits.HasCoproduct fun a => CategoryTheory.Limits.pullback g (CategoryTheory.Limits.Sigma.ι X a)<VAR>∀ {Z : C} (g : Z ⟶ ∐ X), CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc fun a => CategoryTheory.Limits.pullback.fst g (CategoryTheory.Limits.Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>hg : CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Sigma.desc π) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Sigma.desc π)<GOAL>CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Sigma.desc e) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Sigma.desc e)
<VAR>obj : Type u<VAR>self : CategoryTheory.Groupoid obj<VAR>X Y : obj<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.Groupoid.inv f) = CategoryTheory.CategoryStruct.id X
<VAR>obj : Type u<VAR>self : CategoryTheory.Groupoid obj<VAR>X Y : obj<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv f) f = CategoryTheory.CategoryStruct.id Y
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.Groupoid.inv f = CategoryTheory.inv f
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>X Y : C<GOAL>∀ (a : X ⟶ Y), CategoryTheory.Groupoid.invEquiv a = CategoryTheory.Groupoid.inv a
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>X Y : C<GOAL>∀ (a : Y ⟶ X), CategoryTheory.Groupoid.invEquiv.symm a = CategoryTheory.Groupoid.inv a
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Quiver.reverse f = CategoryTheory.Groupoid.inv f
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>unop : C<GOAL>(CategoryTheory.Groupoid.invFunctor C).obj unop = Opposite.op unop
<VAR>C : Type u<VAR>CategoryTheory.Groupoid C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Groupoid.invFunctor C).map f = (CategoryTheory.Groupoid.inv f).op
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>i : I<VAR>X Y Z : C i<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.Sigma.SigmaHom.mk f).comp (CategoryTheory.Sigma.SigmaHom.mk g) = CategoryTheory.Sigma.SigmaHom.mk (CategoryTheory.CategoryStruct.comp f g)
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X Y Z W : (i : I) × C i<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : Z ⟶ W<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X Y : (i : I) × C i<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>X Y : (i : I) × C i<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>i : I<GOAL>∀ {X Y : C i} (a : X ⟶ Y), (CategoryTheory.Sigma.incl i).map a = CategoryTheory.Sigma.SigmaHom.mk a
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>i : I<VAR>X : C i<GOAL>(CategoryTheory.Sigma.incl i).obj X = ⟨i, X⟩
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor ((i : I) × C i) D<VAR>h : (i : I) → (CategoryTheory.Sigma.incl i).comp F ⟶ (CategoryTheory.Sigma.incl i).comp G<VAR>i : I<VAR>X : C i<GOAL>(CategoryTheory.Sigma.natTrans h).app ⟨i, X⟩ = (h i).app X
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : (i : I) → CategoryTheory.Functor (C i) D<VAR>X : (i : I) × C i<GOAL>(CategoryTheory.Sigma.desc F).obj X = (F X.fst).obj X.snd
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : (i : I) → CategoryTheory.Functor (C i) D<VAR>i : I<VAR>X Y : C i<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Sigma.desc F).map (CategoryTheory.Sigma.SigmaHom.mk f) = (F i).map f
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : (i : I) → CategoryTheory.Functor (C i) D<VAR>i : I<VAR>X : C i<GOAL>(CategoryTheory.Sigma.inclDesc F i).hom.app X = CategoryTheory.CategoryStruct.id ((F i).obj X)
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : (i : I) → CategoryTheory.Functor (C i) D<VAR>i : I<VAR>X : C i<GOAL>(CategoryTheory.Sigma.inclDesc F i).inv.app X = CategoryTheory.CategoryStruct.id ((F i).obj X)
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : (i : I) → CategoryTheory.Functor (C i) D<VAR>q : CategoryTheory.Functor ((i : I) × C i) D<VAR>h : (i : I) → (CategoryTheory.Sigma.incl i).comp q ≅ F i<VAR>i : I<VAR>X : C i<GOAL>(CategoryTheory.Sigma.descUniq F q h).hom.app ⟨i, X⟩ = (h i).hom.app X
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : (i : I) → CategoryTheory.Functor (C i) D<VAR>q : CategoryTheory.Functor ((i : I) × C i) D<VAR>h : (i : I) → (CategoryTheory.Sigma.incl i).comp q ≅ F i<VAR>i : I<VAR>X : C i<GOAL>(CategoryTheory.Sigma.descUniq F q h).inv.app ⟨i, X⟩ = (h i).inv.app X
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>q₁ q₂ : CategoryTheory.Functor ((i : I) × C i) D<VAR>h : (i : I) → (CategoryTheory.Sigma.incl i).comp q₁ ≅ (CategoryTheory.Sigma.incl i).comp q₂<GOAL>(CategoryTheory.Sigma.natIso h).inv = CategoryTheory.Sigma.natTrans fun i => (h i).inv
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>q₁ q₂ : CategoryTheory.Functor ((i : I) × C i) D<VAR>h : (i : I) → (CategoryTheory.Sigma.incl i).comp q₁ ≅ (CategoryTheory.Sigma.incl i).comp q₂<GOAL>(CategoryTheory.Sigma.natIso h).hom = CategoryTheory.Sigma.natTrans fun i => (h i).hom
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₂<VAR>g : J → I<VAR>j : J<VAR>X : C (g j)<GOAL>(CategoryTheory.Sigma.map C g).obj ⟨j, X⟩ = ⟨g j, X⟩
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₂<VAR>g : J → I<VAR>j : J<VAR>X Y : C (g j)<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Sigma.map C g).map (CategoryTheory.Sigma.SigmaHom.mk f) = CategoryTheory.Sigma.SigmaHom.mk f
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₂<VAR>g : J → I<VAR>j : J<VAR>X : C (g j)<GOAL>(CategoryTheory.Sigma.inclCompMap C g j).inv.app X = CategoryTheory.CategoryStruct.id ⟨g j, X⟩
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₂<VAR>g : J → I<VAR>j : J<VAR>X : C (g j)<GOAL>(CategoryTheory.Sigma.inclCompMap C g j).hom.app X = CategoryTheory.CategoryStruct.id ⟨g j, X⟩
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<GOAL>∀ (x : (i : I) × (fun i => C (id i)) i), (CategoryTheory.Sigma.mapId I C).hom.app x = CategoryTheory.CategoryStruct.id ⟨x.fst, x.snd⟩
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<GOAL>∀ (x : (i : I) × (fun i => C (id i)) i), (CategoryTheory.Sigma.mapId I C).inv.app x = CategoryTheory.CategoryStruct.id ⟨x.fst, x.snd⟩
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₂<VAR>K : Type w₃<VAR>f : K → J<VAR>g : J → I<VAR>X : (i : K) × (fun i => C (g (f i))) i<GOAL>(CategoryTheory.Sigma.mapComp C f g).hom.app X = CategoryTheory.CategoryStruct.id ⟨g (f X.fst), X.snd⟩
<VAR>I : Type w₁<VAR>C : I → Type u₁<VAR>(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)<VAR>J : Type w₂<VAR>K : Type w₃<VAR>f : K → J<VAR>g : J → I<VAR>X : (i : K) × (fun i => C (g (f i))) i<GOAL>(CategoryTheory.Sigma.mapComp C f g).inv.app X = CategoryTheory.CategoryStruct.id ⟨g (f X.fst), X.snd⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>g : CategoryTheory.Over Y<GOAL>((CategoryTheory.Over.pullback f).obj g).hom = CategoryTheory.Limits.pullback.snd g.hom f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>g : CategoryTheory.Over Y<GOAL>((CategoryTheory.Over.pullback f).obj g).left = CategoryTheory.Limits.pullback g.hom f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>g : CategoryTheory.Over Y<VAR>h : CategoryTheory.Over Y<VAR>k : g ⟶ h<GOAL>((CategoryTheory.Over.pullback f).map k).left = CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g.hom f) k.left) (CategoryTheory.Limits.pullback.snd g.hom f) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>∀ (X_1 : CategoryTheory.Over X), (CategoryTheory.Over.mapPullbackAdj f).unit.app X_1 = CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id X_1.left) X_1.hom ⋯) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>∀ (Y_1 : CategoryTheory.Over Y), (CategoryTheory.Over.mapPullbackAdj f).counit.app Y_1 = CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.fst Y_1.hom f) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>CategoryTheory.Limits.HasBinaryProducts C<GOAL>∀ (X_1 : C), ((CategoryTheory.Over.star X).obj X_1).left = (X ⨯ X_1)