English
If c1 and c2 are colimit cofans and bc is a colimit binary cofan on their cocone points, then the cofan built from combPairHoms is a colimit cocone.
Русский
Если c1 и c2 — коголимитные ко-фаны, а bc — коголимитный двоичный ко-фан над их коконными точками, тогда ко-фан, построенный из combPairHoms, является коголимитным коконом.
LaTeX
$$$ \\text{combPairIsColimit} : IsColimit (Cofan.mk bc.pt (combPairHoms c1 c2 bc))$$$
Lean4
/-- If `c₁` and `c₂` are colimit cofans and `bc` is a colimit binary cofan on their cocone
points, then the cofan constructed from `combPairHoms` is a colimit cocone. -/
def combPairIsColimit : IsColimit (Cofan.mk bc.pt (combPairHoms c₁ c₂ bc)) :=
mkCofanColimit _
(fun s ↦
Cofan.IsColimit.desc h <| fun i ↦ by
cases i
· exact Cofan.IsColimit.desc h₁ (fun a ↦ s.inj (.inl a))
· exact Cofan.IsColimit.desc h₂ (fun a ↦ s.inj (.inr a)))
(fun s w ↦ by
cases w <;>
· simp only [cofan_mk_inj, combPairHoms, Category.assoc]
erw [h.fac]
simp only [Cofan.mk_ι_app, Cofan.IsColimit.fac])
(fun s m hm ↦
Cofan.IsColimit.hom_ext h _ _ <| fun w ↦ by
cases w
· refine Cofan.IsColimit.hom_ext h₁ _ _ (fun a ↦ by aesop)
· refine Cofan.IsColimit.hom_ext h₂ _ _ (fun a ↦ by aesop))
