ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>h : CategoryTheory.HasLiftingProperty i p<GOAL>CategoryTheory.HasLiftingProperty p.op i.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : Cᵒᵖ<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>h : CategoryTheory.HasLiftingProperty i p<GOAL>CategoryTheory.HasLiftingProperty p.unop i.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : C<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<GOAL>CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty p.op i.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y : Cᵒᵖ<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<GOAL>CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty p.unop i.unop
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B A' B' X Y : C<VAR>i : A ⟶ B<VAR>i' : A' ⟶ B'<VAR>e : CategoryTheory.Arrow.mk i ≅ CategoryTheory.Arrow.mk i'<VAR>p : X ⟶ Y<VAR>hip : CategoryTheory.HasLiftingProperty i p<GOAL>CategoryTheory.HasLiftingProperty i' p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y X' Y' : C<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>p' : X' ⟶ Y'<VAR>e : CategoryTheory.Arrow.mk p ≅ CategoryTheory.Arrow.mk p'<VAR>hip : CategoryTheory.HasLiftingProperty i p<GOAL>CategoryTheory.HasLiftingProperty i p'
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B A' B' X Y : C<VAR>i : A ⟶ B<VAR>i' : A' ⟶ B'<VAR>e : CategoryTheory.Arrow.mk i ≅ CategoryTheory.Arrow.mk i'<VAR>p : X ⟶ Y<GOAL>CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty i' p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>A B X Y X' Y' : C<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>p' : X' ⟶ Y'<VAR>e : CategoryTheory.Arrow.mk p ≅ CategoryTheory.Arrow.mk p'<GOAL>CategoryTheory.HasLiftingProperty i p ↔ CategoryTheory.HasLiftingProperty i p'
<VAR>X : Type u<VAR>Preorder X<VAR>x : X<VAR>h : x ≤ x<GOAL>h.hom = CategoryTheory.CategoryStruct.id x
<VAR>X : Type u<VAR>Preorder X<VAR>x y z : X<VAR>h : x ≤ y<VAR>k : y ≤ z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE h) (CategoryTheory.homOfLE k) = CategoryTheory.homOfLE ⋯
<VAR>X : Type u<VAR>Preorder X<VAR>x y : X<VAR>h : x ⟶ y<GOAL>x ≤ y
<VAR>X : Type u<VAR>Preorder X<VAR>x y : X<VAR>h : x ≤ y<GOAL>⋯ = h
<VAR>X : Type u<VAR>Preorder X<VAR>x y : X<VAR>h : x ⟶ y<GOAL>⋯.hom = h
<VAR>X : Type u<VAR>Preorder X<VAR>x y : X<VAR>h : x ≤ y<VAR>heq : x = y<GOAL>CategoryTheory.IsIso (CategoryTheory.homOfLE h)
<VAR>X : Type u<VAR>Preorder X<VAR>a b c : X<VAR>hab : a ≤ b<VAR>hbc : b = c<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hab) (CategoryTheory.eqToHom hbc) = CategoryTheory.homOfLE ⋯
<VAR>X : Type u<VAR>Preorder X<VAR>a b c : X<VAR>hab : a = b<VAR>hbc : b ≤ c<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hab) (CategoryTheory.homOfLE hbc) = CategoryTheory.homOfLE ⋯
<VAR>X : Type u<VAR>Preorder X<VAR>a b c : X<VAR>hab : b ≤ a<VAR>hbc : Opposite.op b = Opposite.op c<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hab).op (CategoryTheory.eqToHom hbc) = (CategoryTheory.homOfLE ⋯).op
<VAR>X : Type u<VAR>Preorder X<VAR>a b c : X<VAR>hab : Opposite.op a = Opposite.op b<VAR>hbc : c ≤ b<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hab) (CategoryTheory.homOfLE hbc).op = (CategoryTheory.homOfLE ⋯).op
<VAR>X : Type u<VAR>Preorder X<VAR>x y : Xᵒᵖ<VAR>h : x ⟶ y<GOAL>Opposite.unop y ≤ Opposite.unop x
<VAR>X : Type u<VAR>Preorder X<GOAL>∀ {X_1 Y : Xᵒᵖ} (f : X_1 ⟶ Y), (CategoryTheory.orderDualEquivalence X).inverse.map f = CategoryTheory.homOfLE ⋯
<VAR>X : Type u<VAR>Preorder X<GOAL>∀ {X_1 Y : Xᵒᵈ} (f : X_1 ⟶ Y), (CategoryTheory.orderDualEquivalence X).functor.map f = (CategoryTheory.homOfLE ⋯).op
<VAR>X : Type u<VAR>Preorder X<VAR>x : Xᵒᵖ<GOAL>(CategoryTheory.orderDualEquivalence X).inverse.obj x = OrderDual.toDual (Opposite.unop x)
<VAR>X : Type u<VAR>Preorder X<GOAL>(CategoryTheory.orderDualEquivalence X).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id Xᵒᵈ)
<VAR>X : Type u<VAR>Preorder X<VAR>x : Xᵒᵈ<GOAL>(CategoryTheory.orderDualEquivalence X).functor.obj x = Opposite.op (OrderDual.ofDual x)
<VAR>X : Type u<VAR>Preorder X<GOAL>(CategoryTheory.orderDualEquivalence X).counitIso = CategoryTheory.Iso.refl ({ obj := fun x => OrderDual.toDual (Opposite.unop x), map := fun {X_1 Y} f => CategoryTheory.homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun x => Opposite.op (OrderDual.ofDual x), map := fun {X_1 Y} f => (CategoryTheory.homOfLE ⋯).op, map_id := ⋯, map_comp := ⋯ })
<VAR>X : Type u<VAR>Y : Type v<VAR>Preorder X<VAR>Preorder Y<VAR>f : X → Y<VAR>h : Monotone f<GOAL>h.functor.obj = f
<VAR>X : Type u<VAR>Y : Type v<VAR>Preorder X<VAR>Preorder Y<VAR>e : X ≃o Y<GOAL>e.equivalence.unitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
<VAR>X : Type u<VAR>Y : Type v<VAR>Preorder X<VAR>Preorder Y<VAR>e : X ≃o Y<GOAL>e.equivalence.functor = ⋯.functor
<VAR>X : Type u<VAR>Y : Type v<VAR>Preorder X<VAR>Preorder Y<VAR>e : X ≃o Y<GOAL>e.equivalence.counitIso = CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
<VAR>X : Type u<VAR>Y : Type v<VAR>Preorder X<VAR>Preorder Y<VAR>e : X ≃o Y<GOAL>e.equivalence.inverse = ⋯.functor
<VAR>X : Type u<VAR>Y : Type v<VAR>Preorder X<VAR>Preorder Y<VAR>f : CategoryTheory.Functor X Y<GOAL>Monotone f.obj
<VAR>X : Type u<VAR>PartialOrder X<VAR>x y : X<VAR>f : x ≅ y<GOAL>x = y
<VAR>X : Type u<VAR>Y : Type v<VAR>PartialOrder X<VAR>PartialOrder Y<VAR>e : X ≌ Y<VAR>x : X<GOAL>e.toOrderIso x = e.functor.obj x
<VAR>X : Type u<VAR>Y : Type v<VAR>PartialOrder X<VAR>PartialOrder Y<VAR>e : X ≌ Y<VAR>y : Y<GOAL>e.toOrderIso.symm y = e.inverse.obj y
<VAR>X : Type u_3<VAR>to_prod : X × X<GOAL>(Bipointed.of to_prod).X = X
<VAR>X Y : Bipointed<VAR>self : X.Hom Y<GOAL>self.toFun X.toProd.1 = Y.toProd.1
<VAR>X Y : Bipointed<VAR>self : X.Hom Y<GOAL>self.toFun X.toProd.2 = Y.toProd.2
<VAR>X : Bipointed<VAR>a : X.X<GOAL>(Bipointed.Hom.id X).toFun a = id a
<VAR>X Y Z : Bipointed<VAR>f : X.Hom Y<VAR>g : Y.Hom Z<GOAL>∀ (a : X.X), (f.comp g).toFun a = (g.toFun ∘ f.toFun) a
<VAR>X : Bipointed<GOAL>(Bipointed.swap.obj X).X = X.X
<VAR>X : Bipointed<GOAL>(Bipointed.swap.obj X).toProd = X.toProd.swap
<GOAL>∀ {X Y : Bipointed} (f : X ⟶ Y) (a : X.X), (Bipointed.swap.map f).toFun a = f.toFun a
<VAR>X : Bipointed<VAR>a : ((𝟭 Bipointed).obj X).X<GOAL>(Bipointed.swapEquiv.counitIso.inv.app X).toFun a = a
<VAR>X : Bipointed<GOAL>(Bipointed.swapEquiv.inverse.obj X).toProd = X.toProd.swap
<VAR>X : Bipointed<GOAL>(Bipointed.swapEquiv.functor.obj X).X = X.X
<VAR>X : Bipointed<GOAL>∀ (a : ((Bipointed.swap ⋙ Bipointed.swap).obj X).X), (Bipointed.swapEquiv.unitIso.inv.app X).toFun a = (Bipointed.swap.map (Bipointed.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ }) ≫ Bipointed.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ } ≫ { toFun := id, map_fst := ⋯, map_snd := ⋯ }).toFun ((𝟙 (Bipointed.swap.obj (Bipointed.swap.obj X))).toFun a)
<VAR>X : Bipointed<GOAL>(Bipointed.swapEquiv.functor.obj X).toProd = X.toProd.swap
<VAR>X : Bipointed<GOAL>(Bipointed.swapEquiv.inverse.obj X).X = X.X
<VAR>X : Bipointed<VAR>a : ((Bipointed.swap ⋙ Bipointed.swap).obj X).X<GOAL>(Bipointed.swapEquiv.counitIso.hom.app X).toFun a = a
<VAR>X : Bipointed<GOAL>∀ (a : ((𝟭 Bipointed).obj X).X), (Bipointed.swapEquiv.unitIso.hom.app X).toFun a = (𝟙 (Bipointed.swap.obj (Bipointed.swap.obj X))).toFun (({ toFun := id, map_fst := ⋯, map_snd := ⋯ } ≫ Bipointed.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ } ≫ Bipointed.swap.map (Bipointed.swap.map { toFun := id, map_fst := ⋯, map_snd := ⋯ })).toFun a)
<GOAL>∀ {X Y : Bipointed} (f : X ⟶ Y) (a : X.X), (Bipointed.swapEquiv.functor.map f).toFun a = f.toFun a
<GOAL>∀ {X Y : Bipointed} (f : X ⟶ Y) (a : X.X), (Bipointed.swapEquiv.inverse.map f).toFun a = f.toFun a
<GOAL>Bipointed.swapEquiv.symm = Bipointed.swapEquiv
<GOAL>bipointedToPointedFst ⋙ CategoryTheory.forget Pointed = CategoryTheory.forget Bipointed
<GOAL>bipointedToPointedSnd ⋙ CategoryTheory.forget Pointed = CategoryTheory.forget Bipointed
<GOAL>Bipointed.swap ⋙ bipointedToPointedFst = bipointedToPointedSnd
<GOAL>Bipointed.swap ⋙ bipointedToPointedSnd = bipointedToPointedFst
<GOAL>pointedToBipointedFst ⋙ Bipointed.swap = pointedToBipointedSnd
<GOAL>pointedToBipointedSnd ⋙ Bipointed.swap = pointedToBipointedFst
<VAR>X : Pointed<VAR>a : ((𝟭 Pointed).obj X).X<GOAL>(pointedToBipointedCompBipointedToPointedFst.inv.app X).toFun a = a
<VAR>X : Pointed<VAR>a : ((pointedToBipointed ⋙ bipointedToPointedFst).obj X).X<GOAL>(pointedToBipointedCompBipointedToPointedFst.hom.app X).toFun a = a
<VAR>X : Pointed<VAR>a : ((pointedToBipointed ⋙ bipointedToPointedSnd).obj X).X<GOAL>(pointedToBipointedCompBipointedToPointedSnd.hom.app X).toFun a = a
<VAR>X : Pointed<VAR>a : ((𝟭 Pointed).obj X).X<GOAL>(pointedToBipointedCompBipointedToPointedSnd.inv.app X).toFun a = a
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<GOAL>∀ (a : Type u), (CategoryTheory.ofTypeMonad m).obj a = m a
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<GOAL>∀ {X Y : Type u} (f : X ⟶ Y) (a : m X), (CategoryTheory.ofTypeMonad m).map f a = f <$> a
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>α : Type u<VAR>a : m (m α)<GOAL>(CategoryTheory.ofTypeMonad m).μ.app α a = joinM a
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>α : Type u<GOAL>∀ (a : α), (CategoryTheory.ofTypeMonad m).η.app α a = pure a
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>X : CategoryTheory.KleisliCat m<GOAL>(CategoryTheory.eq m).functor.obj X = X
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<VAR>X : CategoryTheory.Kleisli (CategoryTheory.ofTypeMonad m)<GOAL>(CategoryTheory.eq m).inverse.obj X = X
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<GOAL>(CategoryTheory.eq m).unitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl X) ⋯
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<GOAL>(CategoryTheory.eq m).counitIso = CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Iso.refl X) ⋯
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<GOAL>∀ {X Y : CategoryTheory.Kleisli (CategoryTheory.ofTypeMonad m)} (f : X ⟶ Y) (a : X), (CategoryTheory.eq m).inverse.map f a = f a
<VAR>m : Type u → Type u<VAR>Monad m<VAR>LawfulMonad m<GOAL>∀ {X Y : CategoryTheory.KleisliCat m} (f : X ⟶ Y) (a : X), (CategoryTheory.eq m).functor.map f a = f a
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U V : CategoryTheory.Over X<VAR>f g : U ⟶ V<VAR>h : f.left = g.left<GOAL>f = g
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U : CategoryTheory.Over X<GOAL>U.right = { as := PUnit.unit }
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U : CategoryTheory.Over X<GOAL>(CategoryTheory.CategoryStruct.id U).left = CategoryTheory.CategoryStruct.id U.left
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>a b c : CategoryTheory.Over X<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>(CategoryTheory.CategoryStruct.comp f g).left = CategoryTheory.CategoryStruct.comp f.left g.left
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>A B : CategoryTheory.Over X<VAR>f : A ⟶ B<GOAL>CategoryTheory.CategoryStruct.comp f.left B.hom = A.hom
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y : T<VAR>f : Y ⟶ X<GOAL>(CategoryTheory.Over.mk f).left = Y
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y : T<VAR>f : Y ⟶ X<GOAL>(CategoryTheory.Over.mk f).hom = f
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U V : CategoryTheory.Over X<VAR>f : U.left ⟶ V.left<VAR>w : CategoryTheory.CategoryStruct.comp f V.hom = U.hom := by aesop_cat<GOAL>⋯ = ⋯
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U V : CategoryTheory.Over X<VAR>f : U.left ⟶ V.left<VAR>w : CategoryTheory.CategoryStruct.comp f V.hom = U.hom := by aesop_cat<GOAL>(CategoryTheory.Over.homMk f w).left = f
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f g : CategoryTheory.Over X<VAR>hl : f.left ≅ g.left<VAR>hw : CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom := by aesop_cat<GOAL>(CategoryTheory.Over.isoMk hl hw).inv.left = hl.inv
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f g : CategoryTheory.Over X<VAR>hl : f.left ≅ g.left<VAR>hw : CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom := by aesop_cat<GOAL>(CategoryTheory.Over.isoMk hl hw).hom.left = hl.hom
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f g : CategoryTheory.Over X<VAR>hl : f.left ≅ g.left<VAR>hw : CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom := by aesop_cat<GOAL>⋯ = ⋯
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U : CategoryTheory.Over X<GOAL>(CategoryTheory.Over.forget X).obj U = U.left
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U V : CategoryTheory.Over X<VAR>f : U ⟶ V<GOAL>(CategoryTheory.Over.forget X).map f = f.left
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>self : CategoryTheory.Comma (CategoryTheory.Functor.id T) (CategoryTheory.Functor.fromPUnit X)<GOAL>(CategoryTheory.Over.forgetCocone X).ι.app self = self.hom
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<GOAL>(CategoryTheory.Over.forgetCocone X).pt = X
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y : T<VAR>f : X ⟶ Y<VAR>U : CategoryTheory.Over X<GOAL>((CategoryTheory.Over.map f).obj U).left = U.left
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y : T<VAR>f : X ⟶ Y<VAR>U : CategoryTheory.Over X<GOAL>((CategoryTheory.Over.map f).obj U).hom = CategoryTheory.CategoryStruct.comp U.hom f
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y : T<VAR>f : X ⟶ Y<VAR>U V : CategoryTheory.Over X<VAR>g : U ⟶ V<GOAL>((CategoryTheory.Over.map f).map g).left = g.left
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>Y : T<GOAL>CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.Functor.id (CategoryTheory.Over Y)
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y : T<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Over.map f).comp (CategoryTheory.Over.forget Y) = CategoryTheory.Over.forget X
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U V : CategoryTheory.Over X<VAR>e : U = V<GOAL>(CategoryTheory.eqToHom e).left = CategoryTheory.eqToHom ⋯
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y Z : T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.Over.map (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.Over.map f).comp (CategoryTheory.Over.map g)
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<GOAL>∀ {X Y : T} (f : X ⟶ Y), (CategoryTheory.Over.mapFunctor T).map f = CategoryTheory.Over.map f
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<GOAL>(CategoryTheory.Over.mapFunctor T).obj X = CategoryTheory.Cat.of (CategoryTheory.Over X)
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f g : CategoryTheory.Over X<VAR>k : f ⟶ g<VAR>hk : CategoryTheory.Epi k.left<GOAL>CategoryTheory.Epi k
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f g : CategoryTheory.Over X<VAR>k : f ⟶ g<VAR>hk : CategoryTheory.Mono k.left<GOAL>CategoryTheory.Mono k
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f : CategoryTheory.Over X<GOAL>∀ {X_1 Y : CategoryTheory.Over f} (κ : X_1 ⟶ Y), f.iteratedSliceForward.map κ = CategoryTheory.Over.homMk κ.left.left ⋯
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f : CategoryTheory.Over X<VAR>α : CategoryTheory.Over f<GOAL>f.iteratedSliceForward.obj α = CategoryTheory.Over.mk α.hom.left
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f : CategoryTheory.Over X<GOAL>∀ {X_1 Y : CategoryTheory.Over f.left} (α : X_1 ⟶ Y), f.iteratedSliceBackward.map α = CategoryTheory.Over.homMk (CategoryTheory.Over.homMk α.left ⋯) ⋯
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f : CategoryTheory.Over X<VAR>g : CategoryTheory.Over f.left<GOAL>f.iteratedSliceBackward.obj g = CategoryTheory.Over.mk (CategoryTheory.Over.homMk g.hom ⋯)
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f : CategoryTheory.Over X<GOAL>f.iteratedSliceEquiv.functor = f.iteratedSliceForward
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f : CategoryTheory.Over X<GOAL>f.iteratedSliceEquiv.unitIso = CategoryTheory.NatIso.ofComponents (fun g => CategoryTheory.Over.isoMk (CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Over f)).obj g).left.left) ⋯) ⋯) ⋯
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f : CategoryTheory.Over X<GOAL>f.iteratedSliceEquiv.counitIso = CategoryTheory.NatIso.ofComponents (fun g => CategoryTheory.Over.isoMk (CategoryTheory.Iso.refl ((f.iteratedSliceBackward.comp f.iteratedSliceForward).obj g).left) ⋯) ⋯
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f : CategoryTheory.Over X<GOAL>f.iteratedSliceEquiv.inverse = f.iteratedSliceBackward
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f : CategoryTheory.Over X<GOAL>f.iteratedSliceForward.comp (CategoryTheory.Over.forget f.left) = (CategoryTheory.Over.forget f).comp (CategoryTheory.Over.forget X)
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f : CategoryTheory.Over X<GOAL>f.iteratedSliceBackward.comp ((CategoryTheory.Over.forget f).comp (CategoryTheory.Over.forget X)) = CategoryTheory.Over.forget f.left
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor T D<GOAL>∀ {X_1 Y : CategoryTheory.Over X} (f : X_1 ⟶ Y), (CategoryTheory.Over.post F).map f = CategoryTheory.Over.homMk (F.map f.left) ⋯
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor T D<VAR>Y : CategoryTheory.Over X<GOAL>(CategoryTheory.Over.post F).obj Y = CategoryTheory.Over.mk (F.map Y.hom)
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor D T<VAR>X : T<GOAL>∀ (X_1 : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)), ((CategoryTheory.CostructuredArrow.toOver F X).obj X_1).right = X_1.right
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor D T<VAR>X : T<GOAL>∀ (X_1 : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)), ((CategoryTheory.CostructuredArrow.toOver F X).obj X_1).hom = X_1.hom
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor D T<VAR>X : T<GOAL>∀ {X_1 Y : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)} (f : X_1 ⟶ Y), ((CategoryTheory.CostructuredArrow.toOver F X).map f).right = CategoryTheory.CategoryStruct.id X_1.right
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor D T<VAR>X : T<GOAL>∀ {X_1 Y : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)} (f : X_1 ⟶ Y), ((CategoryTheory.CostructuredArrow.toOver F X).map f).left = F.map f.left
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor D T<VAR>X : T<GOAL>∀ (X_1 : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)), ((CategoryTheory.CostructuredArrow.toOver F X).obj X_1).left = F.obj X_1.left
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U V : CategoryTheory.Under X<VAR>f g : U ⟶ V<VAR>h : f.right = g.right<GOAL>f = g
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U : CategoryTheory.Under X<GOAL>U.left = { as := PUnit.unit }
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U : CategoryTheory.Under X<GOAL>(CategoryTheory.CategoryStruct.id U).right = CategoryTheory.CategoryStruct.id U.right
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>a b c : CategoryTheory.Under X<VAR>f : a ⟶ b<VAR>g : b ⟶ c<GOAL>(CategoryTheory.CategoryStruct.comp f g).right = CategoryTheory.CategoryStruct.comp f.right g.right
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>A B : CategoryTheory.Under X<VAR>f : A ⟶ B<GOAL>CategoryTheory.CategoryStruct.comp A.hom f.right = B.hom
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y : T<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Under.mk f).right = Y
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y : T<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Under.mk f).hom = f
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U V : CategoryTheory.Under X<VAR>f : U.right ⟶ V.right<VAR>w : CategoryTheory.CategoryStruct.comp U.hom f = V.hom := by aesop_cat<GOAL>(CategoryTheory.Under.homMk f w).right = f
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U V : CategoryTheory.Under X<VAR>f : U.right ⟶ V.right<VAR>w : CategoryTheory.CategoryStruct.comp U.hom f = V.hom := by aesop_cat<GOAL>⋯ = ⋯
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f g : CategoryTheory.Under X<VAR>hr : f.right ≅ g.right<VAR>hw : CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom<GOAL>(CategoryTheory.Under.isoMk hr hw).hom.right = hr.hom
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>f g : CategoryTheory.Under X<VAR>hr : f.right ≅ g.right<VAR>hw : CategoryTheory.CategoryStruct.comp f.hom hr.hom = g.hom<GOAL>(CategoryTheory.Under.isoMk hr hw).inv.right = hr.inv
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U : CategoryTheory.Under X<GOAL>(CategoryTheory.Under.forget X).obj U = U.right
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U V : CategoryTheory.Under X<VAR>f : U ⟶ V<GOAL>(CategoryTheory.Under.forget X).map f = f.right
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<GOAL>(CategoryTheory.Under.forgetCone X).pt = X
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>self : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (CategoryTheory.Functor.id T)<GOAL>(CategoryTheory.Under.forgetCone X).π.app self = self.hom
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y : T<VAR>f : X ⟶ Y<VAR>U : CategoryTheory.Under Y<GOAL>((CategoryTheory.Under.map f).obj U).right = U.right
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y : T<VAR>f : X ⟶ Y<VAR>U : CategoryTheory.Under Y<GOAL>((CategoryTheory.Under.map f).obj U).hom = CategoryTheory.CategoryStruct.comp f U.hom
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y : T<VAR>f : X ⟶ Y<VAR>U V : CategoryTheory.Under Y<VAR>g : U ⟶ V<GOAL>((CategoryTheory.Under.map f).map g).right = g.right
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>Y : T<GOAL>CategoryTheory.Under.map (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.Functor.id (CategoryTheory.Under Y)
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y : T<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.Under.map f).comp (CategoryTheory.Under.forget X) = CategoryTheory.Under.forget Y
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X : T<VAR>U V : CategoryTheory.Under X<VAR>e : U = V<GOAL>(CategoryTheory.eqToHom e).right = CategoryTheory.eqToHom ⋯
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<VAR>X Y Z : T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.Under.map (CategoryTheory.CategoryStruct.comp f g) = (CategoryTheory.Under.map g).comp (CategoryTheory.Under.map f)
<VAR>T : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} T<GOAL>∀ {X Y : Tᵒᵖ} (f : X ⟶ Y), (CategoryTheory.Under.mapFunctor T).map f = CategoryTheory.Under.map f.unop