ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>G H : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct G H<VAR>hG : CategoryTheory.IsSeparator G<GOAL>CategoryTheory.IsSeparator (G ⨿ H)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>G H : C<VAR>CategoryTheory.Limits.HasBinaryCoproduct G H<VAR>hH : CategoryTheory.IsSeparator H<GOAL>CategoryTheory.IsSeparator (G ⨿ H)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>β : Type w<VAR>f : β → C<VAR>CategoryTheory.Limits.HasCoproduct f<GOAL>CategoryTheory.IsSeparator (∐ f) ↔ CategoryTheory.IsSeparating (Set.range f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>β : Type w<VAR>f : β → C<VAR>CategoryTheory.Limits.HasCoproduct f<VAR>b : β<VAR>hb : CategoryTheory.IsSeparator (f b)<GOAL>CategoryTheory.IsSeparator (∐ f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>G H : C<VAR>CategoryTheory.Limits.HasBinaryProduct G H<GOAL>CategoryTheory.IsCoseparator (G ⨯ H) ↔ CategoryTheory.IsCoseparating {G, H}
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>G H : C<VAR>CategoryTheory.Limits.HasBinaryProduct G H<VAR>hG : CategoryTheory.IsCoseparator G<GOAL>CategoryTheory.IsCoseparator (G ⨯ H)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>G H : C<VAR>CategoryTheory.Limits.HasBinaryProduct G H<VAR>hH : CategoryTheory.IsCoseparator H<GOAL>CategoryTheory.IsCoseparator (G ⨯ H)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>β : Type w<VAR>f : β → C<VAR>CategoryTheory.Limits.HasProduct f<GOAL>CategoryTheory.IsCoseparator (∏ᶜ f) ↔ CategoryTheory.IsCoseparating (Set.range f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>β : Type w<VAR>f : β → C<VAR>CategoryTheory.Limits.HasProduct f<VAR>b : β<VAR>hb : CategoryTheory.IsCoseparator (f b)<GOAL>CategoryTheory.IsCoseparator (∏ᶜ f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsDetector G ↔ (CategoryTheory.coyoneda.obj (Opposite.op G)).ReflectsIsomorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : C<GOAL>CategoryTheory.IsCodetector G ↔ (CategoryTheory.yoneda.obj G).ReflectsIsomorphisms
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>G : C<VAR>hG : CategoryTheory.IsDetector G<GOAL>CategoryTheory.WellPowered C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>self : CategoryTheory.Triangulated.TStructure C<GOAL>self.GE 1 ≤ self.GE 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>self : CategoryTheory.Triangulated.TStructure C<VAR>n a n' : ℤ<VAR>h : a + n' = n<VAR>X : C<VAR>hX : self.LE n X<GOAL>self.LE n' ((CategoryTheory.shiftFunctor C a).obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>self : CategoryTheory.Triangulated.TStructure C<VAR>n : ℤ<GOAL>CategoryTheory.ClosedUnderIsomorphisms (self.GE n)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>self : CategoryTheory.Triangulated.TStructure C<VAR>n a n' : ℤ<VAR>h : a + n' = n<VAR>X : C<VAR>hX : self.GE n X<GOAL>self.GE n' ((CategoryTheory.shiftFunctor C a).obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>self : CategoryTheory.Triangulated.TStructure C<VAR>n : ℤ<GOAL>CategoryTheory.ClosedUnderIsomorphisms (self.LE n)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>self : CategoryTheory.Triangulated.TStructure C<VAR>A : C<GOAL>∃ X Y, ∃ (_ : self.LE 0 X) (_ : self.GE 1 Y), ∃ f g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>self : CategoryTheory.Triangulated.TStructure C<GOAL>self.LE 0 ≤ self.LE 1
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>self : CategoryTheory.Triangulated.TStructure C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hX : self.LE 0 X<VAR>hY : self.GE 1 Y<GOAL>f = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>t : CategoryTheory.Triangulated.TStructure C<VAR>A : C<VAR>n₀ n₁ : ℤ<VAR>h : n₀ + 1 = n₁<GOAL>∃ X Y, ∃ (_ : t.LE n₀ X) (_ : t.GE n₁ Y), ∃ f g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>t : CategoryTheory.Triangulated.TStructure C<VAR>a n n' : ℤ<VAR>hn' : a + n = n'<GOAL>CategoryTheory.PredicateShift (t.LE n) a = t.LE n'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>t : CategoryTheory.Triangulated.TStructure C<VAR>a n n' : ℤ<VAR>hn' : a + n = n'<GOAL>CategoryTheory.PredicateShift (t.GE n) a = t.GE n'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>t : CategoryTheory.Triangulated.TStructure C<GOAL>Monotone t.LE
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>t : CategoryTheory.Triangulated.TStructure C<GOAL>Antitone t.GE
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>t : CategoryTheory.Triangulated.TStructure C<VAR>X : C<VAR>n : ℤ<VAR>self : t.IsLE X n<GOAL>t.LE n X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>t : CategoryTheory.Triangulated.TStructure C<VAR>X : C<VAR>n : ℤ<VAR>self : t.IsGE X n<GOAL>t.GE n X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>t : CategoryTheory.Triangulated.TStructure C<VAR>X : C<VAR>n : ℤ<VAR>t.IsLE X n<GOAL>t.LE n X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>CategoryTheory.HasShift C ℤ<VAR>∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>CategoryTheory.Pretriangulated C<VAR>t : CategoryTheory.Triangulated.TStructure C<VAR>X : C<VAR>n : ℤ<VAR>t.IsGE X n<GOAL>t.GE n X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M : Comon_ C<VAR>N : Mon_ C<GOAL>1 = CategoryTheory.CategoryStruct.comp M.counit N.one
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>M : Comon_ C<VAR>N : Mon_ C<VAR>f g : CategoryTheory.Conv M N<GOAL>f * g = CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f M.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft N.X g) N.mul))
<VAR>R : Type w<VAR>Ring R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>X : C<VAR>Y : Cᵒᵖ<GOAL>((CategoryTheory.linearYoneda R C).obj X).obj Y = ModuleCat.of R (Opposite.unop Y ⟶ X)
<VAR>R : Type w<VAR>Ring R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<VAR>Y : Cᵒᵖ<GOAL>((CategoryTheory.linearYoneda R C).map f).app Y = ModuleCat.ofHom (CategoryTheory.Linear.rightComp R (Opposite.unop Y) f)
<VAR>R : Type w<VAR>Ring R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>X : C<GOAL>∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y), ((CategoryTheory.linearYoneda R C).obj X).map f = ModuleCat.ofHom (CategoryTheory.Linear.leftComp R X f.unop)
<VAR>R : Type w<VAR>Ring R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>Y : Cᵒᵖ<VAR>X : C<GOAL>((CategoryTheory.linearCoyoneda R C).obj Y).obj X = ModuleCat.of R (Opposite.unop Y ⟶ X)
<VAR>R : Type w<VAR>Ring R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>Y : Cᵒᵖ<GOAL>∀ {X Y_1 : C} (f : X ⟶ Y_1), ((CategoryTheory.linearCoyoneda R C).obj Y).map f = ModuleCat.ofHom (CategoryTheory.Linear.rightComp R (Opposite.unop Y) f)
<VAR>R : Type w<VAR>Ring R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>Y₁ Y₂ : Cᵒᵖ<VAR>f : Y₁ ⟶ Y₂<VAR>X : C<GOAL>((CategoryTheory.linearCoyoneda R C).map f).app X = ModuleCat.ofHom (CategoryTheory.Linear.leftComp R X f.unop)
<VAR>R : Type w<VAR>Ring R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<GOAL>(CategoryTheory.linearYoneda R C).comp ((CategoryTheory.whiskeringRight Cᵒᵖ (ModuleCat R) (Type v)).obj (CategoryTheory.forget (ModuleCat R))) = CategoryTheory.yoneda
<VAR>R : Type w<VAR>Ring R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<GOAL>(CategoryTheory.linearYoneda R C).comp ((CategoryTheory.whiskeringRight Cᵒᵖ (ModuleCat R) AddCommGrp).obj (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)) = CategoryTheory.preadditiveYoneda
<VAR>R : Type w<VAR>Ring R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<GOAL>(CategoryTheory.linearCoyoneda R C).comp ((CategoryTheory.whiskeringRight C (ModuleCat R) (Type v)).obj (CategoryTheory.forget (ModuleCat R))) = CategoryTheory.coyoneda
<VAR>R : Type w<VAR>Ring R<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<GOAL>(CategoryTheory.linearCoyoneda R C).comp ((CategoryTheory.whiskeringRight C (ModuleCat R) AddCommGrp).obj (CategoryTheory.forget₂ (ModuleCat R) AddCommGrp)) = CategoryTheory.preadditiveCoyoneda
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<GOAL>CategoryTheory.WithTerminal.down (CategoryTheory.CategoryStruct.id (CategoryTheory.WithTerminal.of X)) = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y Z : C<VAR>f : CategoryTheory.WithTerminal.of X ⟶ CategoryTheory.WithTerminal.of Y<VAR>g : CategoryTheory.WithTerminal.of Y ⟶ CategoryTheory.WithTerminal.of Z<GOAL>CategoryTheory.WithTerminal.down (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.WithTerminal.down f) (CategoryTheory.WithTerminal.down g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X : C<VAR>f : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.of X<GOAL>False
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : CategoryTheory.Functor C D<VAR>X Y : CategoryTheory.WithTerminal C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.WithTerminal.map F).map f = match X, Y, f with | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.of y, f => F.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.star, x => PUnit.unit | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => PUnit.unit
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F : CategoryTheory.Functor C D<VAR>X : CategoryTheory.WithTerminal C<GOAL>(CategoryTheory.WithTerminal.map F).obj X = match X with | CategoryTheory.WithTerminal.of x => CategoryTheory.WithTerminal.of (F.obj x) | CategoryTheory.WithTerminal.star => CategoryTheory.WithTerminal.star
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.WithTerminal C<GOAL>(CategoryTheory.WithTerminal.mapId C).hom.app X = (match X with | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of x) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).hom
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.WithTerminal C<GOAL>(CategoryTheory.WithTerminal.mapId C).inv.app X = (match X with | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of x) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>E : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} D<VAR>CategoryTheory.Category.{u_4, u_2} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>X : CategoryTheory.WithTerminal C<GOAL>(CategoryTheory.WithTerminal.mapComp F G).inv.app X = (match X with | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of (G.obj (F.obj x))) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).inv
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>E : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} D<VAR>CategoryTheory.Category.{u_4, u_2} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>X : CategoryTheory.WithTerminal C<GOAL>(CategoryTheory.WithTerminal.mapComp F G).hom.app X = (match X with | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of (G.obj (F.obj x))) | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F G : CategoryTheory.Functor C D<VAR>η : F ⟶ G<VAR>X : CategoryTheory.WithTerminal C<GOAL>(CategoryTheory.WithTerminal.map₂ η).app X = match X with | CategoryTheory.WithTerminal.of x => η.app x | CategoryTheory.WithTerminal.star => CategoryTheory.CategoryStruct.id CategoryTheory.WithTerminal.star
<GOAL>∀ {a b : CategoryTheory.Cat} {f g : a ⟶ b} (η : f ⟶ g), CategoryTheory.WithTerminal.prelaxfunctor.map₂ η = CategoryTheory.WithTerminal.map₂ η
<GOAL>∀ {X Y : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑X ↑Y), CategoryTheory.WithTerminal.prelaxfunctor.map F = CategoryTheory.WithTerminal.map F
<VAR>C : CategoryTheory.Cat<GOAL>CategoryTheory.WithTerminal.prelaxfunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.WithTerminal ↑C)
<GOAL>∀ {a b c : CategoryTheory.Cat} (F : CategoryTheory.Functor ↑a ↑b) (G : CategoryTheory.Functor ↑b ↑c), CategoryTheory.WithTerminal.pseudofunctor.mapComp F G = CategoryTheory.WithTerminal.mapComp F G
<GOAL>CategoryTheory.WithTerminal.pseudofunctor.toPrelaxFunctor = CategoryTheory.WithTerminal.prelaxfunctor
<VAR>C : CategoryTheory.Cat<GOAL>CategoryTheory.WithTerminal.pseudofunctor.mapId C = CategoryTheory.WithTerminal.mapId ↑C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → F.obj x ⟶ Z<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x<VAR>X : CategoryTheory.WithTerminal C<GOAL>(CategoryTheory.WithTerminal.lift F M hM).obj X = match X with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → F.obj x ⟶ Z<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x<VAR>X Y : CategoryTheory.WithTerminal C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.WithTerminal.lift F M hM).map f = match X, Y, f with | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.of y, f => F.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => M x | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → F.obj x ⟶ Z<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x<VAR>X : C<GOAL>(CategoryTheory.WithTerminal.inclLift F M hM).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → F.obj x ⟶ Z<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x<VAR>X : C<GOAL>(CategoryTheory.WithTerminal.inclLift F M hM).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithTerminal.incl.obj X with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → F.obj x ⟶ Z<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x<GOAL>(CategoryTheory.WithTerminal.liftStar F M hM).hom = CategoryTheory.CategoryStruct.id Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → F.obj x ⟶ Z<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x<GOAL>(CategoryTheory.WithTerminal.liftStar F M hM).inv = CategoryTheory.CategoryStruct.id Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>M : (x : C) → F.obj x ⟶ Z<VAR>hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x<VAR>x : C<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.lift F M hM).map (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.incl.obj x))) (CategoryTheory.WithTerminal.liftStar F M hM).hom = CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.inclLift F M hM).hom.app x) (M x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>hZ : CategoryTheory.Limits.IsTerminal Z<VAR>X Y : CategoryTheory.WithTerminal C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.WithTerminal.liftToTerminal F hZ).map f = match X, Y, f with | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.of y, f => F.map (CategoryTheory.WithTerminal.down f) | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => hZ.from (F.obj x) | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>hZ : CategoryTheory.Limits.IsTerminal Z<VAR>X : CategoryTheory.WithTerminal C<GOAL>(CategoryTheory.WithTerminal.liftToTerminal F hZ).obj X = match X with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>hZ : CategoryTheory.Limits.IsTerminal Z<VAR>X : C<GOAL>(CategoryTheory.WithTerminal.inclLiftToTerminal F hZ).hom.app X = CategoryTheory.CategoryStruct.id (match CategoryTheory.WithTerminal.incl.obj X with | CategoryTheory.WithTerminal.of x => F.obj x | CategoryTheory.WithTerminal.star => Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>hZ : CategoryTheory.Limits.IsTerminal Z<VAR>X : C<GOAL>(CategoryTheory.WithTerminal.inclLiftToTerminal F hZ).inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>hZ : CategoryTheory.Limits.IsTerminal Z<VAR>G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D<VAR>h : CategoryTheory.WithTerminal.incl.comp G ≅ F<VAR>hG : G.obj CategoryTheory.WithTerminal.star ≅ Z<VAR>X : CategoryTheory.WithTerminal C<GOAL>(CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).hom.app X = (match X with | CategoryTheory.WithTerminal.of x => h.app x | CategoryTheory.WithTerminal.star => hG).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>Z : D<VAR>F : CategoryTheory.Functor C D<VAR>hZ : CategoryTheory.Limits.IsTerminal Z<VAR>G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D<VAR>h : CategoryTheory.WithTerminal.incl.comp G ≅ F<VAR>hG : G.obj CategoryTheory.WithTerminal.star ≅ Z<VAR>X : CategoryTheory.WithTerminal C<GOAL>(CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).inv.app X = (match X with | CategoryTheory.WithTerminal.of x => h.app x | CategoryTheory.WithTerminal.star => hG).inv