isColimitTrans — Mathlib

Lean4
/-- A coproduct of coproducts is a coproduct -/
def isColimitTrans {X : α → C} (c : Cofan X) (hc : IsColimit c) {β : α → Type*} {Y : (a : α) → β a → C}
    (π : (a : α) → (b : β a) → Y a b ⟶ X a) (hs : ∀ a, IsColimit (Cofan.mk (X a) (π a))) :
    IsColimit (Cofan.mk (f := fun ⟨a, b⟩ => Y a b) c.pt (fun (⟨a, b⟩ : Σ a, _) ↦ π a b ≫ c.inj a)) :=
  by
  refine mkCofanColimit _ ?_ ?_ ?_
  · exact fun t ↦ hc.desc (Cofan.mk _ fun a ↦ (hs a).desc (Cofan.mk t.pt (fun b ↦ t.inj ⟨a, b⟩)))
  · intro t ⟨a, b⟩
    simp only [mk_pt, cofan_mk_inj, Category.assoc]
    erw [hc.fac, (hs a).fac]
    rfl
  · intro t m h
    refine hc.hom_ext fun ⟨a⟩ ↦ (hs a).hom_ext fun ⟨b⟩ ↦ ?_
    erw [hc.fac, (hs a).fac]
    simpa using h ⟨a, b⟩
Похожие утверждения