ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>X : I₁ ⊕ I₂ → C<VAR>c : CategoryTheory.Limits.Cofan X<VAR>c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)<VAR>c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>hc₁ : CategoryTheory.Limits.IsColimit c₁<VAR>hc₂ : CategoryTheory.Limits.IsColimit c₂<VAR>CategoryTheory.Limits.MonoCoprod C<VAR>inr : c₂.pt ⟶ c.pt<VAR>hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)<GOAL>CategoryTheory.Mono inr
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.MonoCoprod C<VAR>I : Type u_2<VAR>J : Type u_3<VAR>X : I → C<VAR>ι : J → I<VAR>hι : Function.Injective ι<VAR>c : CategoryTheory.Limits.Cofan X<VAR>c₁ : CategoryTheory.Limits.Cofan (X ∘ ι)<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>hc₁ : CategoryTheory.Limits.IsColimit c₁<VAR>c₂ : CategoryTheory.Limits.Cofan fun k => X ↑k<VAR>hc₂ : CategoryTheory.Limits.IsColimit c₂<GOAL>CategoryTheory.Mono (CategoryTheory.Limits.Cofan.IsColimit.desc hc₁ fun i => c.inj (ι i))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.MonoCoprod C<VAR>I : Type u_2<VAR>J : Type u_3<VAR>X : I → C<VAR>ι : J → I<VAR>hι : Function.Injective ι<VAR>c : CategoryTheory.Limits.Cofan X<VAR>c₁ : CategoryTheory.Limits.Cofan (X ∘ ι)<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>hc₁ : CategoryTheory.Limits.IsColimit c₁<VAR>CategoryTheory.Limits.HasCoproduct fun k => X ↑k<GOAL>CategoryTheory.Mono (CategoryTheory.Limits.Cofan.IsColimit.desc hc₁ fun i => c.inj (ι i))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.MonoCoprod C<VAR>I : Type u_2<VAR>J : Type u_3<VAR>X : I → C<VAR>ι : J → I<VAR>hι : Function.Injective ι<VAR>CategoryTheory.Limits.HasCoproduct (X ∘ ι)<VAR>CategoryTheory.Limits.HasCoproduct X<VAR>CategoryTheory.Limits.HasCoproduct fun k => X ↑k<GOAL>CategoryTheory.Mono (CategoryTheory.Limits.Sigma.desc fun j => CategoryTheory.Limits.Sigma.ι X (ι j))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Limits.MonoCoprod C<VAR>I : Type u_2<VAR>J : Type u_3<VAR>X : I → C<VAR>ι : J → I<VAR>hι : Function.Injective ι<VAR>CategoryTheory.Limits.HasCoproduct (X ∘ ι)<VAR>CategoryTheory.Limits.HasCoproduct X<VAR>CategoryTheory.Limits.HasCoproduct fun k => X ↑k<GOAL>CategoryTheory.Mono (CategoryTheory.Limits.Sigma.map' ι fun j => 𝟙 ((X ∘ ι) j))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Limits.MonoCoprod C<VAR>I : Type u_2<VAR>X : I → C<VAR>c : CategoryTheory.Limits.Cofan X<VAR>h : CategoryTheory.Limits.IsColimit c<VAR>i : I<VAR>CategoryTheory.Limits.HasCoproduct fun k => X ↑k<GOAL>CategoryTheory.Mono (c.inj i)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>F : C ⥤ D<VAR>CategoryTheory.Limits.MonoCoprod D<VAR>CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>F.ReflectsMonomorphisms<GOAL>CategoryTheory.Limits.MonoCoprod C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X : C<VAR>a : CategoryTheory.Subobject X<GOAL>(CategoryTheory.Abelian.subobjectIsoSubobjectOp X) a = CategoryTheory.Subobject.lift (fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.cokernel.π f).op) ⋯ a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Abelian C<VAR>X : C<VAR>a : (CategoryTheory.Subobject (Opposite.op X))ᵒᵈ<GOAL>(RelIso.symm (CategoryTheory.Abelian.subobjectIsoSubobjectOp X)) a = CategoryTheory.Subobject.lift (fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f.unop)) ⋯ a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>F : CategoryTheory.Functor I C<VAR>CategoryTheory.Limits.HasColimit F<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).inv (CategoryTheory.Limits.limit.π F.op (Opposite.op i)) = (CategoryTheory.Limits.colimit.ι F i).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>F : CategoryTheory.Functor I C<VAR>CategoryTheory.Limits.HasColimit F<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).hom (CategoryTheory.Limits.colimit.ι F i).op = CategoryTheory.Limits.limit.π F.op (Opposite.op i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>F : CategoryTheory.Functor Iᵒᵖ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).inv (CategoryTheory.Limits.limit.π F.rightOp i) = (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>F : CategoryTheory.Functor Iᵒᵖ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).hom (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op = CategoryTheory.Limits.limit.π F.rightOp i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>F : CategoryTheory.Functor I C<VAR>CategoryTheory.Limits.HasColimit F<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda F).hom (CategoryTheory.Limits.limit.π (F.op.comp CategoryTheory.coyoneda) (Opposite.op i)) = CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>F : CategoryTheory.Functor I C<VAR>CategoryTheory.Limits.HasColimit F<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda F).inv (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op) = CategoryTheory.Limits.limit.π (F.op.comp CategoryTheory.coyoneda) (Opposite.op i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>F : CategoryTheory.Functor I C<VAR>CategoryTheory.Limits.HasColimit F<VAR>CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)<VAR>A : C<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda F A).hom (CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj A)) (Opposite.op i)) = (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op).app A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>F : CategoryTheory.Functor I C<VAR>CategoryTheory.Limits.HasColimit F<VAR>CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)<VAR>A : C<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda F A).inv ((CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op).app A) = CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj A)) (Opposite.op i)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>F : CategoryTheory.Functor Iᵒᵖ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F).hom (CategoryTheory.Limits.limit.π (F.rightOp.comp CategoryTheory.coyoneda) i) = CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>F : CategoryTheory.Functor Iᵒᵖ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F).inv (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op) = CategoryTheory.Limits.limit.π (F.rightOp.comp CategoryTheory.coyoneda) i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>F : CategoryTheory.Functor Iᵒᵖ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)<VAR>A : C<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A).hom (CategoryTheory.Limits.limit.π (F.rightOp.comp (CategoryTheory.yoneda.obj A)) i) = (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op).app A
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>F : CategoryTheory.Functor Iᵒᵖ C<VAR>CategoryTheory.Limits.HasColimit F<VAR>CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)<VAR>A : C<VAR>i : I<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A).inv ((CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op).app A) = CategoryTheory.Limits.limit.π (F.rightOp.comp (CategoryTheory.yoneda.obj A)) i
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>D : CategoryTheory.Functor Iᵒᵖ C<VAR>F : CategoryTheory.Functor C (Type u₂)<VAR>CategoryTheory.Limits.HasColimit (D.rightOp.comp CategoryTheory.coyoneda)<VAR>CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))<VAR>f : CategoryTheory.Limits.colimit (D.rightOp.comp CategoryTheory.coyoneda) ⟶ F<VAR>i : I<GOAL>CategoryTheory.Limits.limit.π (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) (Opposite.op i) ((CategoryTheory.Limits.colimitCoyonedaHomIsoLimit D F).hom f) = { down := f.app (D.obj (Opposite.op i)) ((CategoryTheory.Limits.colimit.ι (D.rightOp.comp CategoryTheory.coyoneda) i).app (D.obj (Opposite.op i)) (CategoryTheory.CategoryStruct.id (D.obj (Opposite.op i)))) }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>CategoryTheory.Category.{v₂, v₁} I<VAR>D : CategoryTheory.Functor I C<VAR>F : CategoryTheory.Functor C (Type u₂)<VAR>CategoryTheory.Limits.HasColimit (D.op.comp CategoryTheory.coyoneda)<VAR>CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))<VAR>f : CategoryTheory.Limits.colimit (D.op.comp CategoryTheory.coyoneda) ⟶ F<VAR>i : I<GOAL>CategoryTheory.Limits.limit.π (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) i ((CategoryTheory.Limits.colimitCoyonedaHomIsoLimit' D F).hom f) = { down := f.app (D.obj i) ((CategoryTheory.Limits.colimit.ι (D.op.comp CategoryTheory.coyoneda) (Opposite.op i)).app (D.obj i) (CategoryTheory.CategoryStruct.id (D.obj i))) }
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))<VAR>X : J<GOAL>(CategoryTheory.Comma.limitAuxiliaryCone F c₁).π.app X = CategoryTheory.CategoryStruct.comp (L.map (c₁.π.app X)) (F.obj X).hom
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))<GOAL>(CategoryTheory.Comma.limitAuxiliaryCone F c₁).pt = L.obj c₁.pt
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R<VAR>c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))<VAR>c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))<VAR>t₂ : CategoryTheory.Limits.IsLimit c₂<GOAL>(CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.right = c₂.pt
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R<VAR>c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))<VAR>c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))<VAR>t₂ : CategoryTheory.Limits.IsLimit c₂<GOAL>(CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.left = c₁.pt
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R<VAR>c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))<VAR>c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))<VAR>t₂ : CategoryTheory.Limits.IsLimit c₂<GOAL>(CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.hom = (CategoryTheory.Limits.isLimitOfPreserves R t₂).lift (CategoryTheory.Comma.limitAuxiliaryCone F c₁)
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R<VAR>c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))<VAR>c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))<VAR>t₂ : CategoryTheory.Limits.IsLimit c₂<VAR>j : J<GOAL>((CategoryTheory.Comma.coneOfPreserves F c₁ t₂).π.app j).left = c₁.π.app j
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R<VAR>c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R))<VAR>c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))<VAR>t₂ : CategoryTheory.Limits.IsLimit c₂<VAR>j : J<GOAL>((CategoryTheory.Comma.coneOfPreserves F c₁ t₂).π.app j).right = c₂.π.app j
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))<VAR>X : J<GOAL>(CategoryTheory.Comma.colimitAuxiliaryCocone F c₂).ι.app X = CategoryTheory.CategoryStruct.comp (F.obj X).hom (R.map (c₂.ι.app X))
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))<GOAL>(CategoryTheory.Comma.colimitAuxiliaryCocone F c₂).pt = R.obj c₂.pt
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L<VAR>c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))<VAR>t₁ : CategoryTheory.Limits.IsColimit c₁<VAR>c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))<GOAL>(CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.right = c₂.pt
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L<VAR>c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))<VAR>t₁ : CategoryTheory.Limits.IsColimit c₁<VAR>c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))<GOAL>(CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.left = c₁.pt
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L<VAR>c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))<VAR>t₁ : CategoryTheory.Limits.IsColimit c₁<VAR>c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))<VAR>j : J<GOAL>((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).left = c₁.ι.app j
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L<VAR>c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))<VAR>t₁ : CategoryTheory.Limits.IsColimit c₁<VAR>c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))<GOAL>(CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.hom = (CategoryTheory.Limits.isColimitOfPreserves L t₁).desc (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂)
<VAR>J : Type w<VAR>CategoryTheory.Category.{w', w} J<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>L : CategoryTheory.Functor A T<VAR>R : CategoryTheory.Functor B T<VAR>F : CategoryTheory.Functor J (CategoryTheory.Comma L R)<VAR>CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L<VAR>c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))<VAR>t₁ : CategoryTheory.Limits.IsColimit c₁<VAR>c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))<VAR>j : J<GOAL>((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).right = c₂.ι.app j
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>X : T<VAR>G : CategoryTheory.Functor A T<VAR>CategoryTheory.Limits.HasPullbacks A<VAR>CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G<VAR>Y Z : CategoryTheory.StructuredArrow X G<VAR>f : Y ⟶ Z<GOAL>CategoryTheory.Mono f ↔ CategoryTheory.Mono f.right
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>T : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} T<VAR>G : CategoryTheory.Functor A T<VAR>X : T<VAR>CategoryTheory.Limits.HasPushouts A<VAR>CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan G<VAR>Y Z : CategoryTheory.CostructuredArrow G X<VAR>f : Y ⟶ Z<GOAL>CategoryTheory.Epi f ↔ CategoryTheory.Epi f.left
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} C<VAR>CategoryTheory.Abelian C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>X : ChainComplex C α<VAR>A : Type u_4<VAR>Ring A<VAR>CategoryTheory.Linear A C<VAR>Y : C<VAR>i j : α<GOAL>(X.linearYonedaObj A Y).d i j = ModuleCat.ofHom (CategoryTheory.Linear.leftComp A Y (X.d j i))
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} C<VAR>CategoryTheory.Abelian C<VAR>α : Type u_3<VAR>AddRightCancelSemigroup α<VAR>One α<VAR>X : ChainComplex C α<VAR>A : Type u_4<VAR>Ring A<VAR>CategoryTheory.Linear A C<VAR>Y : C<VAR>i : α<GOAL>(X.linearYonedaObj A Y).X i = ModuleCat.of A (X.X i ⟶ Y)
<VAR>R : Type u_1<VAR>Ring R<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Abelian C<VAR>CategoryTheory.Linear R C<VAR>CategoryTheory.EnoughProjectives C<VAR>X Y : C<VAR>CategoryTheory.Projective X<VAR>n : ℕ<GOAL>CategoryTheory.Limits.IsZero (((Ext R C (n + 1)).obj (Opposite.op X)).obj Y)
<VAR>J : Type w<VAR>X : CategoryTheory.Limits.WidePullbackShape J<GOAL>CategoryTheory.Limits.WidePullbackShape.Hom.id X = 𝟙 X
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → objs j ⟶ B<VAR>j : CategoryTheory.Limits.WidePullbackShape J<GOAL>(CategoryTheory.Limits.WidePullbackShape.wideCospan B objs arrows).obj j = Option.casesOn j B objs
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → objs j ⟶ B<GOAL>∀ {X Y : CategoryTheory.Limits.WidePullbackShape J} (f : X ⟶ Y), (CategoryTheory.Limits.WidePullbackShape.wideCospan B objs arrows).map f = CategoryTheory.Limits.WidePullbackShape.Hom.casesOn (motive := fun a a_1 t => X = a → Y = a_1 → HEq f t → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) f (fun X_1 h => Eq.ndrec (motive := fun X_2 => Y = X_2 → HEq f (CategoryTheory.Limits.WidePullbackShape.Hom.id X_2) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) (fun h => Eq.ndrec (motive := fun {Y} => (f : X ⟶ Y) → HEq f (CategoryTheory.Limits.WidePullbackShape.Hom.id X) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) (fun f h => 𝟙 ((fun j => Option.casesOn j B objs) X)) ⋯ f) h) (fun j h => Eq.ndrec (motive := fun {X} => (f : X ⟶ Y) → Y = none → HEq f (CategoryTheory.Limits.WidePullbackShape.Hom.term j) → ((fun j => Option.casesOn j B objs) X ⟶ (fun j => Option.casesOn j B objs) Y)) (fun f h => Eq.ndrec (motive := fun {Y} => (f : some j ⟶ Y) → HEq f (CategoryTheory.Limits.WidePullbackShape.Hom.term j) → ((fun j => Option.casesOn j B objs) (some j) ⟶ (fun j => Option.casesOn j B objs) Y)) (fun f h => arrows j) ⋯ f) ⋯ f) ⋯ ⋯ ⋯
<VAR>J : Type w<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Limits.WidePullbackShape J ⥤ C<VAR>X : C<VAR>f : X ⟶ F.obj none<VAR>π : (j : J) → X ⟶ F.obj (some j)<VAR>w : ∀ (j : J), π j ≫ F.map (CategoryTheory.Limits.WidePullbackShape.Hom.term j) = f<VAR>j : CategoryTheory.Limits.WidePullbackShape J<GOAL>(CategoryTheory.Limits.WidePullbackShape.mkCone f π w).π.app j = match j with | none => f | some j => π j