English
A componentwise proof shows the required compatibilities for the limit property holds when moving along the indexing in the cone.
Русский
Доказательство по компонентам показывает, что требуемая совместимость сохраняется при индексации конуса.
LaTeX
$$$\text{IsLimit}(\text{coneOfHasLimitCurryCompLim } G)\
=\text{IsLimit\; proof via compatibilities across indices}$$$
Lean4
/-- The cocone `coconeOfHasColimitCurryCompColim` is in fact a limit cocone.
-/
noncomputable def isColimitCoconeOfHasColimitCurryCompColim : IsColimit (coconeOfHasColimitCurryCompColim G) :=
let Q : DiagramOfCocones (curry.obj G) := .mkOfHasColimits _
let Q' : ∀ j, IsColimit (Q.obj j) := fun j => colimit.isColimit _
{ desc c' := colimit.desc (F := curry.obj G ⋙ colim) (coconeOfCoconeCurry G Q' c')
fac c' f := by simp [coconeOfHasColimitCurryCompColim, Q, Q']
uniq c' f
h := by
dsimp [coconeOfHasColimitCurryCompColim] at f h ⊢
refine colimit.hom_ext (F := curry.obj G ⋙ colim) (fun j ↦ colimit.hom_ext (fun k ↦ ?_))
simp [← h ⟨j, k⟩, Q'] }
